skip to main content
research-article
Free Access

Boolean satisfiability from theoretical hardness to practical success

Published:01 August 2009Publication History
Skip Abstract Section

Abstract

Satisfiability solvers can now be effectively deployed in practical applications.

References

  1. ]]Barrett, C., sebastiani, R., Seshia, S., and Tinelli, C. Satisfiability modulo theories. A. Biere, H. van Maaren, T. Walsh, Eds. Handbook of Satisfiability 4, 8 (2009), IOS Press, Amsterdam.Google ScholarGoogle Scholar
  2. ]]Bayardo R., and Schrag, R. Using CSP look-back techniques to solve real-world SAT instances. National Conference on Artificial Intelligence, 1997. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. ]]Biere, A., Cimatti, A., Clarke, E. M., and Zhu, Y. Symbolic model checking without BDDs. Tools and Algorithms for the Analysis and Construction of Systems, 1999. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. ]]Braunstein, A., Mezard, M., and Zecchina, R. Survey propagation: An algorithm for Satisfiability. Random Structures and Algorithms 27 (2005), 201--226. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. ]]Bryant, R.E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35 (1986), 677--691. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. ]]Clarke, E.M., Grumberg, O., and Peled, D.A. Model Checking. MIT Press, Cambridge, MA, 1999. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. ]]Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., and Vardi, M.Y. Benefits of bounded model checking at an industrial setting. Proceedings of the 13th International Conference on Computer-Aided Verification, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. ]]Cook, S.A. The complexity of theorem-proving procedures. Third Annual ACM Symposium on Theory of Computing, 1971. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. ]]Davis, M., Logemann, G., and Loveland, D. A machine program for theorem proving. Comm. ACM 5 (1962), 394--397. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. ]]Davis, M., and Putnam, H. A computing procedure for quantification theory. JACM 7 (1960), 201--215. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. ]]Eén, N., and Biere, A. Effective preprocessing in SAT through variable and clause elimination. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. ]]Garey, M.R., and Johnson, D.S. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979 Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. ]]Gomes, C. P., Selman, B., and Kautz, H. Boosting combinatorial search through randomization. In Proceedings of National Conference on Artificial Intelligence (Madison, WI, 1998). Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. ]]Hamadi, Y., Jabbour, S., and Sais, L. ManySat: Solver description. Microsoft Research, TR-2008-83.Google ScholarGoogle Scholar
  15. ]]Huth, M. and Ryan, M. Logic in Computer Science: Modeling and Reasoning about Systems. Cambridge University Press, 2004. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. ]]Hutter, F., Babic, D., Hoos, H.H., and Hu, A. J. Boosting verification by automatic tuning of decision procedures. In Proceedings of the International Conference on Formal Methods in Computer-Aided Design, (Austin, TX, Nov. 2007). Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. ]]Jackson, D., and Vaziri, M., Finding bugs with a constraint solver. In Proceedings of the International Symposium on Software Testing and Analysis (Portland, OR, 2000). Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. ]]Jain, H. Verification using satisfiability checking, predicate abstraction, and Craig interpolation. Ph.D. Thesis, Carnegie-Mellon University, School of Computer Science, CMU-CS-08-146, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. ]]Johnson, D.S., Mehrotra, A., and Trick, M. A. Preface: special issue on computational methods for graph coloring and its generalizations. Discrete Applied Mathematics 156, 2; Computational Methods for Graph Coloring and its Generalizations. (Jan. 15, 2008), 145--146. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. ]]Kautz, H. and Selman, B. Planning as satisfiability. European Conference on Artificial Intelligence, 1992. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. ]]Larrabee, T. Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design (Jan. 1992) 4--15.Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. ]]Madigan, M.W., Madigan, C.F., Zhao, Y., Zhang, L., and Malik, S. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Conference on Design Automation. (New York, NY, 2001). Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. ]]Marchiori, E. and Rossi, C. A flipping genetic algorithm for hard 3-SAT problems. In Proceedings of the Genetic and Evolutionary Computation Conference (Orlando, FL, 1999), 393--400.Google ScholarGoogle Scholar
  24. ]]Marques-Silva, J.P, and Sakallah, K.A. Conflict analysis in search algorithms for propositional satisfiability. IEEE International Conference on Tools with Artificial Intelligence, 1996. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. ]]Mazure, B., Sas L., and Grgoire, E., Tabu search for SAT. In Proceedings of the 14th National Conference on Artificial Intelligence (Providence, RI, 1997). Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. ]]McMillan, K.L., Applying SAT methods in unbounded symbolic model checking. In Proceedings of the 14th International Conference on Computer Aided Verification. Lecture Notes In Computer Science 2404 (2002). Springer-Verlag, London, 250--264. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. ]]Muscettola, N., Pandurang Nayak, P., Pell, B., and Williams, B.C. Remote agent: To boldly go where no AI system has gone before. Artificial Intelligence 103, 1--2, (1998), 5--47. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. ]]Nam, G.-J., Sakallah, K. A., and Rutenbar, R.A. Satisfiability-based layout revisited: Detailed routing of complex FPGAs via search-based Boolean SAT. International Symposium on Field-Programmable Gate Arrays (Monterey, CA, 1999). Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. ]]Narain, S., Levin, G., Kaul, V., Malik, S. Declarative infrastructure configuration and debugging. Journal of Network Systems and Management, Special Issue on Security Configuration. Springer, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. ]]Selman, B., Kautz, H.A., and Cohen, B. Noise strategies for improving local search. In Proceedings of the 12th National Conference on Artificial Intelligence (Seattle, WA, 1994). American Association for Artificial Intelligence, Menlo Park, CA, 337--343. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. ]]Selman, B., Levesque, H., and Mitchell, D. A new method for solving hard satisfiability problems. In Proceedings of the 10th National Conference on Artificial Intelligence, (1992) 440--446.Google ScholarGoogle ScholarDigital LibraryDigital Library
  32. ]]Seshia, S.A., Lahiri, S.K., and Bryant, R.E. a hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In Proceedings of the 40th Conference on Design Automation (Anaheim, CA, June 2--6, 2003). ACM, NY, 425--430; http://doi.acm.org/10.1145/775832.775945. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. ]]Spears, W.M. Simulated annealing for hard satisfiability problems. Cliques, Coloring and Satisfiability, Second DIMACS Implementation Challenge. DIMACS Series in Discrete Mathematics and Theoretical Computer Science. D.S. Johnson and M.A. Trick, Eds. American Mathematical Society (1993), 533--558.Google ScholarGoogle Scholar
  34. ]]Spears, W. M. A NN algorithm for Boolean satisfiability problems. In Proceedings of the 1996 International Conference on Neural Networks, 1121--1126.Google ScholarGoogle Scholar
  35. ]]Stålmarck, G. A system for determining prepositional logic theorems by applying values and rules to triplets that are generated from a formula. U.S. Patent Number 5276897, 1994.Google ScholarGoogle Scholar
  36. ]]Tseitin, G. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 2 (1968), 115--125. Reprinted in Automation of reasoning vol. 2. J. Siekmann and G. Wrightson, Eds. Springer Verlag, Berlin, 1983, 466--483.Google ScholarGoogle Scholar
  37. ]]Williams, R., Gomes, C., and Selman, B. Backdoors to typical case complexity. In Proceedings. of the 18th International Joint Conference on Artificial Intelligence (2003), 1173--1178. Google ScholarGoogle ScholarDigital LibraryDigital Library
  38. ]]Williams, R., Gomes, C., and Selman, B. On the connections between heavy-tails, backdoors, and restarts in combinatorial search. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, 2003.Google ScholarGoogle Scholar
  39. ]]Xu, L., Hutter, F., Hoos, H. H., Leyton-Brown, K. SATzilla: Portfolio-based algorithm selection for SAT. Journal of Artificial Intelligence Research 32, (2008), 565--606. Google ScholarGoogle ScholarDigital LibraryDigital Library
  40. ]]Zhang, H. Generating college conference basketball schedules by a SAT solver. In Proceedings of the 5th International Symposium on Theory and Applications of Satisfiability Testing. (Cincinnati, OH, 2002).Google ScholarGoogle Scholar

Index Terms

  1. Boolean satisfiability from theoretical hardness to practical success
    Index terms have been assigned to the content through auto-classification.

    Recommendations

    Comments

    Login options

    Check if you have access through your login credentials or your institution to get full access on this article.

    Sign in

    Full Access

    • Published in

      cover image Communications of the ACM
      Communications of the ACM  Volume 52, Issue 8
      A Blind Person's Interaction with Technology
      August 2009
      132 pages
      ISSN:0001-0782
      EISSN:1557-7317
      DOI:10.1145/1536616
      Issue’s Table of Contents

      Copyright © 2009 ACM

      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      • Published: 1 August 2009

      Permissions

      Request permissions about this article.

      Request Permissions

      Check for updates

      Qualifiers

      • research-article
      • Popular
      • Refereed

    PDF Format

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    HTML Format

    View this article in HTML Format .

    View HTML Format