Proof complexity of Mal'tsev CSP

TL;DR

This paper formalizes the polynomial-time algorithm for Mal'tsev CSPs within bounded arithmetic and demonstrates that unsatisfiable instances have short extended Frege proofs, connecting algebraic properties with proof complexity.

Contribution

It proves that the Mal'tsev CSP algorithm's correctness can be formalized in bounded arithmetic, leading to short propositional proofs for unsatisfiable instances.

Findings

Bounded arithmetic $V^1$ proves the soundness of Mal'tsev CSP algorithm.

Unsatisfiable Mal'tsev CSP instances have short extended Frege proofs.

Extended results apply to generalized majority-minority CSPs.

Abstract

Constraint Satisfaction Problems (CSPs) form a broad class of combinatorial problems, which can be formulated as homomorphism problems between relational structures. The CSP dichotomy theorem classifies all such problems over finite domains into two categories: NP-complete and polynomial-time, see Zhuk (2017), Bulatov (2017). Polynomial-time CSPs can be further subdivided into smaller subclasses. Mal'tsev CSPs are defined by the property that every relation in the problem is invariant under a Mal'tsev operation, a ternary operation $\mu$ satisfying $\mu(x, y, y) = \mu(y, y, x) = x$ for all $x, y$. Bulatov and Dalmau proved that Mal'tsev CSPs are solvable in polynomial time, presenting an algorithm for such CSPs (2006). The negation of an unsatisfiable CSP instance can be expressed as a propositional tautology. We formalize the algorithm for Mal'tsev CSPs within bounded arithmetic $V^1$, which captures polynomial-time reasoning and corresponds to the extended Frege proof system. We show that $V^1$ proves the soundness of Mal'tsev algorithm, implying that tautologies expressing the non-existence of a solution for unsatisfiable instances of Mal'tsev CSPs admit short extended Frege proofs. In addition, with small adjustments, we achieved an analogous result for Dalmau's algorithm that solves generalized majority-minority CSPs -- a common generalization of near-unanimity operations and Mal'tsev operations.