Instead of focusing on classical, flat **target compilation languages based on CNF and DNF, we**
consider a richer, nested **class based on representing propositional sentences using directed acyclic**
graphs, which we refer to as NNF**. We identify a number of target compilation languages that have**
been presented in the AI, formal verification, and computer science literature and show that they are special cases of NNF**. For each such class, we list the extra conditions that need to be imposed**
on NNF **to obtain the specific class, and then identify the set of queries and transformations that the**
class supports in polytime. We also provide cross-rankings of the different subsets of NNF**, according**
to their succinctness and the polytime operations they support.

The main contribution of this paper is then a map **for deciding the target compilation language**
that is most suitable for a particular application. Specifically, we propose that one starts by identifying the set of queries and transformations needed for their given application, and then choosing the most succinct language that supports these operations in polytime.

This paper is structured as follows. We start by formally defining the NNF **language in Section 2,**
where we list a number of conditions on NNF **that give rise to a variety of target compilation languages.**
We then study the succinctness of these languages in Section 3 and provide a cross-ranking that compares them according to this measure. We consider a number of queries and their applications in Section 4 and compare the different target compilation languages according to their tractability with respect to these queries. Section 5 is then dedicated to a class of transformations, their applications, and their tractability with respect to the different target compilation languages. We finally close in Section 6 by some concluding remarks. Proofs of all theorems are delegated to Appendix A.

## 2. The Nnf **Language**

We consider more than a dozen languages in this paper, all of which are subsets of the NNF **language,**
which is defined formally as follows (Darwiche, 1999, 2001a).

Definition 2.1 **Let PS be a denumerable set of propositional variables. A sentence in** NNFPS is a rooted, directed acyclic graph (DAG) where each leaf node is labeled with true, false, X or ¬X, X ∈ PS; and each internal node is labeled with ∧ or ∨ **and can have arbitrarily many children.**
The size of a sentence Σ in NNFPS, denoted | Σ |**, is the number of its DAG edges. Its height is the**
maximum number of edges from the root to some leaf in the DAG.

Figure 1 depicts a sentence in NNF**, which represents the odd parity function (we omit reference**
to variables PS when no confusion is anticipated). Any propositional sentence can **be represented**
as a sentence in NNF**, so the** NNF language is **complete**.

It is important here to distinguish between a representation language and a **target compilation**
language. A representation language is one which we expect humans to read and write with some ease. The language of CNF is a popular representation language, and so is the language of Horn clauses (especially when expressed in rules form). On other hand, a target compilation **language does**
not need to be suitable for human specification and interpretation, but should be tractable enough to permit a non-trivial number of polytime queries and/or transformations. We will consider a number of target compilation languages that do not qualify as representation languages from this perspective, as they are not suitable for humans to construct or interpret. We will also consider a number of representation languages that do not qualify as target compilation languages.1 A formal characterization of representation languages is outside the scope of this paper. But for a language to qualify as a target compilation language, we will require that it permits a polytime clausal entailment test. Note that a polytime consistency test is not sufficient here, as only one consistency test on a given theory does not justify its compilation. Given this definition, NNF **does**