PI satisfies FO (see below), the prime implicates of ∃Vars(γ).(Σ ∧γ**) can be computed in**
polytime. But these are exactly the prime implicates of Σ | γ **according to Lemma A.12.**
- IP**. Let Σ =** Wn i=1 γi **be a formula in prime implicants form. It is clear that the formula**
(Wn i=1 γi) | γ is a DNF formula equivalent to Σ | γ**. Now, our claim is that the formula Σ**∗
obtained by keeping only the logically weakest terms γi| γ **among (**Wn i=1 γi) | γ **is a prime**
implicants formula equivalent to Σ | γ**. Removing such terms clearly is truth-preserving.** Since generating Σ∗ **requires only** O(n 2**) entailment tests among terms, and since such**
tests can be easily achieved in polynomial time, we obtain that IP satisfies CD**. Now,**
how to prove that Σ∗ **is in prime implicants form? Since any pair of different terms of** Σ∗ **cannot be compared w.r.t. logical entailment, the correctness of Quine's consensus**
algorithm for generating prime implicants shows that it is sufficient to prove that every consensus among two terms of Σ∗ is inconsistent or entails another term of Σ∗**. Let's**
recall that consensus is to DNF formulas what resolution is to CNF formulas. **Since Σ**
is in prime implicants form, every consensus among two terms of Σ is inconsistent or entails another term of Σ. What happens to the terms (here, the prime implicants) of Σ
when conditioned by γ? All those containing the negation of a literal of γ **are removed**
and the remaining ones are shortened by removing from them every literal of γ**. Hence,**
for every pair of terms γ1, γ2 of Σ, if there is no consensus between γ1 and γ2**, then**
there is no consensus between γ1|γ and γ2|γ**: conditioning cannot create new consensus.**
Now, it remains to prove that no unproductive consensus between terms of Σ can be rendered productive through conditioning. Formally, let γ1 = γ
′
1 ∧ l and γ2 = γ
′
2 ∧ ¬l be two prime implicates of Σ s.t. l (resp. ¬l**) does not appear in** γ
′
1**(resp.** γ
′
2**). There is a**
consensus γ
′
1∧γ
′
2 between γ1 and γ2. Let us assume that both γ1 and γ2 **have survived the**
conditioning: this means that both γ1|γ and γ2|γ are consistent. Especially, l **belongs to** γ1|γ and ¬l belongs to γ2|γ. Accordingly, there is a consensus between γ1|γ and γ2|γ**. By**
construction, this consensus is equivalent to (γ
′
1|γ)∧(γ
′
2|γ**), hence equivalent to (**γ
′
1∧γ
′
2)|γ.

Now, if γ
′
1 ∧ γ
′
2**is inconsistent, then (**γ
′
1 ∧ γ
′
2)|γ **is inconsistent as well and we are done.**
Otherwise, let us assume that there exists a prime implicant γ3 **of Σ s.t.** γ
′
1 ∧ γ
′
2|= γ3 holds. Necessarily, γ3 is preserved by the conditioning of Σ by γ. Otherwise, γ3 **would**
contain the negation of a literal of γ, but since every literal of γ3 is a literal of γ1 **or a** literal of γ2, γ2 and γ3 **would not have both survived the conditioning. Since** γ
′
1 ∧γ
′
2|= γ3 holds, we necessarily have (γ
′
1 ∧ γ
′
2)|γ |= γ3|γ**. This completes the proof.**
- MODS**. Direct consequence of Lemma A.12 and the fact that** MODS satisfies ∧BC and FO
(see below).

- FO.

- DNNF and DNF**. It is known that** DNNF satisfies FO **(Darwiche, 2001a). It is also known**
that DNF satisfies FO **(Lang et al., 2000).**
- NNF, s-NNF, f-NNF, d-NNF, BDD and CNF**. Let Σ be a sentence in** CNF**. We now show that**
if any of the previous languages satisfies FO**, then we can test the consistency of Σ in**
polytime. Since CNF does not satisfy CO **(see Proposition 4.1), it then follows that none**
of the previous languages satisfy FO unless P = NP**. First, we note that Σ must also**
belong to NNF and f-NNF**. Moreover, Σ can be turned into a sentence in** BDD **in polytime** (Lemma A.8) or a sentence in s-NNF **in polytime (see the proof of Lemma A.1). We**
also have that Σ can be turned into a sentence in d-NNF **in polytime since** BDD ⊆ d-NNF.

Suppose now that one of the previous languages, call it L, satisfy FO**. We can test the**
consistency of Σ in polytime as follows:
∗ Convert Σ into a sentence Σ∗ in L **in polytime (as shown above).**
∗ Compute ∃Vars(Σ∗).Σ∗**, which can be done in polytime by assumption.**