Boolean satisfiability from theoretical hardness to practical success

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.
• 2: Bayardo R., and Schrag, R. Using CSP look-back techniques to solve real-world SAT instances. National Conference on Artificial Intelligence, 1997.
• 3: Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
• 4: A. Braunstein , M. Mézard , R. Zecchina, Survey propagation: An algorithm for satisfiability, Random Structures & Algorithms, v.27 n.2, p.201-226, September 2005 [doi>10.1002/rsa.v27:2]
• 5: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 6: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 7: Fady Copty , Limor Fix , Ranan Fraer , Enrico Giunchiglia , Gila Kamhi , Armando Tacchella , Moshe Y. Vardi, Benefits of Bounded Model Checking at an Industrial Setting, Proceedings of the 13th International Conference on Computer Aided Verification, p.436-453, July 18-22, 2001
• 8: Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing, p.151-158, May 03-05, 1971, Shaker Heights, Ohio, United States [doi>10.1145/800157.805047]
• 9: Martin Davis , George Logemann , Donald Loveland, A machine program for theorem-proving, Communications of the ACM, v.5 n.7, p.394-397, July 1962 [doi>10.1145/368273.368557]
• 10: Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
• 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.
• 12: Michael R. Garey , David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman & Co., New York, NY, 1979
• 13: Carla P. Gomes , Bart Selman , Henry Kautz, Boosting combinatorial search through randomization, Proceedings of the fifteenth national/tenth conference on Artificial intelligence/Innovative applications of artificial intelligence, p.431-437, July 1998, Madison, Wisconsin, United States
• 14: Hamadi, Y., Jabbour, S., and Sais, L. ManySat: Solver description. Microsoft Research, TR-2008-83.
• 15: Michael Huth , Mark Ryan, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, New York, NY, 2004
• 16: Frank Hutter , Domagoj Babic , Holger H. Hoos , Alan J. Hu, Boosting Verification by Automatic Tuning of Decision Procedures, Proceedings of the Formal Methods in Computer Aided Design, p.27-34, November 11-14, 2007 [doi>10.1109/FMCAD.2007.13]
• 17: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 18: Himanshu Jain , Edmund M. Clarke, Verification using satisfiability checking, predicate abstraction, and craig interpolation, Carnegie Mellon University, Pittsburgh, PA, 2008
• 19: David S. Johnson , Anuj Mehrotra , Michael A. Trick, Preface: Special issue on computational methods for graph coloring and its generalizations, Discrete Applied Mathematics, v.156 n.2, p.145-146, January, 2008 [doi>10.1016/j.dam.2007.10.007]
• 20: Henry Kautz , Bart Selman, Planning as satisfiability, Proceedings of the 10th European conference on Artificial intelligence, p.359-363, August 1992, Vienna, Austria
• 21: Larrabee, T. Test pattern generation using Boolean satisfiability. IEEE Transactions on Computer-Aided Design (Jan. 1992) 4--15.
• 22: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th annual Design Automation Conference, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 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.
• 24: Joao P. Marques Silva , Karem A. Sakallah, Conflict Analysis in Search Algorithms for Satisfiability, Proceedings of the 8th International Conference on Tools with Artificial Intelligence, p.467, November 16-19, 1996
• 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).
• 26: Kenneth L. McMillan, Applying SAT Methods in Unbounded Symbolic Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.250-264, July 27-31, 2002
• 27: Nicola Muscettola , P. Pandurang Nayak , Barney Pell , Brian C. Williams, Remote Agent: to boldly go where no AI system has gone before, Artificial Intelligence, v.103 n.1-2, p.5-47, Aug. 1998 [doi>10.1016/S0004-3702(98)00068-X]
• 28: Gi-Joon Nam , Karem A. Sakallah , Rob A. Rutenbar, Satisfiability-based layout revisited: detailed routing of complex FPGAs via search-based Boolean SAT, Proceedings of the 1999 ACM/SIGDA seventh international symposium on Field programmable gate arrays, p.167-175, February 21-23, 1999, Monterey, California, United States [doi>10.1145/296399.296450]
• 29: Sanjai Narain , Gary Levin , Sharad Malik , Vikram Kaul, Declarative Infrastructure Configuration Synthesis and Debugging, Journal of Network and Systems Management, v.16 n.3, p.235-258, September 2008 [doi>10.1007/s10922-008-9108-y]
• 30: Bart Selman , Henry A. Kautz , Bram Cohen, Noise strategies for improving local search, Proceedings of the twelfth national conference on Artificial intelligence (vol. 1), p.337-343, October 1994, Seattle, Washington, United States
• 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.
• 32: Sanjit A. Seshia , Shuvendu K. Lahiri , Randal E. Bryant, A hybrid SAT-based decision procedure for separation logic with uninterpreted functions, Proceedings of the 40th annual Design Automation Conference, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775945]
• 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.
• 34: Spears, W. M. A NN algorithm for Boolean satisfiability problems. In Proceedings of the 1996 International Conference on Neural Networks, 1121--1126.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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).