Beyond SAT - Proofs for QBF, and more
summary
Overview of what is known and what still fails: four concrete QBF proof paradigms — expansion, universal reduction — plus literal merging/long‑distance resolution and explicit counter‑model construction — yield a lattice of systems with exponential separations. Many lower bounds come from embedded propositional hardness and from efficient strategy extraction to small circuit models; genuine QBF hardness is formalized via oracles or semantic measures (cost, capacity, gauge). CDCL‑style and expansion solvers map to some proof fragments, dependency schemes help or hurt, and several pragmatic proof‑system/solver equivalences remain open.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:01Quantified Boolean Formulas
- 2:57The two-player evaluation game
- 6:37Proof Systems for refuting QBFs (by example)
- 10:09Some QBF Proof Systems - The simulation order
- 12:14Augmenting PPS to QBF proof systems
- 13:44Lower Bounds: Transferring Propositional Hardness
- 18:20What is "Genuine QBF Hardness"?
- 21:15Lower Bounds: Transferring Computational Hardness - 1
- 27:09Lower Bounds: Identify semantic hardness
- 30:13Questions
- 33:19Proof Systems and QBF solving
- 38:21Q-CDCL: Some surprises? distractions?
- 41:02Sliding the Cook-Reckhow framework
related talks
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
40mUtilizing Structure in Combinatorial Solving and Reasoning
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
01h 05mVerifying Infinitely Many Programs at Once
21mMechanised Hypersafety Proofs about Structured Data
18mOn the Verification of a Subgraph Construction Algorithm
58mA New Perspective on Commutativity in Verification