[Proof Complexity] Fwd: Prague seminar on Monday - Azza Gaysin

[thapen]

Azza Gaysin will give the second part of her talk on CSPs in our logic 
seminar tomorrow, Monday 11th April, at 16:00 Prague time.

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