Proof Complexity Meets Algebra

TL;DR

This paper explores how algebraic and logical reductions between constraint satisfaction problems influence their proof complexity, establishing algebraic characterizations of classes with small refutations and analyzing the behavior of various proof systems.

Contribution

It demonstrates that key reductions preserve proof complexity across several proof systems and introduces a new proof system with desirable properties, advancing understanding of proof complexity in CSPs.

Findings

Classical reductions preserve proof complexity in propositional, algebraic, and semi-algebraic systems.

A gap theorem characterizes languages with constant-width resolution refutations versus those lacking subexponential-depth Frege refutations.

Bounded-degree Lovász-Schrijver proof system exhibits both good reduction behavior and small size refutations.

Abstract

We analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, 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 constant 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 refutations of sublinear degree in Sums-of-Squares and Polynomial Calculus over the real-field, for which we provide alternative proofs. We then 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 Lov\'asz-Schrijver satisfies both requirements. Finally, building on the known lower bounds, we demonstrate the applicability of the method of reducibilities and construct new explicit hard instances of the graph 3-coloring problem for all studied proof systems.