Polynomial Bounds of CFLOBDDs against BDDs
summary
Shows that, given the same variable ordering, a CFLOBDD for any Boolean function is at most polynomially larger than a BDD: groupings count = O(b log b), vertices = O(b^2), edges = O(b^3) when the BDD has size b, and a family of functions realizes the Ω(b^3) lower bound. Proof builds CFLOBDDs simulate BDD patches and uses level locality prevents cascade duplication, so repeated procedure-call sharing blocks exponential blowup despite possible local duplication.
AI-written summary · about
chapters (11)
- 0:00Polynomial bounds of CFLOBDDs
- 0:42Binary Decision Diagrams background
- 1:24Context-Free Language OBDDs overview
- 2:51CFLOBDD execution example
- 3:56BDDs vs CFLOBDDs sizes
- 5:05Worst-case size relationship
- 6:31Duplication and locality in CFLOBDDs
- 8:36Polynomial bound proof
- 10:23Polynomial size bounds derivation
- 11:26Conclusion and open problems
- 12:11Q&A
related talks
21mWeighted Context-Free-Language Ordered Binary Decision Diagrams
49mCompiling FO Sentences to Circuits: Upper Bounds and Lower Bounds on the Size of the Circuit
39mStructure of the Fourier Spectrum of Boolean Functions and Complexity
30mMulti-variable Quantification of BDDs in External Memory using Nested Sweeping
20mBit Blasting Probabilistic Programs
25mSolving Queries for Boolean Fault Tree Logic via Quantified SAT
31mPfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagr...
47mHardness Amplification and the Approximate Degree of Constant-Depth Circuits