Skip to main content
SpringerLink
Log in

Cube-and-Conquer for Satisfiability

  • Chapter
  • First Online:
Book cover Handbook of Parallel Constraint Reasoning

Abstract

Satisfiability (SAT) is considered to be one of the most important core technologies in formal verification and related areas. Even though there is steady progress in improving practical SAT solving, there are limits on the scalability of SAT solvers. In this chapter, we present the cube-and-conquer paradigm which addresses this issue and targets reducing solving time on hard instances. This two-phase approach partitions a problem into many thousands (or millions) of cubes using lookahead techniques. Afterwards, a conflict-driven solver tackles the problem, using the cubes to guide the search. On several hard competition benchmarks, our hybrid approach outperforms both lookahead and conflict-driven solvers. Moreover, because cube-and-conquer is natural to parallelize, it is a competitive alternative for solving SAT problems in parallel. We demonstrate the strength of cube-and-conquer on the Boolean Pythagorean Triples problem, a recently solved challenge from Ramsey Theory. Cube-and-conquer achieves linear-time speedups on this problem even when using thousands of cores. Moreover, we show how to compute a proof for such a hard problem when solving it using cube-and-conquer.

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 89.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 119.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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. Tanbir Ahmed, Oliver Kullmann, and Hunter Snevily. On the van der Waerden numbers w(2;3; t). Discrete Applied Mathematics, 174:27–51, September 2014.

    Google Scholar 

  2. Fahiem Bacchus. Enhancing Davis Putnam with extended binary clause reasoning. In AAAI 2002, pages 613–619, 2002.

    Google Scholar 

  3. Armin Biere. PicoSAT essentials. JSAT, 4(2-4):75–97, 2008.

    Google Scholar 

  4. Armin Biere. Bounded model checking. In Biere et al. [6], chapter 14, pages 455–481.

    Google Scholar 

  5. Armin Biere. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT race 2010. 2010.

    Google Scholar 

  6. Armin Biere, Marijn J.H. Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of FAIA. IOS Press, February 2009.

    Google Scholar 

  7. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394–397, 1962.

    Google Scholar 

  8. Olivier Dubois and Gilles Dequen. A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In Bernhard Nebel, editor, IJCAI, pages 248–253. Morgan Kaufmann, 2001.

    Google Scholar 

  9. Niklas Eén and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, St. Andrews, UK, June 19-23, 2005, Proceedings, volume 3569 of Lecture Notes in Computer Science, pages 61–75. Springer, 2005.

    Google Scholar 

  10. Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, SAT, volume 2919 of LNCS, pages 502–518. Springer, 2003.

    Google Scholar 

  11. Niklas Eén and Niklas Sörensson. Temporal induction by incremental SAT solving. Electr. Notes Theor. Comput. Sci., 89(4):543–560, 2003.

    Google Scholar 

  12. Youssef Hamadi. Conclusion to the special issue on parallel SAT solving. JSAT, 6(4):263, 2009.

    Google Scholar 

  13. Youssef Hamadi, Saïd Jabbour, and Lakhdar Sais. ManySAT: a parallel SAT solver. JSAT, 6(4):245–262, 2009.

    Google Scholar 

  14. Robert M. Haralick and Gordon L. Elliott. Increasing tree search efficiency for constraint satisfaction problems. Artif. Intell., 14(3):263–313, 1980.

    Google Scholar 

  15. Willim D. Harvey and Matthew L. Ginsberg. Limited discrepancy search. In IJCAI 1995, pages 607–613, 1995.

    Google Scholar 

  16. Marijn J.H. Heule. The DRAT format and DRAT-trim checker. CoRR, http://arXiv.org/abs/1610.06229, 2016. Source code available from: https://github.com/marijnheule/drat-trim.

  17. Marijn J.H. Heule, Warren A. Hunt, Jr, and Nathan Wetzler. Verifying refutations with Extended Resolution. In CADE, volume 7898 of LNAI, pages 345–359. Springer, 2013.

    Google Scholar 

  18. Marijn J.H. Heule and Hans van Maaren. Look-Ahead Based SAT Solvers, chapter 5, pages 155–184. Volume 185 of Biere et al. [6], February 2009.

    Google Scholar 

  19. Marijn J.H. Heule, Mark Dufour, Joris E. van Zwieten, and Hans van Maaren. March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver. In Holger H. Hoos and David G. Mitchell, editors, SAT (Selected Papers, volume 3542 of Lecture Notes in Computer Science, pages 345–359. Springer, 2004.

    Google Scholar 

  20. Marijn J.H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the boolean Pythagorean Triples problem via Cube-and-Conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016, volume 9710 of Lecture Notes in Computer Science, pages 228–245. Springer, 2016.

    Google Scholar 

  21. Marijn J.H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding CDCL SAT solvers by lookaheads. In Kerstin Eder, João Lourenço, and Onn Shehory, editors, Hardware and Software: Verification and Testing (HVC 2011), volume 7261 of Lecture Notes in Computer Science (LNCS), pages 50–65. Springer, 2012.

    Google Scholar 

  22. Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Partitioning SAT instances for distributed solving. In LPAR-17, volume 6397 of LNCS, pages 372–386, 2010.

    Google Scholar 

  23. Antti E. J. Hyvärinen, Tommi Junttila, and Ilkka Niemelä. Grid-based SAT solving with iterative partitioning and clause learning. In CP 2011, volume 6876 of LNCS, 2011.

    Google Scholar 

  24. Hans Kleine Büning and Oliver Kullmann. Minimal Unsatisfiability and Autarkies, chapter 11, pages 339–401. Volume 185 of Biere et al. [6], February 2009.

    Google Scholar 

  25. Oliver Kullmann. Investigating the behaviour of a SAT solver on random formulas. Technical Report CSR 23-2002, University of Wales Swansea, Computer Science Report Series, October 2002. 119 pages.

    Google Scholar 

  26. Oliver Kullmann. Fundaments of Branching Heuristics, chapter 7, pages 205–244. Volume 185 of Biere et al. [6], February 2009.

    Google Scholar 

  27. Oliver Kullmann. The OKlibrary: Introducing a “holistic” research platform for (generalised) SAT solving. Studies in Logic, 2(1):20–53, 2009.

    Google Scholar 

  28. Oliver Kullmann. Green-Tao numbers and SAT. In Ofer Strichman and Stefan Szeider, editors, SAT 2010, volume 6175 of LNCS, pages 352–362. Springer, 2010.

    Google Scholar 

  29. Chu Min Li and Anbulagan. Heuristics based on unit propagation for satisfiability problems. In IJCAI (1), pages 366–371, 1997.

    Google Scholar 

  30. Norbert Manthey, Marijn J.H. Heule, and Armin Biere. Automated reencoding of Boolean formulas. In Proceedings of Haifa Verification Conference 2012, 2012.

    Google Scholar 

  31. Joao P. Marques-Silva, Ines Lynce, and Sharad Malik. Conflict-Driven Clause Learning SAT Solvers, chapter 4, pages 131–153. Volume 185 of Biere et al. [6], February 2009.

    Google Scholar 

  32. Sid Mijnders, Boris de Wilde, and Marijn J.H. Heule. Symbiosis of search and heuristics for random 3-SAT. In David Mitchell and Eugenia Ternovska, editors, LaSh 2010, 2010.

    Google Scholar 

  33. Peter van Beek. Backtracking search algorithms. In Francesca Rossi, Peter van Beek, and Toby Walsh, editors, Handbook of Constraint Programming, chapter 4, pages 85–134. 2006.

    Google Scholar 

  34. Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In ISAIM, 2008.

    Google Scholar 

  35. Nathan Wetzler, Marijn J.H. Heule, and Warren A. Hunt, Jr. DRAT-trim: Efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, SAT 2014, volume 8561 of LNCS, pages 422–429. Springer, 2014.

    Google Scholar 

  36. Siert Wieringa, Matti Niemenmaa, and Keijo Heljanko. Tarmo: A framework for parallelized bounded model checking. In Lubos Brim and Jaco van de Pol, editors, PDMC, volume 14 of EPTCS, pages 62–76, 2009.

    Google Scholar 

  37. Hantao Zhang. Combinatorial designs by SAT solvers. In Biere et al. [6], chapter 17, pages 533–568.

    Google Scholar 

  38. Lintao Zhang and Sharad Malik. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In DATE, pages 10880–10885, 2003.

    Google Scholar 

Download references

Acknowledgements

The authors thank Siert Wieringa for his contributions to Section 2.6.2 and Peter van der Tak for his contributions to Section 2.7.2.

Author information

Authors and Affiliations

  1. The University of Texas at Austin, Austin, USA

    Marijn J. H. Heule

  2. Swansea University, Swansea, UK

    Oliver Kullmann

  3. Johannes Kepler University, Linz, Austria

    Armin Biere

Authors
  1. Marijn J. H. Heule
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Oliver Kullmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Armin Biere
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marijn J. H. Heule .

Editor information

Editors and Affiliations

  1. Laboratoire d'informatique (LIX) de l'École polytechnique, Palaiseau, France

    Youssef Hamadi

  2. CRIL, CNRS UMR 8188, Université d'Artois, Lens, France

    Lakhdar Sais

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Heule, M.J.H., Kullmann, O., Biere, A. (2018). Cube-and-Conquer for Satisfiability. In: Hamadi, Y., Sais, L. (eds) Handbook of Parallel Constraint Reasoning. Springer, Cham. https://doi.org/10.1007/978-3-319-63516-3_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63516-3_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63515-6

  • Online ISBN: 978-3-319-63516-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation