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.ICALP.2017.110
URN: urn:nbn:de:0030-drops-74956
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7495/
Go to the corresponding LIPIcs Volume Portal

Atserias, Albert ; Ochremiak, Joanna

Proof Complexity Meets Algebra

pdf-format:
LIPIcs-ICALP-2017-110.pdf (0.5 MB)

Abstract

We analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional and semi-algebraic proof systems, the classical constructions of pp-interpretability, homomorphic equivalence and addition of constants to a core preserve the proof complexity of the CSP. As a result, for those proof systems, the classes of constraint languages for which small unsatisfiability certificates exist can be characterised algebraically. We illustrate our results by a gap theorem saying that a constraint language either has resolution refutations of bounded width, or does not have bounded-depth Frege refutations of subexponential size. The former holds exactly for the widely studied class of constraint languages of bounded width. This class is also known to coincide with the class of languages with Sums-of-Squares refutations of sublinear degree, a fact for which we provide an alternative proof. We hence ask for the existence of a natural proof system with good behaviour with respect to reductions and simultaneously small size refutations beyond bounded width. We give an example of such a proof system by showing that bounded-degree Lovasz-Schrijver satisfies both requirements.

BibTeX - Entry

@InProceedings{atserias_et_al:LIPIcs:2017:7495,
  author =	{Albert Atserias and Joanna Ochremiak},
  title =	{{Proof Complexity Meets Algebra}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{110:1--110:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Ioannis Chatzigiannakis and Piotr Indyk and Fabian Kuhn and Anca Muscholl},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7495},
  URN =		{urn:nbn:de:0030-drops-74956},
  doi =		{10.4230/LIPIcs.ICALP.2017.110},
  annote =	{Keywords: Constraint Satisfaction Problem, Proof Complexity, Reductions, Gap Theorems}
}

Keywords: Constraint Satisfaction Problem, Proof Complexity, Reductions, Gap Theorems
Collection: 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)
Issue Date: 2017
Date of publication: 07.07.2017

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