  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.
