[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
Passcode: 017107 (if required)


  Speaker:Azza Gaysin, Charles University
  Title: Proof complexity of CSP on algebras with linear congruence


  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 

  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

More information about the Proof-Complexity mailing list