2026-08-05T23:42:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10981 2024-03-06T10:46:58Z ddc:004 open_access

Resolution Lower Bounds for Refutation Statements Garlík, Michal reflection principles refutation statements Resolution proof complexity 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]). Schloss Dagstuhl – Leibniz-Zentrum für Informatik Michal Garlík 2019 Is Part Of LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2019.37 urn:nbn:de:0030-drops-109817 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.37 eng https://creativecommons.org/licenses/by/3.0/legalcode