This is an old revision of the document!
Definition of Propositional Resolution
Recall:
- literal is a propositional variable or its negation .
- 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:
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:
\[ \frac{C \cup \{p\}\ \ \ D \cup \{\lnot p\}}
{C \cup D}
\]
Here are clauses and is a propositional variable.
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.
- Keep applying resolution rule until either
- empty clause is derived
- application of the resolution rule produces no new clauses