Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Present and Future of Practical SAT Solving

  • Chapter
Complexity of Constraints

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

Abstract

We review current SAT solving, concentrating on the two paradigms of conflict-driven and look-ahead solvers, and with a view towards the unification of these two paradigms. A general “modern” scheme for DPLL algorithms is presented, which allows natural representations for “modern” solvers of these two types.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook
USD 15.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 15.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.

Similar content being viewed by others

References

  1. Ansótegui, C., Bonet, M.L., Levy, J., Manyà, F.: Mapping CSP into many-valued SAT. In: Marques-Silva and Sakallah [38], pp. 10–15, ISBN 978-3-540-72787-3

    Google Scholar 

  2. Bacchus, F., Winter, J.: Effective preprocessing with hyper-resolution and equality reduction. In: Giunchiglia and Tacchella [12], pp. 341–355, ISBN 3-540-20851-8

    Google Scholar 

  3. Beame, P., Kautz, H., Sabharwal, A.: Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research 22, 319–351 (2004)

    MathSciNet  MATH  Google Scholar 

  4. Böhm, M.: Verteilte Lösung harter Probleme: Schneller Lastausgleich. Ph.D thesis, Universität Köln (1996)

    Google Scholar 

  5. Dalal, M., Etherington, D.W.: A hierarchy of tractable satisfiability problems. Information Processing Letters 44, 173–180 (1992)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  7. Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM 7, 201–215 (1960)

    Article  MathSciNet  MATH  Google Scholar 

  8. Dequen, G., Dubois, O.: Kcnfs: An efficient solver for random k-SAT formulae. In: Giunchiglia and Tacchella [12], pp. 486–501, ISBN 3-540-20851-8

    Google Scholar 

  9. Dershowitz, N., Hanna, Z., Nadel, A.: Towards a better understanding of the functionality of a conflict-driven SAT solver. In: Marques-Silva and Sakallah [38], pp. 287–293, ISBN 978-3-540-72787-3

    Google Scholar 

  10. Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia and Tacchella [12], pp. 502–518, ISBN 3-540-20851-8

    Google Scholar 

  11. Freeman, J.W.: Improvements to propositional satisfiability search algorithms. PhD thesis, University of Pennsylvania (1995)

    Google Scholar 

  12. Giunchiglia, E., Tacchella, A. (eds.): SAT 2003. LNCS, vol. 2919. Springer, Heidelberg (2004)

    Google Scholar 

  13. Heule, M., Dufour, M., van Zwieten, J., van Maaren, H.: March_eq: Implementing additional reasoning into an efficient look-ahead SAT solver. In: Hoos and Mitchell [17], pp. 345–359, ISBN 3-540-27829-X

    Google Scholar 

  14. Heule, M., van Maaren, H.: Aligning CNF- and equivalence-reasoning. In: Hoos and Mitchell [17], pp. 145–156, ISBN 3-540-27829-X

    Google Scholar 

  15. Heule, M., van Maaren, H.: Effective incorporation of double look-ahead procedures. In: Marques-Silva and Sakallah [38], pp. 258–271, ISBN 978-3-540-72787-3

    Google Scholar 

  16. Heule, M.J.H., van Maaren, H.: Whose side are you on? Finding solutions in a biased search-tree (October 2007) (to appear)

    Google Scholar 

  17. Hoos, H.H., Mitchell, D.G. (eds.): SAT 2004. LNCS, vol. 3542. Springer, Heidelberg (2005)

    Google Scholar 

  18. Knuth, D.E.: Dancing links. Technical Report cs/0011047v1, arXiv (November 2000), http://www.arxiv.org/abs/cs/0011047v1

  19. Kullmann, O.: Investigating a general hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs. Technical Report TR99-041, Electronic Colloquium on Computational Complexity (ECCC) (October 1999)

    Google Scholar 

  20. Kullmann, O.: New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science 223(1-2), 1–72 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  21. Kullmann, O.: On a generalization of extended resolution. Discrete Applied Mathematics 96-97(1-3), 149–176 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  22. Kullmann, O.: Investigations on autark assignments. Discrete Applied Mathematics 107, 99–137 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  23. Kullmann, O.: On the use of autarkies for satisfiability decision. In: Kautz, H., Selman, B. (eds.) LICS 2001 Workshop on Theory and Applications of Satisfiability Testing (SAT 2001). Electronic Notes in Discrete Mathematics (ENDM), vol. 9. Elsevier Science, Amsterdam (2001)

    Google Scholar 

  24. Kullmann, O.: Investigating the behaviour of a SAT solver on random formulas. Technical Report CSR 23-2002, Swansea University, Computer Science Report Series (October 2002), http://www-compsci.swan.ac.uk/reports/2002.html

  25. Kullmann, O.: Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets. Discrete Applied Mathematics 130, 209–249 (2003)

    Article  MathSciNet  MATH  Google Scholar 

  26. Kullmann, O.: Upper and lower bounds on the complexity of generalised resolution and generalised constraint satisfaction problems. Annals of Mathematics and Artificial Intelligence 40(3-4), 303–352 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  27. Kullmann, O.: Constraint satisfaction problems in clausal form: Autarkies and minimal unsatisfiability. Technical Report TR 07-055, Electronic Colloquium on Computational Complexity (ECCC) (June 2007)

    Google Scholar 

  28. Kullmann, O.: Polynomial time SAT decision for complementation-invariant clause-sets, and sign-non-singular matrices. In: Marques-Silva and Sakallah [38], pp. 314–327, ISBN 978-3-540-72787-3

    Google Scholar 

  29. Kullmann, O.: Fundaments of branching heuristics. In: Biere, A., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. IOS Press, Amsterdam (2008)

    Google Scholar 

  30. Kullmann, O.: Fundaments of branching heuristics: Theory and examples. Technical Report CSR 7-2008, Swansea University, Computer Science Report Series (April 2008), http://www.swan.ac.uk/compsci/research/reports/2008/index.html

  31. Kullmann, O., Luckhardt, H.: Deciding propositional tautologies: Algorithms and their complexity, 82 pages (preprint) (January 1997), http://cs.swan.ac.uk/~csoliver/

  32. Kullmann, O., Luckhardt, H.: Algorithms for SAT/TAUT decision based on various measures, 71 pages (preprint) (December 1998), http://cs.swan.ac.uk/~csoliver/

  33. Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of clauses in conjunctive normal forms: Minimally unsatisfiable sub-clause-sets and the lean kernel. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 22–35. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  34. Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of 15th International Joint Conference on Artificial Intelligence (IJCAI 1997), pp. 366–371. Morgan Kaufmann Publishers, San Francisco (1997)

    Google Scholar 

  35. Liffiton, M., Sakallah, K.: Searching for autarkies to trim unsatisfiable clause sets. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 182–195. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  36. Lovász, L., Naor, M., Newman, I., Wigderson, A.: Search problems in the decision tree model. SIAM Journal on Discrete Mathematics 8(1), 119–132 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  37. Mahajan, Y.S., Fu, Z., Malik, S.: Zchaff2004: An efficient SAT solver. In: Hoos and Mitchell [17], pp. 360–375, ISBN 3-540-27829-X

    Google Scholar 

  38. Marques-Silva, J., Sakallah, K.A. (eds.): SAT 2007. LNCS, vol. 4501. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  39. Mitchell, D.G., Hwang, J.: 2-way vs. d-way branching for CSP. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 343–357. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  40. Monien, B., Speckenmeyer, E.: Solving satisfiability in less than 2n steps. Discrete Applied Mathematics 10, 287–295 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  41. Purdom, P.W.: Solving satisfiability with less searching. IEEE Transactions on Pattern Analysis and Machine Intelligence 6(4), 510–513 (1984)

    Article  MATH  Google Scholar 

  42. Segerlind, N.: The complexity of propositional proofs. The Bulletin of Symbolic Logic 13(4), 417–481 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  43. Marques Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999)

    Article  MathSciNet  Google Scholar 

  44. Simon, L., Le Berre, D.: The essentials of the SAT 2003 competition. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 452–467. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  45. Simon, L., Le Berre, D., Hirsch, E.A.: The SAT2002 competition. Annals of Mathematics and Artificial Intelligence 43, 307–342 (2005)

    Article  Google Scholar 

  46. Urquhart, A.: The complexity of propositional proofs. The Bulletin of Symbolic Logic 1(4), 425–467 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  47. Zhang, L.: On subsumption removal and on-the-fly CNF simplification. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 482–489. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  48. Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of the International Conference on Computer Aided Design (ICCAD), pp. 279–285. IEEE Press, Los Alamitos (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Swansea University, Swansea, SA2 8PP, UK

    Oliver Kullmann

Authors
  1. Oliver Kullmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. LIF (CNRS UMR 6166), Aix-Marseille Université, 163 avenue de Luminy, F-13288, Marseille, France

    Nadia Creignou

  2. IBM Almaden Research Center, Computer Science Principles and Methodologies, and Computer Science Department, University of California, Santa Cruz, USA

    Phokion G. Kolaitis

  3. Institut für Theoretische Informatik, Leibniz, Universität Hannover, Appelstr. 4, 30167, Hannover, Germany

    Heribert Vollmer

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Kullmann, O. (2008). Present and Future of Practical SAT Solving. In: Creignou, N., Kolaitis, P.G., Vollmer, H. (eds) Complexity of Constraints. Lecture Notes in Computer Science, vol 5250. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-92800-3_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-92800-3_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-92799-0

  • Online ISBN: 978-3-540-92800-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation