Resolution Lower Bounds for Refutation Statements

Author Michal Garlík

Thumbnail PDF


  • Filesize: 460 kB
  • 13 pages

Document Identifiers

Author Details

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

Cite AsGet 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)


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]).

Subject Classification

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


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


  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:
  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:
  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:
  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:
  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