Skip to main content
SpringerLink
Log in
Book cover

International Conference on Integration of Artificial Intelligence (AI) and Operations Research (OR) Techniques in Constraint Programming

CPAIOR 2007: Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems pp 71–83Cite as

Eliminating Redundant Clauses in SAT Instances

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4510))

Abstract

In this paper, we investigate to which extent the elimination of a class of redundant clauses in SAT instances could improve the efficiency of modern satisfiability provers. Since testing whether a SAT instance does not contain any redundant clause is NP-complete, a logically incomplete but polynomial-time procedure to remove redundant clauses is proposed as a pre-treatment of SAT solvers. It relies on the use of the linear-time unit propagation technique and often allows for significant performance improvements of the subsequent satisfiability checking procedure for really difficult real-world instances.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Selman, B., Levesque, H.J., Mitchell, D.G.: A new method for solving hard satisfiability problems. In: Proceedings of the Tenth National Conference on Artificial Intelligence (AAAI’92), pp. 440–446 (1992)

    Google Scholar 

  2. Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem-proving. Communications of the ACM 5(7), 394–397 (1962)

    Article  MATH  MathSciNet  Google Scholar 

  3. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC’01), pp. 530–535 (2001)

    Google Scholar 

  4. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)

    Google Scholar 

  5. Dubois, O., Dequen, G.: A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI’01), pp. 248–253 (2001)

    Google Scholar 

  6. Williams, R., Gomes, C.P., Selman, B.: Backdoors to typical case complexity. In: Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI’03), pp. 1173–1178 (2003)

    Google Scholar 

  7. Liberatore, P.: The complexity of checking redundancy of CNF propositional formulae. In: Proceedings of the 15th European Conference on Artificial Intelligence (ECAI’02), pp. 262–266 (2002)

    Google Scholar 

  8. Grégoire, É., Ostrowski, R., Mazure, B., Saïs, L.: Automatic extraction of functional dependencies. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 122–132. Springer, Heidelberg (2005)

    Google Scholar 

  9. Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, pp. 151–158. Association for Computing Machinery, New York (1971)

    Chapter  Google Scholar 

  10. Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1, 146–160 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  11. Even, S., Itai, A., Shamir, A.: On the complexity of timetable and multicommodity flow problems. SIAM J. Comput. 5, 691–703 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  12. Dowling, W.H., Gallier, J.H.: Linear-time algorithms for testing satisfiability of propositional horn formulae. Journal of Logic Programming 1(3), 267–284 (1984)

    Article  MathSciNet  Google Scholar 

  13. Wei, W., Selman, B.: Accelerating random walks. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 216–232. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  14. Kautz, H.A., Ruan, Y., Achlioptas, D., Gomes, C.P., Selman, B., Stickel, M.E.: Balance and filtering in structured satisfiable problems. In: Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI’01), pp. 351–358 (2001)

    Google Scholar 

  15. Dubois, O., André, P., Boufkhad, Y., Carlier, Y.: SAT vs. UNSAT. In: Second DIMACS implementation challenge: cliques, coloring and satisfiability. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 415–436. American Mathematical Society, New York (1996)

    Google Scholar 

  16. Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI’97), pp. 366–371 (1997)

    Google Scholar 

  17. Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)

    Google Scholar 

  18. Subbarayan, S., Pradhan, D.K.: NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 276–291. Springer, Heidelberg (2005)

    Google Scholar 

  19. Crawford, J.: A polynomial-time preprocessor (”compact”) (1996), http://www.cirl.uoregon.edu/crawford/

  20. Zhang, W.: Configuration landscape analysis and backbone guided local search: Part i: Satisfiability and maximum satisfiability. Artificial Intelligence 158(1), 1–26 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  21. Le Berre, D.: Exploiting the real power of unit propagation lookahead. In: Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT’01), Boston University, Massachusetts, USA (2001)

    Google Scholar 

  22. Ostrowski, R., Mazure, B., Saïs, L., Grégoire, É.: Eliminating redundancies in SAT search trees. In: Proceedings of the 15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI’2003), Sacramento, pp. 100–104 (2003)

    Google Scholar 

  23. Darras, S., Dequen, G., Devendeville, L., Mazure, B., Ostrowski, R., Saïs, L.: Using boolean constraint propagation for sub-clauses deduction. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 757–761. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  24. Boufkhad, Y., Roussel, O.: Redundancy in random SAT formulas. In: Proceedings of the 17th National Conference on Artificial Intelligence (AAAI’00), pp. 273–278 (2000)

    Google Scholar 

  25. Liberatore, P.: Redundancy in logic i: CNF propositional formulae. Artificial Intelligence 163(2), 203–232 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  26. Selman, B., Kautz, H.A.: Knowledge compilation using horn approximations. In: Proceedings of the 9th National Conference on Artificial Intelligence (AAAI’91), pp. 904–909 (1991)

    Google Scholar 

  27. del Val, A.: Tractable databases: How to make propositional unit resolution complete through compilation. In: Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR’94), pp. 551–561 (1994)

    Google Scholar 

  28. Marquis, P.: Knowledge compilation using theory prime implicates. In: Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI’95), Montréal, Canada, pp. 837–843 (1995)

    Google Scholar 

  29. Mazure, B., Marquis, P.: Theory reasoning within implicant cover compilations. In: Proceedings of the ECAI’96 Workshop on Advances in Propositional Deduction, Budapest, Hungary, pp. 65–69 (1996)

    Google Scholar 

  30. Grégoire, É., Mazure, B., Piette, C.: Extracting MUSes. In: Proceedings of the 17th European Conference on Artificial Intelligence (ECAI’06), Trento, Italy, pp. 387–391 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIL CNRS & IRCICA, Université d’Artois, Rue Jean Souvraz SP18, F-62307 Lens Cedex, France

    Olivier Fourdrinoy, Éric Grégoire, Bertrand Mazure & Lakhdar Saïs

Authors
  1. Olivier Fourdrinoy
    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

Pascal Van Hentenryck Laurence Wolsey

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer Berlin Heidelberg

About this paper

Cite this paper

Fourdrinoy, O., Grégoire, É., Mazure, B., Saïs, L. (2007). Eliminating Redundant Clauses in SAT Instances. In: Van Hentenryck, P., Wolsey, L. (eds) Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems. CPAIOR 2007. Lecture Notes in Computer Science, vol 4510. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72397-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-72397-4_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-72396-7

  • Online ISBN: 978-3-540-72397-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation