LARA

This is an old revision of the document!


Definition of Propositional Resolution

Recall:

  • literal is a propositional variable $p \in V$ or its negation $\lnot p$.
  • clause is a disjunction of literals

Clauses as Sets of Literlas

The order and the number of occurrences of literals in clauses do not matter, because of these valid formulas:

  • $\models (L_1 \lor (L_2 \lor L_3) \leftrightarrow (L_1 \lor L_2) \lor L_3)$
  • $\models (L_1 \lor L_2 \leftrightarrow L_2 \lor L_1)$
  • $\models (L \lor L \leftrightarrow L)$

We therefore represent clauses as sets of literals. For example, we represent the clause $\lnot p_3 \lor p_1 \lor \lnot p_2 \lor p_1$ as the set $\{p_1,\lnot p_2,\lnot p_3\}$. We represent false as an empty clause and we do not represent true.

Resolution Rule

Applying Resolution Rule to Check Satisfiability

Steps:

  1. If we wish to check validity, negate the formula. From now on, assume we are checking satisfiability.
  2. Convert formula into polynomially large equisatisfiable formula in conjunctive normal form
  3. Keep applying resolution rule until either
    1. empty clause $\emptyset$ is derived
    2. application of the resolution rule produces no new clauses