Definition of Propositional Resolution
- 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.
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
- 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
- empty clause is derived
- 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.