A deterministic \((2-2/(k+1))^{n}\) algorithm for \(k\)-SAT based on local search. (English) Zbl 1061.68071
Summary: Local search is widely used for solving the propositional satisfiability problem. Papadimitriou (1991) showed that randomized local search solves 2-SAT in polynomial time. Recently, Schöning (1999) proved that a close algorithm for \(k\)-SAT takes time \((2-2/k)^{n}\) up to a polynomial factor. This is the best known worst-case upper bound for randomized 3-SAT algorithms (cf. also recent preprint by Schuler et al.). We describe a deterministic local search algorithm for \(k\)-SAT running in time \((2-2/(k+1))^{n}\) up to a polynomial factor. The key point of our algorithm is the use of covering codes instead of random choice of initial assignments. Compared to other “weakly exponential” algorithms, our algorithm is technically quite simple. We also describe an improved version of local search. For 3-SAT the improved algorithm runs in time \(1.481^{n}\) up to a polynomial factor. Our bounds are better than all previous bounds for deterministic \(k\)-SAT algorithms.
MSC:
| 68Q25 | Analysis of algorithms and problem complexity |
References:
| [1] | Ash, R. B., Information Theory (1965), Dover: Dover New York · Zbl 0141.34904 |
| [2] | Bolc, L.; Cytowski, J., Search Methods for Artificial Intelligence (1992), Academic Press: Academic Press New York · Zbl 0817.68122 |
| [3] | Cohen, G.; Honkala, I.; Litsyn, S.; Lobstein, A., Covering Codes. Covering Codes, Mathematical Library, vol. 54 (1997), Elsevier: Elsevier Amsterdam · Zbl 0874.94001 |
| [4] | E. Dantsin, Two propositional proof systems based on the splitting method (in Russian). Zapiski Nauchnykh Seminarov LOM1, 105 (1981) 24-44 (English translation: Journal of Soviet Mathematics, 22(3) (1983) 1293-1305.); E. Dantsin, Two propositional proof systems based on the splitting method (in Russian). Zapiski Nauchnykh Seminarov LOM1, 105 (1981) 24-44 (English translation: Journal of Soviet Mathematics, 22(3) (1983) 1293-1305.) |
| [5] | J. Gu, Q.-P. Gu, Average time complexity of the SAT 1.2 algorithm, in: D.-Z. Du, X.-S. Zhang (Eds.), Proc. Fifth Annu. Internat. Symp. Algorithms Comput., ISAAC’94, Lecture Notes in Computer Science, vol. 834, Springer, Berlin, 1994, pp. 146-154.; J. Gu, Q.-P. Gu, Average time complexity of the SAT 1.2 algorithm, in: D.-Z. Du, X.-S. Zhang (Eds.), Proc. Fifth Annu. Internat. Symp. Algorithms Comput., ISAAC’94, Lecture Notes in Computer Science, vol. 834, Springer, Berlin, 1994, pp. 146-154. · Zbl 0953.68552 |
| [6] | Gu, J.; Purdom, P.; Franco, J.; Wah, B. W., Algorithms for the Satisfiability Problem. Algorithms for the Satisfiability Problem, Cambridge Tracts in Theoretical Computer Science (2000), Cambridge University Press: Cambridge University Press Cambridge |
| [7] | Hirsch, E. A., New worst-case upper bounds for SAT, J. Automat. Reason., 24, 4, 397-420 (2000) · Zbl 0960.03009 |
| [8] | Hirsch, E. A., SAT local search algorithms: worst-case study, J. Automat. Reason., 24, 1/2, 127-143 (2000) · Zbl 0967.68146 |
| [9] | Hochbaum (Ed.), D. S., Approximation Algorithms for NP-hard Problems (1997), PWS Publishing Company: PWS Publishing Company MA |
| [10] | Koutsoupias, E.; Papadimitriou, C. H., On the greedy algorithm for satisfiability, Inform. Process. Lett., 43, 1, 53-55 (1992) · Zbl 0780.68062 |
| [11] | Kullmann, O., Worst-case analysis, 3-SAT decision and lower bounds: approaches for improved SAT algorithms, (Du, D.; Gu, J.; Pardalos, P. M., Satisfiability Problem: Theory and Applications (DIMACS Workshop March 11-13, 1996). Satisfiability Problem: Theory and Applications (DIMACS Workshop March 11-13, 1996), DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 35 (1997), AMS: AMS Providence, RI), 261-313 · Zbl 0889.03030 |
| [12] | Kullmann, O., New methods for 3-SAT decision and worst-case analysis, Theoret. Comput. Sci., 223, 1-2, 1-72 (1999) · Zbl 0930.68066 |
| [13] | O. Kullmann, H. Luckhardt, Deciding propositional tautologies: Algorithms and their complexity, preprint, 82 pp. http://www.cs.toronto.edu/∼kullmann, a journal version is submitted to Information and Computation, 1997.; O. Kullmann, H. Luckhardt, Deciding propositional tautologies: Algorithms and their complexity, preprint, 82 pp. http://www.cs.toronto.edu/∼kullmann, a journal version is submitted to Information and Computation, 1997. |
| [14] | Minton, S.; Johnston, M. D.; Philips, A. B.; Lair, P., Minimizing conflicts: a heuristic repair method for constraint satisfaction and scheduling problems, Artif. Intell., 58, 161-205 (1992) · Zbl 0782.90054 |
| [15] | Monien, B.; Speckenmeyer, E., Solving satisfiability in less than \(2^n\) steps, Discrete Appl. Math., 10, 287-295 (1985) · Zbl 0603.68092 |
| [16] | C.H. Papadimitriou, On selecting a satisfying truth assignment, in: Proc. 32nd Annu. IEEE Symp. on Foundations of Computer Science, FOCS’91, 1991, pp. 163-169.; C.H. Papadimitriou, On selecting a satisfying truth assignment, in: Proc. 32nd Annu. IEEE Symp. on Foundations of Computer Science, FOCS’91, 1991, pp. 163-169. |
| [17] | R. Paturi, P. Pudlák, M.E. Saks, F. Zane, An improved exponential-time algorithm for \(k\); R. Paturi, P. Pudlák, M.E. Saks, F. Zane, An improved exponential-time algorithm for \(k\) · Zbl 1297.68217 |
| [18] | R. Paturi, P. Pudlák, F. Zane, Satisfiability coding lemma, in: Proc. 38th Annu. IEEE Symp. on Foundations of Computer Science, FOCS’97, 1997, pp. 566-574.; R. Paturi, P. Pudlák, F. Zane, Satisfiability coding lemma, in: Proc. 38th Annu. IEEE Symp. on Foundations of Computer Science, FOCS’97, 1997, pp. 566-574. · Zbl 0940.68049 |
| [19] | I. Schiermeyer, Pure literal look ahead: An \(O^n\); I. Schiermeyer, Pure literal look ahead: An \(O^n\) |
| [20] | U. Schöning, A probabilistic algorithm for \(k\); U. Schöning, A probabilistic algorithm for \(k\) |
| [21] | R. Schuler, U. Schöning, O. Watanabe, An improved randomized algorithm for 3-SAT, Dept. Math. Comput. Sci., Tokyo Inst. of Tech., 2001, TR-C146.; R. Schuler, U. Schöning, O. Watanabe, An improved randomized algorithm for 3-SAT, Dept. Math. Comput. Sci., Tokyo Inst. of Tech., 2001, TR-C146. |
| [22] | Selman, B.; Levesque, H.; Mitchell, D., A new method for solving hard satisfiability problems, (Swartout, W., Proc. Tenth National Conf. Artif. Intell. AAAI-92 (1992), MIT Press: MIT Press Cambridge, MA), 440-446 |
| [23] | Zhang, W., Number of models and satisfiability of sets of clauses, Theoret. Comput. Sci., 155, 277-288 (1996) · Zbl 0873.68094 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
