Proof complexity of CSP

TL;DR

This paper investigates the proof complexity of negative instances of polynomial-time solvable CSPs, showing their proofs can be efficiently simulated within certain propositional proof systems.

Contribution

It demonstrates that the soundness of Zhuk's polynomial-time CSP algorithm can be formalized in a bounded arithmetic theory, enabling efficient proofs of negative instances.

Findings

Proof of Zhuk's algorithm soundness in bounded arithmetic

Existence of polynomial-size proofs in certain propositional proof systems

Formalization of CSP proof complexity within a logical theory

Abstract

The CSP (constraint satisfaction problems) is a class of problems deciding whether there exists a homomorphism from an instance relational structure to a target one. The CSP dichotomy is a profound result recently proved by Zhuk (2020, J. ACM, 67) and Bulatov (2017, FOCS, 58). It establishes that for any fixed target structure, CSP is either NP-complete or $p$-time solvable. Zhuk's algorithm solves CSP in polynomial time for constraint languages having a weak near-unanimity polymorphism. For negative instances of $p$-time CSPs, it is reasonable to explore their proof complexity. We show that the soundness of Zhuk's algorithm can be proved in a theory of bounded arithmetic, namely in the theory $V^1$ augmented by three special universal algebra axioms. This implies that any propositional proof system that simulates both Extended Resolution and a theory that proves the three axioms admits $p$-size proofs of all negative instances of a fixed $p$-time CSP.