Abstract
We propose a new decision heuristic for DPLL-based propositional SAT solvers. Its essence is that both the initial and the conflict clauses are arranged in a list and the next decision variable is chosen from the top-most unsatisfied clause. Various methods of initially organizing the list and moving the clauses within it are studied. Our approach is an extension of one used in Berkmin, and adopted by other modern solvers, according to which only conflict clauses are organized in a list, and a literal-scoring-based secondary heuristic is used when there are no more unsatisfied conflict clauses. Our approach, implemented in the 2004 version of zChaff solver and in a generic Chaff-based SAT solver, results in a significant performance boost on hard industrial benchmarks.
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.
Similar content being viewed by others
References
Alfredsson, J.: The SAT solver Oepir, http://www.lri.fr/~simon/contest/results/ONLINEBOOKLET/OepirA.ps (viewed January 16, 2005)
Bayardo Jr., R., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the National Conference on Artificial Intelligence, pp. 203–208 (1997)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM (5), 394–397 (1962)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT-solver. In: Design, Automation, and Test in Europe (DATE 2002), March 2002, pp. 142–149 (2002)
Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of the National Conference on Artificial Intelligence (July 1998)
Jeroslaw, R.G., Wang, J.: Solving propositional satisfiability problems. Annals of mathematics and Artificial Intelligence (1), 167–187 (1990)
Kautz, H., Selman, B.: Planning as satisfiability. In: Proceedings of the 10th European conference on Artificial intelligence (1992)
Le Berre, D., Simon, L.: Fifty-five solvers in Vancouver: The SAT 2004 competition. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 321–344. Springer, Heidelberg (2005)
Mahajan, Y.S., Fu, Z., Malik, S.: ZChaff2004: an efficient SAT solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 360–375. Springer, Heidelberg (2005)
Marques-Silva, J.P.: The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS (LNAI), vol. 1695, pp. 62–74. Springer, Heidelberg (1999)
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers (48), 506–521 (1999)
Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the Design Automation Conference (2001)
Prasad, M.R., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. Intl. Journal on Software Tools for Technology Transfer (STTT) (7), 156–173 (2005)
Ryan, L.: Efficient algorithms for clause-learning SAT solvers. Masters thesis, Simon Fraser University (February 2004)
Hoos, H.H., Mitchell, D.G. (eds.): SAT 2004. LNCS, vol. 3542. Springer, Heidelberg (2005), http://satlive.org/SATCompetition/2004/ (viewed September 1, 2004)
Zabih, R., McAllester, D.A.: A rearrangement search strategy for determining propositional satisfiability. In: Proceedings of National Conference on Artificial Intelligence, pp. 155–160 (1988)
Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: International Conference on Computer-Aided Design (ICCAD 2001), November 2001, pp. 279–285 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dershowitz, N., Hanna, Z., Nadel, A. (2005). A Clause-Based Heuristic for SAT Solvers. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_4
Download citation
DOI: https://doi.org/10.1007/11499107_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26276-3
Online ISBN: 978-3-540-31679-4
eBook Packages: Computer ScienceComputer Science (R0)