Ilario Bonacina: Lower bounds: from circuits to QBF proof systems

PRACTICALITIES

 Lunch is served at 12:00 noon (register at this doodle at the latest the Saturday before, but preferably earlier). The presentation starts at 12:10 pm and ends at 1 pm. Those of us who wish reconvene after a short break for ca two hours of more technical discussions.

 

ABSTRACT

A general and long-standing belief in the proof complexity community asserts that there is a close connection between progress in lower bounds for Boolean circuits and progress in proof size lower bounds for strong propositional proof systems. Although there are famous examples where a transfer from ideas and techniques from circuit complexity to proof complexity has been effective, a formal connection between the two areas has never been established so far. Here we provide such a formal relation between lower bounds for circuit classes and lower bounds for Frege systems for quantified Boolean formulas (QBF). Using the full spectrum of the state-of-the-art circuit complexity lower bounds we will prove lower bounds for very strong QBF proof systems (e.g. for what we called AC0[p]-FREGE + \forall red). Such lower bounds correspond, in the propositional case, to major open problems in proof complexity.

This talk is based on the joint work with Olaf Beyersdorff and Leroy Chew (ECCC TR15-133 and ITCS16, to appear).