Branching on Formulas: A Perspective From Knowledge Compilation

on YouTube ↗55m

" summary

Claims that branching on formulas (not just variables) gives exponential savings and that knowledge compilation provides the right lens. Uses DNNF, deterministic DNNF and SDD/decision-DNNF separations, plus the fact that existential quantification is polytime on DNNF but not on deterministic DNNF, to formalize traces of DPLL-style search. Proposes using auxiliary variables (bounded variable addition) to emulate formula branching; theory shows a single added variable can produce exponential succinctness and small experiments with a CTB-style compiler validate cases where compilation succeeds only after addition.

AI-written summary · about

" chapters (26)

1. 0:00Intro
2. 1:09Branching (Case Analysis) on Variables
3. 2:30Branching (Case Analysis) on Formulas
4. 5:17Extended Resolution: We Know This
5. 6:42What is "Knowledge Compilation?"
6. 8:31Negation Normal Form Circuits
7. 10:07Decomposability (DNNF)
8. 10:59Existential Quantification
9. 11:59Determinism (d-DNNF)
10. 12:47Model Counting (#SAT)
11. 15:59Exponential Separations
12. 18:14Knowledge Compilation Map
13. 22:07Orthonormal Expansions
14. 23:20Ordered Binary Decision Diagrams OBDDs
15. 25:54Variable Orders & Vtrees
16. 27:16Sentential Decision Diagrams (SDDs)
17. 29:55The Trace of Exhaustive DPLL
18. 31:54Dealing with redundancy: Unique node
19. 32:47Dealing with redundancy: Formula caching
20. 33:13Component Analysis
21. 35:26Limitation of Branching on Variables
22. 38:35Branching on Formulas via Auxiliary Variables
23. 41:43Beyond Determinism
24. 44:05Bounded Variable Addition (BVA)
25. 46:12Conclusion: Thinking About Branching
26. 48:08Automated Reasoning Group