Document Open Access Logo

Strong ETH and Resolution via Games and the Multiplicity of Strategies

Authors Ilario Bonacina, Navid Talebanfard

PDF
Thumbnail PDF

File

LIPIcs.IPEC.2015.248.pdf
  • Filesize: 463 kB
  • 10 pages

Document Identifiers

Author Details

Ilario Bonacina
Navid Talebanfard

Cite As Get BibTex

Ilario Bonacina and Navid Talebanfard. Strong ETH and Resolution via Games and the Multiplicity of Strategies. In 10th International Symposium on Parameterized and Exact Computation (IPEC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 43, pp. 248-257, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.IPEC.2015.248

Abstract

We consider a restriction of the Resolution proof system in which at most a fixed number of variables can be resolved more than once along each refutation path. This system lies between regular Resolution, in which no variable can be resolved more than once along any path, and general Resolution where there is no restriction on the number of such variables. We show that when the number of re-resolved variables is not too large, this proof system is consistent with the Strong Exponential Time Hypothesis (SETH). More precisely for large n and k we show that there are unsatisfiable k-CNF formulas which require Resolution refutations of size 2^{(1 - epsilon_k)n}, where n is the number of variables and epsilon_k=~O(k^{-1/5}), whenever in each refutation path we only allow at most ~O(k^{-1/5})n variables to be resolved multiple times. However, these re-resolved variables along different paths do not need to be the same. Prior to this work, the strongest proof system shown to be consistent with SETH was regular Resolution [Beck and Impagliazzo, STOC'13]. This work strengthens that result and gives a different and conceptually simpler game-theoretic proof for the case of regular Resolution.

Subject Classification

Keywords
  • Strong Exponential Time Hypothesis
  • resolution
  • proof systems

Metrics

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

References

  1. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323-334, 2008. Google Scholar
  2. Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. (JAIR), 40:353-373, 2011. Google Scholar
  3. Paul Beame, Christopher Beck, and Russell Impagliazzo. Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In Howard J. Karloff and Toniann Pitassi, editors, Proceedings of the 44th Symposium on Theory of Computing Conference, STOC 2012, New York, NY, USA, May 19-22, 2012, pages 213-232. ACM, 2012. Google Scholar
  4. Christopher Beck and Russell Impagliazzo. Strong ETH Holds for Regular Resolution. In Proceedings of the Forty-fifth Annual ACM Symposium on Theory of Computing, STOC'13, pages 487-494. ACM, 2013. Google Scholar
  5. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. Google Scholar
  6. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  7. Ruiwen Chen, Valentine Kabanets, Antonina Kolokolova, Ronen Shaltiel, and David Zuckerman. Mining circuit lower bound proofs for meta-algorithms. In IEEE 29th Conference on Computational Complexity, CCC, pages 262-273, 2014. Google Scholar
  8. Ruiwen Chen, Valentine Kabanets, and Nitin Saurabh. An improved deterministic #SAT algorithm for small de morgan formulas. In Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS, pages 165-176, 2014. Google Scholar
  9. Shiteng Chen, Dominik Scheder, Navid Talebanfard, and Bangsheng Tang. Exponential Lower Bounds for the PPSZ k-SAT Algorithm. In SODA, pages 1253-1263, 2013. Google Scholar
  10. Stefan S. Dantchev. Relativisation provides natural separations for resolution-based proof systems. In Computer Science - Theory and Applications, First International Computer Science Symposium in Russia, CSR 2006, St. Petersburg, Russia, June 8-12, 2006, Proceedings, pages 147-158, 2006. Google Scholar
  11. Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch, Ravi Kannan, Jon M. Kleinberg, Christos H. Papadimitriou, Prabhakar Raghavan, and Uwe Schöning. A deterministic (2-2/(k+1))ⁿ algorithm for k-SAT based on local search. Theor. Comput. Sci., 289(1):69-83, 2002. Google Scholar
  12. Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem-proving. Commun. ACM, 5(7):394-397, 1962. Google Scholar
  13. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, 1960. Google Scholar
  14. Armin Haken. The intractability of resolution. Theor. Comput. Sci., 39:297-308, 1985. Google Scholar
  15. Russell Impagliazzo and Ramamohan Paturi. On the Complexity of k-SAT. J. Comput. Syst. Sci., 62(2):367-375, 2001. Google Scholar
  16. Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Benjamin Kuipers and Bonnie L. Webber, editors, Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27-31, 1997, Providence, Rhode Island., pages 203-208. AAAI Press / The MIT Press, 1997. Google Scholar
  17. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535. ACM, 2001. Google Scholar
  18. 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. Google Scholar
  19. Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. In 38th Annual Symposium on Foundations of Computer Science, FOCS, pages 566-574, 1997. Google Scholar
  20. Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artif. Intell., 175(2):512-525, 2011. Google Scholar
  21. Pavel Pudlák. Proofs as games. American Mathematical Monthly, 107(6):541-550, 2000. Google Scholar
  22. Pavel Pudlák and Russell Impagliazzo. A lower bound for DLL algorithms for k-SAT (preliminary version). In SODA, pages 128-136, 2000. Google Scholar
  23. Rahul Santhanam. Fighting perebor: New and improved algorithms for formula and QBF satisfiability. In 51th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2010, pages 183-192, 2010. Google Scholar
  24. Uwe Schöning. A probabilistic algorithm for k-SAT and constraint satisfaction problems. In 40th Annual Symposium on Foundations of Computer Science, FOCS,, pages 410-414, 1999. Google Scholar
  25. João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999. Google Scholar
  26. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. Google Scholar
  27. Ryan Williams. Improving exhaustive search implies superpolynomial lower bounds. In Proceedings of the 42nd ACM Symposium on Theory of Computing, STOC, pages 231-240, 2010. Google Scholar
  28. Ryan Williams. Non-uniform ACC circuit lower bounds. In Proceedings of the 26th Annual IEEE Conference on Computational Complexity, CCC, pages 115-125, 2011. 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