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 Λ, V, ¬ 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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Jain, H., Bartzis, C., & Clarke, E. (2006). Satisfiability checking of non-clausal formulas using general matings. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4121 LNCS, pp. 75–89). Springer Verlag. https://doi.org/10.1007/11814948_10
Mendeley helps you to discover research relevant for your work.