Solving non-clausal formulas with DPLL search

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