Logic seminar

usually takes place each Monday at 16:00 in IM, rear building, ground floor
Chair: Pavel Pudlak, Neil Thapen, Jan Krajíček
More information on the old seminar web page. The programme is announced via the mailing list.

Nisan-Wigderson generators in Proof Complexity: New lower bounds

Erfan Khaniki

Institute of Mathematics

Monday, 14. March 2022 - 16:00 to 17:30

A map g:{0,1}^n --> {0,1}^m (m>n) is a hard proof complexity generator for a proof system P iff for every string b in {0,1}^m\Rng(g) the formula \tau_b(g), naturally expressing b \not \in Rng(g), requires superpolynomial size P-proofs. One of the well-studied maps in the theory of proof complexity generators is the Nisan-Wigderson generator. Razborov (Annals of Mathematics 2015) conjectured that if A is a suitable matrix and f is a NP \cap CoNP function hard-on-average for P/poly, then NW_{f, A} is a hard proof complexity generator for Extended Frege.

In this talk, we prove a form of Razborov's conjecture for AC0-Frege. We show that for any symmetric NP \cap CoNP function f that is exponentially hard for depth two AC0 circuits, NW_{f, A} is a hard proof complexity generator for AC0-Frege in a natural setting.

On Semi-Algebraic Proofs and Algorithms

Robert Robere

McGill University

Monday, 7. March 2022 - 16:00 to 17:30

We discuss a new characterization of the Sherali-Adams proof system, a standard propositional proof system considered in both proof complexity and combinatorial optimization, showing that there is a degree-d Sherali-Adams refutation of an unsatisfiable CNF formula F if and only if there is an ε > 0 and a degree-d conical junta J such that viol(x) − ε = J, where viol(x) counts the number of falsified clauses of F on an input x. This result implies that the linear separation complexity, a complexity measure recently studied by Hrubes (and independently by de Oliveira Oliveira and Pudlak under the name of weak monotone linear programming gates), monotone feasibly interpolates Sherali-Adams proofs, sharpening a feasible interpolation result of Hakoniemi. On the lower-bound side, we prove a separation between the conical junta degree of viol(x) - 1 and Resolution width; since Sherali-Adams can simulate Resolution this also separates the conical junta degree of viol(x) - 1 and viol(x) -... more

slides

Resolution, Heavy Width and Pseudorandom Generators

Dmitry Sokolov

St Petersburg State University and PDMI RAS

Monday, 21. February 2022 - 16:00 to 17:30

Following the paper of Alekhnovich, Ben-Sasson, Razborov, Wigderson we call a pseudorandom generator hard for a propositional proof system P if P cannot efficiently prove the (properly encoded) statement that b is outside of the image for any string b \in {0, 1}^m.

In ABRW04 the authors suggested the "functional encoding" of the considered statement for Nisan--Wigderson generator that allows the introduction of "local" extension variables and gave a lower bound on the length of Resolution proofs if the number of extension variables is bounded by the n^2 (where n is the number of inputs of the PRG).

In this talk, we discuss a "heavy width" measure for Resolution that allows us to show a lower bound on the length of Resolution proofs of the considered statement for the Nisan--Wigderson generator with a superpolynomial number of local extension variables. It is a solution to one of the open problems from ABRW04.

A revision of the width method

Michal Garlik

St. Petersburg Department of Steklov Institute of Mathematics and Euler International Mathematical Institute

Monday, 10. January 2022 - 16:00 to 17:30

We consider a framework for proving lower bounds on the length of proofs in logical calculi that can be seen as a generalization of the game framework in which Pudlák presented Haken's lower bound for resolution. Our framework, while still requiring some notion of width, can be applied in a way that avoids the use of the random restriction technique. As an example, we demonstrate this for resolution, obtaining a proof in which the calculations are very simple.