

![0_image_0.png](0_image_0.png)

![0_image_1.png](0_image_1.png)

L NNF DNNF d-DNNF FBDD OBDD OBDD< DNF CNF PI IP MODS sd-DNNF
NNF ≤ ≤ ≤ ≤ ≤ ≤ ≤ ≤ ≤ ≤ ≤ ≤
DNNF 6≤∗ ≤ ≤ ≤ ≤ ≤ ≤ 6≤∗ ≤ ≤ ≤
d-DNNF 6≤∗ 6≤∗ ≤ ≤ ≤ ≤ 6≤∗ 6≤∗ ≤ ≤
FBDD 6≤ 6≤ 6≤ ≤ ≤ ≤ 6≤ 6≤ 6≤ 6≤ ≤ 6≤
OBDD 6≤ 6≤ 6≤ 6≤ ≤ ≤ 6≤ 6≤ 6≤ 6≤ ≤ 6≤

![0_image_2.png](0_image_2.png)

## Table 15:

CNF sentence Σ, allowing clausal entailment to be achieved in polynomial time. The **existence of**
such (¬Σ)∗ **for every** CNF **sentence Σ implies the collapse of the polynomial hierarchy (Selman &**
Kautz, 1996; Cadoli & Donini, 1997). Hence, we obtain that d-DNNF 6≤∗ DNF**. As a consequence, we**
also have d-DNNF 6≤∗ DNNF**. Finally, since every** d-DNNF **sentence can be turned in polynomial time**
into an equivalent sd-DNNF **sentence by Lemma A.1, we have** sd-DNNF ≤ d-DNNF**. Moreover, since** d-DNNF ≤ sd-DNNF**, we obtain** sd-DNNF 6≤∗ DNF, sd-DNNF 6≤∗ DNNF, sd-DNNF ≤ FBDD, sd-DNNF ≤ OBDD, sd-DNNF ≤ OBDD<, FBDD 6≤ sd-DNNF, OBDD< 6≤ sd-DNNF, DNF 6≤ sd-DNNF, CNF 6≤ sd-DNNF, PI 6≤ sd-DNNF and IP 6≤ sd-DNNF.

Table 15: **Let us now show that** MODS **is not less succinct than** PI, IP, sd-DNNF and OBDD.

First, let us consider the formula Σ = Wn i=1 xi**. Σ can be represented by** PI, IP, sd-DNNF and OBDD
formulas of size polynomial in n**. Contrastingly, Σ cannot be represented by a** MODS **formula of**
size polynomial in n since Σ has 2n − 1 models over Vars**(Σ). Now, it is well-known that the old**
good Quine-McCluskey's algorithm for generating prime implicants from a MODS **representation of**
a propositional formula Σ runs in time polynomial in the number of models of Σ (Wegener, 1987).

This shows that IP ≤ MODS**. As to** CNF and OBDD<**, it is obvious that a decision tree (or Shannon tree)**
for Σ that respects a given total ordering over Vars**(Σ) can be generated in polynomial time from a**
MODS representation of Σ. Such a decision tree has m 1-leaves where m **is the number of models of**
Σ over Vars(Σ). Accordingly, it has at most n ∗ m 0-leaves where n = |Vars(Σ)|**. Since the set of all**
paths from the root of the tree to any 0-leaf can be read as a CNF **representation of Σ, we obtain that**
CNF ≤ MODS**. On the other hand, since reducing a decision tree to derive a corresponding OBDD**<
can be done in polynomial time, it follows that an OBDD< **representation of Σ can also be generated**
from a MODS **representation of it. Hence,** OBDD< ≤ MODS**. The remaining results in this table follow**
from the language inclusions reported in Figure 4. ✷

## Proof Of Proposition 4.1

The proof of this proposition is broken down into twelve steps. In each step, **we prove a number** of results. Associated with each step of the proof is a table in which we mark all results that are proved in that step. The table of the last step includes all results declared by this proposition.

Table 16: **Every classical CNF or DNF formula can be translated in a straightforward way into**
an equivalent f-NNF **sentence (with a tree structure) in polytime. Moreover, every** NNF **sentence** can be translated into an equivalent s-NNF **sentence in polytime (Lemma A.1). Given that** CO
is NP**-hard (resp.** VA is coNP**-hard) for classical CNF (resp. DNF) sentences, and the inclusion**
between the various NNF **subsets reported in Figure 4, we obtain the table.**
Table 17: SE implies both CO and VA (Lemma A.10). Moreover, since CT **implies both** CO
and VA, IM implies VA (valid term), and CE implies CO **(inconsistent clause), we obtain the**
table.