Most state-of-the-art SAT solvers are based on DPLL search and require the input formula to be in clausal form (cnf). However,
typical formulas that arise in practice are non-clausal. We present a new non-clausal SAT-solver based on General Matings
instead of DPLL search. Our technique is able to handle non-clausal formulas involving ∨,∧,¬ operators without destroying
their structure or introducing new variables. We present techniques for performing search space pruning, learning, non-chronological
backtracking in the context of a General Matings based SAT solver. Experimental results show that our SAT solver is competitive
to current state-of-the-art SAT solvers on a class of non-clausal benchmarks.
This research was sponsored by the Gigascale Systems Research Center (GSRC), the Semiconductor Research Corporation (SRC),
the Office of Naval Research (ONR), the Naval Research Laboratory (NRL), the Army Research Office (ARO), and the General Motors
Collaborative Research Lab at CMU.