[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, |