Skip to main content
SpringerLink
Log in

Recovering and Exploiting Structural Knowledge from CNF Formulas

  • Conference paper
  • First Online:
Book cover Principles and Practice of Constraint Programming - CP 2002 (CP 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2470))

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. First international competition and symposium on satisfiability testing, March 1996. Beijing (China).

    Google Scholar 

  2. 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.

    Google Scholar 

  3. 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.

    Google Scholar 

  4. M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Journal of the Association for Computing Machinery, 5:394–397, 1962.

    Article  MathSciNet  MATH  Google Scholar 

  5. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the Association for Computing Machinery, 7:201–215, 1960.

    Article  MathSciNet  MATH  Google Scholar 

  6. Second Challenge on Satisfiability Testing organized by the Center for Discrete Mathematics and Computer Science of Rutgers University, 1993. http://dimacs.rutgers.edu/Challenges/.

  7. 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.

    Google Scholar 

  8. 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.

    Google Scholar 

  9. B. Dunham and H. Wang. Towards feasible solution of the tautology problem. Annals of Mathematical Logic, 10:117–154, 1976.

    Article  MathSciNet  MATH  Google Scholar 

  10. 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.

    Google Scholar 

  11. Robert G. Jeroslow and Jinchang Wang. Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence, 1:167–187, 1990.

    Article  MATH  Google Scholar 

  12. 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.

    Google Scholar 

  13. 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.

    Google Scholar 

  14. Oliver Kullmann. New methods for 3-sat decision and worst-case analysis. Theoretical Computer Science, pages 1–72, 1997.

    Google Scholar 

  15. 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.

    Google Scholar 

  16. 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.

    Google Scholar 

  17. 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.

    Google Scholar 

  18. 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.

    Google Scholar 

  19. 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.

    Google Scholar 

  20. Shtrichman Oler. Tuning sat checkers for bounded model checking. In Proceedings of Computer Aided Verification (CAV’00), 2000.

    Google Scholar 

  21. 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.

    Google Scholar 

  22. Workshop on theory and applications of satisfiability testing, 2001. http://www.cs.washington.edu/homes/kautz/sat2001/.

  23. Fifth international symposium on the theory and applications of satisfiability testing, May 2002. http://gauss.ececs.uc.edu/Conferences/SAT2002/.

  24. 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.

    Google Scholar 

  25. 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.

    Google Scholar 

  26. 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.

    Google Scholar 

  27. 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.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIL CNRS — Université d’Artois, rue Jean Souvraz SP-18, F-62307, Lens Cedex, France

    Richard Ostrowski, Éric Grégoire, Bertrand Mazure & Lakhdar Saïs

Authors
  1. Richard Ostrowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Éric Grégoire
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bertrand Mazure
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lakhdar Saïs
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Brown University, Box 1910, Providence, RI, 02912, USA

    Pascal Van Hentenryck

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation