Document Open Access Logo

Super Strong ETH Is True for PPSZ with Small Resolution Width

Authors Dominik Scheder, Navid Talebanfard

PDF

File

Thumbnail PDF
PDF
LIPIcs.CCC.2020.3.pdf
  • Filesize: 0.6 MB
  • 12 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • k-SAT
  • PPSZ
  • Resolution

Metrics

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

Abstract

We construct k-CNFs with m variables on which the strong version of PPSZ k-SAT algorithm, which uses resolution of width bounded by O(√{log log m}), has success probability at most 2^{-(1-(1 + ε)2/k)m} for every ε > 0. Previously such a bound was known only for the weak PPSZ algorithm which exhaustively searches through small subformulas of the CNF to see if any of them forces the value of a given variable, and for strong PPSZ the best known previous upper bound was 2^{-(1-O(log(k)/k))m} (Pudlák et al., ICALP 2017).

Cite As Get BibTex

Dominik Scheder and Navid Talebanfard. Super Strong ETH Is True for PPSZ with Small Resolution Width. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 3:1-3:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CCC.2020.3

Author Details

Dominik Scheder
  • Shanghai Jiaotong University, China
Navid Talebanfard
  • Institute of Mathematics, The Czech Academy of Sciences, Prague, Czech Republic

Funding

  • Scheder, Dominik: Supported by the National Natural Science Foundation of China under grant 61502300 and 11671258.
  • Talebanfard, Navid: Supported by GAČR grant 19-27871X.

References

  1. Dana Angluin and A Gardiner. Finite common coverings of pairs of regular graphs. Journal of Combinatorial Theory, Series B, 30(2):184-187, 1981. URL: https://doi.org/10.1016/0095-8956(81)90062-9.
  2. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323-334, 2008. URL: https://doi.org/10.1016/j.jcss.2007.06.025.
  3. Shiteng Chen, Dominik Scheder, Navid Talebanfard, and Bangsheng Tang. 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: https://doi.org/10.1137/1.9781611973105.91.
  4. Paul Erdős and Horst Sachs. Reguläre graphen gegebener taillenweite mit minimaler knotenzahl. (regular graphs with given girth and minimal number of knots.). Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg, Math.-Naturwiss., 12:251-258, 1963. Google Scholar
  5. Thomas Dueholm Hansen, Haim Kaplan, Or Zamir, and Uri Zwick. Faster k-sat algorithms using biased-ppsz. In Moses Charikar and Edith Cohen, editors, Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, pages 578-589. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316359.
  6. Timon Hertli. 3-SAT faster and simpler - unique-SAT bounds for PPSZ hold in general. SIAM J. Comput., 43(2):718-729, 2014. URL: https://doi.org/10.1137/120868177.
  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, 2005. URL: https://doi.org/10.1145/1066100.1066101.
  8. Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. Chicago J. Theor. Comput. Sci., 1999, 1999. Google Scholar
  9. Pavel Pudlák, Dominik Scheder, and Navid Talebanfard. Tighter hard instances for PPSZ. In 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, pages 85:1-85:13, 2017. URL: https://doi.org/10.4230/LIPIcs.ICALP.2017.85.
  10. Dominik Scheder. PPSZ for k 5: More is better. TOCT, 11(4):25:1-25:22, 2019. URL: https://doi.org/10.1145/3349613.
  11. Uwe Schöning. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In 40th Annual Symposium on Foundations of Computer Science, FOCS '99, 17-18 October, 1999, New York, NY, USA, pages 410-414. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/SFFCS.1999.814612.
  12. Nikhil Vyas and R. Ryan Williams. 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, pages 406-423, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_28.
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