skip to main content
article

An improved exponential-time algorithm for k-SAT

Published: 01 May 2005 Publication History

Abstract

We propose and analyze a simple new randomized algorithm, called ResolveSat, for finding satisfying assignments of Boolean formulas in conjunctive normal form. The algorithm consists of two stages: a preprocessing stage in which resolution is applied to enlarge the set of clauses of the formula, followed by a search stage that uses a simple randomized greedy procedure to look for a satisfying assignment. Currently, this is the fastest known probabilistic algorithm for k-CNF satisfiability for k ≥ 4 (with a running time of O(20.5625n) for 4-CNF). In addition, it is the fastest known probabilistic algorithm for k-CNF, k ≥ 3, that have at most one satisfying assignment (unique k-SAT) (with a running time O(2(2 ln 2 − 1)n + o(n)) = O(20.386 … n) in the case of 3-CNF). The analysis of the algorithm also gives an upper bound on the number of the codewords of a code defined by a k-CNF. This is applied to prove a lower bounds on depth 3 circuits accepting codes with nonconstant distance. In particular we prove a lower bound Ω(21.282…√>i<n>/i<) for an explicitly given Boolean function of n variables. This is the first such lower bound that is asymptotically bigger than 2√>i<n>/i< + o(√>i<n>/i<).

References

[1]
Alon, N., Spencer, J., and Erdös, P. 1992. The Probabilistic Method. Wiley, New York.
[2]
Dantsin, E., Goerdt, A., Hirsch, E. A., Kannan, R., Kleinberg, J., Papadimitriou, C., Raghavan, P., and Schöning, U. 2002. A deterministic (2 &minus; 2/k &plus; 1)n algorithm for k-SAT based on local search. Theoret. Comput. Sci. 289, 69--83.
[3]
Davis, M., Logemann, G., and Loveland, D. 1962. A machine program for theorem proving, Commun. ACM 5, 394--397.
[4]
Galil, Z. 1975. On the validity and complexity of bounded resolution. In Proceedings of the 7th ACM Symposium on Theory of Computing. ACM, New York, 72--82.
[5]
Harris, T. E. 1960. A lower bound for the critical probability in a certain percolation process. Proc. Camb. Phil. Soc. 56, 13--20.
[6]
Håstad, J. 1986. Almost optimal lower bounds for small depth circuits. In Proceedings of the 18th ACM Symposium on Theory of Computing. ACM, New York, 6--20.
[7]
Håstad, J., Jukna, S., and Pudlák, P. 1993. Top--down lower bounds for depth 3 circuits. In Proceedings of the 34th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 124--129.
[8]
Hirsch, E. 2000. New worst-case upper bounds for SAT. J. Automat. Reas. 24, 4, 397--420.
[9]
Hirsch, E., and Kojevnikov, A. 2002. Unit Walk: A new SAT solver that uses local search guided by unit clause elimination. In Proceedings of 5th International Symposium on the Theory and Applications of Satisfiability Testing (SAT 2002). 35--42
[10]
Hofmeister, T., Schöning, U., Schuler, R., and Watanabe, O. 2002. A probabilistic 3-SAT algorithm further improved. In STACS 2002. Lecture Notes in Computer Science, vol. 2285. Springer-Verlag, New York, 192--202.
[11]
Kullmann, O. 1999. New methods for 3-SAT decision and worst-case analysis. Theoret. Comput. Sci. 223, 1-2 (July), 1--72.
[12]
Kullmann, O., and Luckhardt, H. 1998. Algorithms for SAT/TAUT decision based on various measures. Preprint, 81 pages http://www.cs.utoronto.ca/kullmann/.
[13]
MacWilliams, F. J., and Sloane, N. J. 1977. The Theory of Error-Correcting Codes. North-Holland, Amsterdam The Netherland.
[14]
Monien, B., and Speckenmeyer, E. 1985. Solving satisfiability in less than 2n steps. Discr. Appl. Math. 10, 287--295.
[15]
Paturi, R., Pudlák, P., Saks, M., and Zane, F. 1998. An improved exponential-time algorithm for k-SAT. In Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 628--637.
[16]
Paturi, R., Pudlák, P., and Zane, F. 1997. Satisfiability coding lemma. In Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 566--574. (See also Chicago J. Theor. Comput. Sci. (Dec. 1999), http://cjtcs.cs.uchicago.edu/.)
[17]
Razborov, A. A. 1986. Lower bounds on the size of bounded depth networks over a complete basis with logical addition. Matematicheskie Zametki 41, 598--607 (in Russian). (English Translation in Mathematical Notes of the Academy of Sciences of the USSR 41, 333--338.)
[18]
Schiermeyer, I. 1993. Solving 3-satisfiability in less than 1.579n steps. In Selected papers from CSL '92. Lecture Notes in Computer Science, vol. 702. Springer-Verlag, New York, 379--394.
[19]
Schöning, U. 1999. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In Proceedings of the 40th Annual Symposium on Foundations of Computer Science. IEEE Computer Society Press, Los Alamitos, Calif., 410--414.
[20]
Valiant, L. G. 1977. Graph-theoretic arguments in low-level complexity. In Proceedings of the 6th Symposium on Mathematical Foundations of Computer Science, Lecture Notes in Computer Science, vol. 53, Springer-Verlag, New York, 162--176.
[21]
Zhang, W. 1996. Number of models and satisfiability of sets of clauses. Theoret. Comput. Sci. 155, 277--288.

Cited By

View all
  • (2025)Fast exact algorithms for the SAT problem with bounded occurrences of variablesTheoretical Computer Science10.1016/j.tcs.2024.1150371029(115037)Online publication date: Mar-2025
  • (2025)On conflict-free cuts: Algorithms and complexityInformation Processing Letters10.1016/j.ipl.2024.106503187(106503)Online publication date: Jan-2025
  • (2024)Efficient Quantum Circuit Synthesis for SAT-Oracle With Limited Ancillary QubitIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.332597443:3(868-877)Online publication date: 1-Mar-2024
  • Show More Cited By

Index Terms

  1. An improved exponential-time algorithm for k-SAT

    Recommendations

    Comments

    Information & Contributors

    Information

    Published In

    cover image Journal of the ACM
    Journal of the ACM  Volume 52, Issue 3
    May 2005
    178 pages
    ISSN:0004-5411
    EISSN:1557-735X
    DOI:10.1145/1066100
    Issue’s Table of Contents

    Publisher

    Association for Computing Machinery

    New York, NY, United States

    Publication History

    Published: 01 May 2005
    Published in JACM Volume 52, Issue 3

    Permissions

    Request permissions for this article.

    Check for updates

    Author Tags

    1. CNF satisfiability
    2. randomized algorithms

    Qualifiers

    • Article

    Contributors

    Other Metrics

    Bibliometrics & Citations

    Bibliometrics

    Article Metrics

    • Downloads (Last 12 months)39
    • Downloads (Last 6 weeks)4
    Reflects downloads up to 30 Jan 2025

    Other Metrics

    Citations

    Cited By

    View all
    • (2025)Fast exact algorithms for the SAT problem with bounded occurrences of variablesTheoretical Computer Science10.1016/j.tcs.2024.1150371029(115037)Online publication date: Mar-2025
    • (2025)On conflict-free cuts: Algorithms and complexityInformation Processing Letters10.1016/j.ipl.2024.106503187(106503)Online publication date: Jan-2025
    • (2024)Efficient Quantum Circuit Synthesis for SAT-Oracle With Limited Ancillary QubitIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.332597443:3(868-877)Online publication date: 1-Mar-2024
    • (2024)Depth-3 circuits for inner productInformation and Computation10.1016/j.ic.2024.105192300:COnline publication date: 1-Oct-2024
    • (2024)PPSZ for General k-SAT and CSP—Making Hertli’s Analysis Simpler and 3-SAT Fastercomputational complexity10.1007/s00037-024-00259-y33:2Online publication date: 4-Nov-2024
    • (2024)Advancing Quantum Computing with Formal MethodsFormal Methods10.1007/978-3-031-71177-0_25(420-446)Online publication date: 9-Sep-2024
    • (2023)Fast algorithms for SAT with bounded occurrences of variablesProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/223(2004-2012)Online publication date: 19-Aug-2023
    • (2023)Hybrid divide-and-conquer approach for tree search algorithmsQuantum10.22331/q-2023-03-23-9597(959)Online publication date: 23-Mar-2023
    • (2023)Mind the Gap: Achieving a Super-Grover Quantum Speedup by Jumping to the EndProceedings of the 55th Annual ACM Symposium on Theory of Computing10.1145/3564246.3585203(1131-1144)Online publication date: 2-Jun-2023
    • (2023)Algorithmic Applications of Hypergraph and Partition ContainersProceedings of the 55th Annual ACM Symposium on Theory of Computing10.1145/3564246.3585163(985-998)Online publication date: 2-Jun-2023
    • Show More Cited By

    View Options

    Login options

    Full Access

    View options

    PDF

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader

    Figures

    Tables

    Media

    Share

    Share

    Share this Publication link

    Share on social media