Solving non-clausal SAT formulas.
Published: 2004
Language: eng
Number of pages: 81
Description: State-of-the-art SAT solvers usually require that the input be in Conjunctive Normal Form. Unfortunately, the conversion to CNF loses a considerable amount of structural information. Recent research has shown that a solver could use this information to significantly improve the search. In this work, we show that conversion to CNF is unnecessary by building a non-clausal solver, NOCLAUSE, that implements the techniques commonly found in modern clausal solvers. We show that efficient data structures, powerful inference rules, clause learning and conflict-driven heuristics can all be modified to a non-clausal setting. In addition, we present two simple structure-based optimizations that would be difficult to implement in a CNF solver. Our experiments show that NOCLAUSE  is comparable to a highly optimized CNF solver and yields significant advantages on large problems. Throughout this work, we lay the foundation for a new generation of superior SAT solvers that reason directly from the original formula.
Notes: Adviser:  Fahiem Bacchus.

Thesis (M.Sc.)--University of Toronto, 2004.

Electronic version licensed for access by U. of T. users.

Source: Masters Abstracts International, Volume: 43-03, page: 0891.

MICR copy on microfiche (1 microfiche).