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 Literals

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

Viewing clauses as sets, propositional resolution is the following rule:

$\begin{equation*} \frac{C \cup \{\lnot p\}\ \ \ D \cup \{p\}} {C \cup D} \end{equation*}$

Here $C,D$ are clauses and $p \in V$ is a propositional variable.

Intuition: consider equivalent formulas

$\begin{equation*} \frac{((\lnot C) \rightarrow (\lnot p))\ \ \ ((\lnot p) \rightarrow D)} {(\lnot C) \rightarrow D} \end{equation*}$

Applying Resolution Rule to Check Satisfiability

Steps:

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

Example of Using Propositional Resolution

Soundness of Resolution Rule

Suppose that $I \models C \lor p$ and $I \models D \lor \lnot p$ . If $I(p)={\it true}$ , then from $I \models D \lor \lnot p$ we conclude $I \models D$ and therefore $I \models C\lor D$ . Similarly, if $I(p)={\it false}$ , then from $I \models C \lor p$ we conclude $I \models C$ and therefore $I \models C\lor D$ .

Therefore, if $C_1,C_2 \in S$ and $C_3$ is the result of applying resolution rule to $C_1,C_2$ , then $I \models S$ if and only if $I \models (S \cup \{ C_3 \})$ . Consequently, if we obtain an empty clause (false) by applying resolution, then the original set is not satisfiable either.