[Proof Complexity] MIAO seminar Fri Apr 25 at 10:00 CET with Leroy Chew: Quantified Boolean formulas, proof and strategy extraction

[Jakob Nordström]

Dear all,

Capping of a busy seminar week, on Friday April 25 at 10:00 CET (note 
the time!) we will have the opportunity to listen to Leroy Chew from TU 
Wien, who will give a talk titled "Quantified Boolean formulas, proof 
and strategy extraction". You find the abstract at the bottom of this 
message.

We will run this as a MIAO hybrid seminar at Lund University. Local 
participants are warmly welcome to seminar room E:1426 at Ole Römers väg 
3, while other participants are equally warmly welcome to join virtually 
at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this 
information with colleagues who you think might be interested. We are 
also hoping to record the seminar and post on the MIAO Research YouTube 
channel https://youtube.com/@MIAOresearch for people who would like to 
hear the talk but cannot attend.

More information about the MIAO seminar series can be found at 
https://jakobnordstrom.se/miao-seminars/ . If you do not wish to receive 
these announcements, or receive several copies of them, please send a 
message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

/Friday Apr 25 at 10:00 (note the time!) in seminar room E:1426, Ole 
Römers väg 3, Lund University, and on Zoom
*Quantified Boolean formulas, proof and strategy extraction
*(Leroy Chew, Technische Universität Wien)
/
Proof complexity is a large part of the theory of solving Quantified 
Boolean Formulas (QBFs). QBFs are important in computer science as they 
form the canonical PSPACE-complete problem. Restrictions on the 
quantifier complexity form complete problems for every class of the 
polynomial hierarchy.

In this talk, we will look at lower bounds and p-simulations in QBF 
proof systems. A key aspect is strategy extraction, which is the 
property that Skolem or Herbrand functions can be efficiently 
constructed as circuits with the aid of a proof. Strategy extraction can 
be a huge benefit practically, as QBF solvers can be used on synthesis 
or game related instances, and these require the strategies as well as 
the answer. But strategy extraction can also be a weakness that can be 
exploited to find p-simulations and in some cases unconditional proof 
size lower bounds by linking QBF proof complexity to circuit complexity.

We will present the successful p-simulations by QBF Extended Frege using 
strategy extraction as well as the separations between the expansion 
based and clause learning techniques used in QBF solvers. We also look 
at the interesting case of QRAT, where strategy extraction does not 
work, and discuss the potential of systems where strategy extraction is 
dropped in favour of stronger proof rules.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se