License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.MFCS.2019.37
URN: urn:nbn:de:0030-drops-109817
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10981/
Go to the corresponding LIPIcs Volume Portal

Garlík, Michal

Resolution Lower Bounds for Refutation Statements

pdf-format:
LIPIcs-MFCS-2019-37.pdf (0.4 MB)

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

BibTeX - Entry

@InProceedings{garlk:LIPIcs:2019:10981,
  author =	{Michal Garl{\'\i}k},
  title =	{{Resolution Lower Bounds for Refutation Statements}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{37:1--37:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Peter Rossmanith and Pinar Heggernes and Joost-Pieter Katoen},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10981},
  URN =		{urn:nbn:de:0030-drops-109817},
  doi =		{10.4230/LIPIcs.MFCS.2019.37},
  annote =	{Keywords: reflection principles, refutation statements, Resolution, proof complexity}
}

Keywords: reflection principles, refutation statements, Resolution, proof complexity
Collection: 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
Issue Date: 2019
Date of publication: 20.08.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI