CDCL vs Resolution: The Picture in QBF

on YouTube ↗29m

" summary

The paper proves classical QCDCL and Q-Resolution are incomparable and then pins down which algorithmic changes give exact matches: allowing arbitrary decision order (ANY-ORD) together with forbidding universal reductions during unit propagation (NO-RED) yields a QCDCL variant p-equivalent to Q-Res; permitting selective reductions yields a QCDCL that simulates a slightly modified long-distance system (mLDQ-Res); enabling universal literal propagation matches QU-Res. Experiments show an ANY-ORD variant improves on standard benchmarks for some families.

AI-written summary · about

" chapters (16)

1. 0:00CDCL vs Resolution in QBF
2. 1:08Quantified Boolean formulas
3. 2:16QBF refutation proof systems
4. 4:47QCDCL, CDCL and resolution
5. 7:22QCDCL vs resolution systems
6. 9:33QCDCL vs Q-Resolution limits
7. 11:48QCDCL to match Q-Resolution
8. 13:10Decision policy in QCDCL
9. 14:15Reduction policy in propagation
10. 17:07Modified QCDCL equals Q-Resolution
11. 17:55QCDCL simulates long-distance Q-Resolution
12. 20:29Characterized proof systems
13. 21:11QU-Resolution propagation policy
14. 23:10Final QU-Resolution characterization
15. 24:18Practical implications
16. 25:04Q&A on variants and results