Proof complexity of CSP on algebras with linear congruence

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 says that for each fixed target structure CSP is either NP-complete or $p$-time. Zhuk's algorithm for $p$-time case of the problem eventually leads to algebras with linear congruence. We show that Zhuk's algorithm for algebras with linear congruence can be formalized in theory $V^1$. Thus, using known methods of proof complexity Zhuk's algorithm for negative instances of the problem can be augmented by extra information: it not only rejects $\mathcal{X}$ that cannot be homomorphically mapped into $\mathcal{A}$, but produces a certificate - a short extended Frege (EF) propositional proof - that this rejection is correct.Comment: The error is found in the main statement (chapters 3.2, 5.2): the recursive step of Zhuk's algorithm does not necessarily preserve the algebra with linear congruence (that is, on the smaller domains algorithm runs all from the beginning), so it is not possible to treat the linear step of the algorithm separately. The paper will be revisite