Abstract
This paper discusses several techniques to make the look- ahead architecture for satisfiability (Sat) solvers more competitive. Our contribution consists of reduction of the computational costs to perform look-ahead and a cheap integration of both equivalence reasoning and local learning. Most proposed techniques are illustrated with experimental results of their implementation in our solver march_eq.
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
Mitchel, D., Selmon, B., Levesque, H.: Hard and easy distributions of SAT problems. In: Proceedings of AIII 1992, pp. 459–465 (1992)
Le Berre, D.: Exploiting the Real Power of Unit Propagation Lookahead. In: LICS Workshop on Theory and Applications of Satisfiability Testing (2001)
Le Berre, D., Simon, L.: The essentials of the SAT 2003 Competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 452–467. Springer, Heidelberg (2004)
Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM 5, 394–397 (1962)
Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard3-sat formulae. In: International Joint Conference on Artificial Intelligence 2001, vol. 1, pp. 248–253 (2001)
Heule, M.J.H., van Maaren, H.: Aligning CNF- and Equivalence-Reasoning. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 145–156. Springer, Heidelberg (2005)
Kullmann, O.: Investigating the behaviour of a SAT solver on random formulas. In: Submitted to Annals of Mathematics and Artificial Intelligence (2002)
Li, C.M., Anbulagan: Look-Ahead versus Look-Back for Satisfiability Problems. In: Smolka, G. (ed.) CP 1997. LNCS, vol. 1330, pp. 342–356. Springer, Heidelberg (1997)
Li, C.M.: Equivalent literal propagation in the DLL procedure. The Renesse issue on satisfiability (2000). Discrete Appl. Math. 130(2), 251–276 (2003)
Simon, L.: Competition homepage. In: Sat (2004), http://www.lri.fr/~simon/contest/results/
Simon, L., Le Berre, D., Hirsch, E.: The SAT 2002 competition. Accepted for publication in Annals of Mathematics and Artificial Intelligence (AMAI) 43, 343–378 (2005)
Warners, J.P., van Maaren, H.: A two phase algorithm for solving a class of hard satisfiability problems. Oper. Res. Lett. 23(3-5), 81–88 (1998)
Zhang, H., Stickel, M.E.: Implementing the Davis-Putnam Method. In: SAT 2000, pp. 309–326 (2000)
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
Heule, M., Dufour, M., van Zwieten, J., van Maaren, H. (2005). March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver. In: Hoos, H.H., Mitchell, D.G. (eds) Theory and Applications of Satisfiability Testing. SAT 2004. Lecture Notes in Computer Science, vol 3542. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11527695_26
Download citation
DOI: https://doi.org/10.1007/11527695_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27829-0
Online ISBN: 978-3-540-31580-3
eBook Packages: Computer ScienceComputer Science (R0)