Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR19-084 | 26th May 2019 00:35

Resolution Lower Bounds for Refutation Statements

RSS-Feed




TR19-084
Authors: Michal Garlik
Publication: 6th June 2019 01:34
Downloads: 69
Keywords: 


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-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 [Atserias-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 [Segerlind-Buss-Impagliazzo,2004]).



ISSN 1433-8092 | Imprint