Abstract
This paper proposes a stochastic, and complete, backtrack search algorithm for Propositional Satisfiability (SAT). In recent years, randomization has become pervasive in SAT algorithms. Incomplete algorithms for SAT, for example the ones based on local search, often resort to randomization. Complete algorithms also resort to randomization. These include, state-of-the-art backtrack search SAT algorithms that often randomize variable selection heuristics. Moreover, it is plain that the introduction of randomization in other components of backtrack search SAT algorithms can potentially yield new competitive search strategies. As a result, we propose a stochastic backtrack search algorithm for SAT, that randomizes both the variable selection and the backtrack steps of the algorithm. In addition, we describe and compare different organizations of stochastic backtrack search. Finally, experimental results provide empirical evidence that the new search algorithm for SAT results in a very competitive approach for solving hard real-world instances.
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
L. Baptista, I. Lynce, and J. Marques-Silva. Complete search restart strategies for satisfiability. In IJCAI Workshop on Stochastic Search Algorithms, August 2001.
L. Baptista and J. P. Marques-Silva. Using randomization and learning to solve hard real-world instances of satisfiability. In International Conference on Principles and Practice of Constraint Programming, pages 489–494, September 2000.
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, pages 203–208, 1997.
M. Davis, G. Logemann, and D. Loveland. A machine program for theoremproving. Communications of the Association for Computing Machinery, 5:394–397, July 1962.
M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201–215, 1960.
M. Ginsberg and D. McAllester. GSAT and dynamic backtracking. In Proceedings of the International Conference on Principles of Knowledge and Reasoning, pages 226–237, 1994.
C. P. Gomes, B. Selman, and H. Kautz. Boosting combinatorial search through randomization. In Proceedings of the National Conference on Artificial Intelligence, July 1998.
I. Lynce, L. Baptista, and J. Marques-Silva. Stochastic systematic search algorithms for satisfiability. In LICS Workshop on Theory and Applications of Satisfiability Testing, June 2001.
J. P. Marques-Silva and K. A. Sakallah. GRASP-A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506–521, May 1999.
D. McAllester, B. Selman, and H. Kautz. Evidence of invariants in local search. In Proceedings of the National Conference on Artificial Intelligence, pages 321–326, August 1997.
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference, 2001.
S. Prestwich. A hybrid search architecture applied to hard random 3-sat and lowautocorrelation binary sequences. In Proceedings of the International Conference on Principles and Practice of Constraint Programming, pages 337–352, September 2000.
E. T. Richards and B. Richards. Restart-repair and learning: An empirical study of single solution 3-sat problems. In CP Workshop on the Theory and Practice of Dynamic Constraint Satisfaction, 1997.
M. N. Velev and R. E. Bryant. Superscalar processor verification using efficient reductions from the logic of equality with uninterpreted functions to propositional logic. In Proceedings of Correct Hardware Design and Verification Methods, LNCS 1703, pages 37–53, September 1999.
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
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lynce, I., Baptista, L., Marques-Silva, J. (2001). Towards Provably Complete Stochastic Search Algorithms for Satisfiability. In: Brazdil, P., Jorge, A. (eds) Progress in Artificial Intelligence. EPIA 2001. Lecture Notes in Computer Science(), vol 2258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45329-6_35
Download citation
DOI: https://doi.org/10.1007/3-540-45329-6_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43030-8
Online ISBN: 978-3-540-45329-1
eBook Packages: Springer Book Archive