
| L       | CO   | VA   | CE   | IM   | EQ   | CT   | SE   | ME   |
|---------|------|------|------|------|------|------|------|------|
| NNF     | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| DNNF    | √    | ◦    | √    | ◦    | ◦    | ◦    | ◦    | √    |
| d-NNF   | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| d-DNNF  | √    | √    | √    |      |      |      |      |      |
| BDD     | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| FBDD    | √    | √    | √    | √    | √    | √    |      |      |
| OBDD    | √    | √    | √    | √    | √    | √    | ◦    | √    |
| OBDD<   | √    | √    | √    | √    | √    | √    | √    | √    |
| DNF     | √    | ◦    | √    | ◦    | ◦    | ◦    | ◦    | √    |
| CNF     | ◦    | √    | ◦    | √    | ◦    | ◦    | ◦    | ◦    |
| PI      | √    | √    | √    | √    | √    | ◦    | √    | √    |
| IP      | √    | √    | √    | √    | √    | ◦    | √    | √    |
| MODS    | √    | √    | √    | √    | √    | √    | √    | √    |
| s-NNF   | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| f-NNF   | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| sd-DNNF | √    | √    | √    |      |      |      |      |      |

| L       | CO   | VA   | CE   | IM   | EQ   | CT   | SE   | ME   |
|---------|------|------|------|------|------|------|------|------|
| NNF     | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| DNNF    | √    | ◦    | √    | ◦    | ◦    | ◦    | ◦    | √    |
| d-NNF   | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| d-DNNF  | √    | √    | √    | √    | √    | √    |      |      |
| BDD     | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| FBDD    | √    | √    | √    | √    | √    | √    |      |      |
| OBDD    | √    | √    | √    | √    | √    | √    | ◦    | √    |
| OBDD<   | √    | √    | √    | √    | √    | √    | √    | √    |
| DNF     | √    | ◦    | √    | ◦    | ◦    | ◦    | ◦    | √    |
| CNF     | ◦    | √    | ◦    | √    | ◦    | ◦    | ◦    | ◦    |
| PI      | √    | √    | √    | √    | √    | ◦    | √    | √    |
| IP      | √    | √    | √    | √    | √    | ◦    | √    | √    |
| MODS    | √    | √    | √    | √    | √    | √    | √    | √    |
| s-NNF   | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| f-NNF   | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    | ◦    |
| sd-DNNF | √    | √    | √    | √    | √    | √    |      |      |

only)). Since PI satisfies CE, it also satisfies CO. Since it satisfies CD **as well (cf. Proposition 5.1),**
it also satisfies ME **(Lemma A.3). Contrastingly, the models counting problem for monotone Krom**
formulas (i.e. conjunctions of clauses containing at most two literals and only **positive literals)**
is \#P**-complete (Roth, 1996). Such formulas can easily be turned into prime implicates form in**
polynomial time (Marquis, 2000), hence PI does not satisfy CT**. Now, since the negation of a**
formula Σ in prime implicates form is a formula in prime implicants form **(cf. Lemma A.14), and**
since the number of models of ¬Σ over Vars(Σ) is 2|Vars(Σ)| **minus the number of models of Σ over**
Vars(Σ), we necessarily have that IP does not satisfy CT. This also imply that IP **satisfies** VA,
leading to the table.

Table 25: In the proof of Proposition 3.1, we have shown that the prime implicants **of Σ can**
be computed in polytime from a MODS **representation of Σ. As an immediate consequence, since** IP satisfies IM, EQ and SE**, we obtain that** MODS satisfies IM, EQ and SE**, leading to the table.**
Table 26: **Since** d-DNNF satisfies CT (Darwiche, 2001b), it also satisfies VA**. Since it satisfies**
CD (Proposition 5.1), it also satisfies IM **as well (Lemma A.7). Since** sd-DNNF ⊆ d-DNNF**, these**
results follow for sd-DNNF**. Hence, we obtain the table.**
Table 27: **It is known that determining whether the conjunction of two** FBDD formulas α1 and α2 is consistent is NP**-complete (Gergov & Meinel, 1994b) Moreover,** FBDD satisfies ¬C**. Since** α1 ∧ α2 is inconsistent iff α1 |= ¬α2**, we can reduce the consistency test into an entailment test. Hence,** FBDD
does not satisfy SE**. Since** FBDD ⊆ d-DNNF, d-DNNF does not satisfy SE **either. Finally, since every**
d-DNNF **can be translated into an equivalent** sd-DNNF **sentence in polytime (Lemma A.1),** sd-DNNF
does not satisfy SE **either. This leads to the final table above.** ✷