Solving Non-clausal Formulas with DPLL Search

Great progress has been made on DPLL based SAT solvers operating on CNF encoded SAT theories. However, for most problems CNF is not a very natural representation. Typically these problems are more easily expressed using unrestricted propositional formulae and hence must be converted to CNF before modern SAT solvers can be applied. This conversion entails a considerable loss of information about the problem’s structure. In this work we demonstrate that conversion to CNF is both unnecessary and undesirable. In particular, we demonstrate that a SAT solver which operates directly on a propositional formula can achieve the same efficiency as a highly optimized modern CNF solver. Furthermore, since the original formula remains intact, such a solver can exploit the original problem structure to improve over CNF solvers. We present empirical evidence showing that exploiting the original structure can yield considerable benefits.