[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
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
More information about the Proof-Complexity
mailing list