Abstract
Satisfiability solvers can now be effectively deployed in practical applications.
- ]]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 Scholar
- ]]Bayardo R., and Schrag, R. Using CSP look-back techniques to solve real-world SAT instances. National Conference on Artificial Intelligence, 1997. Google ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]Braunstein, A., Mezard, M., and Zecchina, R. Survey propagation: An algorithm for Satisfiability. Random Structures and Algorithms 27 (2005), 201--226. Google ScholarDigital Library
- ]]Bryant, R.E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35 (1986), 677--691. Google ScholarDigital Library
- ]]Clarke, E.M., Grumberg, O., and Peled, D.A. Model Checking. MIT Press, Cambridge, MA, 1999. Google ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]Cook, S.A. The complexity of theorem-proving procedures. Third Annual ACM Symposium on Theory of Computing, 1971. Google ScholarDigital Library
- ]]Davis, M., Logemann, G., and Loveland, D. A machine program for theorem proving. Comm. ACM 5 (1962), 394--397. Google ScholarDigital Library
- ]]Davis, M., and Putnam, H. A computing procedure for quantification theory. JACM 7 (1960), 201--215. Google ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]Garey, M.R., and Johnson, D.S. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979 Google ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]Hamadi, Y., Jabbour, S., and Sais, L. ManySat: Solver description. Microsoft Research, TR-2008-83.Google Scholar
- ]]Huth, M. and Ryan, M. Logic in Computer Science: Modeling and Reasoning about Systems. Cambridge University Press, 2004. Google ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]Kautz, H. and Selman, B. Planning as satisfiability. European Conference on Artificial Intelligence, 1992. Google ScholarDigital Library
- ]]Larrabee, T. Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design (Jan. 1992) 4--15.Google ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 Scholar
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 ScholarDigital Library
- ]]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 Scholar
- ]]Spears, W. M. A NN algorithm for Boolean satisfiability problems. In Proceedings of the 1996 International Conference on Neural Networks, 1121--1126.Google Scholar
- ]]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 Scholar
- ]]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 Scholar
- ]]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 ScholarDigital Library
- ]]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 Scholar
- ]]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 ScholarDigital Library
- ]]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 Scholar
Index Terms
Boolean satisfiability from theoretical hardness to practical success
Recommendations
A satisfiability procedure for quantified boolean formulae
The renesse issue on satisfiabilityWe present a satisfiability tester QSAT for quantified Boolean formulae and a restriction QSATCNF of QSAT to unquantified conjunctive normal form formulae. QSAT makes use of procedures which replace subformulae of a formula by equivalent formulae. By a ...
Backjumping for quantified Boolean logic satisfiability
The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision procedures have been proposed in the last few years, most of ...
Backjumping for quantified Boolean logic satisfiability
IJCAI'01: Proceedings of the 17th international joint conference on Artificial intelligence - Volume 1The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision procedures have been proposed in the last few years, most of ...
Comments