[Proof Complexity] new paper

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

 Dear colleagues,

The preprint of my new 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 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 V1. 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 X that cannot be homomorphically
mapped into A, but produces a certificate - a short extended Frege (EF)
propositional proof - that this rejection is correct.