DROPS

Document

DOI: 10.4230/LIPIcs.CCC.2024.33

Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It

Authors: Michal Garlík

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)

Abstract

We show that for every integer k ≥ 2, the Res(k) propositional proof system does not have the weak feasible disjunction property. Next, we generalize a result of Atserias and Müller [Atserias and Müller, 2019] to Res(k). We show that if NP is not included in P (resp. QP, SUBEXP) then for every integer k ≥ 1, Res(k) is not automatable in polynomial (resp. quasi-polynomial, subexponential) time.

Cite as

Michal Garlík. Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 33:1-33:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{garlik:LIPIcs.CCC.2024.33,
  author =	{Garl{\'\i}k, Michal},
  title =	{{Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{33:1--33:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.33},
  URN =		{urn:nbn:de:0030-drops-204295},
  doi =		{10.4230/LIPIcs.CCC.2024.33},
  annote =	{Keywords: reflection principle, feasible disjunction property, k-DNF Resolution}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2019.37

Resolution Lower Bounds for Refutation Statements

Authors: Michal Garlík

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

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

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)

Copy BibTex To Clipboard

@InProceedings{garlik:LIPIcs.MFCS.2019.37,
  author =	{Garl{\'\i}k, Michal},
  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 =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.37},
  URN =		{urn:nbn:de:0030-drops-109817},
  doi =		{10.4230/LIPIcs.MFCS.2019.37},
  annote =	{Keywords: reflection principles, refutation statements, Resolution, proof complexity}
}

Search Results

Documents authored by Garlík, Michal

Failure of Feasible Disjunction Property for k-DNF Resolution and NP-Hardness of Automating It

Abstract

Cite as

Resolution Lower Bounds for Refutation Statements

Abstract

Cite as

Thanks for your feedback!

Could not send message