State of the art SAT solvers solve CNF encoded SAT theories. However most problems are not originally expressed in CNF. Thus these problems must be coverted to CNF. Although the Tseitin-style encodings commonly utilized for this conversion generate CNF formulas whose size is within a constant factor of the original non-clausal representation, the conversion to CNF still entails considerable loss of structural information.
In this paper we demonstrate that the conversion to clausal form is not required. Instead a DPLL tree search can operate directly on a non-clausal represenation with similar efficiency. Furthermore, all of the important techniques utilized in modern solvers, like clause learning, can still be utilized.
More importantly the structure that is retained in the non-clausal representation allows both theoretical as well as practical improvements in solving power. In this paper we demonstrate a non-clausal solver whose raw performance (decisions per second) is comparable to modern clausal DPLL solver. Furthermore, we show how the non-clausal information can be utilized to achieve further improvements in its solving power. These improvements would not be as easy to achieve in a clausal solver.