[Proof Complexity] new paper

Азза Гайсин azza.gaysin at gmail.com
Wed Jan 5 08:29:08 CET 2022

 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

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.

More information about the Proof-Complexity mailing list