Abstract
The currently fastest known algorithm for k-SAT is PPSZ, named after its inventors (Paturi et al. in J ACM 52(3):337-364, 2005. http://dx.doi.org/10.1145/1066100.1066101). 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 the analysis of Hertli (in 2011 IEEE 52nd Annual Symposium on Foundations of Computer Science-FOCS 2011, Los Alamitos, 2011) for input formulas with multiple satisfying assignments. Second, we show a “lifting 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. In combination this with results by Hansen et al. (in Charikar and Cohen (ed) Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, 2019) and Scheder (in 62nd IEEE Annual Symposium on Foundations of Computer Science, 2021), who all prove improved time bounds for Unique-k-SAT, this gives improved bounds for general k-SAT. We also generalize our results to the domain of Constraint Satisfaction Problems, i.e., satisfiability with more than two truth values.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Shiteng Chen, Dominik Scheder, Navid Talebanfard & Bangsheng Tang (2013). Exponential lower bounds for the PPSZ k- SAT algorithm. In Proceedings of the Twenty-Fourth Annual ACMSIAM Symposium on Discrete Algorithms, SODA 2013, New Orleans, Louisiana, USA, January 6-8, 2013, Sanjeev Khanna, editor, 1253– 1263. SIAM. ISBN 978-1-61197-251-1. URL http://dx.doi.org/10.1137/1.9781611973105.91.
Thomas Dueholm Hansen, Haim Kaplan, Or Zamir & Uri Zwick (2019). Faster k-SAT algorithms using biased-PPSZ. In Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, Moses Charikar & Edith Cohen, editors, 578–589. ACM. URL https://doi.org/10.1145/3313276.3316359.
Timon Hertli (2011). 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, 277–284. IEEE Computer Soc., Los Alamitos, CA. URL http://dx.doi.org/10.1109/FOCS.2011.22.
Timon Hertli (2014). Breaking the PPSZ barrier for Unique 3-SAT. In Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part I, Javier Esparza, Pierre Fraigniaud, Thore Husfeldt & Elias Koutsoupias, editors, volume 8572 of Lecture Notes in Computer Science, 600–611. Springer. ISBN 978-3-662-43947-0. URL http://dx.doi.org/10.1007/978-3-662-43948-7_50.
Timon Hertli, Isabelle Hurbain, Sebastian Millius, Robin A. Moser, Dominik Scheder & May Szedlák (2016). The PPSZ algorithm for constraint satisfaction problems on more than two colors. In Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings, Michel Rueher, editor, volume 9892 of Lecture Notes in Computer Science, 421–437. Springer. URL https://doi.org/10.1007/978-3-319-44953-1_27.
Timon Hertli, Robin A. Moser & Dominik Scheder (2011). Improving PPSZ for 3-SAT using Critical Variables. In Proceedings of STACS, 237–248.
Russell Impagliazzo & Ramamohan Paturi (2001). On the complexity of k-SAT. J. Comput. Syst. Sci. 62(2), 367–375. URL http://dx.doi.org/10.1006/jcss.2000.1727.
Kazuo Iwama, Kazuhisa Seto, Tadashi Takai & Suguru Tamaki (2010). Improved randomized algorithms for 3-SAT. In Algorithms and Computation, volume 6506 of Lecture Notes in Comput. Sci., 73–84. Springer Berlin / Heidelberg.
Kazuo Iwama & Suguru Tamaki (2004). Improved upper bounds for 3-SAT. In Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, 328–329 (electronic). ACM, New York.
Shibo Li & Dominik Scheder (2021). Impatient PPSZ - a faster algorithm for CSP. In 32nd International Symposium on Algorithms and Computation, ISAAC 2021, December 6-8, 2021, Fukuoka, Japan, Hee-Kap Ahn & Kunihiko Sadakane, editors, volume 212 of LIPIcs, 33:1–33:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL https://doi.org/10.4230/LIPIcs.ISAAC.2021.33.
Ramamohan Paturi, Pavel Pudlák, Michael E. Saks & Francis Zane (2005). An improved exponential-time algorithm for k-SAT. J.ACM 52(3), 337–364 (electronic). ISSN 0004-5411. URL http://dx.doi.org/10.1145/1066100.1066101.
Ramamohan Paturi, Pavel Pudlák & Francis Zane (1999). Satisfiability coding lemma. Chicago J. Theoret. Comput. Sci. Article 11, 19 pp. (electronic). ISSN 1073-0486.
Pavel Pudlák, Dominik Scheder & Navid Talebanfard (2017). Tighter hard instances for PPSZ. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, 85:1–85:13.
Tong Qin & Osamu Watanabe (2020). An improvement of the algorithm of Hertli for the unique 3SAT problem. Theor. Comput. Sci. 806, 70–80. URL https://doi.org/10.1016/j.tcs.2018.11.023.
Daniel Rolf (2006). Improved bound for the PPSZ/Schöningalgorithm for 3-SAT. Journal on Satisfiability, Boolean Modeling and Computation 1, 111–122.
Dominik Scheder (2019). PPSZ for k ≥ 5: more is better. TOCT 11(4), 25:1–25:22. URL https://doi.org/10.1145/3349613.
Dominik Scheder (2021). PPSZ is better than you think. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, 205–216. IEEE. URL https://doi.org/10.1109/FOCS52979.2021.00028.
Dominik Scheder & John P. Steinberger (2017). PPSZ for general k-SAT - making Hertli’s analysis simpler and 3-SAT faster. In 32nd Computational Complexity Conference, CCC 2017, July 6-9, 2017, Riga, Latvia, Ryan O’Donnell, editor, volume 79 of LIPIcs, 9:1–9:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. ISBN 978-3-95977- 040-8. URL https://doi.org/10.4230/LIPIcs.CCC.2017.9.
Dominik Scheder & Navid Talebanfard (2020). Super strong ETH is true for PPSZ with small resolution width. In 35th Computational Complexity Conference, CCC 2020, July 28-31, 2020, Saarbrücken, Germany (Virtual Conference), Shubhangi Saraf, editor, volume 169 of LIPIcs, 3:1–3:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL https://doi.org/10.4230/LIPIcs.CCC.2020.3.
Uwe Schöning (1999). A probabilistic algorithm for k-SAT and constraint satisfaction problems. In Proceedings of the 40th Annual Symposium on Foundations of Computer Science, 410–414. IEEE Computer Society, Los Alamitos, CA. URL http://dx.doi.org/10.1109/SFFCS.1999.814612.
Nikhil Vyas & R. Ryan Williams (2019). On super strong ETH. In Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings, Mikolás Janota & Inês Lynce, editors, volume 11628 of Lecture Notes in Computer Science, 406–423. Springer. URL https://doi.org/10.1007/978-3-030-24258-9_28.
Or Zamir (2021). Faster algorithm for unique (k, 2)-CSP. CoRR abs/2110.03122. URL https://arxiv.org/abs/2110.03122.
Acknowledgements
Dominik Scheder gratefully acknowledges support by the National Natural Science Foundation of China under grant 61502300.
Funding
Open Access funding enabled and organized by Projekt DEAL.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Scheder , D., Steinberger, J. PPSZ for General k-SAT and CSP—Making Hertli’s Analysis Simpler and 3-SAT Faster. comput. complex. 33, 13 (2024). https://doi.org/10.1007/s00037-024-00259-y
Published:
DOI: https://doi.org/10.1007/s00037-024-00259-y