Abstract
We analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional and semialgebraic proof systems, the classical constructions of ppinterpretability, 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 boundeddepth 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 SumsofSquares 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 boundeddegree LovaszSchrijver 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:1110:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770415},
ISSN = {18688969},
year = {2017},
volume = {80},
editor = {Ioannis Chatzigiannakis and Piotr Indyk and Fabian Kuhn and Anca Muscholl},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7495},
URN = {urn:nbn:de:0030drops74956},
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 