Recall the succinctness ordering DNNF < d-DNNF < FBDD < OBDD < OBDD< < MODS
from Figure 5. By adding decomposability (DNNF**), we obtain polytime tests for consistency and**
clausal entailment, in addition to a polytime model enumeration algorithm. By adding determinism to decomposability (d-DNNF**), we obtain polytime tests for validity, implicant and model counting,**
which are quite significant. It is not clear, however, whether the combination of decomposability and determinism leads to a polytime test for equivalence. Moreover, adding the decision property on top of decomposability and determinism (FBDD**) does not appear to increase tractability with respect to**
the given queries3**, although it does lead to reducing language succinctness as shown in Figure 5. On**
the other hand, adding the ordering property on top of decomposability, determinism and **decision,**
leads to polytime tests for equivalence (OBDD and OBDD<**) as well as sentential entailment provided** that the ordering < **is fixed (**OBDD<).

As for the succinctness ordering NNF < DNNF < DNF < IP < MODS **from Figure 5, note that**
DNNF **is obtained by imposing decomposability on** NNF**, while** DNF **is obtained by imposing flatness** and simple-conjunction (which is stronger than decomposability). What is interesting is that DNF is less succinct than DNNF**, yet does not support any more polytime queries; see Figure 4. However, the**
addition of smoothness (and determinism) on top of flatness and simple-conjunction (MODS**) leads to**
five additional polytime queries, including equivalence and entailment tests.4 We close this section by noting that determinism appears to be necessary (but not sufficient) for polytime model counting: only deterministic languages, d-DNNF, sd-DNNF, FBDD, OBDD, OBDD< and MODS**, support polytime counting. Moreover, polytime counting implies a polytime test of validity,**
but the opposite is not true.

## 5. Transforming A Compiled Theory

A query is an operation that returns information about a theory without changing it. A transformation, on the other hand, is an operation that returns a modified theory, which is then operated on using queries. Many applications require a combination of transformations **and queries.**
Definition 5.1 (∧C,∨C) Let L **be a subset of** NNF. L satisfies ∧C (∨C**) iff there exists a polytime**
algorithm that maps every finite set of formulas Σ1,... , Σn from L to a formula of L **that is logically**
equivalent to Σ1 ∧ ... ∧ Σn (Σ1 ∨ ... ∨ Σn).

Definition 5.2 (¬C) Let L **be a subset of** NNF. L satisfies ¬C **iff there exists a polytime algorithm**
that maps every formula Σ from L to a formula of L **that is logically equivalent to** ¬Σ.

If a language satisfies one of the above properties, we will say that it is closed **under the corresponding operator. Closure under logical connectives is important for two key reasons. First, it has**
implications on how compilers are constructed for a given target language. For example, if a clause can be easily compiled into some language L**, then closure under conjunction implies that compiling**
a CNF sentence into L **is easy. Second, it has implications on the class of polytime queries supported**
by the target language: If a language L satisfies CO **and is closed under negation and conjunction,**
then it must satisfy SE (to test whether ∆ |**= Γ, all we have to do, by the Refutation Theorem,** is test whether ∆ ∧ ¬Γ is inconsistent). Similarly, if a language satisfies VA **and is closed under**
negation and disjunction, it must satisfy SE **by the Deduction Theorem.**
3. Deciding the equivalence of two sentences in FBDD, d-DNNF**, or in** sd-DNNF**, can be easily shown to be in** coNP.

However, we do not have a proof of coNP**-hardness, nor do we have deterministic polytime algorithms for deciding**
these problems. Actually, the latter case is quite unlikely **as the equivalence problem for** FBDD **has been intensively** studied, with no such algorithm in sight. Note, however, that the equivalence of two sentences in FBDD **can be**
decided probabilistically in polytime (Blum, Chandra, & Wegman, 1980), and similarly for sentences in d-DNNF
(Darwiche & Huang, 2002).

4. Given flatness, simple-conjunction and smoothness, we can **obtain determinism by simply removing duplicated**
terms.