Abstract
This paper studies the practical impact of the branching heuristics used in Propositional Satisfiability (SAT) algorithms, when applied to solving real-world instances of SAT. In addition, different SAT algorithms are experimentally evaluated. The main conclusion of this study is that even though branching heuristics are crucial for solving SAT, other aspects of the organization of SAT algorithms are also essential. Moreover, we provide empirical evidence that for practical instances of SAT, the search pruning techniques included in the most competitive SAT algorithms may be of more fundamental significance than branching heuristics.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
P. Barth. A Davis-Putnam enumeration procedure for linear pseudo-boolean optimization. Technical Report MPI-I-2-003, MPI, January 1995.
R. Bayardo Jr. and R. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the National Conference on Artificial Intelligence, 1997.
M. Bruynooghe. Analysis of dependencies to improve the behaviour of logic programs. In Proceedings of the 5th Conference on Automated Deduction, pages 293–305, 1980.
M. Buro and H. Kleine-Büning. Report on a SAT competition. Technical report, University of Paderborn, November 1992.
J. Crawford and L. Auton. Experimental results on the cross-over point in satisfiability problems. In Proceedings of the National Conference on Artificial Intelligence, pages 22–28, 1993.
M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201–215, 1960.
D. Du, J. Gu, and P. M. Pardalos, editors. Satisfiability Problem: Theory and Applications, volume 35. American Mathematical Society, 1997.
O. Dubois, P. Andre, Y. Boufkhad, and J. Carlier. SAT versus UNSAT. In D. S. Johnson and M. A. Trick, editors, Second DIMACS Implementation Challenge. American Mathematical Society, 1993.
J. W. Freeman. Improvements to Propositional Satisfiability Search Algorithms. PhD thesis, University of Pennsylvania, Philadelphia, PA, May 1995.
J. Gaschnig. Performance Measurement and Analysis of Certain Search Algorithms. PhD thesis, Carnegie-Mellon University, Pittsburgh, PA, May 1979.
A. Van Gelder and Y. K. Tsuji. Satisfiability testing with more reasoning and less guessing. In D. S. Johnson and M. A. Trick, editors, Second DIMACS Implementation Challenge. American Mathematical Society, 1993.
J. N. Hooker and V. Vinay. Branching rules for satisfiability. Journal of Automated Reasoning, 15:359–383, 1995.
R. G. Jeroslow and J. Wang. Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1:167–187, 1990.
D. S. Johnson and M. A. Trick, editors. Second DIMACS Implementation Challenge. American Mathematical Society, 1993.
H. Kautz and B. Selman. Pushing the envelope: Planning, propositional logic, and stochastic search. In Proceedings of the National Conference on Artificial Intelligence, 1996.
T. Larrabee. Test pattern generation using boolean satisfiability. IEEE Transactions on Computer-Aided Design, 11(1):4–15, January 1992.
C. M. Li and Anbulagan. Look-ahead versus look-back for satisfiability problems. In Proceedings of International Conference on Principles and Practice of Constraint Programming, 1997.
J. P. Marques-Silva and K. A. Sakallah. GRASP-A new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design, November 1996.
D. Pretolani. Efficiency and stability of hypergraph sat algorithms. In D. S. Johnson and M. A. Trick, editors, Second DIMACS Implementation Challenge. American Mathematical Society, 1993.
B. Selman and H. Kautz. Domain-independent extensions to GSAT: Solving large structured satisfiability problems. In Proceedings of the International Joint Conference on Artificial Intelligence, pages 290–295, 1993.
B. Selman, H. Levesque, and D. Mitchell. A new method for solving hard satisfiability problems. In Proceedings of the National Conference on Artificial Intelligence, pages 440–446, 1992.
R. M. Stallman and G. J. Sussman. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence, 9:135–196, October 1977.
R. Zabih and D. A. McAllester. A rearrangement search strategy for determining propositional satisfiability. In Proceedings of the National Conference on Artificial Intelligence, pages 155–160, 1988.
H. Zhang. SATO: An efficient propositional prover. In Proceedings of the International Conference on Automated Deduction, pages 272–275, July 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marques-Silva, J. (1999). The Impact of Branching Heuristics in Propositional Satisfiability Algorithms. In: Barahona, P., Alferes, J.J. (eds) Progress in Artificial Intelligence. EPIA 1999. Lecture Notes in Computer Science(), vol 1695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48159-1_5
Download citation
DOI: https://doi.org/10.1007/3-540-48159-1_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66548-9
Online ISBN: 978-3-540-48159-1
eBook Packages: Springer Book Archive