• English only

Definition of Propositional Resolution

Recall:

• literal is a propositional variable or its negation .
• 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:

We therefore represent clauses as sets of literals. For example, we represent the clause as the set . 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:

Here are clauses and is a propositional variable.

Intuition: consider equivalent formulas

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 (see Normal Forms for Propositional Logic)
3. Keep applying resolution rule until either
1. empty clause is derived
2. application of the resolution rule produces no new clauses

Soundness of Resolution Rule

Suppose that and . If , then from we conclude and therefore . Similarly, if , then from we conclude and therefore .

Therefore, if and is the result of applying resolution rule to , then if and only if . Consequently, if we obtain an empty clause (false) by applying resolution, then the original set is not satisfiable either.