Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček

More information on the old seminar web page. The programme is announced via the mailing list.

IM CAS

Monday, 2. May 2022 - 16:00 to 17:30

In the first half of my talk I will mention the history of our logic group in our institute and how we gradually moved from studying metamathematics of Peano Arithmetic to weak fragments, and eventually to proof complexity of propositional logic. In the second part I will talk about my project to define a hierarchy of propositional proof systems indexed by ordinals up to epsilon_0 with the aim to prove that they characterize the proof system associated with Peano Arithmetic.

TU Wien

Monday, 25. April 2022 - 16:00 to 17:30

Quantified Boolean Formulas (QBF) extend propositional formulas with Boolean quantifiers. Solving a QBF is PSPACE complete, and QBFSAT is seen as a natural extension of the SAT problem. Just as propositional proof complexity underlies the theory behind SAT solving, QBF proof complexity underlies the theory behind QBF solving. Here we will focus on the relative strengths of QBF proof systems via p-simulation.

On the surface QBF proof systems seem harder to compare to one another since they vary considerably in how they deal with quantification. In particular there's a vast difference between theory systems that generalise from propositional logic, the proof systems that capture the process of CDCL solving and the proof systems that capture the expansion and CEGAR based solvers. And many results do formally show an incomparability in the proof complexity between different systems as we suspect. However, there are a few non-obvious cases where a simulation is possible. In this talk we... more

Charles University

Monday, 11. April 2022 - 16:00 to 17:30

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.

Charles University

Monday, 4. April 2022 - 16:00 to 17:30

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.