Connections Between QBF Proof Complexity and Circuit Complexity

on YouTube ↗33m

" summary

Proves a tight correspondence: QBF refutations in Frege-like systems exactly mirror circuit lower bounds via strategy extraction that yields programs in C-decision lists (depth increases by two). Constructs Q_f (exists x forall z z ≠ f(x)) so any universal winning strategy must compute f, so small Q-Frege proofs imply small C-circuits and conversely. Gives iff statements (e.g. Q-Frege superpolynomial lower bounds ↔ PSPACE ⊄ non-uniform NC1), produces new QBF separations (AC0 mod p, Sipser gaps), and characterizes Q-Res by unified decision lists with n^d blowup for d alternations.

AI-written summary · about

" chapters (23)

1. 0:00Hard problems everywhere?
2. 2:20The proof complexity theme song
3. 2:34Proofs vs circuits: what's the question exactly?
4. 5:07Game semantics of QBFs
5. 6:03A core QBF system: QU-Resolution
6. 8:00From propositional proof systems to QBF
7. 9:46Key example: Frege systems
8. 10:27Important propositional proof systems
9. 11:16Genuine QBF lower bounds.
10. 12:12QBF proof systems with NP oracles
11. 13:27Reasons for QBF hardness
12. 13:52Precise characterisations in QBF
13. 15:37Strategy extraction by decision lists
14. 18:02From decision lists to circuits
15. 20:16From circuit lower bounds to proof size lower bounds
16. 21:29Strong separations
17. 22:59The current frontier: propositional vs QBF
18. 23:20What happens for resolution?
19. 24:11Unified decision lists
20. 25:04The characterisation for Q-Res
21. 26:30Comparison to QBF Frege
22. 27:25Proof ingredients - Part 1
23. 28:10Conclusion

" related talks

• 18mOn the Verification of a Subgraph Construction AlgorithmLucas Böltz, Viorica Sofronie-Stokkermans, Hannes Frey · VMCAI 2024
• 37mJourney with Eric Allender: From Turing Machines to Circuits, and BackMichal Koucky · Lower Bounds, Learning, and Average-Case Complexity
• 55mLower Bounds for Subgraph Isomorphism and Consequences in First-Order LogicBenjamin Rossman · Symmetry, Logic, Computation 2016
• 01h 22mTutorial 5: The GCT Chasm IIKetan Mulmuley · Geometric Complexity Theory 2014
• 32mA Finite Alternation Result for Reversible Boolean CircuitsPeter Selinger · Symmetry, Logic, Computation 2016
• 53mNew Lower Bounds and Derandomization for ACC, and a...Lijie Chen · Lower Bounds, Learning, and Average-Case Complexity
• 01h 08mThe Simple, Little and Slow Things Count: On Parameterized Counting ComplexityRadu-Cristian Curticapean · Counting Complexity and Phase Transitions Boot Camp
• 01h 17mInapproximability of Constraint Satisfaction Problems VJohan Håstad · Real Analysis Boot Camp 2013