Document Open Access Logo

Resolution Lower Bounds for Refutation Statements

Author Michal Garlík

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2019.37.pdf
  • Filesize: 460 kB
  • 13 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • reflection principles
  • refutation statements
  • Resolution
  • proof complexity

Metrics

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

Abstract

For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolution refutations of a propositional statement that the formula has a resolution refutation. We describe three applications. (1) An open question in [Atserias and Müller, 2019] asks whether a certain natural propositional encoding of the above statement is hard for Resolution. We answer by giving an exponential size lower bound. (2) We show exponential resolution size lower bounds for reflection principles, thereby improving a result in [Albert Atserias and María Luisa Bonet, 2004]. (3) We provide new examples of CNFs that exponentially separate Res(2) from Resolution (an exponential separation of these two proof systems was originally proved in [Nathan Segerlind et al., 2004]).

Cite As Get BibTex

Michal Garlík. Resolution Lower Bounds for Refutation Statements. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 37:1-37:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.MFCS.2019.37

Author Details

Michal Garlík
  • Dept. Ciències de la Computació, Universitat Politècnica de Catalunya, C. Jordi Girona, 1-3, 08034 Barcelona, Spain

Funding

Funded by European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme, grant agreement ERC-2014-CoG 648276 (AUTAR).

References

  1. Albert Atserias and María Luisa Bonet. On the automatizability of resolution and related propositional proof systems. Information and Computation, 189(2):182-201, 2004. Google Scholar
  2. Albert Atserias and Moritz Müller. Automating Resolution is NP-Hard. arXiv e-prints, April 2019. URL: http://arxiv.org/abs/1904.02991v1.
  3. María Luisa Bonet, Toniann Pitassi, and Ran Raz. On Interpolation and Automatization for Frege Systems. SIAM J. Comput., 29(6):1939-1967, 2000. URL: https://doi.org/10.1137/S0097539798353230.
  4. Stephen A. Cook and Robert A. Reckhow. The Relative Efficiency of Propositional Proof Systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  5. Michal Garlík. Resolution Lower Bounds for Refutation Statements. arXiv e-prints, May 2019. URL: http://arxiv.org/abs/arXiv:1905.12372v1.
  6. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297-308, 1985. Google Scholar
  7. Jan Krajíček, Alan Skelley, and Neil Thapen. NP search problems in low fragments of bounded arithmetic. The Journal of Symbolic Logic, 72(2):649-672, 2007. Google Scholar
  8. Pavel Pudlák. Proofs as Games. American Mathematical Monthly, 107(6):541-550, 2000. URL: https://doi.org/10.2307/2589349.
  9. Pavel Pudlák. On reducibility and symmetry of disjoint NP-pairs. Theoretical Computer Science, 295:323-339, 2003. Google Scholar
  10. Nathan Segerlind, Samuel R. Buss, and Russel Impagliazzo. A switching lemma for small restrictions and lower bounds for k-DNF resolution. SIAM Journal on Computing, 33(5):1171-1200, 2004. Google Scholar
  11. Neil Thapen. A Tradeoff Between Length and Width in Resolution. Theory of Computing, 12(5):1-14, 2016. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact