Document Open Access Logo

PPSZ for General k-SAT - Making Hertli's Analysis Simpler and 3-SAT Faster

Authors Dominik Scheder, John P. Steinberger

PDF

File

Thumbnail PDF
PDF
LIPIcs.CCC.2017.9.pdf
  • Filesize: 0.54 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Boolean satisfiability
  • exponential algorithms
  • randomized algorithms

Metrics

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

Abstract

The currently fastest known algorithm for k-SAT is PPSZ named after its inventors Paturi, Pudlak, Saks, and Zane. Analyzing its running time is much easier for input formulas with a unique satisfying assignment. In this paper, we achieve three goals. First, we simplify Hertli's analysis for input formulas with multiple satisfying assignments. Second, we show a "translation result": if you improve PPSZ for k-CNF formulas with a unique satisfying assignment, you will immediately get a (weaker) improvement for general k-CNF formulas. Combining this with a result by Hertli from 2014, in which he gives an algorithm for Unique-3-SAT slightly beating PPSZ, we obtain an algorithm beating PPSZ for general 3-SAT, thus obtaining the so far best known worst-case bounds for 3-SAT.

Cite As Get BibTex

Dominik Scheder and John P. Steinberger. PPSZ for General k-SAT - Making Hertli's Analysis Simpler and 3-SAT Faster. In 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 79, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CCC.2017.9

Author Details

Dominik Scheder
John P. Steinberger

References

  1. Timon Hertli. 3-SAT faster and simpler - unique-SAT bounds for PPSZ hold in general. In 2011 IEEE 52nd Annual Symposium on Foundations of Computer Science - FOCS 2011, pages 277-284. IEEE Computer Soc., Los Alamitos, CA, 2011. URL: http://dx.doi.org/10.1109/FOCS.2011.22.
  2. Timon Hertli. Breaking the PPSZ Barrier for Unique 3-SAT. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part I, volume 8572 of Lecture Notes in Computer Science, pages 600-611. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-43948-7_50.
  3. Timon Hertli, Robin A. Moser, and Dominik Scheder. Improving PPSZ for 3-SAT using critical variables. In Proceedings of STACS, pages 237-248, 2011. URL: http://arxiv.org/abs/1009.4830.
  4. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-sat. J. Comput. Syst. Sci., 62(2):367-375, 2001. URL: http://dx.doi.org/10.1006/jcss.2000.1727.
  5. Kazuo Iwama, Kazuhisa Seto, Tadashi Takai, and Suguru Tamaki. Improved randomized algorithms for 3-SAT. In Algorithms and Computation, volume 6506 of Lecture Notes in Comput. Sci., pages 73-84. Springer Berlin / Heidelberg, 2010. 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, pages 328-329 (electronic), New York, 2004. ACM. Google Scholar
  7. 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 (electronic), 2005. URL: http://dx.doi.org/10.1145/1066100.1066101.
  8. Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. Chicago J. Theoret. Comput. Sci., pages Article 11, 19 pp. (electronic), 1999. Google Scholar
  9. Daniel Rolf. Improved Bound for the PPSZ/Schöning-Algorithm for 3-SAT. Journal on Satisfiability, Boolean Modeling and Computation, 1:111-122, 2006. Google Scholar
  10. Dominik Scheder, Bangsheng Tang, Shiteng Chen, and Navid Talebanfard. Exponential lower bounds for the PPSZ k-sat algorithm. In Sanjeev Khanna, editor, Proceedings of the Twenty-Fourth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2013, New Orleans, Louisiana, USA, January 6-8, 2013, pages 1253-1263. SIAM, 2013. URL: http://dx.doi.org/10.1137/1.9781611973105.91.
  11. Uwe Schöning. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In Proceedings of the 40th Annual Symposium on Foundations of Computer Science, pages 410-414. IEEE Computer Society, Los Alamitos, CA, 1999. URL: http://dx.doi.org/10.1109/SFFCS.1999.814612.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact