Abstract
We show that satisfiability of formulas in k-CNF can be decided deterministically in time close to (2k/(k + 1))n, where n is the number of variables in the input formula. This is the best known worst-case upper bound for deterministic k-SAT algorithms. Our algorithm can be viewed as a derandomized version of Schöning’s probabilistic algorithm presented in [15]. The key point of our algorithm is the use of covering codes together with local search. Compared to other “weakly exponential” algorithms, our algorithm is technically quite simple. We also show how to improve the bound above by moderate technical effort. For 3-SAT the improved bound is 1.481n.
Work done in part while visiting Department of Computer Science of University of Manchester. Supported by grants from TFR, INTAS, and RFBR.
Supported by INTAS project 96-0760 and RFBR grant 99-01-00113.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
R. B. Ash. Information Theory. Dover, 1965.
L. Bolc and J. Cytowski. Search Methods for Artificial Intelligence. Academic Press, 1992.
G. Cohen, I. Honkala, S. Litsyn, and A. Lobstein. Covering Codes, volume 54 of Mathematical Library. Elsevier, 1997.
E. Dantsin. Two propositional proof systems based on the splitting method (in Russian). Zapiski Nauchnykh Seminarov LOMI, 105:24–44, 1981. English translation: Journal of Soviet Mathematics, 22(3):1293–1305, 1983.
E. A. Hirsch. Two new upper bounds for SAT. In Proceedings of the 9th Annual ACM-SIAM Symposium on Discrete Algorithms, SODA’98, pages 521–530, 1998. A journal version is to appear in Journal of Automated Reasoning, 2000.
O. Kullmann. Worst-case analysis, 3-SAT decision and lower bounds: approaches for improved SAT algorithms. In D. Du, J. Gu, and P. M. Pardalos, editors, Satisfiability Problem: Theory and Applications (DIMACS Workshop March 11–13, 1996), volume 35 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 261–313. AMS, 1997.
O. Kullmann. New methods for 3-SAT decision and worst-case analysis. Theoretical Computer Science, 223(1–2):1–72, 1999.
O. Kullmann and H. Luckhardt. Deciding propositional tautologies: Algorithms and their complexity. Preprint, 82 pages, http://www.cs.toronto.edu/kullmann. A journal version is submitted to Information and Computation, January 1997.
S. Minton, M. D. Johnston, A. B. Philips, and P. Lair. Minimizing conflicts: a heuristic repair method for constraint satisfaction and scheduling problems. Artificial Intelligence, 58:161–205, 1992.
B. Monien and E. Speckenmeyer. Solving satisfiability in less then 2n steps. Discrete Applied Mathematics, 10:287–295, 1985.
C. H. Papadimitriou. On selecting a satisfying truth assignment. In Proceedings of the 32nd Annual IEEE Symposium on Foundations of Computer Science, FOCS’91, pages 163–169, 1991.
R. Paturi, P. Pudlák, M. E. Saks, and F. Zane. An improved exponential-time algorithm for k-SAT. In Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science, FOCS’98, pages 628–637, 1998.
R. Paturi, P. Pudlák, and F. Zane. Satisfiability coding lemma. In Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science, FOCS’97, pages 566–574, 1997.
I. Schiermeyer. Pure literal look ahead: An O(1,497n) 3-satisfiability algorithm. Workshop on the Satisfiability Problem, Siena, April 29–May 3, 1996. Technical Report 96-230, University Köln, 1996.
U. Schöning. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In Proceedings of the 40th Annual IEEE Symposium on Foundations of Computer Science, FOCS’99, pages 410–414, 1999.
W. Zhang. Number of models and satisfiability of sets of clauses. Theoretical Computer Science, 155:277–288, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dantsin, E., Goerdt, A., Hirsch, E.A., Schöning, U. (2000). Deterministic Algorithms for k-SAT Based on Covering Codes and Local Search. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds) Automata, Languages and Programming. ICALP 2000. Lecture Notes in Computer Science, vol 1853. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45022-X_21
Download citation
DOI: https://doi.org/10.1007/3-540-45022-X_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67715-4
Online ISBN: 978-3-540-45022-1
eBook Packages: Springer Book Archive