[Proof Complexity] Prague seminar on Monday - Leroy Chew

thapen thapen at math.cas.cz
Thu Apr 21 09:15:11 CEST 2022

Leroy Chew will give a proof complexity talk in our logic seminar on 
Monday 25th 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:Leroy Chew, TU Wien
  Title: Simulations in QBF Proof Complexity


  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 will examine the landscape of simulation in 
QBF, looking at the results over the last decade, as well as our own 
recent work with simulations based on strategy extraction and 
propositionalisation. We will interpret the theoretical and practical 
importance of these results.

  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