Git Repo: git@github.com:Wenling/DPLL-Algorithm.git
There are three satisfiability-preserving transformations in DP.
• The 1-literal rule
• The affirmative-negative rule
• The rule for eliminating atomic formulas
The first two steps reduce the total number of literals in the formula.
The last step reduces the number of variables in the formula.
By repeatedly applying these rules, eventually we obtain a formula containing an
empty clause, indicating unsatisfiability, or a formula with no clauses, indicating
satisfiability.
The DPLL algorithm replaces resolution with a splitting rule.
• Choose a propositional symbol p occuring in the formula.
• Let delta be the current set of clauses.
• Test the satisfiability of delta and {p}.
• If satisfiable, return true.
• Otherwise, return the result of testing delta and {¬p} for satisfiability.
