Abstract
In this paper, a new pre-processing step is proposed in the resolution of SAT instances, that recovers and exploits structural knowledge that is hidden in the CNF. It delivers an hybrid formula made of clauses together with a set of equations of the form y = f(x 1,..., x n ) where f is a standard connective operator among (∨, ∧, ⇔) and where y and x i are boolean variables of the initial SAT instance. This set of equations is then exploited to eliminate clauses and variables, while preserving satisfiability. These extraction and simplification techniques allowed us to implement a new SAT solver that proves to be the most efficient current one w.r.t. several important classes of 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
First international competition and symposium on satisfiability testing, March 1996. Beijing (China).
Yacine Boufkhad and Olivier Roussel. Redundancy in random sat formulas. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI’00), pages 273–278, 2000.
Ronen I. Brafman. A simplifier for propositional formulas with many binary clauses. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI’01), 2001.
M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Journal of the Association for Computing Machinery, 5:394–397, 1962.
Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201–215, 1960.
Second Challenge on Satisfiability Testing organized by the Center for Discrete Mathematics and Computer Science of Rutgers University, 1993. http://dimacs.rutgers.edu/Challenges/.
Olivier Dubois, Pascal André, Yacine Boufkhad, and Jacques Carlier. Sat versus unsat. In D. S. Johnson and M. A. Trick, editors, Second DIMACS Challenge, DIMACS Series in Discrete Mathematics and Theorical Computer Science, American Mathematical Society, pages 415–436, 1996.
Olivier Dubois and Gilles Dequen. A backbone-search heuristic for efficient solving of hard 3-sat formulae. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI’01), volume 1, pages 248–253, Seattle, Washington (USA), August 4–10 2001.
B. Dunham and H. Wang. Towards feasible solution of the tautology problem. Annals of Mathematical Logic, 10:117–154, 1976.
E. Giunchiglia, M. Maratea, A. Tacchella, and D. Zambonin. Evaluating search heuristics and optimization techniques in propositional satisfiability. In Proceedings of International Joint Conference on Automated Reasoning (IJCAR’01), Siena, June 2001.
Robert G. Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1:167–187, 1990.
Henry A. Kautz, David McAllester, and Bart Selman. Exploiting variable dependency in local search. In Abstract appears in ”Abstracts of the Poster Sessions of IJCAI-97”, Nagoya (Japan), 1997.
Oliver Kullmann. Worst-case analysis, 3-sat decision and lower bounds: Approaches for improved sat algorithms. In DIMACS Proceedings SAT Workshop, DIMACS Series in Discrete Mathematics and Theorical Computer Science, American Mathematical Society, 1996.
Oliver Kullmann. New methods for 3-sat decision and worst-case analysis. Theoretical Computer Science, pages 1–72, 1997.
Jérome Lang and Pierre Marquis. Complexity results for independence and definability in propositional logic. In Proceedings of the Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR’98), pages 356–367, Trento, 1998.
Daniel Le Berre. Exploiting the real power of unit propagation lookahead. In Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001), Boston University, Massachusetts, USA, June 14th–15th 2001.
Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI’97), pages 366–371, Nagoya (Japan), August 1997.
C. M. Li. Integrating equivalency reasoning into davis-putnam procedure. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI’00), pages 291–296, 2000.
Joao P. Marques-Silva. Algebraic simplification techniques for propositional satisfiability. In Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP’2000), September 2000.
Shtrichman Oler. Tuning sat checkers for bounded model checking. In Proceedings of Computer Aided Verification (CAV’00), 2000.
Antoine Rauzy, Lakhdar Saïs, and Laure Brisoux. Calcul propositionnel: vers une extension du formalisme. In Actes des Cinquièmes Journées Nationales sur la Résolution Pratique de Problèmes NP-complets (JNPC’99), pages 189–198, Lyon, 1999.
Workshop on theory and applications of satisfiability testing, 2001. http://www.cs.washington.edu/homes/kautz/sat2001/.
Fifth international symposium on the theory and applications of satisfiability testing, May 2002. http://gauss.ececs.uc.edu/Conferences/SAT2002/.
Bart Selman, Henry A. Kautz, and David A. McAllester. Computational challenges in propositional reasoning and search. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI’97), volume 1, pages 50–54, Nagoya (Japan), August 1997.
A. Van Gelder. Extracting (easily) checkable proofs from a satisfiability solver that employs both preorder and postorder resolution. Annals of Mathematics and Artificial Intelligence, 2002. to appear.
Joost P. Warners and Hans van Maaren. A two phase algorithm for solving a class of hard satisfiability problems. Operations Research Letters, 23(3–5):81–88, 1999.
L. Zhang, C. Madigan, M. Moskewicz, and S. Malik. Efficient conflict driven learning in a boolean satisfiability solver. In Proceedigns of ICCAD’2001, pages 279–285, San Jose, CA (USA), November 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ostrowski, R., Grégoire, É., Mazure, B., Saïs, L. (2002). Recovering and Exploiting Structural Knowledge from CNF Formulas. In: Van Hentenryck, P. (eds) Principles and Practice of Constraint Programming - CP 2002. CP 2002. Lecture Notes in Computer Science, vol 2470. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46135-3_13
Download citation
DOI: https://doi.org/10.1007/3-540-46135-3_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44120-5
Online ISBN: 978-3-540-46135-7
eBook Packages: Springer Book Archive