[Proof Complexity] Prague seminar on Monday - Leroy Chew

[thapen]

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
https://cesnet.zoom.us/j/472648284?pwd=ZTlxeHhqWlltR1AzZC9CTHgzZ2tRZz09
Passcode: 017107 (if required)

  
-------------------------------------------------------------------------

  Speaker:Leroy Chew, TU Wien
  Title: Simulations in QBF Proof Complexity

  Abstract

  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
https://list.math.cas.cz/listinfo/logic-seminar