[Proof Complexity] Prague seminar on Monday - Azza Gaysin
thapen
thapen at math.cas.cz
Wed Mar 30 15:16:53 CEST 2022
Azza Gaysin will give a proof complexity talk in our logic seminar on
Monday 4th April, at 16:00 Prague time - see the announcement below.
It will be broadcast on zoom. To join use the link
https://cesnet.zoom.us/j/472648284?pwd=ZTlxeHhqWlltR1AzZC9CTHgzZ2tRZz09
Passcode: 017107 (if required)
-------------------------------------------------------------------------
Speaker:Azza Gaysin, Charles University
Title: Proof complexity of CSP on algebras with linear congruence
Abstract
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 the 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 the 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 X that cannot be
homomorphically mapped into A but produces a certificate - a short
extended Frege (EF) propositional proof - that this rejection is
correct.
For more information see the seminar web page at
https://calendar.math.cas.cz/logic-seminar-actual .
_______________________________________________
Logic-seminar mailing list
Logic-seminar at math.cas.cz
https://list.math.cas.cz/listinfo/logic-seminar
More information about the Proof-Complexity
mailing list