[Proof Complexity] The preprint of new paper

[Азза Гайсин]

 Dear colleagues,

The preprint of my paper "Proof complexity of CSP" (the revision of the
paper "Proof complexity of CSP on algebras with linear congruence") is
available on arxiv.org: https://arxiv.org/abs/2201.00913
Any comments are very welcome.

Best regards,
Azza Gaysin

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 V1 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.