Lemma A.11 Let Σ **be a sentence in** d-DNNF and let γ be a clause. The validity of Σ ∨ γ **can be**
tested in time polynomial in the size of Σ and γ.

Proof: Construct Σ ∨ γ **in polytime as given in Lemma A.6 and check its validity, which can be**
done in polytime too. ✷
Lemma A.12 For every propositional formula Σ and every consistent term γ**, we have** Σ|γ is equivalent to
∃**Vars**(γ).(Σ ∧ γ).

Proof: **Without loss of generality, assume that Σ is given by the disjunctively-interpreted set of**
its models (over Vars(Σ)). Conditioning Σ on γ leads (1) to removing every model of ¬γ**, then**
(2) projecting the remaining models so that every variable of γ **is removed. Conjoining Σ with** γ leads exactly to (1), while forgetting every variable of γ **in the resulting formula leads exactly to (2)**
(Lang, Liberatore, & Marquis, 2000). ✷
Lemma A.13 **Each sentence** Σ in f-NNF can be converted into an equivalent sentence Σ∗ in polynomial time, where Σ∗ ∈ CNF or Σ∗ ∈ DNF.

Proof: **We consider three cases for the sentence Σ:**

1. The root node of Σ is an and-node. In this case, Σ can be turned into a CNF **sentence Σ**∗ in polynomial time by simply ensuring that each or-node in Σ is a clause (that is, **a disjunction**
of literals that share no variables). Let C **be an or-node in Σ. Since Σ is flat and its root is**
an and-node, C must be a child of the root of Σ and the children of C **must be leaves. Hence,** we can easily ensure that C **is a clause as follows:**
- If we have one edge from C to some leaf X and another edge from C to ¬X (C **is valid),**
we replace the edge from the root to C by an edge from the root to **true**.

- If we have more than one edge from C to the same leaf node X**, we keep only one of these**
edges and delete the rest.
2. The root of Σ is an or-node. Σ can be turned into a DNF sentence Σ∗ **in a dual way.**5 3. The root of Σ is a leaf node. Σ is already a CNF **sentence.**
✷

Lemma A.14 α is a prime implicant (resp. an essential prime implicant) of sentence Σ iff ¬α is a prime implicate (resp. an essential prime implicate) of ¬Σ.

6 Proof: **This is a folklore result, immediate from the definitions.** ✷

## Proof Of Proposition 3.1

The proof of this proposition is broken down into eight steps. In each step, we prove a number of succinctness relationships between different languages, and then apply transitivity of the **succinctness**
relation to infer even more relationships. Associated with each step of the proof is a table in which