A computing procedure for quantification theory. (English) Zbl 0212.34203


68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI


[1] Davis M, Putnam H. A computer procedure for quantification theory. J ACM, 1960, 7: 202-215 · Zbl 0212.34203
[2] Zhang H, Stickel M. Implementing the Davis-Putnam method. J Autom Reasoning, 2000, 24: 277-296 · Zbl 0967.68148
[3] Papadimitiou C H. On selecting a satisfying truth assignment. In: Proceedings of the 32nd Annual IEEE Symposium on Foundations of Computer Science. San Juan: IEEE Computer Society, 1991. 163-169
[4] Selman B, Levesque H, Mitchell D. A new method for solving hard satisfiability problems. In: Proceedings of 10th National Conference on Artificial Intelligence (AAAI-92). San Jose: AAAI Press, 1992. 440-446
[5] Selman B, Kautz H A, Cohen B. Noise strategies for improving local search. In: Proceedings of 12th National Conference on Artificial Intelligence (AAAI-94). Seattle: AAAI Press, 1994. 337-343
[6] Schöning U. A probabilistic algorithm for \(k\)-SAT and constraint satisfaction problems. In: Proceedings of the 40 th Annual Symposium on Foundation of Computer Science. New York, 1999. 410-414
[7] Hirsch E A, Kojevnikov A. UnitWalk: a new SAT solver that uses local search guided by unit clause elimination. Ann Math Artif Intel, 2005, 43: 91-111 · Zbl 1100.68621
[8] Mezard M, Parisi G, Zecchina R. Analytic and algorithmic solution of random satisfiability problems. Science, 2002, 297: 812-815
[9] Braunstein A, Mezard M, Zecchina R. Survey propagation: an algorithm for satisfiability. Random Struct Algor, 2005, 27: 201-226 · Zbl 1087.68126
[10] Paturi P, Pudlak P, Saks M E, et al. An improved exponential-time algorithm for \(k\)-SAT. J ACM, 2005, 52: 337-364 · Zbl 1297.68217
[11] Alekhnovich M, Ben-Sasson E. Linear upper bounds for random walk on small density random 3-CNF. SIAM J Comput, 2006, 36: 1248-1263 · Zbl 1124.68041
[12] Broder A, Frieze A, Upeal E. On the satisfiability and maximum satisfiability of random 3-CNF formulas. In: Proceedings of the 4th Annual ACM-SIAM Symposium on Discrete Algorithms. Austin: Society for Industrial and Applied Mathematics, 1993. 322-330 · Zbl 0801.68082
[13] Coja-Oghlan A, Feige U, Frieze A, et al. On smoothed \(k\)-CNF formulas and the Walksat algorithm. In: Proceedings of the 20th Annual ACM-SIAM Symposium on Discrete Algorithms. New York: Society for Industrial and Applied Mathematics, 2009. 451-460 · Zbl 1421.68059
[14] Parkes A J. Scaling properties of pure random walk on random 3-SAT. In: Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming. London: Springer-Verlag, 2002. 708-713
[15] Zhou Y, He J, Nie Q. A comparative runtime analysis of heuristic algorithms for satisfiability problems. Artif Intell, 2009, 173: 240-257 · Zbl 1192.68655
[16] Cook S. The complexity of theorem-proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing. New York: ACM Press, 1971. 151 · Zbl 0253.68020
[17] Garey M R, Johnson D S. Computers and Intractability-a Guide to the Theory of NP-Completeness. New York: Freeman, 1979 · Zbl 0411.68039
[18] Frieze A, McDiarmid C. Algorithm theory of random graphs. Random Struct algor, 1997, 10: 5-42 · Zbl 0868.05048
[19] Iosifescu M. Finite Markov Processes and their Applications. Chichester. New York: John Wiley & Sons, 1980 · Zbl 0436.60001
[20] He J,
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.