Document Open Access Logo

Chain, Generalization of Covering Code, and Deterministic Algorithm for k-SAT

Author Sixue Liu

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2018.88.pdf
  • Filesize: 0.53 MB
  • 13 pages

Document Identifiers

Author Details

Sixue Liu
  • Department of Computer Science, Princeton University , 35 Olden Street, Princeton, NJ 08540, USA, http://www.cs.princeton.edu/~sixuel

Cite As Get BibTex

Sixue Liu. Chain, Generalization of Covering Code, and Deterministic Algorithm for k-SAT. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 88:1-88:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ICALP.2018.88

Abstract

We present the current fastest deterministic algorithm for k-SAT, improving the upper bound (2-2/k)^{n + o(n)} due to Moser and Scheder in STOC 2011. The algorithm combines a branching algorithm with the derandomized local search, whose analysis relies on a special sequence of clauses called chain, and a generalization of covering code based on linear programming.
We also provide a more intelligent branching algorithm for 3-SAT to establish the upper bound 1.32793^n, improved from 1.3303^n.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial algorithms
Keywords
  • Satisfiability
  • derandomization
  • local search

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Tobias Brüggemann and Walter Kern. An improved deterministic local search algorithm for 3-sat. Theoretical Computer Science, 329(1-3):303-313, 2004. Google Scholar
  2. Evgeny Dantsin, Andreas Goerdt, Edward A Hirsch, Ravi Kannan, Jon Kleinberg, Christos Papadimitriou, Prabhakar Raghavan, and Uwe Schöning. A deterministic (2-2/(k+1))^n algorithm for k-sat based on local search. Theoretical Computer Science, 289(1):69-83, 2002. Google Scholar
  3. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394-397, 1962. Google Scholar
  4. Timon Hertli. 3-sat faster and simpler - unique-sat bounds for ppsz hold in general. SIAM Journal on Computing, 43(2):718-729, 2014. Google Scholar
  5. Thomas Hofmeister, Uwe Schöning, Rainer Schuler, and Osamu Watanabe. A probabilistic 3-sat algorithm further improved. In 19th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2002, pages 192-202. Springer, 2002. Google Scholar
  6. Kazuo Iwama and Suguru Tamaki. Improved upper bounds for 3-sat. In Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, volume 4, pages 328-328, 2004. Google Scholar
  7. Hans Kleine Büning and Oliver Kullmann. Minimal unsatisfiability and autarkies. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 339-401. IOS Press, 2009. URL: http://dx.doi.org/10.3233/978-1-58603-929-5-339.
  8. Oliver Kullmann. New methods for 3-sat decision and worst-case analysis. Theoretical Computer Science, 223(1-2):1-72, 1999. Google Scholar
  9. Kazuhisa Makino, Suguru Tamaki, and Masaki Yamamoto. Derandomizing the HSSW algorithm for 3-sat. Algorithmica, 67(2):112-124, 2013. Google Scholar
  10. Burkhard Monien and Ewald Speckenmeyer. Solving satisfiability in less than 2ⁿ steps. Discrete Applied Mathematics, 10(3):287-295, 1985. Google Scholar
  11. Robin A. Moser and Dominik Scheder. A full derandomization of schöning’s k-sat algorithm. In Proceedings of the Forty-third Annual ACM Symposium on Theory of Computing, STOC 2011, pages 245-252, 2011. Google Scholar
  12. Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Francis Zane. An improved exponential-time algorithm for k-sat. J. ACM, 52(3):337-364, 2005. URL: http://dx.doi.org/10.1145/1066100.1066101.
  13. Daniel Rolf. Derandomization of PPSZ for unique- k-sat. In Theory and Applications of Satisfiability Testing, 8th International Conference, SAT 2005, pages 216-225, 2005. Google Scholar
  14. Dominik Scheder. Guided search and a faster deterministic algorithm for 3-sat. In the 3rd Latin American Theoretical Informatics Symposium, LATIN 2008, pages 60-71, 2008. Google Scholar
  15. Ingo Schiermeyer. Solving 3-satisfiability in less than 1.579ⁿ steps. Computer Science Logic, pages 379-394, 1970. Google Scholar
  16. Uwe Schöning. A probabilistic algorithm for k-sat and constraint satisfaction problems. In 40th Annual Symposium on Foundations of Computer Science, FOCS 1999, pages 410-414, 1999. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact