Skip to main content
SpringerLink
Log in
Book cover

International Conference on Theory and Applications of Satisfiability Testing

SAT 2005: Theory and Applications of Satisfiability Testing pp 143–157Cite as

Resolution Tunnels for Improved SAT Solver Performance

  • Conference paper

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

Abstract

We show how to aggressively add uninferred constraints, in a controlled manner, to formulae for finding Van der Waerden numbers during search. We show that doing so can improve the performance of standard SAT solvers on these formulae by orders of magnitude. We obtain a new and much greater lower bound for one of the Van der Waerden numbers, specifically a bound of 1132 for W(2,6). We believe this bound to actually be the number we seek. The structure of propositional formulae for solving Van der Waerden numbers is similar to that of formulae arising from Bounded Model Checking. Therefore, we view this as a preliminary investigation into solving hard formulae in the area of Formal Verification.

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. Akers, S.B.: Binary decision diagrams. IEEE Transactions on Computers C-27(6), 509–516 (1978)

    Article  MATH  Google Scholar 

  2. Beame, P., Pitassi, T.: Simplified and improved resolution lower bounds. In: Proc. 37th Annual Symposium on Foundations of Computer Science, pp. 274–282 (1996)

    Google Scholar 

  3. Beame, P., Karp, R.M., Pitassi, T., Saks, M.: On the complexity of unsatisfiability proofs for random k-CNF formulas. In: Proc. 30th Annual Symposium on the Theory of Computing, pp. 561–571 (1998)

    Google Scholar 

  4. Ben-Sasson, E., Wigderson, A.: Short proofs are narrow - resolution made simple. Journal of the Association for Computing Machinery 48, 149–169 (2001)

    MATH  MathSciNet  Google Scholar 

  5. Brace, K.S., Rudell, R.R., Bryant, R.E.: Efficient implementation of a BDD package. In: Proc. 27th ACM/IEEE Design Automation Conf., pp. 40–45 (1990)

    Google Scholar 

  6. Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. on Comp. C-35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  7. Burch, J., Clark, E., Long, D.: Symbolic model checking with partitioned transitions relations. In: Halaas, A., Denyer, P.B. (eds.) Intnl. Conf. on VLSI. IFIP Transactions, pp. 49–58. North-Holland, Amsterdam (1991)

    Google Scholar 

  8. Chvátal, V., Szemerédi, E.: Many hard examples for resolution. Journal of the Association for Computing Machinery 35, 759–768 (1988)

    MATH  MathSciNet  Google Scholar 

  9. Cooke, M.: Van der Waerden numbers, Available from http://home.comcast.net/~rm_cooke/vdw.html

  10. Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the Association of Computing Machinery 5, 394–397 (1962)

    MATH  MathSciNet  Google Scholar 

  11. Dransfield, M.R., Liu, L., Marek, V., Truszczynski, M.: Using Answer-Set Programming to study van der Waerden numbers. Logic and Artificial Intelligence Laboratory, Computer Science Department, College of Enginnering, University of Kentucky (September 2004), Available from http://cs.engr.uky.edu/ai/vdw/

  12. Dransfield, M., Bryant, R.E.: Using ordered binary decision diagrams to solve highly structured satisfiability problems. Unpublished technical report CMU-CS-1996, Carnegie Mellon University (1996)

    Google Scholar 

  13. Galil, Z.: On resolution with clauses of bounded size. SIAM Journal on Computing 6, 444–459 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  14. Gent, I.P., Walsh, T.: Towards an understanding of hill-climbing procedures for SAT. In: Proc. 11th National Conference on Artificial Intelligence, pp. 28–33 (1993)

    Google Scholar 

  15. Groote, J.F.: Hiding propositional constants in BDDs. Logic Group Preprint Series 120, Utrecht University (1994)

    Google Scholar 

  16. Gu, J.: Efficient local search for very large-scale satisfiability problems. ACM SIGART Bulletin 3(1), 8–12 (1992)

    Article  Google Scholar 

  17. Gu, J., Purdom, P.W., Franco, J., Wah, J.: Algorithms for the Satisfiability problem: a survey. DIMACS Series on Discrete Mathematics and Theoretical Computer Science, vol. 35, pp. 19–151 (1997)

    Google Scholar 

  18. Haken, A.: The intractability of resolution. Theoretical Computer Science 39, 297–308 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  19. Lee, C.Y.: Representation of switching circuits by binary-decision programs. Bell System Technical Journal 38, 985–999 (1959)

    MathSciNet  Google Scholar 

  20. McAllester, D., Selman, B., Kautz, H.A.: Evidence for invariants in local search. In: Proc. International Joint Conference on Artificial Intelligence, pp. 321–326 (1997)

    Google Scholar 

  21. Monien, B., Speckenmeyer, E.: Solving satisfiability in less than 2n steps. Discrete Applied Mathematics 10, 117–133 (1983)

    MathSciNet  Google Scholar 

  22. Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12, 23–41 (1965)

    Article  MATH  Google Scholar 

  23. Pan, G., Vardi, M.Y.: Search vs. symbolic techniques in satisfiability solving. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 235–250. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  24. San Miguel Aguirre, A., Vardi, M.Y.: Random 3-SAT and BDDs: The plot thickens further. In: Walsh, T. (ed.) CP 2001. LNCS, vol. 2239, pp. 121–136. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  25. Selman, B., Kautz, H.A., Cohen, B.: Noise strategies for improving local search. In: Proc. 12th National Conference on Artificial Intelligence, pp. 337–343 (1994)

    Google Scholar 

  26. Somenzi, F.: Colorado University Decision Diagram package, Available from http://vlsi.colorado.edu/~fabio/CUDD/

  27. Song, H.Y., Golomb, S.W., Taylor, H.: Progressions in Every Two-coloration of Z n . Journal of Combinatorial Theory, Series A 61(2), 211–221 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  28. Rabung, J.R.: Some Progression-Free Partitions Constructed Using Folkman’s Method. Canadian Mathematical Bulletin 22(1), 87–91 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  29. Urquhart, A.: Hard examples for resolution. Journal of the Association for Computing Machinery 34, 209–219 (1987)

    MATH  MathSciNet  Google Scholar 

  30. Van der Waerden, B.L.: Beweis einer Baudetschen Veermutung. Nieuw Archief voor Wiskunde 15, 212–216 (1927)

    Google Scholar 

  31. Weaver, S.A., Franco, J., Schlipf, J.S.: Extending Existential Quantification in Conjunctions of BDDs. University of Cincinnati Technical Report

    Google Scholar 

  32. Weisstein, E.W., et al.: van der Waerden Number, From MathWorld–A Wolfram Web Resource, http://mathworld.wolfram.com/vanderWaerdenNumber.html

Download references

Author information

Authors and Affiliations

  1. University of Cincinnati, Cincinnati, OH, 45221-0030, USA

    Michal Kouril & John Franco

Authors
  1. Michal Kouril
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. John Franco
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Toronto, Canada

    Fahiem Bacchus

  2. Dept. of Computer Science, Trinity College, Dublin 2

    Toby Walsh

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kouril, M., Franco, J. (2005). Resolution Tunnels for Improved SAT Solver Performance. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_11

Download citation

  • DOI: https://doi.org/10.1007/11499107_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-26276-3

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation