that we report in Tables 5 and 7. They also exhibit different succinctness relationships than the ones we report in Table 3.

Horn theories (and renamable Horn theories) represent another target compilation **subset of** CNF,
but we do not consider it here since we restrict our attention to complete languages L **only, i.e., we**
require that every propositional sentence is logically equivalent to an element of L.

We now consider nested **subsets of the** NNF **language, which do not impose any restriction on**
the height of a sentence. Instead, these subsets result from imposing one or more of the following conditions: decomposability, determinism, smoothness, decision, and ordering. **We start by defining**
the first three properties. From here on, if C **is a node in an** NNF, then Vars(C**) denotes the set of**
all variables that label the descendants of node C**. Moreover, if Σ is an** NNF **sentence rooted at** C,
then Vars(Σ) is defined as **Vars**(C).

- Decomposability **(Darwiche, 1999, 2001a). An** NNF satisfies this property if for each conjunction C **in the** NNF, the conjuncts of C do not share variables. That is, if C1,... ,Cn are the children of and-node C, then Vars(Ci) ∩ Vars(Cj ) = ∅ for i 6= j**. Consider the and-node**
marked in Figure 1(a). This node has two children, the first contains variables A,B **while the**
second contains variables C,D**. This and-node is then decomposable since the two children do**
not share variables. Each other and-node in Figure 1(a) is also decomposable and, **hence, the**
NNF **in this figure is decomposable.**
- Determinism **(Darwiche, 2001b): An** NNF **satisfies this property if for each disjunction** C
in the NNF, each two disjuncts of C are logically contradictory. That is, if C1,... ,Cn are the children of or-node C, then Ci ∧ Cj |= false for i 6= j**. Consider the or-node marked** in Figure 1(b), which has two children corresponding to sub-sentences ¬A ∧ B and ¬B ∧ A.

The conjunction of these two sub-sentences is logically contradictory. The or-node is then deterministic and so are the other or-nodes in Figure 1(b). Hence, the NNF **in this figure is**
deterministic.

- Smoothness **(Darwiche, 2001b): An** NNF satisfies this property if for each disjunction C **in the**
NNF, each disjunct of C mentions the same variables. That is, if C1,... ,Cn **are the children of**
or-node C, then Vars(Ci) = Vars(Cj ) for i 6= j**. Consider the marked or-node in Figure 1(c).**
This node has two children, each of which mentions variables A,B**. This or-node is then**
smooth and so are the other or-nodes in Figure 1(c). Hence, the NNF **in this figure is smooth.**
It is hard to ensure decomposability. It is also hard to ensure determinism while **preserving decomposability. Yet any sentence in** NNF **can be smoothed in polytime, while preserving decomposability**
and determinism. Preserving flatness, however, may blow-up the size of given NNF**. Hence, smoothness is not that important from a complexity viewpoint unless we have flatness.**
The properties of decomposability, determinism and smoothness lead to a number of **interesting**
subsets of NNF.

Definition 2.5 **The language** DNNF **is the subset of** NNF **satisfying decomposability;** d-NNF **is the subset satisfying determinism;** s-NNF **is the subset satisfying smoothness;** d-DNNF **is the subset satisfying**
decomposability and determinism; and sd-DNNF **is the subset satisfying decomposability, determinism**
and smoothness.

Note that DNF **is a strict subset of** DNNF (Darwiche, 1999, 2001a). The following decision **property**
comes from the literature on binary decision diagrams **(Bryant, 1986).**
Definition 2.6 (Decision) A decision node N **in an** NNF **sentence is one which is labeled with true,**
false, or is an or-node having the form (X ∧ α) ∨ (¬X ∧ β), where X is a variable, α and β are decision nodes. In the latter case, dVar (N) **denotes the variable** X.

Definition 2.7 **The language** BDD **is the set of** NNF **sentences, where the root of each sentence is a**
decision node.