Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Edimacs format, www.satcompetition.org/2005/edimacs.pdf
Minisat sat solver, http://www.cs.chalmers.se/cs/research/formalmethods/minisat/
SatMate website, http://www.cs.cmu.edu/~modelcheck/satmate
Siege (version 4) sat solver, http://www.cs.sfu.ca/~loryan/personal/
TPS and ETPS, http://gtps.math.cmu.edu/tps-papers.html
Andrews, P.B.: Theorem Proving via General Matings. J. ACM 28(2), 193–214 (1981)
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: to Truth through Proof, 2nd edn. Kluwer Academic Publishers, Dordrecht (2002)
Bibel, W.: On Matrices with Connections. J. ACM 28(4), 633–645 (1981)
Ganai, M.K., Ashar, P., Gupta, A., Zhang, L., Malik, S.: Combining Strengths of Circuit-based and CNF-based Algorithms for a High-performance SAT solver. In: DAC (2002)
Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust Sat-Solver. In: DATE (2002)
Marques-Silva, J.P., Sakallah, K.A.: GRASP - A New Search Algorithm for Satisfiability. In: ICCAD, pp. 220–227 (1996)
McAllester, D., Selman, B., Kautz, H.: Evidence for invariants in local search. In: AAAI, Providence, Rhode Island, pp. 321–326 (1997)
Meier, A., Sorge, V.: A new set of algebraic benchmark problems for sat solvers. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 459–466. Springer, Heidelberg (2005)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: DAC, June 2001, pp. 530–535 (2001)
Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3) (1986)
Smullyan, R.M.: First Order Logic. Springer, Heidelberg (1968)
Thiffault, C., Bacchus, F., Walsh, T.: Solving Non-clausal Formulas with DPLL Search. In: SAT (2004)
Zhang, H.: Sato: An efficient propositional prover. In: CADE-14, pp. 272–275 (1997)
Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: ICCAD, pp. 279–285 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jain, H., Bartzis, C., Clarke, E. (2006). Satisfiability Checking of Non-clausal Formulas Using General Matings. In: Biere, A., Gomes, C.P. (eds) Theory and Applications of Satisfiability Testing - SAT 2006. SAT 2006. Lecture Notes in Computer Science, vol 4121. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11814948_10
Download citation
DOI: https://doi.org/10.1007/11814948_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37206-6
Online ISBN: 978-3-540-37207-3
eBook Packages: Computer ScienceComputer Science (R0)