
| Notation   | Query                                |
|------------|--------------------------------------|
| CO         | polytime consistency check           |
| VA         | polytime validity check              |
| CE         | polytime clausal entailment check    |
| IM         | polytime implicant check             |
| EQ         | polytime equivalence check           |
| SE         | polytime sentential entailment check |
| CT         | polytime model counting              |
| ME         | polytime model enumeration           |

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

Table 4 summarizes the queries we are interested in and their acronyms.

The following proposition states what we know about the availability of polytime algorithms for answering the above queries, with respect to all languages we introduced in Section 2. Proposition 4.1 **The results in Table 5 hold.**
The results of Proposition 4.1 are summarized in Figure 4. One can draw a number of conclusions based on the results in this figure. First, NNF, s-NNF, d-NNF, f-NNF**, and** BDD **fall in one equivalence** class that does not support any polytime queries and CNF satisfies only VA and IM**; hence, none**
of them qualifies as a target compilation language in this case. But the remaining languages all support polytime tests for consistency and clausal entailment. Therefore, simply imposing either of smoothness (s-NNF**), determinism (**d-NNF**), flatness (**f-NNF**), or decision (**BDD**) on the** NNF **language does not lead to tractability with respect to any of the queries we consider—neither of these**
properties seem to be significant in isolation. Decomposability (DNNF**), however, is an exception and**
leads immediately to polytime tests for both consistency and clausal entailment, and to a polytime algorithm for model enumeration.