ABSTRACT OF THE DISSERTATION Implementations of the DPLL Algorithm

In this dissertation, we examine variations of the DPLL algorithm, a popular algorithm for solving the satisfiability problem, which is NP-complete. The variations include operations in the Davis-Putnam kernel (monotone literal fixing and the subsumption rule) and five branching rules in the literature (the Jeroslow-Wang rule, the two-sided Jeroslow-Wang rule, the DSJ rule, the MinLen rule, and the C-SAT rule.) Experimental performances on random 3-SAT formulas and on DIMACS benchmark formulas are reported. Monotone literal fixing and the subsumption rule are of little use on random 3-SAT formulas, but they can speed up the DPLL algorithm significantly when solving some of the DIMACS formulas. Among the five branching rules, the C-SAT rule is best for random 3-SAT formulas. However, the results on the DIMACS formulas are mixed. New branching rules are described that are better than other branching rules on random 3-SAT formulas. A sequence of formulas is described that fools a variety of “sensible ” branching rules in the following sense: when the formula has n variables, each of the “sensible” branching rules brings about Ω(2 n/5) recursive calls of the DPLL algorithm, even though only O(1) such calls are necessary. i