Source-linked AI summary
Lower Bounds for Exact Model Counting and Applications in Probabilistic Databases
Paul Beame, Jerry Li, Sudeepa Roy, Dan Suciu
TL;DR
Exact model counting and satisfying-probability computation rely on methods that produce decision-DNNFs, raising the question of how compact these representations can be. The paper translates decision-DNNFs into FBDDs and applies known FBDD lower bounds to derive limits for exact-counting algorithms and probabilistic-database queries.
Problem
Exact model counting asks for the number of satisfying assignments of a Boolean formula, and current exact methods produce decision-DNNFs.
Source: §1 · pp. 1–2Method
The paper translates decision-DNNFs into equivalent FBDDs with quasipolynomial size increase generally and polynomial increase for monotone k-DNF.
Source: §1 · p. 2Results
Takeaways & Limitations
The bounds apply to natural formula classes and extend to query evaluation in probabilistic databases.
Source: §1 · p. 2, §7 · p. 9The translation gives only a quasipolynomial bound in general, and the authors leave open whether a polynomial simulation exists.
Source: §7 · p. 9
Abstract
from arXiv · showhide
The best current methods for exactly computing the number of satisfying assignments, or the satisfying probability, of Boolean formulas can be seen, either directly or indirectly, as building 'decision-DNNF' (decision decomposable negation normal form) representations of the input Boolean formulas. Decision-DNNFs are a special case of 'd-DNNF's where 'd' stands for 'deterministic'. We show that any decision-DNNF can be converted into an equivalent 'FBDD' (free binary decision diagram) -- also known as a 'read-once branching program' (ROBP or 1-BP) -- with only a quasipolynomial increase in representation size in general, and with only a polynomial increase in size in the special case of monotone k-DNF formulas. Leveraging known exponential lower bounds for FBDDs, we then obtain similar exponential lower bounds for decision-DNNFs which provide lower bounds for the recent algorithms. We also separate the power of decision-DNNFs from d-DNNFs and a generalization of decision-DNNFs known as AND-FBDDs. Finally we show how these imply exponential lower bounds for natural problems associated with probabilistic databases.
1 Introduction
Exact model counting and probability computation are supported by algorithms that produce decision-DNNF representations, motivating lower bounds on their size. The paper translates decision-DNNFs into FBDDs and uses known FBDD lower bounds to derive consequences for exact counting and probabilistic databases.
1 Introduction
- Modern exact model-counting methods, including DPLL-based and knowledge-compilation approaches, can be viewed as producing decision-DNNFs.Knowledge-compilation efficiency depends both on representation size and construction time.Source: §1 · pp. 1–2
- Known exponential FBDD lower bounds transfer to decision-DNNFs through a quasipolynomial-size translation, yielding lower bounds for modern exact model-counting algorithms.For monotone k-DNF formulas, the translation has only polynomial size increase.Source: §1 · p. 2
- Decision-DNNFs differ from FBDDs by exploiting decompositions into connected components, but those decompositions yield at most quasipolynomial improvements, or polynomial improvements for monotone k-DNF.Without dynamic component caching, DPLL trace extensions yield FBDDs.Source: §1 · p. 2
- The translation also establishes exponential representational separations between decision-DNNFs and both d-DNNFs and AND-FBDDs.The argument transfers known FBDD lower bounds for functions with linear-size representations in those other formalisms.Source: §1 · p. 3
- For probabilistic databases, query evaluation reduces to computing probabilities of positive k-DNF formulas, and the results yield query classes requiring exponential-size decision-DNNFs.Consequently, recent evaluation algorithms that produce decision-DNNFs cannot compute those queries efficiently.Source: §1 · p. 3
- Representation size is not the only cost: compiling a formula can take exponential time even when an unsatisfiable formula has a size-1 decision-DNNF.The authors note that they know of no lower bounds on this excess compilation time for the simple, highly satisfiable instances they discuss.Source: §1 · p. 3
2 FBDDs and Decision-DNNFs
The section defines FBDDs as read-once branching representations and decision-DNNFs as a restricted form of AND-FBDD. FBDDs support linear-time probability computation, while decision-DNNFs require disjoint variables across AND branches.
2 FBDDs and Decision-DNNFs
- An FBDD is a decision DAG in which each root-to-leaf path tests any Boolean variable at most once.Its size is the number of nodes, and its output probability is computed by a linear-time dynamic program.Source: §2 · p. 4
- A decision-DNNF is an AND-FBDD whose AND-node children mention pairwise disjoint sets of Boolean variables.An AND-node computes the conjunction of its children's functions.Source: §2 · p. 4
- The paper assumes binary AND-nodes and at most one incoming edge per 1-sink; enforcing these assumptions costs at most a quadratic increase in nodes.Source: §2 · p. 4
3 Main Results
The section bounds the cost of translating decision-DNNFs into equivalent FBDDs, then uses known FBDD lower bounds to establish limitations of decision-DNNFs. It applies these results to DPLL-based algorithms and separates decision-DNNFs from both AND-FBDDs and d-DNNFs.
3 Main Results
- A decision-DNNF with N nodes translates to an equivalent FBDD with at most N2^log2 N nodes, constructible within the same time bound.The general theorem bounds both size and construction time by NM^L; the corollary gives the quasipolynomial size bound.Source: §3 · p. 4
- For monotone k-DNF formulas, every decision-DNNF path has at most k−1 AND-nodes, yielding an equivalent FBDD with at most N^k nodes.This gives a polynomial size increase for this formula class.Source: §3 · p. 4
Lower Bounds for DPLL-based Algorithm
- Any DPLL-based algorithm whose trace is a decision-DNNF takes exponential time on ΨEn and Φn.The cited FBDD lower bound for ΨEn is 2^Ω(√n); the formulas used are monotone 2-DNF and 3-DNF, respectively.Source: Lower Bounds for DPLL-based Algorithm · pp. 4–5
- Decision-DNNFs are exponentially less concise than AND-FBDDs: the dual CNF has an AND-FBDD of at most n^2 nodes, while decision-DNNFs require 2^Ω(n^1/4) nodes.The lower bound follows by converting a decision-DNNF into an FBDD and applying the FBDD lower bound.Source: Lower Bounds for DPLL-based Algorithm · p. 5
- Decision-DNNFs are exponentially less concise than d-DNNFs.The passage describes Γn as having an O(n^2)-size d-DNNF and an FBDD lower bound of 2^Ω(n), implying a decision-DNNF lower bound of 2^Ω(n^1/2).Source: Lower Bounds for DPLL-based Algorithm · p. 5
4 Decision-DNNF to FBDD
The section constructs an equivalent FBDD by replacing decision-DNNF AND-nodes, using copies and child reordering to handle conflicts that defeat simple stacking. It proves the construction’s correctness and size bound, then gives an example showing that this construction’s bound cannot be tightened to polynomial.
4.1 Main Ideas
- Simple stacking fails when a shared 1-sink in one child must redirect to different children; copying subgraphs and reordering AND-node children resolve the conflict.When a decision-DNNF has only one AND-node, stacking its two child FBDDs and redirecting 1-sinks computes their conjunction correctly.Source: §4.1 · p. 5
4.2 The Construction of F
- The construction represents each FBDD node as (u, s), tracking the light edges on a path to u, and uses copies to route 1-sinks across AND-nodes.At a 1-sink, a nonempty s produces a no-op node that connects to the heavy child; an empty s leaves the node a 1-sink.Source: §4.2 · pp. 5–6
4.3 Proof of Theorem 3.1
- F has at most N M^L nodes, where N is the number of decision-DNNF nodes, M the number of light edges, and L the maximum number of light edges on a path.The bound follows by representing F-nodes as pairs (u, s), with at most N choices for u and at most M^L choices for s.Source: §4.3 · p. 6
- The resulting graph is a correct FBDD and computes the same function as the original decision-DNNF.The proof establishes that F is acyclic, reads each variable at most once on every path, and preserves the function’s value on every assignment.Source: §4.3 · pp. 6–7
4.4 A Tight Example
- The construction’s copy count can be 2^Ω(log^2 M), so its size bound cannot be tightened to polynomial for this construction.The paper cautions that this example does not separate FBDDs from decision-DNNFs: a smaller equivalent FBDD may exist.Source: §4.4 · pp. 7–8
5 Monotone k-DNFs
For monotone k-DNFs, the section bounds the number of AND-nodes along a path in terms of k. Its proof uses partial assignments to expose conjunctions of variables and relies on decomposability at AND-nodes.
5 Monotone k-DNFs
- In a monotone function, k is the size of its largest prime implicant, and partial assignments preserve the k-DNF property with width at most k.A prime implicant is a minimal set of variables whose conjunction implies the function.Source: §5 · p. 8
- If Φu is a monotone k-DNF and Au ≥ 1, then k ≥ Au + 1.Here Au is the maximum number of AND-nodes on a path from u to a leaf.Source: §5 · p. 8
- For every such u, a partial assignment can make Φu a conjunction of at least Au + 1 variables.The proof establishes this claim by induction on Au, reducing to an AND-node when u is not one.Source: §5 · p. 8
- At an AND-node, disjoint child variable sets let the proof combine partial assignments into a conjunction whose size is at least Au + 1.The induction handles the first child using its path’s AND-node count, and a nonredundant second child contributes at least one variable.Source: §5 · p. 8
6 Lower Bounds in Probabilistic Databases
The paper applies decision-DNNF lower bounds to probabilistic database query evaluation in data complexity, where the query is fixed and the database instance grows. Every non-hierarchical Boolean union of conjunctive queries has lineage requiring decision-DNNFs of size 2^Ω(√n), for domain size n.
6 Lower Bounds in Probabilistic Databases
- Probabilistic database evaluation computes the probability of a query’s lineage, with each uncertain tuple represented by a Boolean variable.The paper considers a fixed query and a variable database instance.Source: §6 · p. 9
- The query ∃x∃y R(x) ∧ S(x, y) ∧ T(y) has a lineage requiring decision-DNNFs of size 2^Ω(√n).For the proof, the lineage is identified with the formula from Corollary 3.6, up to variable renaming.Source: §6 · p. 9
- For every non-hierarchical Boolean union of conjunctive queries, any decision-DNNF for its lineage has size 2^Ω(√n), where n is the database domain size.The result concerns query evaluation in data complexity: the query is fixed while the database instance grows.Source: §6 · pp. 8–9
- The asthma-patient-with-a-smoker-friend query is non-hierarchical, so its decision-DNNF representations have size at least 2^Ω(√n).Its variables occur in overlapping atom sets: at(x) = {Patient, Friend} and at(y) = {Friend, Smoker}.Source: §6 · p. 9
- The query asking whether a database contains a triangle of friends also requires decision-DNNFs of size 2^Ω(√n).The triangle query is another non-hierarchical query covered by the general theorem.Source: §6 · p. 9
7 Conclusions and Open Problems
The paper concludes that its decision-DNNF-to-FBDD conversion transfers known FBDD lower bounds to decision-DNNFs and yields separations and algorithmic lower bounds. Whether general decision-DNNFs admit polynomial-size FBDD simulations remains open.
7 Conclusions and Open Problems
- A decision-DNNF can be converted to an equivalent FBDD with at most quasipolynomial size increase, or polynomial increase for k-DNF formulas, yielding representation separations and lower bounds for algorithms that produce decision-DNNFs.The separations are from d-DNNFs and AND-FBDDs; the algorithmic bounds include current exact model-counting algorithms.Source: §7 · p. 9
- Whether decision-DNNFs have polynomial-size FBDD simulations in the general case remains an open question.The paper also asks whether the example from Section 4.4 has a polynomial-size FBDD.Source: §7 · p. 9
- The paper leaves open whether another d-DNNF subclass is useful for exact model counting and what limits apply to approximate model counting.Source: §7 · p. 9