Compiling FO Sentences to Circuits: Upper Bounds and Lower Bounds on the Size of the Circuit
summary
Proves a concrete dichotomy: for universally quantified positive FO sentences the optimal OBDDs size is either polynomial in domain size n or exponential, decided by a syntactic inversions condition; gives a product-automaton synthesis for the polynomial side and a reduction-based lower bound for the exponential side. Shows FBDDs and Decision-DNNFs are incomplete by constructing an FO sentence Qw whose provenance admits PTIME weighted model counting via cancellation in inclusion–exclusion yet forces any FBDD/decision‑DNNF to be exponentially large.
AI-written summary · about
chapters (20)
- 0:00Simons Institute workshop intro
- 1:21Workshop logistics
- 3:10Workshop purpose
- 5:13Talk overview
- 8:09Weighted model counting
- 12:11Provenance as Boolean functions
- 13:57Fixed query complexity
- 15:25Hierarchical queries dichotomy
- 17:34Union of conjunctive queries
- 19:23Query static analysis
- 21:31Binary decision diagrams intro
- 25:51FO logic to circuits
- 26:34Ordered binary decision diagrams and synthesis
- 28:03OBDDs for hierarchical queries
- 30:14OBDD limitations
- 33:07Inversions and OBDD size
- 36:23OBDDs for model counting
- 39:41Free binary decision diagrams
- 41:06FBDD and decision-DNNF limits
- 43:19Summary and open problems
related talks
21mCFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams
15mPolynomial Bounds of CFLOBDDs against BDDs
21mWeighted Context-Free-Language Ordered Binary Decision Diagrams
01h 04mKnowledge Compilation for Quantification and Synthesis
32mCircuits for Querying Trees: A Little Survey
01h 01mTop-Down Lower Bounds for Depth-Four Circuits
25mLearning Formulas in Finite Variable Logics
16mOn Oracles and Algorithmic Methods for Proving Lower Bounds