\documentstyle[jair,theapa]{article}
%\documentclass{article}

%\setlength\textheight{9in} \setlength\textwidth{6.5in}
%\setlength\topmargin{-.5in} \setlength\rightmargin{-.5in}
%\setlength\oddsidemargin{0in}
%\setlength{\evensidemargin}{\oddsidemargin}


%\usepackage{times}
%\usepackage{graphicx}
%\usepackage{amsmath}
%\usepackage{latexsym}
%\usepackage{named}

%\usepackage{ijcai01}
%\renewcommand{\baselinestretch}{.98}

\input{epsf.tex}

%\newcommand{\qed}{\rule{2mm}{2mm}}
\newcommand{\qed}{$\Box$}
\newenvironment{proof}{\noindent {\bf Proof:}}{\hfill \qed\\}

\def\L{{\bf L}}
\def\T{{\bf T}}
\def\Q{{\bf Q}}
\def\X{{\bf X}}
\def\Y{{\bf Y}}

\def\dagnnf{{\tt NNF}}
\def\nnf{{\tt NNF}}
\def\nnfps{{\mbox{\tt NNF}_{PS}}}
\def\nnfn{{\tt NNFn}}
\def\ps{{PS}}
\def\true{{\it true}}
\def\false{{\it false}}
\def\vars{{\it Vars}}
\def\var{{\it Var}}
\def\dvar{{\it dVar}}
\def\size{{\it size}}

\def\Dnnf{{\tt DNNF}}
\def\dnnf{{\tt d-NNF}}
\def\snnf{{\tt s-NNF}}
\def\fnnf{{\tt f-NNF}}
\def\flat{{\tt f-NNF}}
\def\dDnnf{{\tt d-DNNF}}
\def\sdDnnf{{\tt sd-DNNF}}
\def\bdd{{\tt BDD}}
\def\obdd{\(\mbox{\tt OBDD}_<\)}
\def\uobdd{{\tt OBDD}}
\def\fbdd{{\tt FBDD}}
\def\dnf{{\tt DNF}}
\def\cnf{{\tt CNF}}
\def\pi{{\tt PI}}
\def\ip{{\tt IP}}
\def\mods{{\tt MODS}}


\def\ok(#1){{\it ok}{#1}}

\def\co{{\sf \bf CO}}
\def\va{{\sf \bf VA}}
\def\ce{{\sf \bf CE}}
\def\im{{\sf \bf IM}}
\def\eq{{\sf \bf EQ}}
\def\ct{{\sf \bf CT}}
\def\se{{\sf \bf SE}}
\def\me{{\sf \bf ME}}

\def\cd{{\sf \bf CD}}
\def\fo{{\sf \bf FO}}
\def\ac{{\sf \bf \wedge C}}
\def\oc{{\sf \bf \vee C}}
\def\nc{{\sf \bf \neg C}}

\def\sfo{{\sf \bf SFO}}
\def\bac{{\sf \bf \wedge BC}}
\def\boc{{\sf \bf \vee BC}}

\def\unk{{\bf ?}}
\def\y{$\surd$}
\def\n{$\circ$}
\def\bn{$\bullet$}


\newcommand{\tqed}{\rule{.8mm}{2mm}}

\def\ny{$\tqed\surd\tqed$}
\def\nn{$\tqed\circ\tqed$}
\def\nbn{$\tqed\bullet\tqed$}

\def\as{{$\leq$}}
\def\nas{{$\not \leq$}}
\def\nasc{{$\not \leq^*$}}

\def\asn{{$\tqed\leq\tqed$}}
\def\nasn{{$\tqed\not\leq\tqed$}}
\def\nascn{{$\tqed\not\leq^*\tqed$}}

\newtheorem{definition}{Definition}[section]
\newtheorem{corollary}{Corollary}[section]
\newtheorem{proposition}{Proposition}[section]
\newtheorem{example}{Example}[section]
\newtheorem{lemma}{Lemma}[section]


\begin{document}


\jairheading{17}{2002}{229-264}{12/01}{9/02}

\ShortHeadings{A Knowledge Compilation Map}{Darwiche \& Marquis}

\firstpageno{229}


\title{A Knowledge Compilation Map}
%\author{Content Areas: automated reasoning, knowledge
%representation, computational complexity \\
%        Tracking Number: 000}

%\author{
%\begin{tabular}{cc}
%Adnan Darwiche &  \\
%Computer Science Department & CRIL\\
%University of California & Universit\'{e} d'Artois  \\
%Los Angeles, CA 90095, USA & F-62307, Lens Cedex, France \\
%darwiche@cs.ucla.edu &
%\end{tabular}
%}

\author{\name Adnan Darwiche \email darwiche@cs.ucla.edu \\
\addr Computer Science Department \\
University of California, Los Angeles \\
Los Angeles, CA 90095, USA \\ \\
\name Pierre Marquis \email  marquis@cril.univ-artois.fr \\
\addr Universit\'{e} d'Artois  \\
F-62307, Lens Cedex, France \\}


\maketitle

\begin{abstract}
We propose a perspective on knowledge compilation which calls for
analyzing different compilation approaches according to two key
dimensions: the succinctness of the target compilation language,
and the class of queries and transformations that the language
supports in polytime. We then provide a knowledge compilation map,
which analyzes a large number of existing target compilation
languages according to their succinctness and their polytime
transformations and queries. We argue that such analysis is
necessary for placing new compilation approaches within the
context of existing ones. We also go beyond classical, flat target
compilation languages based on CNF and DNF, and consider a richer,
nested class based on directed acyclic graphs (such as OBDDs),
which we show to include a relatively large number of target
compilation languages.
\end{abstract}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


Knowledge compilation has emerged recently as a key direction of
research for dealing with the computational intractability of
general propositional reasoning
\cite{darwicheIJCAI99a,CadoliDonini97,Boufkhadetal97,KhardonRo97l,SelmanKautz96,Schrag96,marquis95,delvalKR94,DechterRish94,reiter87}.
According to this direction, a propositional theory is compiled
off-line into a target language, which is then used on-line to
answer a large number of queries in polytime. The key motivation
behind knowledge compilation is to push as much of the
computational overhead into the off-line phase, which is
amortized over all on-line queries. But knowledge compilation can
serve other important purposes as well. For example, target
compilation languages and their associated algorithms can be very
simple, allowing one to develop on-line reasoning systems for
simple software and hardware platforms. Moreover, the simplicity
of algorithms that operate on compiled languages help in
streamlining the effort of algorithmic design into a single task:
that of generating the smallest compiled representations
possible, as that turns out to be the main computational
bottleneck in compilation approaches.

There are three key aspects of any knowledge compilation approach:
the succinctness of the target language into which the
propositional theory is compiled; the class of queries that can
be answered in polytime based on the compiled representation; and
the class of transformations that can be applied to the
representation in polytime. The AI literature has thus far
focused mostly on target compilation languages which are
variations on DNF and CNF formulas, such as Horn theories and
prime implicates. Moreover, it has
 focused mostly on clausal entailment queries, with
%---to the point where
%tractability in the context of knowledge compilation is largely
%taken to mean the ability to answer such queries in polynomial
%time \cite{CadoliDonini97}.
very little discussion of tractable transformations on compiled
theories.
% (although some of these transformations can be quite
%valuable for certain AI applications).

The goal of this paper is to provide a broad perspective on
knowledge compilation by considering a relatively large number of
target compilation languages and analyzing them according to
their {\em succinctness} and the class of {\em
queries/transformations} that they admit in polytime.

Instead of focusing on classical, {\em flat} target compilation
languages based on CNF and DNF, we consider a richer, {\em
%2Pierre: I removed the comma after nested
nested} class based on representing propositional sentences using
directed acyclic graphs, which we refer to as \dagnnf. 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 \dagnnf. For
each such class, we list the extra conditions that need to be
imposed on \dagnnf\ 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 \dagnnf, according to their succinctness and
the polytime operations they support.

The main contribution of this paper is then a {\em 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.

%Another goal of this paper is to stress the need for analyzing any
%new target compilation language across the dimensions that we have
%identified above. For example, it is not that meaningful to claim
%that one compilation language is more succinct than another,
%without a discussion on the tractable class of queries and
%transformations that each language admits.

This paper is structured as follows. We start by formally
defining the \dagnnf\ language in Section~\ref{sec:languages},
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~\ref{sec:succinctness}
and provide a cross-ranking that compares them according to this
 measure.
%2Pierre: I replaced ``then study'' by ``consider''.
We consider a number of queries and their applications in
Section~\ref{sec:queries} and compare the different target
compilation languages according to their tractability with
respect to these queries. Section~\ref{sec:transformations} 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~\ref{sec:discussion} by some concluding remarks. Proofs
of all theorems are delegated to Appendix~\ref{app:proofs}.
%3Pierre: ``are'' was missing.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The \dagnnf\ Language} \label{sec:languages}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We consider more than a dozen languages in this paper, all of
which are subsets of the \dagnnf\ language, which is defined
formally as follows \cite{darwicheIJCAI99a,darwicheJACM-DNNF}.

\begin{definition}\label{def:dagpl}
Let \ps\ be a denumerable
%3Pierre: I replaced ``finite'' by ``denumerable'', i.e. we have
% as many variables as needed at our disposal.
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 \(\neg X\), \(X \in
\ps\); and each internal node is labeled with \(\wedge\) or
\(\vee\) and can have arbitrarily many children. The size of a
sentence \(\Sigma\) in \(\nnfps\), denoted \(\mid \Sigma \mid\),
is the number of its DAG edges. Its height is the maximum number
of edges from the root to some leaf in the DAG.
\end{definition}

%That is, an interpretation is a model
%of this sentence iff it sets an odd number of variables to false.

%The \dagnnf\ language is a generalization of sentential {\em
%negation normal form \cite{Handbook.Math.Logic},} which
%corresponds to the subset of \dagnnf\ where we have a tree
%structure instead of a DAG structure. The use of a DAG structure
%leads to a more space efficient representation as it allows one
%to represent sub-sentences only once even if they are referenced
%multiple times. Moreover,

Figure~\ref{fig:nnf} depicts a sentence in \dagnnf, which
represents the odd parity function (we omit reference to
variables \ps\ when no confusion is anticipated).
%The omission of negation as a
%possible label for internal nodes does not reduce the space
%efficiency of \nnf.
Any propositional sentence can be represented as a sentence in
\nnf, so the \nnf\ language is {\em complete}.
%Pierre: I've put ``complete'' in \em style.

%6Adnan: I expanded the three paragraphs below
It is important here to distinguish between a {\em representation}
language and a {\em target compilation} language. A representation
language is one which we expect humans to read and write with some
ease. The language of CNF
%6Pierre: I replaced ``Conjunctive Normal Form'' by CNF
%since it has already been used before
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
%6Pierre: I replaced ``need not be suitable'' by ``does not need to
%be suitable''
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.\footnote{It appears that
when proposing target compilation languages in the AI literature,
there is usually an implicit requirement that the proposed
language
%2Pierre: I replaced ``be'' by ``is''.
is also a representation language. As we shall see later, however,
the most powerful target compilation languages are not suitable
for humans to specify or interpret directly.}

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,
%6Pierre: I replaced ``as there is only one consistency test on a
%given theory which does not justify its compilation''
%by ``as only one consistency test on a given theory does not
%justify its compilation''.
as only one consistency test on a given theory does not justify
its compilation. Given this definition, \nnf\ does not qualify as
a target compilation language unless {\sf P}={\sf NP}
\cite{Papadimitriou94},
%\footnote{We assume
%that the reader is familiar with some of the basic notions of
%computational complexity. See \cite{Papadimitriou94} otherwise.}
%Pierre: I've added this footnote.
but many of its subsets do. We define a number of these subsets
below, each of which is obtained by imposing further conditions
on \dagnnf.

We will distinguish between two key subsets of \dagnnf: {\em flat}
and {\em nested} subsets. We first consider flat subsets, which
result from imposing combinations of the following properties:
\begin{itemize}
\item {\bf Flatness:} The height of each sentence is at most 2.
The sentence in Figure~\ref{fig:tt} is flat, but the one in
Figure~\ref{fig:nnf} is not.

\item {\bf Simple-disjunction:} The children of each or-node
are leaves that share no variables (the node is a {\em clause}).

\item {\bf Simple-conjunction:} The children of each and-node
are leaves that share no variables (the node is a {\em term}).
The sentence in Figure~\ref{fig:tt} satisfies this property.
\end{itemize}

\begin{definition}
The language \fnnf\ is the subset of \nnf\ satisfying flatness.
The language \cnf\ is the subset of \fnnf\ satisfying
simple--disjunction. The language \dnf\ is the subset of \fnnf\
satisfying simple--conjunction.
\end{definition}
\cnf\ does not permit a polytime clausal entailment test
(unless {\sf P}={\sf NP}) and,
%6Pierre: I moved ``(unless {\sf P}={\sf NP})''.
hence, does not qualify as a target compilation language. But its
%5Pierre: I switch ``dual'' and \dnf\ as asked by a reviewer.
dual \dnf\ does.
%It is important to
%note here that if a sentence satisfies either simple-conjunction
%or simple-disjunction, it can be easily flattened in polytime.
%\footnote{For example, if we have
%simple-conjunction, then for any path \(n_1,n_2,\ldots,n_r\) in
%the sentence, where \(n_1\) is a leaf and \(n_r\) is the root,
%\(n_3,\ldots,n_r\) must all be or-nodes. Hence, the path can be
%easily collapsed into one of length two.}
%Therefore, in the presence of simple-conjunction or
%simple-disjunction, flatness is not significant computationally.
%Yet, it appears to be a necessary property of representational
%languages such as \cnf\ and \dnf.

The following subset of \cnf, {\em prime implicates,} has been
quite influential in computer science:
\begin{definition}
The language \pi\ is the subset of \cnf\ in which each clause
entailed by the sentence is subsumed by a clause that appears in
the sentence; and no clause in the sentence is subsumed by
another.
\end{definition}
A dual of \pi, {\em prime implicants} \ip, can also be defined.
\begin{definition}
The language \ip\ is the subset of \dnf\ in which each term
entailing the sentence subsumes some term that appears in the
sentence; and no term in the sentence is subsumed by another term.
\end{definition}

\begin{figure*}[tb]
\begin{center}
\mbox{\epsfxsize=55mm \leavevmode \epsffile{decomposability.eps}
\epsfxsize=55mm \leavevmode \epsffile{determinism.eps}
\epsfxsize=55mm \leavevmode \epsffile{smoothness.eps}}
\end{center}
\caption{A sentence in \nnf. Its size is 30 and height is 4.
\label{fig:nnf}}
\end{figure*}

%6Adnan: converted footnotes into text
There has been some work on representing the set of prime
implicates of a propositional theory in a compact way, allowing an
exponential number of prime implicates to be represented in
polynomial space in certain cases---see for example
%4Pierre: I've added a few references there.
the TRIE representation in \cite{deKleer92}, the ZBDD
representation used in \cite{SimondelVal01}, and the implicit
representation based on meta-products, as proposed in
\cite{MadreCoudert92}. These representations are different from
the language \pi\ in the sense that they do not necessarily
support the same queries and transformations that we report in
Tables~\ref{tab:queries} and~\ref{tab:transformations}. They also
exhibit different succinctness relationships than the ones we
report in Table~\ref{tab:succinctness}.

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 {\em complete
%5Pierre: I add a few explanations here, even if the notion of complete
%language is given before
languages} $\L$ only, i.e., we require that every propositional
sentence is logically equivalent to an element of $\L$.

We now consider {\em nested} subsets of the \dagnnf\ 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: {\em decomposability, determinism,
smoothness, decision,} and {\em ordering.} We start by defining
the first three properties. From here on, if \(C\) is a node in an
\nnf, then \(\vars(C)\) denotes
%2Pierre:  I added ``denotes the set of all''.
the set of all variables that label the descendants of node
\(C\). Moreover, if \(\Sigma\) is an \nnf\ sentence rooted at
\(C\), then \(\vars(\Sigma)\) is defined as \(\vars(C)\).
\begin{itemize}
\item {\bf Decomposability} \cite{darwicheIJCAI99a,darwicheJACM-DNNF}.
An \nnf\ satisfies this property if for each conjunction \(C\) in
the \nnf, the conjuncts of \(C\) do not share variables. That is,
if \(C_1, \ldots, C_n\) are the children of and-node \(C\), then
\(\vars(C_i)\cap\vars(C_j)=\emptyset\) for \(i \neq j\). Consider
the and-node marked in Figure~\ref{fig:nnf}(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~\ref{fig:nnf}(a) is also decomposable and,
hence, the \nnf\ in this figure is decomposable.

\item {\bf Determinism} \cite{darwicheJANCL}: An \nnf\ satisfies
this property if for each disjunction \(C\) in the \nnf, each two
disjuncts of \(C\) are logically contradictory. That is, if \(C_1,
\ldots, C_n\) are the children of or-node \(C\), then \(C_i
\wedge C_j \models \false\) for \(i \neq j\). Consider the
or-node marked in Figure~\ref{fig:nnf}(b), which has two children
corresponding to sub-sentences \(\neg A\wedge B\) and \(\neg
B\wedge A\).
%6Pierre: I changed ``These two sub-sentences are logically contradictory.''
%by ``The conjunction of these two sub-sentences is logically contradictory.''
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~\ref{fig:nnf}(b). Hence, the \nnf\ in this figure is
deterministic.

\item {\bf Smoothness} \cite{darwicheJANCL}: An \nnf\ satisfies
this property if for each disjunction \(C\) in the \nnf, each
disjunct of \(C\) mentions the same variables. That is, if \(C_1,
\ldots, C_n\) are the children of or-node \(C\), then
\(\vars(C_i)=\vars(C_j)\) for \(i \neq j\). Consider the marked
or-node in Figure~\ref{fig:nnf}(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~\ref{fig:nnf}(c).
Hence, the \nnf\ in this figure is smooth.
\end{itemize}
%6Adnan: move the footnote into text and expanded on it.
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.
\begin{definition}
The language \Dnnf\ is the subset of \nnf\ satisfying
decomposability; \dnnf\ is the subset satisfying determinism;
\snnf\ is the subset satisfying smoothness; \dDnnf\ is the subset
satisfying decomposability and determinism; and \sdDnnf\ is the
subset satisfying decomposability, determinism and smoothness.
\end{definition}

%The \Dnnf\ language is quite interesting because it results from
%imposing a simple condition on \(\dagnnf\), yet is quite
%tractable as we discuss later.

%\begin{figure}[tb]
%\begin{center}
%\mbox{\epsfxsize=55mm \leavevmode
%\epsffile{c:/adnan/latex/Research_Notes/Pierre/nnf-all.eps}}
%\end{center}
%\caption{A sentence in \nnf. Its size is 30 and height is 4.
%\label{fig:nnf}}
%\end{figure}

%The second important condition we consider is that of {\em
%determinism \cite{darwicheJANCL}:}
%\begin{definition}[Determinism]
%The language \dnnf\ is the subset of \nnf\ satisfying the
%following property: If \(C_1, \ldots, C_n\) are the children of
%an or-node, then \(C_i \wedge C_j \models \false\) for \(i \neq
%j\).
%\end{definition}


%The following subset of \dagnnf\ is especially interesting as we
%shall see later.
%\begin{definition}
%The language \dDnnf\ is the intersection of \Dnnf\ and \dnnf.
%\end{definition}
%That is, sentences in \dDnnf\ are both deterministic and
%decomposable. The third property we consider is {\em smoothness:
%\cite{darwicheJANCL}:}
%\begin{definition}[Smoothness]
%The language \snnf\ is the subset of \nnf\ satisfying the
%following property: If \(C_1, \ldots, C_n\) are the children of
%an or-node, then \(\vars(C_i)=\vars(C_j)\) for \(i \neq j\).
%\end{definition}

%\begin{definition}
%The language \sdDnnf\ is the intersection of \snnf\ and \dDnnf.
%\end{definition}
%That is, sentences in \sdDnnf\ are smooth, deterministic and
%decomposable.

Note that \dnf\ is a strict subset of \Dnnf\
\cite{darwicheIJCAI99a,darwicheJACM-DNNF}. The following {\em
decision} property comes from the literature on {\em binary
decision diagrams} \cite{Bryant86}.

\begin{definition}[Decision]
A decision node \(N\) in an \dagnnf\ sentence is one which is
labeled with \(\true\), \(\false\), or is an or-node having the
form \((X \wedge \alpha) \vee (\neg X \wedge \beta)\),
%\mbox{\epsfxsize=12mm \leavevmode
%\epsffile{c:/adnan/latex/Research_Notes/Pierre/decision.eps}},
where \(X\) is a variable, \(\alpha\) and \(\beta\) are decision
nodes. In the latter case, \(\dvar(N)\) denotes the variable
\(X\).
\end{definition}

\begin{definition}
%5Pierre: I modify the definition (reviewer #3)
%6Adnan: I changed that back as the definition suggested by the reviewer
%is not correct
The language \bdd\ is the set of \nnf\ sentences, where the root
of each sentence is a decision node.
% where each internal node is a decision node.
\end{definition}
%Note that \bdd\ is a subset of \dnnf\ since the decision property
%implies determinism.
The \dagnnf\ sentence in
Figure~\ref{fig:bdd} belongs to the \bdd\ subset.

\begin{figure}[tb]
\begin{center}
\mbox{\epsfxsize=75mm \leavevmode \epsffile{bdd.eps}
\epsfxsize=75mm \leavevmode \epsffile{obdd.eps}}
\end{center}
\caption{On the left, a sentence in the \bdd\ language. On the
right, its corresponding binary decision diagram. \label{fig:bdd}}
\end{figure}

The \bdd\ language corresponds to {\em binary decision diagrams
(BDDs),} as known in the formal verification literature
\cite{Bryant86}. Binary decision diagrams are depicted using a
more compact notation though: the labels \(\true\) and \(\false\)
are denoted by \(1\) and \(0\), respectively; and each decision
node %\((X \wedge \alpha) \vee (\neg X \wedge \beta)\)
\mbox{\epsfxsize=12mm \leavevmode \epsffile{decision.eps}} is
denoted by \mbox{\epsfxsize=10mm \leavevmode
\epsffile{decision2.eps}}. The \bdd\ sentence on the left of
Figure~\ref{fig:bdd} corresponds to the binary decision diagram on
the right of Figure~\ref{fig:bdd}.
%Pierre: I've added the next sentence.
Obviously enough, every \dagnnf\ sentence that satisfies the
decision property is also deterministic. Therefore, \bdd\ is a
subset of \dnnf.

As we show later, \bdd\ does not qualify as a target compilation
language (unless {\sf P}={\sf NP}), but the following subset does.
\begin{definition}
\fbdd\ is the intersection of \Dnnf\ and \bdd.
\end{definition}
That is, each sentence in \fbdd\ is decomposable and satisfies
the decision property. The \fbdd\ language corresponds to {\em
free binary decision diagrams (FBDDs),} as known in formal
verification
\cite{GergovMeinel94}. %MeinelFBDD92
An FBDD is usually defined as a BDD that satisfies the {\em
read-once property:} on each path from the root to a leaf, a
variable can appear at most once. FBDDs are also known as
read-once branching programs in the theory literature. Imposing
the read-once property on a BDD is equivalent to imposing the
decomposability property on its corresponding \bdd\ sentence.

A more influential subset of the \bdd\ language is obtained by
imposing the {\em ordering} property:
\begin{definition}[Ordering]
Let \(<\) be a total ordering on the variables \ps. The language
\obdd\ is the subset of \fbdd\ satisfying the following property:
if \(N\) and \(M\) are or-nodes, and if \(N\) is an ancestor of
node \(M\), then \(\dvar(N) < \dvar(M)\).
\end{definition}

%4Pierre: I've introduced the language \uobdd

\begin{definition}
The language \uobdd\ is the union of all \obdd\ languages.
\end{definition}
The \uobdd\ language corresponds to the well--known {\em ordered
binary decision diagrams (OBDDs)} \cite{Bryant86}.


\begin{figure}[tb]
\begin{center}
\mbox{\epsfxsize=50mm \leavevmode \epsffile{mods.eps}}
\end{center}
\caption{A sentence in language \mods. \label{fig:tt}}
\end{figure}

Our final language definition is as follows:
\begin{definition} \label{def:mods}
\mods\ is the subset of \dnf\ where every sentence satisfies
determinism and smoothness.
\end{definition}
%It follows that \mods\ is also a subset of \dnnf\ and, hence,
%sentences in \mods\ are also deterministic.
Figure~\ref{fig:tt} depicts a sentence in \mods. As we show later,
\mods\ is the most tractable \nnf\ subset we shall consider
(together with \obdd). This is not surprising since from the
syntax of a sentence in \mods, one can immediately recover the
sentence models.

%6Adnan
The languages we have discussed so far are depicted in
Figure~\ref{fig:subsets}, where arrows denote set inclusion.
Table~\ref{tab:languageacronyms} lists the acronyms of all of
these languages, together with their descriptions.
Table~\ref{tab:properties} lists the key language properties
discussed in this section, together with a short description of
each.

\begin{figure}
\begin{center}
\mbox{\epsfxsize=70mm \leavevmode \epsffile{subsets2.eps}}
\end{center}
\caption{The set of DAG-based languages considered in this paper.
An edge \(\L_1 \rightarrow \L_2\) means that \(\L_1\) is a
%5Pierre: I add ``proper'' for reviewer #3
proper subset of \(\L_2\). Next to each subset, we list the
polytime queries supported by the subset but not by any of its
ancestors (see Section~\ref{sec:queries}). \label{fig:subsets}}
%Pierre: there is an ambiguity here: does ``not by its ancestors''
%mean ``by at least one of them'' or ``by all of them''.
%Moreover, CNF already satisfies VA and IM.
\end{figure}

\begin{table}
\begin{center}
\begin{small}
\begin{tabular}{|c|c|}\hline
{\bf Acronym} & {\bf Description} \\
\hline \hline
{\nnf} & Negation Normal Form \\
\hline
\Dnnf & Decomposable Negation Normal Form \\
\hline
\dnnf & Deterministic Negation Normal Form \\
\hline
\snnf & Smooth Negation Normal Form \\
\hline
\fnnf & Flat Negation Normal Form \\
\hline
\dDnnf & Deterministic Decomposable Negation Normal Form \\
\hline
\sdDnnf & Smooth Deterministic Decomposable Negation Normal Form \\
\hline
\bdd & Binary Decision Diagram \\
\hline
\fbdd & Free Binary Decision Diagram \\
\hline
\uobdd & Ordered Binary Decision Diagram \\
\hline
\obdd & Ordered Binary Decision Diagram (using order \(<\)) \\
\hline
\dnf & Disjunctive Normal Form \\
\hline
\cnf & Conjunctive Normal Form \\
\hline
\pi & Prime Implicates \\
\hline
\ip & Prime Implicants \\
\hline
\mods & Models \\
 \hline
\end{tabular}
\end{small}
\caption{Language acronyms. \label{tab:languageacronyms}}
\vspace{10mm}
\begin{small}
\begin{tabular}{|c|c|}\hline
{\bf Property} & {\bf Short Description} \\
\hline \hline
{ Flatness} & The height of NNF is at most \(2\) \\
\hline
{ Simple Disjunction} & Every disjunction is a clause, where literals share no variables  \\
\hline
{ Simple Conjunction} & Every conjunction is a
%6Pierre: I replaced ``instantiation'' by ``term''.
term, where literals share no variables \\
\hline
{ Decomposability} & Conjuncts do not share variables \\
\hline
{ Determinism} & Disjuncts are logically disjoint \\
\hline
{ Smoothness} & Disjuncts mention the same set of variables \\
\hline { Decision} & A node of the form \(\true\), \(\false\), or
\((X\wedge\alpha \vee \neg X\wedge \beta)\), \\
         & where \(X\) is a variable and \(\alpha,\beta\) are decision nodes \\
\hline
{ Ordering} & Decision variables appear in the same order on any path in the NNF \\
\hline
\end{tabular}
\end{small}
\caption{Language properties. \label{tab:properties}}
\end{center}
\end{table}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{On the Succinctness of Compiled Theories} \label{sec:succinctness}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We have discussed more than a dozen subsets of the \dagnnf\
language. Some of these subsets are well known and have been
studied extensively in the computer science literature. Others,
such as \Dnnf\ \cite{darwicheJACM-DNNF,darwicheIJCAI99a} and
\dDnnf\ \cite{darwicheJANCL}, are relatively new. The question now
is: What subset should one adopt for a particular application? As
we argue in this paper, that depends on three key properties of
the language: its succinctness, the class of tractable queries it
supports, and the class of tractable transformations it admits.
%Specifically, each application will require a set of queries and
%transformations, so one needs to adopt the most succinct language
%that supports the needed queries and transformations.

Our goal in this and the following sections is to construct a map
on which we place different subsets of the \dagnnf\ language
according to the above criteria. This map will then serve as a
guide to system designers in choosing the target compilation
language most suitable to their application. It also provides an
example paradigm for studying and evaluating further target
compilation languages. We start with a study of
succinctness\footnote{A more general notion of space efficiency
(model preservation for polysize reductions) exists
\cite{Cadolietal96b}, but we do not need its full generality
here.}
%Pierre: I've put back the footnote.
in this section \cite{Gogicetal95}.

\begin{definition}[Succinctness] \label{def:succinctness}
Let \(\L_1\) and \(\L_2\) be two subsets of \dagnnf. \(\L_1\) is
at least as succinct as \(\L_2\), denoted \(\L_1 \leq \L_2\), iff
there exists a polynomial \(p\) such that for every sentence
\(\alpha \in \L_2\), there exists an equivalent sentence \(\beta
\in \L_1\) where \(|\beta| \leq p(|\alpha|)\). Here, \(|\alpha|\)
and \(|\beta|\) are the sizes of \(\alpha\) and \(\beta\),
respectively.
%Pierre: I've added ``a polysize'' in the footnote above.
\end{definition}
%6Adnan: moved footnote into text
We stress here that we do not require that there exists a function
that computes $\beta$ given $\alpha$ in {\em polytime}; we only
require that a {\em polysize} $\beta$ exists. Yet, our proofs in
Appendix~\ref{app:proofs} contain specific algorithms for
computing \(\beta\) from \(\alpha\) in certain cases. The relation
$\leq$ is clearly reflexive and transitive, hence, a pre-ordering.
One can also define the relation \(<\), where \(\L_1 < \L_2\) iff
\(\L_1 \leq \L_2\) and \(\L_2 \not \leq \L_1\).

\begin{proposition}\label{prop:succinctness}
The results in Table~\ref{tab:succinctness} hold.
\end{proposition}


%5Pierre: I add a few explanations about how the table should
%be read.
%6Adnan: rephrased the paragraph a bit

An occurrence of $\leq$ in the cell of row $r$ and column $c$ of
Table~\ref{tab:succinctness} means that the fragment \(\L_r\)
given at row $r$ is at least as succinct as the fragment \(\L_c\)
given at column $c$. An occurrence of $\not \leq$ (or $\not
\leq^*$) means that \(\L_r\) is not at least as succinct as
\(\L_c\) (provided that the polynomial hierarchy does not collapse
in the case of $\not \leq^*$). Finally, the presence of a question
mark reflects our ignorance about whether \(\L_r\) is at least as
succinct as \(\L_c\). Figure~\ref{fig:succinctness} summarizes the
results of Proposition~\ref{prop:succinctness} in terms of a
directed acyclic graph.

%Pierre: I've made some changes here, as required.
A classical result in knowledge compilation states that it is not
possible to compile any propositional formula \(\alpha\) into a
polysize data structure \(\beta\) such that: \(\alpha\) and
\(\beta\) entail the same set of clauses, and clausal entailment
on \(\beta\) can be decided in time polynomial in its size, unless
{\sf NP} $\subseteq$ {\sf P/poly}
\cite{SelmanKautz96,CadoliDonini97}. This last assumption
%2Pierre: I move ``which is considered very unlikely''.
implies the collapse of the polynomial
hierarchy at the second level \cite{KarpLipton80}, which is
considered very unlikely. We use this
classical result from knowledge compilation in some of our proofs
of Proposition~\ref{prop:succinctness}, which explains why some of
its parts are conditioned on the polynomial hierarchy not
collapsing.

%\begin{proposition}\label{prop:succinctness}
%If \(\leq\) appears in cell \((\L_1,\L_2)\) of
%Table~\ref{tab:succinctness}, then language \(\L_1\) is at least
%as succinct as language \(\L_2\), \(\L_1 \leq \L_2\). If \(\not
%\leq\) appears in the cell, then \(\L_1\) is not at least as
%succinct as \(\L_2\), \(\L_1 \not \leq \L_2\). A \nasc\ means
%that the result holds unless the polynomial hierarchy collapses.
%A \unk\ means that the relationship is not known.
%\end{proposition}

%4Pierre: I've updated the table with \uobdd
\begin{table*}[tb]
\begin{small}
\begin{center}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|c|} \hline
\(\L\) & \dagnnf\ & \Dnnf\ & \dDnnf\ & \sdDnnf\ & \fbdd\ & \uobdd\ &\obdd\ & \dnf\ & \cnf\ & \pi\ & \ip\ & \mods \\
\hline \hline
\dagnnf\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ \\
\hline
\Dnnf\ & \nasc\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \nasc\ & \unk & \as\ & \as\ \\
\hline
\dDnnf\ & \nasc\ & \nasc\ & \as\ & \as\ & \as\ & \as\ & \as\ & \nasc\ & \nasc\ & \unk & \unk & \as\ \\
\hline
\sdDnnf\ & \nasc\ & \nasc\ & \as\ & \as\ & \as\ & \as\ & \as\ & \nasc\ & \nasc\ & \unk & \unk & \as\ \\
\hline
\fbdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \as\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ \\
\hline
\uobdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ \\
\hline
\obdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ \\
\hline
\dnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \nas\ & \as\ & \as\ \\
\hline
\cnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ & \as\ \\
\hline
\pi\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \unk \\
\hline
\ip\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ \\
\hline
\mods\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ \\
\hline
\end{tabular}
\caption{Succinctness of target compilation languages. \(*\) means
that the result holds unless the polynomial hierarchy collapses.
%One can define \uobdd\ as the union of \obdd\ for all possible orderings \(<\).
%The succinctness results continue to hold if
%\obdd\ is replaced with \uobdd.
\label{tab:succinctness}}
\end{center}
\end{small}
\end{table*}

\begin{figure}[tb]
\begin{center}
\mbox{\epsfxsize=70mm \leavevmode \epsffile{succinctness2.eps}}
\caption{An edge \(\L_1 \rightarrow \L_2\) indicates that \(\L_1\)
is strictly more succinct than \(\L_2\):
%Pierre: I've added ``strictly''
\(\L_1 < \L_2\), while \(\L_1 = \L_2\) indicates that \(\L_1\) and
\(\L_2\) are equally succinct: \(\L_1 \leq \L_2\) and \(\L_2 \leq
%5Pierre: I add more explanations here
\L_1\). Dotted arrows indicate unknown relationships; for instance,
the dotted arrow from \Dnnf\ to \pi\ means that we do not know whether
\Dnnf\ is at least as succinct as \pi.
%Pierre: there is an ambiguity here (like in Figure 3).
%Moreover, CNF already satisfies VA and IM.
Some of the edges are conditioned on the polynomial hierarchy not
collapsing---see Table~\ref{tab:succinctness}.
\label{fig:succinctness}}
\end{center}
\end{figure}

We have excluded the subsets \bdd, \snnf, \dnnf\ and \fnnf\ from
Table~\ref{tab:succinctness} since they do not qualify as target
compilation languages (see Section~\ref{sec:queries}). We kept
\nnf\ and \cnf\ though given their importance. Consider
Figure~\ref{fig:succinctness} which depicts
Table~\ref{tab:succinctness} graphically. With the exception of
\dagnnf\ and \cnf, all other languages depicted in
Figure~\ref{fig:succinctness} qualify as target compilation
languages. Moreover, with the exception of language \pi, \Dnnf\
is the most succinct among all target compilation languages---we
know that \pi\ is not more succinct than \Dnnf, but we do not
know whether \Dnnf\ is more succinct than \pi.

In between \Dnnf\ and \mods, there is a succinctness
%2Pierre: I replaced ``hierarchy'' by ``ordering''
ordering of target compilation languages:
%4Pierre
\[ \mbox{\Dnnf} <\:\:\:\: \mbox{\dDnnf} <\:\:\:\:
\mbox{\fbdd} <\:\:\:\: \mbox{\uobdd} <\:\:\:\: \mbox{\obdd} \:\:\:\: < \:\: \mbox{\mods}.
\] \Dnnf\ is obtained by imposing decomposability on \dagnnf;
\dDnnf\ by adding determinism; \fbdd\ by adding decision; and
\uobdd\ and \obdd\ by adding ordering (w.r.t. any total ordering
on \ps\ in the first case and a specific one in the second case).
{\em Adding each of these properties reduces language succinctness
(assuming that the polynomial hierarchy does not collapse).}

One important fact to stress here is that adding smoothness to
\dDnnf\ does not affect its succinctness: the \sdDnnf\ and
\dDnnf\ languages are equally succinct. It is also interesting to
compare \sdDnnf\ (which is more succinct than the influential
%4Pierre
\fbdd, \uobdd\ and \obdd\ languages) with \mods, which is a most
tractable language. Both \sdDnnf\ and \mods\ are smooth,
deterministic and decomposable. \mods, however, is flat and
obtains its decomposability from the stronger condition of
simple-conjunction. Therefore, \sdDnnf\ can be viewed as the
result of relaxing from \mods\ the flatness and simple-conjunction
conditions, while maintaining decomposability, determinism and
smoothness. Relaxing these conditions moves the language three
levels up the succinctness hierarchy, although it compromises only
the polytime test for sentential entailment and possibly the one
for equivalence as we show in Section~\ref{sec:queries}.
%Pierre: in order to render things more easy to grasp, I think we
%shoud put a sd-DNNF entry in Tables 2 and 3. I'm going to do it.

%There are a few undetermined relationships between the considered
%languages.
%Specifically, we know that \mods\ is not more
%succinct than \pi, but the opposite is not known. Moreover, we
%know that \pi\ is not more succinct than either \Dnnf\ or \dDnnf,
%but it is not known whether either of \Dnnf\ or \dDnnf\ are more
%succinct than \pi. Finally, we know that \ip\ is not more
%succinct than either \dDnnf\ or \sdDnnf, but it is not known
%whether \dDnnf\ or \sdDnnf\ are more succinct than \ip.
%Once
%these relationships are determined, we will have a complete
%succinctness map for the considered languages.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Querying a Compiled Theory} \label{sec:queries}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

In evaluating the suitability of a target compilation language to
a particular application, the succinctness of the language must be
balanced against the set of queries and transformations that it
supports in polytime. We consider in this section a number of
queries, each of which returns valuable information about a
propositional theory, and then identify target compilation
languages which provide polytime algorithms for answering such
queries. We restrict our attention in this paper to the {\em
existence} of polytime algorithms for answering queries, but we do
not present the algorithms themselves. The interested reader is
referred to
\cite{darwicheJACM-DNNF,darwicheJANCL,darwicheIJCAI99a,Bryant86}
for some of these algorithms and to the proofs of theorems in
Appendix~\ref{app:proofs} for others.
%Some of these queries are especially useful when
%combined with transformations, which we consider in the following
%section.

The queries we consider are tests for consistency, validity,
implicates (clausal entailment), implicants, equivalence, and
sentential entailment. We also consider counting and enumerating
theory models; see Table~\ref{tab:notationqueries}. One can also
consider computing the probability of a propositional sentence,
assuming that all variables are probabilistically independent. For
the subsets we consider, however, this can be done in polytime
whenever models can be counted in polytime.

From here on, \L\ denotes a subset of language \nnf.
\begin{definition}[\co, \va]
\L\ satisfies \co\ (\va) iff there exists a polytime algorithm
that maps every formula $\Sigma$ from \L\ to $1$ if $\Sigma$ is
consistent (valid), and to $0$ otherwise.
\end{definition}
%These tests are not too useful by themselves in a compilation
%context unless combined with transformations as we discuss in the
%next section . For example, if all we want is to test the
%consistency of a propositional theory \(\Delta\), then it may be
%more efficient to simply apply a SAT solver to
%\(\Delta\)---instead of compiling \(\Delta\) and then testing the
%consistency of its compilation. Compiling a theory is advisable
%in two key situations:
%\begin{enumerate}
%\item If we expect to pose a large number of queries to the original
%theory---for example, a large number of clausal entailment
%tests--in which case the compilation cost can be amortized over
%all queries.
%\item If the queries of interests cannot be answered efficiently enough
%using direct techniques. For example, compiling a theory and then
%applying a polytime counting algorithm to the compilation may be
%the best way for counting the models of the original theory.
%\end{enumerate}

One of the main applications of compiling a theory is to enhance
the efficiency of answering clausal entailment queries:
\begin{definition}[\ce]
%Let \L\ be a subset of \nnf.
\L\ satisfies \ce\ iff there exists a
polytime algorithm that maps every formula $\Sigma$ from \L\ and
every clause $\gamma$ from \nnf\ to $1$ if $\Sigma \models
\gamma$ holds, and to $0$ otherwise.
\end{definition}
%If a target compilation language supports a polytime clausal
%entailment test, then it can support a class of {\em dynamic}
%consistency tests. Suppose for example we have a propositional
%theory \(\Delta\) which models the normal behavior of a certain
%device. Suppose further that we are collecting observations about
%the behavior of this device and wish to ask whether an observed
%behavior \(\alpha\) is consistent with the device model
%\(\Delta\). If the observation \(\alpha\) is a term, which is
%typically the case, then its negation \(\neg \alpha\) is a
%clause. In this case, the behavior \(\alpha\) is normal
%(consistent with the device model) iff \(\Delta \not \models \neg
%\alpha\). Hence, it makes sense to compile the device model
%\(\Delta\) into some target language \(\Gamma\) and then answer
%\(\Gamma \not \models \neg \alpha\) queries using a polytime test.

A key application of clausal entailment is in testing equivalence.
Specifically, suppose we have a design expressed as a set of
clauses \(\Delta^d=\bigwedge_i \alpha_i\) and a specification
expressed also as a set of clauses \(\Delta^s = \bigwedge_j
\beta_j\), and we want to test whether the design and
specification are equivalent.
%Pierre: I've changed $^c$ by $^d$ everywhere in the rest of the paragraph.
By compiling each of \(\Delta^d\)
and \(\Delta^s\) to targets \(\Gamma^d\) and \(\Gamma^s\) that
support a polytime clausal entailment test, we can test the
equivalence of \(\Delta^d\) and \(\Delta^s\) in polytime. That
is, \(\Delta^d\) and \(\Delta^s\) are equivalent iff \(\Gamma^d
\models \beta_j\) for all \(j\) and \(\Gamma^s \models \alpha_i\)
for all \(i\).

% equivalence
A number of the target compilation languages we shall consider
support a direct polytime equivalent test:
\begin{definition}[\eq, \se]
%Let \L\ be a subset of \nnf.
\L\ satisfies \eq\ (\se) iff there
exists a polytime algorithm that maps every pair of formulas
$\Sigma$, $\Phi$ from \L\ to $1$ if $\Sigma \equiv \Phi$ (\(\Sigma
\models \Phi\)) holds, and to $0$ otherwise.
\end{definition}
Note that sentential entailment (\se) is stronger than clausal
entailment and equivalence. Therefore, if a language \L\ satisfies
\se, it also satisfies \ce\ and \eq.

% implicant
For completeness, we consider the following dual to \ce:
\begin{definition}[\im]
%Let \L\ be a subset of \nnf.
\L\ satisfies \im\ iff there exists a
polytime algorithm that maps every formula $\Sigma$ from \L\ and
every term $\gamma$ from \nnf\ to $1$ if $\gamma \models \Sigma$
holds, and to $0$ otherwise.
\end{definition}


% counting models
Finally, we consider counting and enumerating models:
\begin{definition}[\ct]
%Let \L\ be a subset of \nnf.
\L\ satisfies \ct\ iff there exists a
polytime algorithm that maps every formula \(\Sigma\) from \L\ to
a nonnegative integer that represents the number of models of
\(\Sigma\) (in binary notation).
\end{definition}

\begin{definition}[\me]
%Let \F\ be a subset of \nnf.
\L\ satisfies \me\ iff there exists a polynomial \(p(.,.)\) and
an algorithm that outputs all models of an arbitrary formula
$\Sigma$ from \L\ in time \(p(n,m)\), where \(n\) is the size of
\(\Sigma\) and \(m\) is the number of its models (over variables
occurring in \(\Sigma\)).
\end{definition}


%5Pierre: an additional table

Table~\ref{tab:notationqueries} summarizes the queries we are
interested in and their acronyms.

\begin{table}[tb]
\begin{center}
\begin{tabular}{|c|c|}\hline
{\bf Notation} & {\bf Query} \\
\hline \hline
\co & polytime consistency check\\
\hline
\va & polytime validity check\\
\hline
\ce & polytime clausal entailment check\\
\hline
\im & polytime implicant check\\
\hline
\eq & polytime equivalence check\\
\hline
\se & polytime sentential entailment check\\
\hline
\ct & polytime model counting\\
\hline
\me & polytime model enumeration\\
\hline
\end{tabular}
\caption{Notations for queries. \label{tab:notationqueries}}
\end{center}
\end{table}

%5Pierre: I add this paragraph again as a matter or transition

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~\ref{sec:languages}.

\begin{proposition}\label{prop:queries}
The results in Table~\ref{tab:queries} hold.
\end{proposition}

%\begin{proposition}\label{prop:queries}
%If \y\ appears in cell \((\L,\Q)\) of Table~\ref{tab:queries},
%then language \(\L\) satisfies \(\Q\). If \n\ appears in the
%cell, then \(\L\) does not satisfy \(\Q\) unless \(\sf P = NP\).
%\end{proposition}

%4Pierre: I've updated the table with \uobdd

\begin{table}[tb]
\begin{small}
\begin{center}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \se\ & \ct\ & \me \\
\hline \hline
\nnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\Dnnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\dnnf\ & \n  & \n & \n & \n & \n & \n & \n & \n \\
\hline
\snnf\ & \n  & \n & \n & \n & \n & \n& \n & \n \\
\hline
\fnnf\ & \n  & \n & \n & \n & \n & \n & \n & \n \\
\hline
\dDnnf\ & \y & \y & \y & \y & \unk & \n & \y & \y \\
\hline
%Pierre: I've added \sdDNNF back.
\sdDnnf\ & \y & \y & \y & \y & \unk & \n & \y & \y \\
\hline
\bdd\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\fbdd\ & \y & \y & \y & \y & \unk & \n & \y & \y \\
\hline
\uobdd\ & \y & \y & \y & \y & \y & \n & \y & \y \\
\hline
\obdd\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\dnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\cnf\ & \n & \y & \n & \y & \n & \n & \n & \n \\
\hline
\pi\ & \y & \y & \y & \y & \y & \y & \n & \y \\
\hline
\ip\ & \y & \y & \y & \y & \y & \y & \n & \y \\
\hline
\mods\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\end{tabular}
\caption{Subsets of the \dagnnf\ language and their corresponding
polytime queries. \y\ means ``satisfies'' and \n\ means ``does
not satisfy unless {\sf P = NP.}'' \label{tab:queries}}
\end{center}
\end{small}
\end{table}

%\begin{figure}[tb]
%\begin{center}
%\mbox{\epsfxsize=65mm \leavevmode
%\epsffile{c:/adnan/latex/Research_Notes/Pierre/queries.eps}}
%\caption{An edge \(\L_1 \rightarrow \L_2\) indicates that the
%polytime queries of \(\L_1\) are a superset of those for \(\L_2\)
%(with the difference shown over the edge). An edge \(\L_1
%\leftrightarrow \L_2\) indicates that \(\L_1\) and \(\L_2\)
%support the same set of queries. \label{fig:queries}}
%\end{center}
%\end{figure}

The results of Proposition~\ref{prop:queries} are summarized in
%2Pierre: I replaced ``Figures'' by ``Figure''.
Figure~\ref{fig:subsets}. One can draw a number of conclusions
based on the results in this figure.
%Pierre: I've made a slight change in the next sentence.
First, \nnf, \snnf, \dnnf, \fnnf, 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
%\Dnnf, \dDnnf, \sdDnnf, \fbdd, \obdd, \dnf, \pi, \ip, and \mods\
all support polytime tests for consistency and clausal entailment.
Therefore, simply imposing either of smoothness (\snnf),
determinism (\dnnf), flatness (\fnnf), 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.

%Pierre: I've replaced ``hierarchy'' by ``ordering'' here.
Recall the succinctness ordering \Dnnf\ \(\:\:<\:\:\) \dDnnf\
%4Pierre
\(\:\:<\:\:\) \fbdd\ \(\:\:<\:\:\) \uobdd\ \(\:\:<\:\:\) \obdd\
\(\:\:<\:\:\) \mods\ from Figure~\ref{fig:succinctness}. 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
(\dDnnf), 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 queries\footnote{Deciding the equivalence of
two sentences in \fbdd, \dDnnf, or in \sdDnnf, can be easily shown
to be in {\sf coNP}. However, we do not have a proof of {\sf
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 \cite{Blumetal80}, and
similarly for sentences in \dDnnf\ \cite{darwicheD123}.},
%Pierre: I've put back some part of the footnote.
%but the authors declare membership to {\sf NP} as an open problem.},
although it does lead to reducing language succinctness as shown
in Figure~\ref{fig:succinctness}. On the other hand, adding the
ordering property on top of decomposability, determinism and
decision, leads to polytime tests for equivalence (\uobdd\ and \obdd)
%4Pierre
as well as sentential entailment provided that the ordering $<$
is fixed (\obdd).

%Pierre: I've made some changes here.
As for the succinctness ordering \nnf\ \(\:\:<\:\:\) \Dnnf\
\(\:\:<\:\:\) \dnf\ \(\:\:<\:\:\) \ip\ \(\:\:<\:\:\) \mods\ from
Figure~\ref{fig:succinctness}, 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~\ref{fig:subsets}. 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.\footnote{Given flatness, simple-conjunction and
smoothness, we can obtain determinism by simply removing
duplicated terms.}

We close this section by noting that determinism appears to be
necessary (but not sufficient) for polytime model counting: only
%4Pierre
deterministic languages, \dDnnf, \sdDnnf, \fbdd, \uobdd, \obdd\ and \mods,
support polytime counting. Moreover, polytime counting implies a
polytime test of validity, but the opposite is not true.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Transforming a Compiled Theory} \label{sec:transformations}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

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.

%We consider in this section seven different transformations on
%sentences:

% and closure

\begin{definition}[\(\ac,\oc\)]
Let \L\ be a subset of \nnf. \L\ satisfies \(\ac\) (\(\oc\)) iff
there exists a polytime algorithm that maps every finite set of
formulas $\Sigma_1, \dots, \Sigma_n$ from \L\ to a formula of \L\
that
%5Pierre: I replace ``represents'' by ``is logically equivalent to''
is logically equivalent to $\Sigma_1 \wedge \dots \wedge \Sigma_n$ ($\Sigma_1
\vee \dots \vee \Sigma_n$).
\end{definition}

% not closure

\begin{definition}[\(\nc\)]
Let \L\ be a subset of \nnf. \L\ satisfies {\bf $\neg$C} iff there
exists a polytime algorithm that maps every formula $\Sigma$ from
\L\ to a formula of \L\ that
%5Pierre: I replace ``represents'' by ``is logically equivalent to''
is logically equivalent to $\neg \Sigma$.
\end{definition}

If a language satisfies one of the above properties, we will say
that it is {\em 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 \(\Delta \models \Gamma\), all we have to do, by
the Refutation Theorem, is test whether \(\Delta \wedge \neg
\Gamma\) is inconsistent). Similarly, if a language satisfies
\va\ and is closed under negation and disjunction, it must
satisfy \se\ by the Deduction Theorem.

It is important to stress here that some languages are closed
under a logical operator, only if the number of operands is
bounded by a constant. We will refer to this as
%6Pierre: I replaced ``bounded-closure'' by ``bounded closure''.
{\em bounded closure.}
%Pierre: I've removed the next two sentences because I'm not sure
%to understand them.
%This distinction is
%important since bounded-closure is all we need to support
%polytime queries. It can also be significant for compiling
%propositional theories.

% bounded and closure
\begin{definition}[\(\bac, \boc\)]
Let \L\ be a subset of \nnf. \L\ satisfies \(\bac\) (\(\boc\)) iff
there exists a polytime algorithm that maps every pair of formulas
\(\Sigma\) and \(\Phi\) from \L\ to a formula of \L\ that
%5Pierre: I replace ``represents'' by ``is logically equivalent to''
is logically equivalent to $\Sigma \wedge \Phi$ (\(\Sigma \vee \Phi\)).
\end{definition}

We now turn to another important transformation:
% conditioning

\begin{definition}[Conditioning] \cite{darwicheIJCAI99a}
Let $\Sigma$ be a propositional formula, and let $\gamma$ be a
consistent term. The conditioning of $\Sigma$ on $\gamma$, noted
$\Sigma \mid \gamma$, is the formula obtained by replacing each
variable $X$ of $\Sigma$ by \true\ (resp. \false) if $X$ (resp.
$\neg X$) is a positive (resp. negative) literal of $\gamma$.
\end{definition}

\begin{definition}[\cd]
Let \L\ be a subset of \nnf. \L\ satisfies \cd\ iff there exists a
polytime algorithm that maps every formula $\Sigma$ from \L\ and
every consistent term $\gamma$ to a formula from \L\ that
%5Pierre: I replace ``represents'' by ``is logically equivalent to''
is logically equivalent to $\Sigma \mid \gamma$.
\end{definition}

Conditioning has a number of applications, and corresponds to {\em
restriction} in the literature on Boolean functions. The main
application of conditioning is due to a theorem, which says that
\(\Sigma \wedge \gamma\) is consistent iff \(\Sigma \mid \gamma\)
is consistent \cite{darwicheJACM-DNNF,darwicheIJCAI99a}.
Therefore, if a language satisfies \co\ and \cd, then it must also
satisfy \ce. Conditioning also plays a key role in building
compilers that enforce decomposability. If two sentences
\(\Delta_1\) and \(\Delta_2\) are both decomposable (belong to
\Dnnf), their conjunction \(\Delta_1 \wedge \Delta_2\) is not
necessarily decomposable since the sentences may share variables.
Conditioning can be used to ensure decomposability in this case
since \(\Delta_1\wedge\Delta_2\) is equivalent to \(\bigvee_\gamma
(\Delta_1\mid\gamma)\wedge(\Delta_2\mid\gamma)\wedge\gamma\),
where \(\gamma\) is a term covering all variables shared by
\(\Delta_1\) and \(\Delta_2\). Note that \(\bigvee_\gamma
(\Delta_1\mid\gamma)\wedge(\Delta_2\mid\gamma)\wedge\gamma\) must
be decomposable since \(\Delta_1\mid\gamma\) and
\(\Delta_2\mid\gamma\) do not mention variables in \(\gamma\). The
previous proposition is indeed a generalization to multiple
variables of the well-known Shannon expansion in the literature on
Boolean functions. It is also the basis for compiling \cnf\ into
\Dnnf\ \cite{darwicheIJCAI99a,darwicheJACM-DNNF}.

Another critical transformation we shall consider is that of
%5Pierre: I add the reference to Boole there
{\em forgetting} (also referred to as marginalization, or
elimination of middle terms \cite{Boole54}):

\begin{definition}[Forgetting]
Let $\Sigma$ be a propositional formula, and let \(\X\) be a
subset of variables from \ps. The {\em forgetting} of \(\X\) from
$\Sigma$, denoted \(\exists \X . \Sigma\), is a formula that does
not mention
%2Pierre: I changed a bit here.
any variable from \X\ and for every formula \(\alpha\) that
does not mention any variable from \X, we have \(\Sigma \models \alpha\) precisely
when \(\exists \X . \Sigma \models \alpha\).
\end{definition}
Therefore, to forget variables from \X\ is to remove any reference to
\X\ from \(\Sigma\), while maintaining all information that
\(\Sigma\) captures about the complement of \X. Note that
\(\exists \X . \Sigma\) is unique up to logical equivalence.

%Pierre: I've added \sfo in the title of the definition.
% And changed ``equivalence'' by ``equivalent''.
\begin{definition}[\fo, \sfo]
Let \L\ be a subset of \nnf. \L\ satisfies \fo\ iff there exists a
polytime algorithm that maps every formula $\Sigma$ from \L\ and
every subset \(\X\) of variables from \ps\ to a formula from \L\
equivalent to \(\exists \X . \Sigma\). If the property holds for
singleton \X, we say that \L\ satisfies \(\sfo\).
\end{definition}

Forgetting is an important transformation as it allows us to
focus/project a theory on a set of variables. For example, if we
know that some variables \(\X\) will never appear in entailment
queries, we can forget these variables from the compiled theory
while maintaining its ability to answer such queries correctly.
Another application of forgetting is in counting/enumerating the
instantiations of some variables \Y, which are consistent with a
theory \(\Delta\). This query can be answered by
counting/enumerating the models of \(\exists \X . \Delta\), where
\X\ is the complement of \Y. Forgetting also has applications to
planning, diagnosis and belief revision. For instance, in the
SATPLAN framework, compiling away fluents or actions amounts to
forgetting variables. In model-based diagnosis, compiling away
every variable except the abnormality ones does not remove any
piece of information required to compute the conflicts and the
diagnoses of a system \cite{darwicheJACM-DNNF}. Forgetting has
also been used to design update operators with valuable properties
\cite{HerzigRifi99}.


\begin{table}[tb]
\begin{center}
\begin{tabular}{|c|c|}\hline
{\bf Notation} & {\bf Transformation} \\
\hline \hline
\cd & polytime conditioning\\
\hline
\fo & polytime forgetting\\
\hline
\sfo & polytime singleton forgetting\\
\hline
\(\ac\) & polytime conjunction\\
\hline
\(\bac\) & polytime bounded conjunction\\
\hline
\(\oc\) & polytime disjunction\\
\hline
\(\boc\) & polytime bounded disjunction\\
\hline
\(\nc\) & polytime negation\\
\hline
\end{tabular}
\caption{Notations for transformations.
\label{tab:notationtransformations}}
\end{center}
\end{table}



%5Pierre: an additional table

Table~\ref{tab:notationtransformations} summarizes the
transformations we are interested in and their acronyms. The
following proposition states what we know about the tractability
of these transformations with respect to the identified target
compilation languages.

%5Pierre: I add a sentence as a matter of transition


\begin{proposition}\label{prop:transformations}
The results in Table~\ref{tab:transformations} hold.
\end{proposition}

%\begin{proposition}\label{prop:transformations}
%If \y\ appears in cell \((\L,\T)\) of
%Table~\ref{tab:transformations}, then language \L\ satisfies
%transformation \T. If \bn\ appears in the cell, then \L\ does not
%satisfy \T. If \n\ appears instead, then \L\ does not satisfy \T\
%unless \({\sf P = NP}\).
%\end{proposition}

%4Pierre: I've updated the table with \uobdd and put results for \dnnf
\begin{table}[tb]
\begin{small}
\begin{center}
\begin{tabular}{|c|c||c|c||c|c||c|c||c|}\hline
\L\ & \cd\ & \fo\ & \sfo\ & \(\ac\) & \(\bac\) & \(\oc\) & \(\boc\) & \(\nc\) \\
\hline \hline
\nnf\ & \y & \n & \y\ & \y & \y & \y & \y & \y \\
\hline
\Dnnf\ & \y & \y & \y\ & \n & \n & \y & \y & \n \\
\hline
\dnnf\ & \y & \n & \y & \y & \y & \y & \y & \y \\
\hline
\snnf\ & \y & \n & \y\ & \y & \y & \y & \y & \y \\
\hline
\fnnf\ & \y & \n & \y & \bn & \bn & \bn & \bn & \y \\
%3Pierre: I replaced two \y by two \bn
\hline
\dDnnf\ & \y & \n & \n & \n & \n  & \n & \n & \unk \\
\hline
%Pierre: I've added \sdDNNF back.
\sdDnnf\ & \y & \n & \n & \n & \n  & \n & \n & \unk \\
\hline
\bdd\ & \y & \n & \y & \y & \y & \y & \y & \y \\
\hline
\fbdd\ & \y & \bn & \n & \bn & \n & \bn & \n & \y \\
\hline
\uobdd\ & \y & \bn & \y & \bn & \n & \bn & \n & \y \\
\hline
\obdd\ & \y & \bn & \y & \bn & \y & \bn & \y & \y \\
\hline
\dnf\ & \y & \y & \y & \bn & \y & \y & \y & \bn \\
\hline
\cnf\ & \y & \n & \y & \y & \y & \bn & \y & \bn \\
\hline
\pi\ & \y & \y & \y & \bn & \bn & \bn & \y & \bn \\
\hline
\ip\ & \y & \bn & \bn & \bn & \y & \bn & \bn & \bn \\
\hline
\mods\ & \y & \y & \y & \bn & \y & \bn & \bn & \bn \\
\hline
\end{tabular}
\caption{Subsets of the \nnf\ language and their polytime
transformations. \y\ means ``satisfies,'' \bn\ means ``does not
satisfy,'' while \n\ means ``does not satisfy unless {\sf P=NP.}''
\label{tab:transformations}}
\end{center}
\end{small}
\end{table}
%3Pierre: I replaced the white dot for (IP, SFO) by a black one.

One can draw a number
%2Pierre: I added ``of''
of observations regarding
Table~\ref{tab:transformations}. First, all languages we consider
satisfy \cd\ and, hence, lend themselves to efficient application
of the conditioning transformation. As for forgetting multiple
variables, only \Dnnf, \dnf, \pi\ and \mods\ permit that in
%4Pierre
polytime. It is important to stress here that none of \fbdd, \uobdd\ and
\obdd\ permits polytime forgetting of multiple variables. This is
%2Pierre: I replaced ``important'' by ``noticeable''.
noticeable since some of the recent applications of \obdd\ to
planning---within the so-called symbolic model checking approach
to planning \cite{Cimattietal97}---depend crucially on the
operation of forgetting and it may be more suitable to use a
language that satisfies \fo\ in
%4Pierre
this case. Note, however, that \uobdd\ and \obdd\ allow the forgetting of a
single variable in polytime, but \fbdd\ does not allow even that.
\dDnnf\ is similar to \fbdd\ as it satisfies neither \fo\ nor
\sfo.

It is also interesting to observe that none of the target
compilation languages is closed under conjunction. A number of
them, however, are closed under
%6Pierre: I replaced ``bounded-conjunction'' by ``bounded conjunction.
bounded conjunction, including
\obdd, \dnf, \ip\ and \mods.

As for disjunction, the only target compilation languages that
are closed under disjunction are \Dnnf\ and \dnf. The \obdd\ and
\pi\ languages, however, are closed under bounded disjunction.
Again, the \dDnnf, \fbdd\ and \uobdd\ languages are closed under neither.

The only target compilation languages that are closed under
%4Pierre
negation are \fbdd, \uobdd\ and \obdd, while it is not known whether
\dDnnf\ or \sdDnnf\ are closed under this operation. Note that
\dDnnf\ and \fbdd\ support the same set of polytime queries
(equivalence checking is unknown for both) so they are
indistinguishable from that viewpoint. Moreover, the only
difference between the two languages in
Table~\ref{tab:transformations} is the closure of \fbdd\ under
negation, which does not seem to be that significant in light of
no closure under either conjunction or disjunction. Note,
however, that \dDnnf\ is more succinct than \fbdd\ as given in
Figure~\ref{fig:succinctness}.

Finally, \obdd\ is the only target compilation language that is
closed under negation, bounded conjunction, and bounded
disjunction. This closure actually plays an important role in
compiling propositional theories into \obdd\ and is the basis of
state-of-the-art compilers for this purpose \cite{Bryant86}.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Conclusion} \label{sec:discussion}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The main contribution of this paper is a methodology for analyzing
propositional compilation approaches according to two key
dimensions: the succinctness of the target compilation language,
and the class of queries and transformations it supports in
polytime. The second main contribution of the paper is a
comprehensive analysis, according to the proposed methodology, of
more than a dozen languages for which we have produced a
knowledge compilation map, which cross-ranks these languages
according to their succinctness, and the polytime queries and
transformations they support. This map allows system designers to
make informed decisions on which target compilation language to
use: after the class of queries/transformations have been decided
based on the application of interest, the designer chooses the
most succinct target compilation language that supports such
operations in polytime. Another key contribution of this paper is
the uniform treatment we have applied to diverse target
compilation languages, showing how they all are subsets of the
\nnf\ language. Specifically, we have identified a number of
simple, yet meaningful, properties, including decomposability,
determinism, decision and flatness, and showed how combinations
of these properties give rise to different target compilation
languages. The studied subsets include some well known languages
such as \pi, which has been influential in AI; \obdd, which has
been influential in formal verification; and \cnf\ and \dnf, which
have been quite influential in computer science. The subsets also
include some relatively new languages such as \Dnnf\ and \dDnnf,
which appear to represent interesting, new balances between
language succinctness and query/transformation tractability.

%Pierre: I've added the next section.
%4Pierre: updated
%\section*{Acknowledgments}

\acks{This is a revised and extended version of the paper ``A
Perspective on Knowledge Compilation,'' in Proceedings of the
$17^{th}$ International Joint Conference on Artificial
Intelligence (IJCAI'01), pp. 175-182, 2001.
%5Pierre: updated with the revoewers
We wish to thank Alvaro del Val, Mark Hopkins, J\'er\^ome Lang and
the anonymous reviewers for some suggestions and comments, as well
as Ingo Wegener for his help with some of the issues discussed in
the paper. This work has been done while the second author was a
visiting researcher with the Computer Science Department at UCLA.
The first author has been partly supported by NSF grant
IIS-9988543 and MURI grant N00014-00-1-0617. The second author has
been partly supported by the IUT de Lens, the Universit\'e
d'Artois, the Nord/Pas-de-Calais R\'egion under the TACT-TIC
project, and by the European Community FEDER Program.}


%\newpage
\appendix

\section{Proofs}
\label{app:proofs}

%5Pierre: I add some explanations there.
%6Adnan: I rephrased a bit
To simplify the proofs of our main propositions later on, we have
identified a number of lemmas that we list below. Some of the
proofs of these lemmas are direct, but we include them for
completeness.


\begin{lemma} \label{lem:sd-DNNF}
Every sentence in \dDnnf\ can be translated to an equivalent
sentence in \sdDnnf\ in polytime.
\end{lemma}
\begin{proof}
Let $\alpha = \alpha_1 \vee \ldots \vee \alpha_n$ be an or-node
in a \dDnnf\ sentence $\Sigma$. Suppose that \(\alpha\) is not
smooth and let $V = \vars(\alpha)$. Consider now the sentence
$\Sigma_s$ obtained by replacing in $\Sigma$ each such node by
$\bigvee_{i=1}^n \alpha_i \wedge \bigwedge_{v \in V \setminus
\vars(\alpha_i)} (\neg v \vee v)$. Then \(\Sigma_s\) is equivalent
to $\Sigma$ and is smooth. Moreover, $\Sigma_s$ can be computed in
time polynomial in the size of $\Sigma$ and it satisfies
decomposability and determinism.
\end{proof}

\begin{lemma} \label{lem:s-FBDD}
Every sentence in \fbdd\ can be translated to an equivalent
sentence in \fbdd\ \(\cap\) \snnf\ in polytime.
\end{lemma}
\begin{proof}
%6Pierre: I added some parentheses in several places.
Let $\Sigma$ be a sentence in \fbdd\ and let \(\alpha\) be a node
in \(\Sigma\). We can always replace \(\alpha\) with
\((Y\wedge\alpha) \vee (\neg Y\wedge\alpha)\), for some variable
\(Y\), while preserving equivalence and the decision property.
Moreover, as long as the variable \(Y\) does not appear in
\(\alpha\) and is not an ancestor of \(\alpha\), then
decomposability is also preserved (that is, the resulting sentence
is in \fbdd). Note here that ``ancestor'' is with respect to the
binary decision diagram notation of \(\Sigma\)--see left of
Figure~\ref{fig:bdd}.

Now, suppose that \((X\wedge\alpha) \vee (\neg X\wedge\beta)\) is
an or-node in \(\Sigma\). Suppose further that the or-node is not
smooth. Hence, there is some \(Y\) which appears in
\(\vars(\beta)\) but not in \(\vars(\alpha)\) (or the other way
around). Since \(\Sigma\) is decomposable, then \(Y\) cannot be
an ancestor of \(\alpha\) (since in that case it would also be an
ancestor of \(\beta\), which is impossible by decomposability of
\(\Sigma\)). Hence, we can replace \(\alpha\) with
\((Y\wedge\alpha) \vee (\neg Y\wedge\alpha)\), while preserving
equivalence, decision and decomposability. By repeating the above
process, we can smooth \(\Sigma\) while preserving all the
necessary properties. Finally, note that for every or-node
\((X\wedge\alpha) \vee (\neg X\wedge\beta)\) in \(\Sigma\), we
need to repeat the above process at most
\(\mid\vars(\alpha)-\vars(\beta)\mid+\mid\vars(\beta)-\vars(\alpha)\mid\)
times. Hence, the smoothing operation can be performed in
polytime.
\end{proof}


\begin{lemma} \label{lem:me}
If a subset \L\ of \nnf\ satisfies \co\ and \cd, then it also
satisfies \me.
\end{lemma}
\begin{proof}
Let \(\Sigma\) be a sentence in \L. First, we test if \(\Sigma\)
is inconsistent (can be done in polytime). If it is, we return the
empty set of models. Otherwise, we construct a decision-tree
representation of the models of $\Sigma$. Given an ordering of
the variables $x_1, \ldots, x_n$ of $\vars(\Sigma)$, we start
with a tree \(T\) consisting of a single root node. For \(i=1\)
to \(n\), we repeat the following for each leaf node \(\alpha\)
(corresponds to a consistent term) in \(T\):
\begin{enumerate}
\item [a.] If $\Sigma \mid \alpha \wedge x_i$ is
consistent, we add $x_i$ as a child to $\alpha$;
\item [b.] If $\Sigma\mid \alpha \wedge \neg x_i$ is
consistent, we add $\neg x_i$ as a child to $\alpha$.
\end{enumerate}
The key points are:
\begin{itemize}
\item Test~(a) and Test~(b) can be performed in time
polynomial in the size of $\Sigma$ (since \L\ satisfies \co\ and
\cd).
\item Either Test~(a) or Test~(b) above must succeed
(since $\Sigma$ is consistent).
\end{itemize}
Hence, the number of tests performed is ${\cal O}(m n)$, where $m$
is the number of leaf nodes in the final decision tree (bounded
by the number of models of $\Sigma$) and $n$ is the number of
variables of $\Sigma$.
\end{proof}


\begin{lemma} \label{lem:ce}
If a subset of \nnf\ satisfies \co\ and \cd, then it also
satisfies \ce.
\end{lemma}
\begin{proof}
To test whether sentence \(\Sigma\) entails non-valid clause
\(\alpha\), \(\Sigma \models \alpha\), it suffices to test whether
\(\Sigma \mid \neg \alpha\) is inconsistent
\cite{darwicheJACM-DNNF}.
\end{proof}

%4Pierre: new lemmata inserted

\begin{lemma}\label{lem:d-validity}
Let \(\alpha\) and \(\beta\) be two sentences that share no
variables. Then \(\alpha\vee\beta\) is valid iff \(\alpha\) is
valid or \(\beta\) is valid.
\end{lemma}
\begin{proof}
\(\alpha\vee\beta\) is valid iff \(\neg\alpha\wedge\neg\beta\) is
inconsistent. Since \(\neg\alpha\) and \(\neg\beta\) share no
variables, then \(\neg\alpha\wedge\neg\beta\) is inconsistent iff
\(\neg\alpha\) is inconsistent or \(\neg\beta\) is. This is true
iff \(\alpha\) is valid or \(\beta\) is valid.
\end{proof}

\begin{lemma} \label{lem:dd-disjoin}
Let \(\Sigma\) be a sentence in \dDnnf\ and let \(\gamma\) be a
clause. Then a sentence in \dDnnf\ which is equivalent to \(\Sigma
\vee \gamma\) can be constructed in polytime in the size of
\(\Sigma\) and \(\gamma\).
\end{lemma}
\begin{proof}
Let \(l_1,\ldots,l_n\) be the literals that appear in clause \(\gamma\).
%6Pierre: I added some parentheses there.
Then \(\beta = \bigvee_{i=1}^n (l_i \wedge
\bigwedge_{j=1}^{i-1} \neg l_j)\) is equivalent to clause
\(\gamma\), is in \dDnnf, and can be constructed in polytime in
size of \(\gamma\). Now let \(\alpha\) be the term equivalent to
\(\neg\gamma\). We have that \(\Sigma \vee \gamma\) is equivalent
to
%6Pierre: I added some parentheses there.
\(((\Sigma\mid\alpha)\wedge\alpha) \vee \beta\). The last
sentence is in \dDnnf\ and can be constructed in polytime in size
of \(\Sigma\) and \(\gamma\).
\end{proof}

%4Pierre: old lemma replaced by the new one
%\begin{lemma} \label{lem:im}
%If a subset of \nnf\ satisfies \va\ and \cd, then it also
%satisfies \im.
%\end{lemma}
%\begin{proof}
%To test whether consistent term \(\alpha\) entails sentence
%\(\Sigma\), \(\alpha \models \Sigma\), it suffices to test
%whether \(\neg \Sigma \models \neg \alpha\). For this, it
%suffices to test whether \(\neg \Sigma \mid \alpha\) is
%inconsistent \cite{darwicheJACM-DNNF}, which is the same as testing
%whether \(\Sigma \mid \alpha\) is valid.
%\end{proof}

\begin{lemma} \label{lem:im}
If a subset of \nnf\ satisfies \va\ and \cd, then it also
satisfies \im.
\end{lemma}
\begin{proof}
To test whether a consistent term \(\alpha\) entails sentence
\(\Sigma\), \(\alpha \models \Sigma\), it suffices to test whether
\(\neg \alpha \vee \Sigma\) is valid. This sentence is equivalent
to \(\neg \alpha \vee (\alpha\wedge\Sigma)\), to \(\neg \alpha
\vee (\alpha\wedge(\Sigma\mid\alpha))\), and to \(\neg \alpha \vee
%6Pierre: I added some parentheses there.
(\Sigma\mid\alpha)\). Since \(\neg\alpha\) and \(\Sigma\mid\alpha\)
share no variables, the disjunction is valid iff \(\neg\alpha\) is
valid or \(\Sigma\mid\alpha\) is valid (by
Lemma~\ref{lem:d-validity}). \(\neg\alpha\) cannot be valid since
\(\alpha\) is consistent. \(\Sigma\mid\alpha\) can be constructed
in polytime since the language satisfies \cd\ and its validity can
be tested in polytime since the language satisfies \va.
\end{proof}


\begin{lemma} \label{lem:bdd}
Every CNF or DNF formula can be translated to an equivalent
sentence in \bdd\ in polytime.
\end{lemma}
\begin{proof}
It is straightforward to convert a clause or term into an
equivalent sentence in \bdd. In order to generate a \bdd\
sentence corresponding to the conjunction (resp. disjunction) of
\bdd\ sentences $\alpha$ and $\beta$, it is sufficient to replace
the $1$-sink (resp. $0$-sink) of $\alpha$ with the root of
$\beta$.
\end{proof}

\begin{lemma} \label{lem:eq}
If a subset of \nnf\ satisfies \eq, then it satisfies \co\ and
\va.
\end{lemma}
\begin{proof}
\true\ and \false\ belong to every \nnf\ subset. \(\Sigma\) is
inconsistent iff it is equivalent to \false. \(\Sigma\) is valid
iff it is equivalent to \true.
\end{proof}


\begin{lemma} \label{lem:se}
If a subset of \nnf\ satisfies \se, then it satisfies \eq, \co\
and \va.
\end{lemma}
\begin{proof}
Sentences \(\Sigma_1\) and \(\Sigma_2\) are equivalent iff
\(\Sigma_1 \models \Sigma_2\) and \(\Sigma_2 \models \Sigma_1\).
\eq\ implies \co\ and \va\ (Lemma~\ref{lem:eq}).
\end{proof}


%4Pierre: old lemma replaced by the new one
\begin{lemma} \label{lem:validity}
Let \(\Sigma\) be a sentence in \dDnnf\ and let \(\gamma\) be a
clause. The validity of \(\Sigma \vee \gamma\) can be tested in
time polynomial in the size of \(\Sigma\) and \(\gamma\).
\end{lemma}
\begin{proof}
Construct $\Sigma \vee \gamma$ in polytime as given in
Lemma~\ref{lem:dd-disjoin} and check its validity, which can be
done in polytime too.
\end{proof}

%4Pierre: old lemma
%\begin{lemma} \label{lem:validity}
%Let \(\Sigma\) be a sentence in \dDnnf\ and let \(\gamma\) be a
%clause. The validity of \(\Sigma \vee \gamma\) can be tested in
%time polynomial in the size of \(\Sigma\) and \(\gamma\).
%\end{lemma}
%\begin{proof}
%In order to check whether $\Sigma \vee \gamma$ is valid in
%polynomial time, what we have to do is just to count its models---
%If $|Vars(\Sigma \vee \gamma)| = n$, then $\Sigma \vee \gamma$ is
%%3Pierre: I replaced ``vars'' by ``Vars''.
%valid iff it has $2^n$ models. We clearly have $\Sigma \vee
%\gamma \equiv (\Sigma \wedge \neg \gamma) \vee \gamma$, and since
%$\Sigma \wedge \neg \gamma \equiv (\Sigma | \neg \gamma) \wedge
%\neg \gamma$ holds, we also have $\Sigma \vee \gamma \equiv
%((\Sigma | \neg \gamma) \wedge \neg \gamma) \vee \gamma$. Now,
%since \dDnnf\ satisfies \cd\ (see
%Proposition~\ref{prop:transformations}) and since by construction
%$\vars(\Sigma | \neg \gamma) \cap \vars(\neg \gamma) = \emptyset$,
%the sentence $(\Sigma | \neg \gamma) \wedge \neg \gamma$ is in
%\dDnnf. Accordingly, we can count its models in polytime (see
%Proposition~\ref{prop:queries}). We can also count the number of
%models of $\gamma$ since every non-tautological clause containing
%$k$ literals without repetition has $\#\gamma = 2^k-1$ models over
%the set of its variables. Because every variable of
%$\vars(\gamma)$ also occurs in $\vars((\Sigma | \neg \gamma)
%\wedge \neg \gamma)$, we just have to normalize the number of
%models $\#\gamma$ of $\gamma$ over the set of its variables by
%multiplying it with $2^l$ where $l = |\vars(\Sigma \setminus
%\vars(\gamma)|$. This results in the number of models of $\gamma$
%over the set $\vars(\Sigma \vee \gamma)$. If this number plus the
%number of models of $(\Sigma | \neg \gamma) \wedge \neg \gamma$
%is equal to $2^n$, then $\Sigma \vee \gamma$ is valid and the
%converse also holds.
%\end{proof}

\begin{lemma}\label{lem:cdviafo}
For every propositional formula $\Sigma$ and every consistent term
$\gamma$, we have $\Sigma | \gamma$ is equivalent to\\
$\exists \vars(\gamma) . (\Sigma \wedge \gamma)$.
\end{lemma}
\begin{proof}
Without loss of generality, assume that $\Sigma$ is given by the
disjunctively-interpreted set of its models (over
$\vars(\Sigma)$). Conditioning $\Sigma$ on $\gamma$ leads (1) to
%3Pierre: typo ``removinf'' -> ``removing''.
removing every model of $\neg \gamma$, then (2) projecting the
remaining models so that every variable of $\gamma$ is removed.
Conjoining $\Sigma$ with $\gamma$ leads exactly to (1), while
forgetting every variable of $\gamma$ in the resulting formula
leads exactly to (2)
%5Pierre: I removed ``(see ...)''.
\cite{LangLiberatoreMarquis00a}.
\end{proof}


\begin{lemma}\label{lem:f-nnf}
Each sentence \(\Sigma\) in \fnnf\ can be converted into an
equivalent sentence \(\Sigma*\) in polynomial time, where
\(\Sigma* \in \cnf\) or \(\Sigma* \in \dnf\).
\end{lemma}
\begin{proof}
%(** Pierre: you referred to this result multiple times, so I
%constructed a lemma for it. Please fill in the proof details. **)
%3Pierre: Here is a proof. Tell me if it is clear enough.
We consider three cases for the sentence \(\Sigma\):
\begin{enumerate}
\item  The root node of $\Sigma$ is an and-node.
 In this case, $\Sigma$ can be turned into a \cnf\ sentence $\Sigma*$
in polynomial time by simply ensuring that each or-node in
\(\Sigma\) is a clause (that is, a disjunction of literals that
share no variables). Let \(C\) be an or-node in \(\Sigma\). Since
$\Sigma$ is flat and its root is an and-node, $C$ must be a child
of the root of \(\Sigma\) and the children of $C$ must be leaves.
Hence, we can easily ensure that \(C\) is a clause as follows:
\begin{itemize}
\item If we have one edge from $C$ to some leaf \(X\) and another edge
from \(C\) to \(\neg X\) (\(C\) is valid), we replace the edge
from the root to $C$ by an edge from the root to $\true$.

\item If we have more than one edge from $C$ to the same leaf node \(X\), we keep
only one of these edges and delete the rest.
\end{itemize}

\item The root of $\Sigma$ is an or-node.
$\Sigma$ can be turned into a \dnf\ sentence $\Sigma*$ in a dual
way.\footnote{Note that \fnnf\ satisfies \(\nc\) and that the
negation of a \cnf\ sentence (resp. \dnf\ sentence) can be turned
into a \dnf\ (resp. \cnf) in linear time.}

\item The root of \(\Sigma\) is a leaf node.
$\Sigma$ is already a \cnf\ sentence.
\end{enumerate}
\end{proof}


%3Pierre: I also added this lemma, since it will serve several times.
\begin{lemma}\label{lem:pivsip}
$\alpha$ is a prime implicant (resp. an essential prime implicant)
of sentence $\Sigma$ iff $\neg \alpha$ is a prime implicate (resp.
an essential prime implicate) of $\neg \Sigma$. \footnote{A prime
implicant (resp. a prime implicate) $\alpha$ of $\Sigma$ is {\em
essential} iff the disjunction (resp. conjunction) of all prime
implicants (resp. prime implicates) of $\Sigma$ except $\alpha$ is
not equivalent to $\Sigma$.}
\end{lemma}
\begin{proof}
This is a folklore result, immediate from the definitions.
\end{proof}


\subsection*{Proof of Proposition~\ref{prop:succinctness}}

%5Pierre: I add a comment to explain how we proceeded
%6Adnan: rephrased the paragraph a bit
The proof of this proposition is broken down into eight steps. In
each step, we prove a number of succinctness relationships between
different languages, and then apply transitivity of the
succinctness relation to infer even more relationships. Associated
with each step of the proof is a table in which we mark all
relationships that are proved in that step--we don't show these
marks in the very first table though.

%Let us explain why the results hold in a progressive way through a
%number of intermediate tables. Whenever a new intermediate table
%is introduced, one or several succinctness results are given and
%the table is then completed by taking advantage of the
%transitivity of the succinctness relation. For the ease of
%reading, the new results derived at each step (i.e., those that
%were not reported in the previous intermediate tables) are marked.

\begin{table}
\begin{center}\begin{tiny}
%4Pierre
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \nnf\ & \Dnnf\ & \dDnnf\ & \fbdd\ & \uobdd & \obdd\ & \dnf\ & \cnf\ & \pi\ & \ip\ & \mods\ & \sdDnnf \\
\hline \hline
\nnf\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ \\
\hline
\Dnnf\ & & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & & & \as\ & \as\ & \as\ \\
\hline
\dDnnf\ & & & \as\ & \as\ & \as\ & \as\ & & & & & \as\ & \as\ \\
\hline
\fbdd\ & & & & \as\ & \as\ & \as\ & & & & & &\\
\hline
\uobdd\ & & & & & \as\ & \as\ & & & & & &\\
\hline
\obdd\ & & & & & & \as\ & & & & & &\\
\hline
\dnf\ & & & & & & & \as\ & & & \as\ & \as\ &\\
\hline
\cnf\ & & & & & & & & \as\ & \as\ & & &\\
\hline
\pi\ & & & & & & & & & \as\ & & &\\
\hline
\ip\ & & & & & & & & & & \as\ & &\\
\hline
\mods\ & & & & & & & & & & & \as\ &\\
\hline
\sdDnnf\ & & & & & & & & & & & \as\ & \as\ \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:s1}}
\end{table}

{\bf Table~\ref{tab:s1}:} Follows immediately from the language
inclusions reported in Figure~\ref{fig:subsets}.

\begin{table}
\begin{center}\begin{tiny}
%4Pierre
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \nnf\ & \Dnnf\ & \dDnnf\ & \fbdd\ & \uobdd & \obdd\ & \dnf\ & \cnf\ & \pi\ & \ip\ & \mods\ & \sdDnnf \\
\hline \hline
\nnf\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ \\
\hline
\Dnnf\ & & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & & & \as\ & \as\ & \as\ \\
\hline
\dDnnf\ & & & \as\ & \as\ & \as\ & \as\ & & & & & \as\ & \as\ \\
\hline
\fbdd\ & & & & \as\ & \as\ & \as\ & & & & & &\\
\hline
\uobdd\ & & & & & \as\ & \as\ & & & & & & \\
\hline
\obdd\ & & & & & & \as\ & & & & & & \\
\hline
\dnf\ & \nasn\ & & & & & & \as\ & \nasn\ & \nasn\ & \as\ & \as\ &\\
\hline
\cnf\ & \nasn\ & \nasn\ & & & & & \nasn\ & \as\ & \as\ & \nasn\ & &\\
\hline
\pi\ & \nasn\ & \nasn\ & & & & & \nasn\ & \nasn\ & \as\ & \nasn\ & &\\
\hline
\ip\ & \nasn\ & \nasn\ & & & & & \nasn\ & \nasn\ & \nasn\ & \as\ & &\\
\hline
\mods\ & & & & & & & & & & & \as\ &\\
\hline
\sdDnnf\ & & & & & & & & & & & \as\ & \as\ \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:s2}}
\end{table}
{\bf Table~\ref{tab:s2}:} We can prove both that \dnf\ \nas\ \pi\
and \cnf\ \nas\ \ip\ (this slightly generalizes the results \dnf\
\nas\ \cnf\ and \cnf\ \nas\ \dnf\ given in \cite{Gogicetal95}).

Let us consider the CNF formula $\Sigma_n = \bigwedge_{i=0}^{n-1}
(x_{2i} \vee x_{2i+1})$. This formula is in prime implicates
form\footnote{The correctness of (the dual of) Quine's consensus
algorithm for computing prime implicants \cite{Quine55} ensures
it, since no clause of $\Sigma_n$ is subsumed by another clause
and no consensi can be performed since there are no negated
variables.} (and each clause in $\Sigma_n$ is an essential prime
implicate of it). Hence its negation $\neg \Sigma_n$ is in prime
implicants form (as an easy consequence of
Lemma~\ref{lem:pivsip}).
%3Pierre: I introduced a lemma before.

Since Quine's early work \cite{Quine59}, we know that the number of essential prime implicants
(resp. prime implicates) of a formula is a lower bound of the number of
terms (resp. clauses) that can be found in any DNF (resp. CNF)
representation of it (indeed, any such representation must include
the essential prime).
%\footnote{(** Pierre: Define essential prime implicates/implicants **)}
%%3Pierre: done (in Lemma lem:pivsip).
$\Sigma_n$ has $2^n$ essential prime
%4Pierre: additional footnote
implicants. Indeed, this can be easily shown by induction on $n$ given that
(i) every literal occurring in $\Sigma_n$ occurs only once,
(ii) the set of prime implicants of any nontautological clause
is the set of literals occurring in it (up to logical equivalence), and
(iii) the distribution property for prime implicants (see e.g., (dual of) Proposition 40 in
\cite{Marquis00}) which states
that ${\it IP}(\alpha \wedge \beta) = max(\{\pi_{\alpha} \wedge \pi_{\beta} \ | \
\pi_{\alpha} \in {\it IP}(\alpha), \pi_{\beta} \in {\it IP}(\beta)\}, \models)$ (up to logical equivalence).
Subsequently, $\neg \Sigma_n$ has $2^n$ essential prime
implicates (cf. Lemma \ref{lem:pivsip}).
%(** Pierre: ref? **).
%3Pierre: it is immediate to show that each term containing
%one variable per clause of $\Sigma_n$ is a prime implicant of it.
%Do you think it is important to write more about it?
Accordingly, we obtain that both \dnf\ \nas\ \pi\ and \cnf\ \nas\
\ip. We also obtain \pi\ \nas\ \ip\ and \ip\ \nas\ \pi. Now, it is
well--known that some DNF formulas have exponentially many prime
implicants (see the proof of
Proposition~\ref{prop:transformations} where we show that \ip\
does not satisfy \sfo). Hence, their negations are CNF formulas
having exponentially many prime implicates. Subsequently \ip\
\nas\ \dnf\ and \pi\ \nas\ \cnf. The remaining results in this
table follow from the transitivity of \as.

\begin{table}
\begin{center}\begin{tiny}
%4Pierre
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \nnf\ & \Dnnf\ & \dDnnf\ & \fbdd\ & \uobdd & \obdd\ & \dnf\ & \cnf\ & \pi\ & \ip\ & \mods\ & \sdDnnf \\
\hline \hline
\nnf\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ \\
\hline
\Dnnf\ & & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & & & \as\ & \as\ & \as\ \\
\hline
\dDnnf\ & & & \as\ & \as\ & \as\ & \as\ & & & & & \as\ & \as\ \\
\hline
\fbdd\ & & & & \as\ & \as\ & \as\ & & & & & &\\
\hline
\uobdd\ & & & & & \as\ & \as\ & & & & & &\\
\hline
\obdd\ & & & & & & \as\ & & & & & &\\
\hline
\dnf\ & \nas\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \as\ & \nas\ & \nas\ & \as\ & \as\ &\\
\hline
\cnf\ & \nas\ & \nas\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nas\ & \as\ & \as\ & \nas\ & &\\
\hline
\pi\ & \nas\ & \nas\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nas\ & \nas\ & \as\ & \nas\ & &\\
\hline
\ip\ & \nas\ & \nas\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nas\ & \nas\ & \nas\ & \as\ & &\\
\hline
\mods\ & & & & & & & & & & & \as\ &\\
\hline
\sdDnnf\ & & & & & & & & & & & \as\ & \as\ \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:s3}}
\end{table}
{\bf Table~\ref{tab:s3}:}
 The parity function $O_n =
\bigoplus_{i=0}^{n-1} x_i$ has linear size OBDD$_<$
representations
%5Pierre: I removed ``(see ...)''.
\cite{Bryant86} but only exponential
size CNF and DNF representations. The reason is that $O_n$ has
$2^n$ essential prime implicants (resp. essential prime
implicates) and the number of essential prime implicants (resp.
essential prime implicates) of a formula is a lower bound of the
size of any of its DNF (resp. CNF) representation. This easily
shows that both \cnf\ \nas\ \uobdd\ and \dnf\ \nas\ \uobdd. The
remaining results in this table follow from the language
inclusions reported in Figure~\ref{fig:subsets}.


\begin{table}
\begin{center}\begin{tiny}
%4Pierre
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \nnf\ & \Dnnf\ & \dDnnf\ & \fbdd\ & \uobdd & \obdd\ & \dnf\ & \cnf\ & \pi\ & \ip\ & \mods\ & \sdDnnf \\
\hline \hline
\nnf\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ \\
\hline
\Dnnf\ & & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & & & \as\ & \as\ & \as\ \\
\hline
\dDnnf\ & & & \as\ & \as\ & \as\ & \as\ & & & & & \as\ & \as\ \\
\hline
\fbdd\ & \nasn\ & \nasn\ & \nasn\ & \as\ & \as\ & \as\ & & & & & &\\
\hline
\uobdd\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \as\ & \as\ & & & & & &\\
\hline
\obdd\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \as\ & & & & & &\\
\hline
\dnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \nas\ & \as\ & \as\ &\\
\hline
\cnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ & &\\
\hline
\pi\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & &\\
\hline
\ip\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & &\\
\hline
\mods\ & & & & & & & & & & & \as\ &\\
\hline
\sdDnnf\ & & & & & & & & & & & \as\ & \as\ \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:s4}}
\end{table}
{\bf Table~\ref{tab:s4}:}
 It is shown in \cite{darwicheJANCL} that
there is a sentence in \dDnnf\ which only has exponential \fbdd\
representations. Accordingly, we have \fbdd\ \nas\ \dDnnf. In
\cite{GergovMeinel94}, it is shown that \uobdd\ \nas\ \fbdd.
Finally, it is easy to show that \obdd\ \nas\ \uobdd\ (for instance,
the formula $\Sigma_n = \bigwedge_{i=1}^n (x_i \Leftrightarrow y_i)$
has an \obdd\ representation of size polynomial in $n$ whenever
$<$ satisfies $x_1 < y_1 < x_2 < \ldots < x_n < y_n$, while it has
an \obdd\ representation of size exponential in $n$ provided that
$<$ is s.t. $x_1 < x_2 < \ldots < x_n < y_1 < y_2 < \ldots < y_n$).
The remaining results in this table follow from the language
inclusions reported in Figure~\ref{fig:subsets}.


\begin{table}
\begin{center}\begin{tiny}
%4Pierre
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \nnf\ & \Dnnf\ & \dDnnf\ & \fbdd\ & \uobdd & \obdd\ & \dnf\ & \cnf\ & \pi\ & \ip\ & \mods\ & \sdDnnf \\
\hline \hline
\nnf\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ \\
\hline
\Dnnf\ & \nascn\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \nascn\ & & \as\ & \as\ & \as\ \\
\hline
\dDnnf\ & \nascn\ & & \as\ & \as\ & \as\ & \as\ & & \nascn\ & & & \as\ & \as\ \\
\hline
\fbdd\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \as\ &  &  & & & &\\
\hline
\uobdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & & & & & &\\
\hline
\obdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & & & & & &\\
\hline
\dnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \nas\ & \as\ & \as\ &\\
\hline
\cnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ & &\\
\hline
\pi\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & &\\
\hline
\ip\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & &\\
\hline
\mods\ & & & & & & & & & & & \as\ &\\
\hline
\sdDnnf\ & \nascn\ & & & & & & & \nascn\ & & & \as\ & \as\ \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:s5}}
\end{table}
{\bf Table~\ref{tab:s5}:} \L' \nasc\ \L\ means that \L' \nas\ \L\
unless the polynomial hierarchy {\sf PH} collapses. The results
in this table follow since the existence of polysize knowledge
compilation functions for clausal entailment implies the collapse
of the polynomial hierarchy {\sf PH}
%5Pierre: I removed ``(see ...)''.
\cite{SelmanKautz96,CadoliDonini97}. Now, if \Dnnf\ \as\ \cnf,
then for each sentence \(\Sigma\) in \cnf\ there exists a polysize
equivalent sentence \(\Gamma\) in \Dnnf. Therefore, we can test
whether a clause is entailed by \(\Sigma\) in polytime by testing
whether the clause is entailed by \(\Gamma\). This proves the
existence of polysize knowledge compilation functions for clausal
entailment, leading to the collapse of the polynomial hierarchy
{\sf PH}. The same is true for \dDnnf\ and \sdDnnf\ since all
these languages support a polytime clausal entailment test (see
Proposition~\ref{prop:queries}).


\begin{table}
\begin{center}\begin{tiny}
%4Pierre
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \nnf\ & \Dnnf\ & \dDnnf\ & \fbdd\ & \uobdd & \obdd\ & \dnf\ & \cnf\ & \pi\ & \ip\ & \mods\ & \sdDnnf \\
\hline \hline
\nnf\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ \\
\hline
\Dnnf\ & \nasc\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \nasc\ & & \as\ & \as\ & \as\ \\
\hline
\dDnnf\ & \nasc\ & & \as\ & \as\ & \as\ & \as\ & & \nasc\ & & & \as\ & \as\ \\
\hline
\fbdd\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \as\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & &\\
\hline
\uobdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & &\\
\hline
\obdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & &\\
\hline
\dnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \nas\ & \as\ & \as\ &\\
\hline
\cnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ & &\\
\hline
\pi\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & &\\
\hline
\ip\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & &\\
\hline
\mods\ & & & & & & & & & & & \as\ &\\
\hline
\sdDnnf\ & \nasc\ & & & & & & & \nasc\ & & & \as\ & \as\ \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:s6}}
\end{table}
{\bf Table~\ref{tab:s6}:}
 In \cite{Wegener87} (Theorem 6.2 pp.
436), a family of $n^2$-variable boolean functions $\Sigma$ is
pointed out. Provided that every interpretation $I$ over these
$n^2$ variables represents a $n$-vertices digraph (for every $1
\leq i$, $j \leq n$, we have $I(x_{i,j}) = 1$ iff $(i, j)$ is an
arc of the digraph), $\Sigma(I) = 1$ iff the digraph represented
by $I$ contains a $k$-clique of a special kind ($k$ is a
parameter of the family). It is shown that for certain values of
$k$ (depending on $n$), every FBDD representation of $\Sigma$ has
exponential size. Moreover, it is shown that $\Sigma$ has only a
cubic number of prime implicants. This shows that \fbdd\ \nas\
\ip, hence \fbdd\ \nas\ \dnf. Because \fbdd\ satisfies \(\nc\)
(see Proposition~\ref{prop:transformations}),\footnote{That is, a
sentence in \fbdd\ can be negated in polytime to yield a sentence
in \fbdd\ too.} it cannot be the case that $\neg \Sigma$ has a
polynomial size \fbdd. Since $\neg \Sigma$ has only a cubic number
of prime implicates, we obtain that \fbdd\ \nas\ \pi, hence \fbdd\
\nas\ \cnf. The remaining results in this table follow since \fbdd \as\ \uobdd\
\as\ \obdd.

\begin{table}
\begin{center}\begin{tiny}
%4Pierre
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \nnf\ & \Dnnf\ & \dDnnf\ & \fbdd\ & \uobdd & \obdd\ & \dnf\ & \cnf\ & \pi\ & \ip\ & \mods\ & \sdDnnf \\
\hline \hline
\nnf\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ \\
\hline
\Dnnf\ & \nasc\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \nasc\ & & \as\ & \as\ & \as\ \\
\hline
\dDnnf\ & \nasc\ & \nascn\ & \as\ & \as\ & \as\ & \as\ & \nascn\ & \nasc\ & & & \as\ & \as\ \\
\hline
\fbdd\ & \nas\ & \nas\ & \nas\ & \as\ &\as\ & \as\ & \nas\ & \nas\ & \nas\ & \nas\ & & \nasn\ \\
\hline
\uobdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ & \nas\ & \nas\ & \nas\ & & \nasn\ \\
\hline
\obdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \nas\ & \nas\ & \nas\ & & \nasn\ \\
\hline
\dnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \nas\ & \as\ & \as\ & \nasn\ \\
\hline
\cnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ & & \nasn\ \\
\hline
\pi\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & & \nasn\ \\
\hline
\ip\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & & \nasn\ \\
\hline
\mods\ & & & & & & & & & & & \as\ & \\
\hline
\sdDnnf\ & \nasc\ & \nascn\ & \asn\ & \asn\ & \asn\ & \asn\ & \nascn\ & \nasc\ & & & \as\ & \as\ \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:s7}}
\end{table}
{\bf Table~\ref{tab:s7}:}
 Assume that \dDnnf\ \as\ \dnf\ holds. As
a consequence, every sentence $\Sigma$ in \dnf\ can be compiled
into an equivalent \dDnnf\ sentence $\Sigma*$ of polynomial size.
Now, checking whether a clause $\gamma$ is entailed by the \cnf\
sentence $\Sigma$ is equivalent to checking whether the \dnf\
sentence $\neg \Sigma \vee \gamma$ is valid. Checking whether
%6Pierre: perhaps it would be adequate to add a box here so
%that the * will remain stuck to $\neg \Sigma$.
$(\neg \Sigma)* \vee \gamma$ is valid---when $(\neg \Sigma)*$ is
a \dDnnf\ sentence and $\gamma$ is a clause---can be achieved in
polynomial time by Lemma~\ref{lem:validity}. Therefore, $(\neg
\Sigma)*$ is a polysize compilation of the \cnf\ sentence
$\Sigma$, allowing clausal entailment to be achieved in
polynomial time. The existence of such $(\neg \Sigma)*$ for every
\cnf\ sentence $\Sigma$ implies the collapse of the polynomial
hierarchy \cite{SelmanKautz96,CadoliDonini97}. Hence, we obtain
that \dDnnf\ \nasc\ \dnf. As a consequence, we also have \dDnnf\
\nasc\ \Dnnf. Finally, since every \dDnnf\ sentence can be turned
in polynomial time into an equivalent \sdDnnf\ sentence by
Lemma~\ref{lem:sd-DNNF}, we have \sdDnnf\ \as\ \dDnnf. Moreover,
since \dDnnf\ \as\ \sdDnnf, we obtain \sdDnnf\ \nasc\ \dnf,
\sdDnnf\ \nasc\ \Dnnf, \sdDnnf\ \as\ \fbdd, \sdDnnf\ \as\ \uobdd,
\sdDnnf\ \as\ \obdd,
\fbdd\ \nas\ \sdDnnf, \obdd\ \nas\ \sdDnnf, \dnf\ \nas\ \sdDnnf,
\cnf\ \nas\ \sdDnnf, \pi\ \nas\ \sdDnnf\ and \ip\ \nas\ \sdDnnf.

\begin{table}
\begin{center}\begin{tiny}
%4Pierre
\begin{tabular}{|c|c|c|c|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \nnf\ & \Dnnf\ & \dDnnf\ & \fbdd\ & \uobdd & \obdd\ & \dnf\ & \cnf\ & \pi\ & \ip\ & \mods\ & \sdDnnf \\
\hline \hline
\nnf\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ \\
\hline
\Dnnf\ & \nasc\ & \as\ & \as\ & \as\ & \as\ & \as\ & \as\ & \nasc\ & & \as\ & \as\ & \as\ \\
\hline
\dDnnf\ & \nasc\ & \nasc\ & \as\ & \as\ & \as\ & \as\ & \nasc\ & \nasc\ & & & \as\ & \as\ \\
\hline
\fbdd\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \as\ & \nas\ & \nas\ & \nas\ & \nas\ & \asn\ & \nas\ \\
\hline
\uobdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ & \nas\ & \nas\ & \nas\ & \asn\ & \nas\ \\
\hline
\obdd\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \nas\ & \nas\ & \nas\ & \asn\ & \nas\ \\
\hline
\dnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ \\
\hline
\cnf\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \as\ & \nas\ & \asn\ & \nas\ \\
\hline
\pi\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \nas\ &  & \nas\ \\
\hline
\ip\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \nas\ & \as\ & \asn\ & \nas\ \\
\hline
\mods\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \nasn\ & \as\ & \nasn\ \\
\hline
\sdDnnf\ & \nasc\ & \nasc\ & \as\ & \as\ & \as\ & \as\ & \nasc\ & \nasc\ & & & \as\ & \as\ \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:s8}}
\end{table}
{\bf Table~\ref{tab:s8}:}
 Let us now show that \mods\ is not less
succinct than \pi, \ip, \sdDnnf\ and \uobdd. First, let us
consider the formula $\Sigma = \bigvee_{i=1}^n x_i$. $\Sigma$ can
be represented by \pi, \ip, \sdDnnf\ and \uobdd\ formulas of size
polynomial in $n$. Contrastingly, $\Sigma$ cannot be represented
by a \mods\ formula of size polynomial in $n$ since $\Sigma$ has
$2^n - 1$ models over $\vars(\Sigma)$. Now, it is well-known that
the old good Quine-McCluskey's algorithm for generating prime
implicants from a \mods\ representation of a propositional
formula $\Sigma$ runs in time polynomial in the number of models
of $\Sigma$
%5Pierre: I removed ``(see ...)''.
\cite{Wegener87}. This shows that \ip\
\as\ \mods. As to \cnf\ and \obdd, it is obvious that a decision
tree (or Shannon tree) for $\Sigma$ that respects a given total
ordering over $\vars(\Sigma)$ can be generated in polynomial time
from a \mods\ representation of $\Sigma$. Such a decision tree
has $m$ $1$-leaves where $m$ is the number of models of $\Sigma$
over $\vars(\Sigma)$. Accordingly, it has at most $n*m$ $0$-leaves
where $n = |\vars(\Sigma)|$. Since the set of all paths from the
root of the tree to any $0$-leaf can be read as a \cnf\
representation of $\Sigma$, we obtain that \cnf\ \as\ \mods. On
the other hand, since reducing a decision tree to derive a
corresponding OBDD$_<$ can be done in polynomial time, it follows
that an \obdd\ representation of $\Sigma$ can also be generated
from a \mods\ representation of it. Hence, \obdd\ \as\ \mods. The
remaining results in this table follow from the language
inclusions reported in Figure \ref{fig:subsets}.~\qed


\subsection*{Proof of Proposition~\ref{prop:queries}}

%5Pierre: I add a comment to explain how we proceeded
%6Adnan: I rephrased the paragraph a bit

The proof of this proposition is broken down into twelve steps. In
each step, we prove a number of results. Associated with each step
of the proof is a table in which we mark all results that are
proved in that step. The table of the last step includes all
results declared by this proposition.

%Here again, let us explain why the results hold in a progressive way
%through a number of intermediate tables. For the ease of reading,
%the new results derived at each step (i.e., those that were not
%reported in the previous intermediate tables) are marked.

\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \nn & \nn & & & & & &\\
\hline
\Dnnf\ & & \nn & & & & & &\\
\hline
\dnnf\ & & & & & & & &\\
\hline
\dDnnf\ & & & & & & & &\\
\hline
\bdd\ & & & & & & & &\\
\hline
\fbdd\ & & & & & & & &\\
\hline
%4Pierre
\uobdd\ & & & & & & & &\\
\hline
\obdd\ & & & & & & & &\\
\hline
\dnf\ & & \nn & & & & & &\\
\hline
\cnf\ & \nn & & & & & & &\\
\hline
\pi\ & & & & & & & &\\
\hline
\ip\ & & & & & & & &\\
\hline
\mods\ & & & & & & & &\\
\hline
\snnf\ & \nn & \nn & & & & & &\\
\hline
\fnnf\ & \nn & \nn & & & & & &\\
\hline
\sdDnnf\ & & & & & & & &\\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q1}}
\end{table}

{\bf Table~\ref{tab:q1}:} Every classical CNF or DNF formula can
be translated in a straightforward way into an equivalent \fnnf\
sentence (with a tree structure) in polytime. Moreover, every
\nnf\ sentence can be translated into an equivalent \snnf\
sentence in polytime (Lemma~\ref{lem:sd-DNNF}). Given that \co\
is {\sf NP}-hard (resp. \va\ is {\sf coNP}-hard) for classical
CNF (resp. DNF) sentences, and the inclusion between the various
\nnf\ subsets reported in Figure~\ref{fig:subsets}, we obtain the
table.

\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \nn & \nn & & \nn & \nn & \\
\hline
\Dnnf\ & & \n & & \nn & & \nn & \nn & \\
\hline
\dnnf\ & & & & & & & & \\
\hline
\dDnnf\ & & & & & & & & \\
\hline
\bdd\ & & & & & & & & \\
\hline
\fbdd\ & & & & & & & & \\
\hline
%4Pierre
\uobdd\ & & & & & & & &\\
\hline
\obdd\ & & & & & & & & \\
\hline
\dnf\ & & \n & & \nn & & \nn & \nn & \\
\hline
\cnf\ & \n &  & \nn & & & \nn & \nn & \\
\hline
\pi\ & & & & & & & & \\
\hline
\ip\ & & & & & & & & \\
\hline
\mods\ & & & & & & & & \\
\hline
\snnf\ & \n & \n & \nn & \nn &  & \nn & \nn & \\
\hline
\fnnf\ & \n & \n & \nn & \nn &  & \nn & \nn & \\
\hline
\sdDnnf\ & & & & & & & &\\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q2}}
\end{table}
{\bf Table~\ref{tab:q2}:}
 \se\ implies both \co\ and \va\
(Lemma~\ref{lem:se}). Moreover, since \ct\ implies both \co\ and
\va, \im\ implies \va\ (valid term), and \ce\ implies \co\
(inconsistent clause), we obtain the table.


\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n & & \n & \n &\\
\hline
\Dnnf\ & & \n & & \n & & \n & \n &\\
\hline
\dnnf\ & & & & & & & &\\
\hline
\dDnnf\ & & & & & & & &\\
\hline
\bdd\ & & & & & & & &\\
\hline
\fbdd\ & & & & & & & &\\
\hline
%4Pierre
\uobdd\ & & & & & & & &\\
\hline
\obdd\ & & & & & & & &\\
\hline
\dnf\ & & \n & & \n & & \n & \n &\\
\hline
\cnf\ & \n &  & \n & & & \n & \n &\\
\hline
\pi\ & & & & & & & &\\
\hline
\ip\ & & & & & & & &\\
\hline
\mods\ & \ny & \ny & & & & \ny & &\\
\hline
\snnf\ & \n & \n & \n & \n &  & \n & \n & \\
\hline
\fnnf\ & \n & \n & \n & \n &  & \n & \n & \\
\hline
\sdDnnf\ & & & & & & & &\\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q3}}
\end{table}
{\bf Table~\ref{tab:q3}:} A sentence $\Sigma$ is consistent
(resp. valid) iff it has a model (resp. $2^n$ models, where $n =
|\vars(\Sigma)|$). Moreover, the number of models of $\Sigma$ is
given by the number of edges outgoing from the
%6Pierre: I added a ``-'' here for ``or node''
or-node in any
\mods\ representation of $\Sigma$. Accordingly, \co, \va\ and
\ct\ can be achieved in polynomial time when $\Sigma$ is given by
a \mods\ formula which gives us the table.




\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n &  & \n & \n &\\
\hline
\Dnnf\ & \ny & \n & \ny & \n & & \n & \n &\\
\hline
\dnnf\ & & & & & & & &\\
\hline
\dDnnf\ & \ny &  & \ny & & & & &\\
\hline
\bdd\ & & & & & & & &\\
\hline
\fbdd\ & & & & & & & &\\
\hline
%4Pierre
\uobdd\ & & & & & & & &\\
\hline
\obdd\ & & & & & & & &\\
\hline
\dnf\ & \ny & \n & \ny & \n & & \n & \n &\\
\hline
\cnf\ & \n & & \n & & & \n & \n &\\
\hline
\pi\ & & & & & & & &\\
\hline
\ip\ & \ny & & \ny & & & & &\\
\hline
\mods\ & \y & \y & \ny & & & \y & & \\
\hline
\snnf\ & \n & \n & \n & \n &  & \n & \n & \\
\hline
\fnnf\ & \n & \n & \n & \n &  & \n & \n & \\
\hline
\sdDnnf\ & \ny & & \ny & & & & &\\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q4}}
\end{table}
{\bf Table~\ref{tab:q4}:}Because \Dnnf\ satisfies \ce\
\cite{darwicheJACM-DNNF}, \ce\ implies \co\ and \mods\ $\subseteq$
\dnf\ $\subseteq$ \Dnnf, \ip $\subseteq$ \dnf\ and\\
\sdDnnf\ $\subseteq$ \dDnnf\ $\subseteq$ \Dnnf, we obtain the table.
%(** Pierre: you need to
%justify the two \y\ for \ip\ **)
%3Pierre: done.

\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n & & \n & \n & \nn \\
\hline
\Dnnf\ & \y & \n & \y & \n & & \n & \n & \ny \\
\hline
\dnnf\ & & & & & & & &\\
\hline
\dDnnf\ & \y &  & \y & & & & & \ny \\
\hline
\bdd\ & & & & & & & &\\
\hline
\fbdd\ & \ny & \ny & \ny & \ny & & \ny & & \ny \\
\hline
%4Pierre
\uobdd\ & \ny & \ny & \ny & \ny & \ny & \ny & \nn & \ny \\
\hline
\obdd\ & \ny & \ny & \ny & \ny & \ny & \ny & \ny & \ny \\
\hline
\dnf\ & \y & \n & \y & \n & & \n & \n & \ny \\
\hline
\cnf\ & \n & & \n & & & \n & \n & \nn \\
\hline
\pi\ & & & & & & & & \\
\hline
\ip\ & \y & & \y & & & & & \ny \\
\hline
\mods\ & \y & \y & \y & & & \y & & \ny \\
\hline
\snnf\ & \n & \n & \n & \n &  & \n & \n & \nn \\
\hline
\fnnf\ & \n & \n & \n & \n &  & \n & \n & \nn \\
\hline
\sdDnnf\ & \y & & \y & & & & & \ny \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q5}}
\end{table}
{\bf Table~\ref{tab:q5}:} We now use the following results:
\begin{itemize}
\item[] \cd\ and \co\ imply \ce\ (Lemma~\ref{lem:ce}).
\item[] \cd\ and \va\ imply \im\ (Lemma~\ref{lem:im}).
\item[] \cd\ and \co\ imply \me\ (Lemma~\ref{lem:me}).
\item[] All considered \nnf\ subsets satify \cd\ (cf. Proposition~\ref{prop:transformations}).
\item[] If an \nnf\ subset does not satisfy \co\ it cannot satisfy \me.
\item[] It is well-known that \fbdd\ satisfies \co, \va\ and
\ct, and that \obdd\ satisfies (in addition) \eq\
\cite{GergovMeinel94,Bryant92}.%FBDDMeinel
\item[] Since $\Sigma \models \alpha$ holds iff $\Sigma \wedge \neg
\alpha$ is inconsistent and since \obdd\ satisfies \co, \(\nc\)
and \(\bac\) (cf. Proposition~\ref{prop:transformations}), \obdd\
also satisfies \se.
%4Pierre
\item[] Obviously enough, any query concerning \uobdd\
is equivalent to the corresponding query concerning \obdd\,
provided that only one DAG is brought into play. Together with the
above results, we conclude that \uobdd\ satisfies \co, \va\ and
\ct. Since this fragment satisfies \cd\ as well, it satisfies \ce,
\im\ and \me\ in addition. It also satisfies \eq\ (see Theorem
8.11 from \cite{MeinelTheobald98}) but does not satisfy \se\
(unless {\sf P} = {\sf NP}). Indeed, it is known that checking the
consistency of two \obdd\ formulas $\alpha$ and $\beta$ (based on
two different variable orderings $<$) is {\sf NP}-complete (Lemma
8.14 from \cite{MeinelTheobald98}). Since \uobdd\ satisfies
\(\nc\) and since $\alpha \wedge \beta$ is consistent iff $\alpha
\not \models \neg \beta$, checking sentential entailment for
\uobdd\ formulas is {\sf coNP}-complete.
\end{itemize}
These results lead to the table.



\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n & & \n & \n & \n \\
\hline
\Dnnf\ & \y & \n & \y & \n & & \n & \n & \y \\
\hline
\dnnf\ & & & & & & & & \\
\hline
\dDnnf\ & \y &  & \y & & & & & \y \\
\hline
\bdd\ & & & & & & & &\\
\hline
\fbdd\ & \y & \y & \y & \y & & \y & & \y \\
\hline
%4Pierre
\uobdd\ & \y & \y & \y & \y & \y & \y & \n & \y \\
\hline
\obdd\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\dnf\ & \y & \n & \y & \n & & \n & \n & \y \\
\hline
\cnf\ & \n & \ny & \n & \ny & & \n & \n & \n \\
\hline
\pi\ & & \ny & & \ny & & & & \\
\hline
\ip\ & \y & & \y & & & & & \y \\
\hline
\mods\ & \y & \y & \y & & & \y & & \y \\
\hline
\snnf\ & \n & \n & \n & \n &  & \n & \n & \n \\
\hline
\fnnf\ & \n & \n & \n & \n &  & \n & \n & \n \\
\hline
\sdDnnf\ & \y & & \y & & & & & \y \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q6}}
\end{table}
{\bf Table~\ref{tab:q6}:} It is known that \im\ is satisfied by
classical CNF formulas (hence, \pi) (in order to check whether a
non-valid clause is implied by a consistent term, it is
sufficient to test that they share a literal). \cnf\ (hence, \pi)
is also known to satisfy \va. We then obtain the table.


\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n & & \n & \n & \n \\
\hline
\Dnnf\ & \y & \n & \y & \n & & \n & \n & \y \\
\hline
\dnnf\ & \nn & \nn & \nn & \nn & & \nn & \nn & \nn \\
\hline
\dDnnf\ & \y &  & \y &  & & & & \y \\
\hline
\bdd\ & \nn & \nn & \nn & \nn & & \nn & \nn & \nn \\
\hline
\fbdd\ & \y & \y & \y & \y & & \y & & \y \\
\hline
%4Pierre
\uobdd\ & \y & \y & \y & \y & \y & \y & \n & \y \\
\hline
\obdd\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\dnf\ & \y & \n & \y & \n & & \n & \n & \y \\
\hline
\cnf\ & \n & \y & \n & \y & & \n & \n & \n \\
\hline
\pi\ & & \y & & \y & & & & \\
\hline
\ip\ & \y & & \y & & & & & \y \\
\hline
\mods\ & \y & \y & \y & & & \y & &\\
\hline
\snnf\ & \n & \n & \n & \n &  & \n & \n & \n \\
\hline
\fnnf\ & \n & \n & \n & \n &  & \n & \n & \n \\
\hline
\sdDnnf\ & \y & & \y & & & & & \y \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q7}}
\end{table}
{\bf Table~\ref{tab:q7}:} Every sentence in \cnf\ or \dnf\ can be
turned into an equivalent sentence in \bdd\ in polytime
(Lemma~\ref{lem:bdd}). Hence, a \n\ in a \cnf\ or \dnf\ cell
implies a \n\ in the corresponding \bdd\ cell. Similarly, since
\bdd\ $\subseteq$ \dnnf, a \n\ in a \bdd\ cell implies a \n\ in
the corresponding \dnnf\ cell. This leads to the table.


\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n & \nn & \n & \n & \n \\
\hline
\Dnnf\ & \y & \n & \y & \n & \nn & \n & \n & \y \\
\hline
\dnnf\ & \n & \n & \n & \n & \nn & \n & \n & \n \\
\hline
\dDnnf\ & \y &  & \y & & & & & \y \\
\hline
\bdd\ & \n & \n & \n & \n & \nn & \n & \n & \n \\
\hline
\fbdd\ & \y & \y & \y & \y & & \y & & \y \\
\hline
%4Pierre
\uobdd\ & \y & \y & \y & \y & \y & \y & \n & \y \\
\hline
\obdd\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\dnf\ & \y & \n & \y & \n & \nn & \n & \n & \y \\
\hline
\cnf\ & \n & \y & \n & \y & \nn & \n & \n & \n \\
\hline
\pi\ & & \y & & \y & & & & \\
\hline
\ip\ & \y & & \y & & & & & \y \\
\hline
\mods\ & \y & \y & \y & & & \y & & \y \\
\hline
\snnf\ & \n & \n & \n & \n & \nn  & \n & \n & \n \\
\hline
\fnnf\ & \n & \n & \n & \n & \nn & \n & \n & \n \\
\hline
\sdDnnf\ & \y & & \y & & & & & \y \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q8}}
\end{table}
{\bf Table~\ref{tab:q8}:} Since \eq\ implies \co\ and \va\
(Lemma~\ref{lem:eq}), a \n\ in a \co\ or \va\ cell implies a \n\
in the corresponding \eq\ cell. This leads to the table.




\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\Dnnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\dnnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\dDnnf\ & \y &  & \y & & & & & \y \\
\hline
\bdd\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\fbdd\ & \y & \y & \y & \y & & \y & & \y \\
\hline
%4Pierre
\uobdd\ & \y & \y & \y & \y & \y & \y & \n & \y \\
\hline
\obdd\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\dnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\cnf\ & \n & \y & \n & \y & \n & \n & \n & \n \\
\hline
\pi\ & \ny & \y & \ny & \y & \ny & \nn & \ny & \ny \\
\hline
\ip\ & \y & \ny & \y & \ny & \ny & \nn & \ny & \y \\
\hline
\mods\ & \y & \y & \y & & & \y & & \y \\
\hline
\snnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\fnnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\sdDnnf\ & \y & & \y & & & & & \y \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q9}}
\end{table}
{\bf Table~\ref{tab:q9}:} By definition, \pi\ satisfies \ce\ and
\ip\ satisfies \im. Since \pi\ $\subseteq$ \cnf\ and \ip\
$\subseteq$ \dnf, this implies that both \pi\ and \ip\ satisfy
\se. Now, \se\ implies \eq, hence both \pi\ and \ip\ satisfy \eq\
(actually, two equivalent formulas share the same prime
implicates and the same prime implicants (both forms are
canonical ones, provided that one representative per equivalence
class is considered, only)).
%(** Pierre: is this true??? **))).
%3Pierre: yes, I added ``provided that one representative per equivalence
%class is considered, only'' to make it more correct (e.g. $a$ and
%$a \vee a$ are the same prime implicate of formula $a$).
Since \pi\ satisfies \ce, it also satisfies \co. Since it
satisfies \cd\ as well (cf.
Proposition~\ref{prop:transformations}), it also satisfies \me\
(Lemma~\ref{lem:me}). Contrastingly, the models counting problem
for monotone Krom formulas (i.e. conjunctions of clauses
containing at most two literals and only positive literals) is
{\sf \#P}-complete
%5Pierre: I removed ``(see ...)''.
\cite{Roth96}. Such formulas can
easily be turned into prime implicates form in polynomial time
%5Pierre: I removed ``(see ...)''.
\cite{Marquis00}, hence \pi\ does not satisfy \ct. Now,
since the negation of a formula $\Sigma$ in prime implicates form
is a formula in prime implicants form
%(** Pierre: reference? **)
%3Pierre: done.
(cf. Lemma \ref{lem:pivsip}), and since the number of models of $\neg
\Sigma$ over $\vars(\Sigma)$ is $2^{|\vars(\Sigma)|}$ minus the
number of models of $\Sigma$ over $\vars(\Sigma)$, we necessarily
have that \ip\ does not satisfy \ct. This also imply that \ip\
satisfies \va, leading to the table.



\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\Dnnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\dnnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\dDnnf\ & \y &  & \y & & & & & \y \\
\hline
\bdd\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\fbdd\ & \y & \y & \y & \y & & \y & & \y \\
\hline
%4Pierre
\uobdd\ & \y & \y & \y & \y & \y & \y & \n & \y \\
\hline
\obdd\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\dnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\cnf\ & \n & \y & \n & \y & \n & \n & \n & \n \\
\hline
\pi\ & \y & \y & \y & \y & \y & \n & \y & \y \\
\hline
\ip\ & \y & \y & \y & \y & \y & \n & \y & \y \\
\hline
\mods\ & \y & \y & \y & \ny & \ny & \y & \ny & \y \\
\hline
\snnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\fnnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\sdDnnf\ & \y & & \y & & & & & \y \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q10}}
\end{table}
{\bf Table~\ref{tab:q10}:} In the proof of
Proposition~\ref{prop:succinctness}, we
%5Pierre: ``will show'' is replaced by ``have shown''
have shown that the prime
implicants of $\Sigma$ can be computed in polytime from a \mods\
representation of $\Sigma$. As an immediate consequence, since
\ip\ satisfies \im, \eq\ and \se, we obtain that \mods\ satisfies
\im, \eq\ and \se, leading to the table.



\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\Dnnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\dnnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\dDnnf\ & \y & \ny & \y & \ny & & \ny & & \y \\
\hline
\bdd\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\fbdd\ & \y & \y & \y & \y & & \y & & \y \\
\hline
%4Pierre
\uobdd\ & \y & \y & \y & \y & \y & \y & \n & \y \\
\hline
\obdd\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\dnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\cnf\ & \n & \y & \n & \y & \n & \n & \n & \n \\
\hline
\pi\ & \y & \y & \y & \y & \y & \n & \y & \y \\
\hline
\ip\ & \y & \y & \y & \y & \y & \n & \y & \y \\
\hline
\mods\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\snnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\fnnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\sdDnnf\ & \y & \ny & \y & \ny & & \ny & & \y \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q11}}
\end{table}
{\bf Table~\ref{tab:q11}:} Since \dDnnf\ satisfies \ct\
\cite{darwicheJANCL}, it also satisfies \va. Since it satisfies
\cd\ (Proposition~\ref{prop:transformations}), it also satisfies
\im\ as well (Lemma~\ref{lem:im}). Since \sdDnnf\ \(\subseteq\)
\dDnnf, these results follow for \sdDnnf. Hence, we obtain the
table.



\begin{table}
\begin{center}\begin{tiny}
\begin{tabular}{|c|c|c|c|c|c|c|c|c|}\hline
\L\ & \co\ & \va\ & \ce\ & \im\ & \eq\ & \ct\ & \se\ & \me\ \\
\hline
\hline \nnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\Dnnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\dnnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\dDnnf\ & \y & \y & \y & \y & & \y & \nn & \y \\
\hline
\bdd\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\fbdd\ & \y & \y & \y & \y & & \y & \nn & \y \\
\hline
%4Pierre
\uobdd\ & \y & \y & \y & \y & \y & \y & \n & \y \\
\hline
\obdd\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\dnf\ & \y & \n & \y & \n & \n & \n & \n & \y \\
\hline
\cnf\ & \n & \y & \n & \y & \n & \n & \n & \n \\
\hline
\pi\ & \y & \y & \y & \y & \y & \n & \y & \y \\
\hline
\ip\ & \y & \y & \y & \y & \y & \n & \y & \y \\
\hline
\mods\ & \y & \y & \y & \y & \y & \y & \y & \y \\
\hline
\snnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\fnnf\ & \n & \n & \n & \n & \n & \n & \n & \n \\
\hline
\sdDnnf\ & \y & \y & \y & \y & & \y & \nn & \y \\
\hline
\end{tabular}
\end{tiny}\end{center}
\caption{\label{tab:q12}}
\end{table}
{\bf Table~\ref{tab:q12}:} It is known that determining whether
the conjunction of two \fbdd\ formulas $\alpha_1$ and $\alpha_2$
is consistent is {\sf NP}-complete \cite{GergovMeinel94b}
%(** Pierre: is this the correct reference? **).
%3Pierre: the referenced paper is by Gergov and Meinel in 94
%but that's not that one. I will check in the .bbl file
%and I changed the key here.
Moreover, \fbdd\
satisfies \(\nc\). Since \(\alpha_1\wedge\alpha_2\) is
inconsistent iff \(\alpha_1 \models \neg \alpha_2\), we can
reduce the consistency test into an entailment test. Hence,
\fbdd\ does not satisfy \se. Since \fbdd\ \(\subseteq\) \dDnnf,
\dDnnf\ does not satisfy \se\ either. Finally, since every
\dDnnf\ can be translated into an equivalent \sdDnnf\ sentence in
polytime (Lemma~\ref{lem:sd-DNNF}), \sdDnnf\ does not satisfy
\se\ either. This leads to the final table above.~\qed



\subsection*{Proof of Proposition~\ref{prop:transformations}}

%5Pierre: I add a comment to explain how we proceeded
%6Adnan: I changed this part as it was not accurate

The proof of this proposition is broken down into eight steps.
Each step corresponds to one of the transformations, where we
prove all results pertaining to that transformation.

%Here again, let us explain why the results hold in a progressive way
%through a number of intermediate tables. For the ease of reading,
%the new results derived at each step (i.e., those that were not
%reported in the previous intermediate tables) are marked.

\begin{itemize}
\item \cd. To show that a language \L\ satisfies \cd, we want to show
that for any sentence \(\Sigma \in \L\) and any consistent term
\(\gamma\), we can construct in polytime a sentence which belongs
to \L\ and is equivalent to \(\Sigma \mid \gamma\).
\begin{itemize}
\item \nnf, \fnnf, \cnf\ and \dnf. The property is
trivially satisfied by these languages: If \(\Sigma\) belongs to
any of these languages, then replacing the literals of $\gamma$
by a Boolean constant in $\Sigma$ results a sentence in the same
language. In the case of \dnf\ (resp. \cnf), some inconsistent
terms (valid clauses) may result through conditioning, but these
can be removed easily in polynomial time.

\item \Dnnf. It is sufficient to prove that conditioning preserves
decomposability. For every propositional sentences $\alpha$,
$\beta$ and every consistent term $\gamma$, if $\alpha$ and
$\beta$ do not share variables, then $\alpha | \gamma$ and $\beta
| \gamma$ do not share variables either since $\vars(\alpha |
\gamma) \subseteq \vars(\alpha)$ and $\vars(\beta | \gamma)
\subseteq \vars(\beta)$.

\item \dnnf\ and \dDnnf. Since \nnf\ and \Dnnf\
satisfy \cd, it is sufficient to prove that conditioning
preserves determinism, i.e. for every propositional formulas
$\alpha$, $\beta$ and every consistent term $\gamma$, if $\alpha
\wedge \beta \models$ \false, then $(\alpha | \gamma) \wedge
(\beta | \gamma) \models$ \false. If $\alpha \wedge \beta
\models$ \false, then for every term $\gamma$, we have $(\alpha
\wedge \beta) \wedge \gamma \models$ \false. Since $(\alpha
\wedge \beta) \wedge \gamma \equiv ((\alpha \wedge \beta)|\gamma)
\wedge \gamma$, this implies that $((\alpha \wedge \beta)|\gamma)
\wedge \gamma \models$ \false. Since $\gamma$ is consistent and
share no variable with $(\alpha \wedge \beta)|\gamma$, it must be
the case that $(\alpha \wedge \beta)|\gamma$ is inconsistent.
This is equivalent to state that $(\alpha | \gamma) \wedge (\beta
| \gamma) \models$ \false.

\item \snnf\ and \sdDnnf. Since \nnf\ satisfies \cd, and since
conditioning preserves decomposability and determinism, all we
have to show is that conditioning also preserves smoothness. This
follows immediately since for two propositional sentences
\(\alpha\), \(\beta\) and a consistent term \(\gamma\), we have
\(\vars(\alpha)=\vars(\beta)\) only if
\(\vars(\alpha\mid\gamma)=\vars(\beta\mid\gamma)\).

%4Pierre
\item \bdd, \fbdd, \uobdd\ and \obdd.
It is well--known that \bdd\ satisfies \cd---the conditioning
operation on binary decision diagrams is known as the {\em
restrict} operation \cite{Bryant86}. To condition a sentence
\(\Sigma\) in \bdd\ on a consistent term \(\gamma\), we replace
every node labeled by a variable in $\gamma$ by one of its two
children, according to the sign of the variable in $\gamma$. The
resulting sentence is also a \bdd\ and is equivalent to
\(\Sigma\mid\gamma\). The same applies to \fbdd, \uobdd\ and \obdd.

\item \pi. The prime implicates of $\Sigma \wedge \gamma$ can be computed in
polytime when $\Sigma$ is in prime implicates form and $\gamma$
is a term (see Proposition 36 in \cite{Marquis00}). Moreover,
since \pi\ satisfies \fo\ (see below), the prime implicates of
$\exists \vars(\gamma).(\Sigma \wedge \gamma)$ can be computed in
polytime. But these are exactly the prime implicates of \(\Sigma
\mid \gamma\) according to Lemma~\ref{lem:cdviafo}.

\item \ip. Let $\Sigma = \bigvee_{i=1}^n \gamma_i$ be a
formula in prime implicants form. It is clear that the formula
%6Pierre: I added some parentheses here.
$(\bigvee_{i=1}^n \gamma_i) \mid \gamma$ is a DNF formula equivalent to
$\Sigma \mid \gamma$. Now, our claim is that the formula $\Sigma*$
obtained by keeping only the logically weakest terms $\gamma_i \mid
\gamma$ among $(\bigvee_{i=1}^n \gamma_i) \mid \gamma$ is a prime
implicants formula equivalent to $\Sigma \mid \gamma$. Removing such
terms clearly is truth-preserving. Since generating $\Sigma*$
requires only ${\cal 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 $\Sigma*$
is in prime implicants form? Since any pair of different terms of
$\Sigma*$ 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 $\Sigma*$ is inconsistent or entails
another term of $\Sigma*$. Let's recall that consensus is to DNF
formulas what resolution is to CNF formulas. Since $\Sigma$ is in
prime implicants form,
%6Pierre: I removed ``it also satisfies this property:''
every consensus among two terms of $\Sigma$ is inconsistent or entails
another term of $\Sigma$. What happens to the terms (here, the
prime implicants) of $\Sigma$ when conditioned by $\gamma$? All
those containing the negation of a literal of $\gamma$ are
removed and the remaining ones are shortened by removing from
them every literal of $\gamma$. Hence, for every pair of terms
$\gamma_1$, $\gamma_2$ of $\Sigma$, if there is no consensus
between $\gamma_1$ and $\gamma_2$, then there is no consensus
between $\gamma_1 | \gamma$ and $\gamma_2 | \gamma$: conditioning
cannot create new consensus. Now, it remains to prove that no
unproductive consensus between terms of $\Sigma$ can be rendered
productive through conditioning. Formally, let $\gamma_1 =
\gamma'_1 \wedge l$ and $\gamma_2 = \gamma'_2 \wedge \neg l$ be
two prime implicates of $\Sigma$ s.t. $l$ (resp. $\neg l$) does
not appear in $\gamma'_1$ (resp. $\gamma'_2$). There is a
consensus $\gamma'_1 \wedge \gamma'_2$ between $\gamma_1$ and
$\gamma_2$. Let us assume that both $\gamma_1$ and $\gamma_2$
have survived the conditioning: this means that both $\gamma_1 |
\gamma$ and $\gamma_2 | \gamma$ are consistent. Especially, $l$
belongs to $\gamma_1 | \gamma$ and $\neg l$ belongs to $\gamma_2
| \gamma$. Accordingly, there is a consensus between $\gamma_1 |
\gamma$ and $\gamma_2 | \gamma$. By construction, this consensus
is equivalent to $(\gamma'_1 | \gamma) \wedge (\gamma'_2 |
\gamma)$, hence equivalent to $(\gamma'_1 \wedge \gamma'_2) |
\gamma$. Now, if $\gamma'_1 \wedge \gamma'_2$ is inconsistent,
then $(\gamma'_1 \wedge \gamma'_2) | \gamma$ is inconsistent as
well and we are done. Otherwise, let us assume that there exists
a prime implicant $\gamma_3$ of $\Sigma$ s.t. $\gamma'_1 \wedge
\gamma'_2 \models \gamma_3$ holds. Necessarily, $\gamma_3$ is
preserved by the conditioning of $\Sigma$ by $\gamma$. Otherwise,
$\gamma_3$ would contain the negation of a literal of $\gamma$,
but since every literal of $\gamma_3$ is a literal of $\gamma_1$
or a literal of $\gamma_2$, $\gamma_2$ and $\gamma_3$ would not
have both survived the conditioning. Since $\gamma'_1 \wedge
\gamma'_2 \models \gamma_3$ holds, we necessarily have
$(\gamma'_1 \wedge \gamma'_2) | \gamma \models \gamma_3 |
\gamma$. This completes the proof.

\item \mods. Direct consequence of Lemma \ref{lem:cdviafo} and the fact that
\mods\ satisfies \(\bac\) and \fo\ (see below).
\end{itemize}


\item \fo.
\begin{itemize}
\item \Dnnf\ and \dnf. It is known that
\Dnnf\ satisfies \fo\ \cite{darwicheJACM-DNNF}. It is also known
that \dnf\ satisfies \fo\
%5Pierre: I removed ``(see ...)''.
\cite{LangLiberatoreMarquis00a}.

\item \nnf, \snnf, \fnnf, \dnnf, \bdd\ and \cnf. Let \(\Sigma\) be
a sentence in \cnf. We now show that if any of the previous
languages satisfies \fo, then we can test the consistency of
\(\Sigma\) in polytime. Since \cnf\ does not satisfy \co\ (see
Proposition~\ref{prop:queries}), it then follows that none of the
previous languages satisfy \fo\ unless {\sf P} = {\sf NP}. First,
we note that \(\Sigma\) must also belong to \nnf\ and \fnnf.
Moreover, \(\Sigma\) can be turned into a sentence in \bdd\ in
polytime (Lemma~\ref{lem:bdd}) or a sentence in \snnf\ in
polytime (see the proof of Lemma~\ref{lem:sd-DNNF}). We also have
that \(\Sigma\) can be turned into a sentence in \dnnf\ in
polytime since \bdd\ $\subseteq$ \dnnf. Suppose now that one of
the previous languages, call it \L, satisfy \fo. We can test the
consistency of \(\Sigma\) in polytime as follows:
\begin{itemize}
\item Convert \(\Sigma\) into a sentence \(\Sigma*\) in \L\ in
polytime (as shown above).

\item Compute \(\exists \vars(\Sigma*) . \Sigma*\), which can be
done in polytime by assumption.

\item Test the validity of \(\exists \vars(\Sigma*) . \Sigma*\),
which can be done in polytime since the sentence contains no
variables---all we have to do is check whether the sentence
evaluates to \(\true\).

\end{itemize}
Finally, note that the definition of forgetting implies that a
sentence $\Gamma$ is consistent iff $\exists \vars(\Gamma) .
\Gamma$ is valid, which completes the proof.

\item \dDnnf\ and \sdDnnf.
Follows immediately since none of these languages satisfies \sfo\
unless {\sf P} = {\sf NP} (see below).

\item \ip. Follows immediately since \ip\ does not satisfy \sfo.

%4Pierre
\item \fbdd, \uobdd\ and \obdd.
We will show that if \fbdd\ (resp. \uobdd, \obdd) satisfies \fo, then for
every sentence \(\Gamma\) in \dnf, there must exist an equivalent
sentence \(\Sigma\) in \fbdd\ (resp. \uobdd, \obdd), which size is
polynomial in the size of \(\Gamma\). This contradicts the fact
that \fbdd\ (resp. \uobdd, \obdd) \nas\ \dnf---see
Table~\ref{tab:succinctness}.

Given a \dnf\ \(\Gamma\) consisting of terms $\gamma_1$, ...,
$\gamma_n$, we can convert each of these terms into equivalent
\fbdd\ (resp. \uobdd, \obdd) sentences
\(\alpha_1,\ldots,\alpha_n\) in polytime. Let \(\{v_1, \ldots,
v_{n-1}\}\) be a set of variables that do not belong to $\ps$.
Construct a new set of variables \(\ps^\prime = \ps\ \cup \{v_1,
\ldots, v_{n-1}\}\). In case of \uobdd\ and \obdd, we also assume
that these new variables are earlier than variables $\ps$ in the
ordering. Consider now the sentence $\Sigma = \exists \{v_1,
\ldots, v_{n-1}\}. \Delta^1$, with respect to variables
\(\ps^\prime\), where $\Delta^i$ is inductively defined by:
\begin{itemize}
\item $\Delta^i = \alpha_i$, for \(i=n\), and
\item $\Delta^i = (\alpha_i \wedge v_i) \vee (\Delta^{i+1} \wedge
\neg v_i)$, for \(i=1,\ldots,n-1\).
\end{itemize}
Clearly enough, an \fbdd\ (resp. \uobdd, \obdd) sentence equivalent to
$\Delta^1$ can be computed in time polynomial in the input size.
Moreover, we have $\Sigma \equiv \bigvee_{i=1}^n \alpha_i \equiv
\bigvee_{i=1}^n \gamma_i \equiv \Gamma$. Hence, if \fbdd\ (resp.
\uobdd, \obdd) satisfies \fo, then we can convert the \dnf\ sentence
\(\Gamma\) into an equivalent \fbdd\ (resp. \uobdd, \obdd) which size is
polynomial in the size of the given \dnf. This is impossible in
general.

\item \pi. It is known that the prime implicates of $\exists
X . \Sigma$ are exactly the prime implicates of $\Sigma$ that do
not contain any variable from $X$ (see Proposition 55 in
\cite{Marquis00}). Hence, such prime implicates can be computed
in time polynomial in the input size when $\Sigma$ is in prime
implicates form.

\item \mods. Given a \mods\ formula $\Sigma$ and a subset $X$
of $\ps$, the formula obtained by removing every leaf node (and
the corresponding incoming edges) of $\Sigma$ labeled by a literal
$x$ or $\neg x$ s.t. $x \in X$ is a \mods\ representation of
$\exists X. \Sigma$---this is an easy consequence of Propositions
18 and 20 from \cite{LangLiberatoreMarquis00a}. See also the
polytime operation of forgetting on \Dnnf, as defined in
\cite{darwicheJACM-DNNF}, which applies to \mods, since\\
\mods\ \(\subseteq\) \Dnnf, and which can be easily modified so it
guarantees that the output is in \mods\ when the input is also in
\mods.

\end{itemize}


\item  \sfo.
\begin{itemize}
\item \Dnnf, \dnf, \pi\ and \mods. Immediate from the fact
that each of these languages satisfies \fo\ (see above).

\item \nnf, \dnnf, \snnf, \fnnf, \bdd, \obdd\ and \cnf.
Direct from the fact that $\exists x. \Sigma \equiv (\Sigma | x)
\vee (\Sigma | \neg x)$ holds and the fact that any of these
fragments satisfies \cd\ and \(\boc\).

%4Pierre
\item \uobdd. Direct from the fact that only one \uobdd\ sentence is
considered in the transformation and \obdd\ satisfies \sfo.

%4Pierre: updated
%\item \dnnf. Unknown.

\item \dDnnf, \sdDnnf\ and \fbdd.
Let $\alpha_1$ and $\alpha_2$ be two \fbdd\ formulas. Let $x$ be
a variable not included in $\vars(\alpha_1) \cup \vars(\alpha_2)$.
The formula $\Sigma = (x \wedge \alpha_1) \vee (\neg x \wedge
\alpha_2)$ is a \fbdd\ formula since decomposability and decision
are preserved by this construction. Since $\exists x . \Sigma$ is
equivalent to $\alpha_1 \vee \alpha_2$, if \fbdd\ would satisfy
\sfo, it would satisfy \(\boc\) as well, but this is not the case
unless {\sf P} = {\sf NP} (see below). The same conclusion can be
drawn for \dDnnf. Hence, \fbdd\ and \dDnnf\ do not satisfy \sfo\
unless {\sf P} = {\sf NP}. Since every \dDnnf\ formula can be
turned in polynomial time into an equivalent \sdDnnf\ formula, we
obtain that \sdDnnf\ does not satisfy \sfo\ unless {\sf P} = {\sf
NP}.

\item \ip.
Let us show that the number of prime implicants of $\exists x .
\Sigma$ can be exponentially greater than the number of prime
implicants of $\Sigma$. Let $\Sigma'$ be the following DNF
formula:

$$\Sigma' = \left( \bigvee_{i=1}^{k} \bigvee_{j=1}^{m} (p_i \wedge
q_{i,j}) \right) \vee \bigwedge_{i=1}^{k} \neg p_i.$$

$\Sigma'$ has $(m+1)^k+mk$ primes implicants
\cite{ChandraMarkowsky78}. Now, let $\Sigma$ be the formula:

$$\Sigma = \left( \bigvee_{i=1}^{k} \bigvee_{j=1}^{m} (x \wedge p_i \wedge
q_{i,j}) \right) \vee (\neg x \wedge \bigwedge_{i=1}^{k} \neg
p_i).$$

Since $\Sigma'$ can be obtained from $\Sigma$ by removing in every
term of $\Sigma$ every occurrence of $x$ and $\neg x$, $\Sigma'$
is equivalent to $\exists \{x\} . \Sigma$ (see
\cite{LangLiberatoreMarquis00a}). Now, $\Sigma$ has only $mk+1$
prime implicants; indeed, every term of it is a prime implicant,
and the converse holds since every term is maximal w.r.t. logical
entailment and every consensus of two terms is inconsistent. This
completes the proof.
%(** Pierre: shouldn't this be a black dot? **)
%3Pierre: yes, I modified it in the paper.
\end{itemize}


\item \(\ac\).
\begin{itemize}
\item \nnf, \snnf, \dnnf, \cnf. The property is trivially
satisfied by these languages since determinism and smoothness are
only concerned with or-nodes. Hence, if
\(\alpha_1,\ldots,\alpha_n\) belong to one of these languages, so
is \(\alpha_1\wedge\ldots\wedge\alpha_n\).

\item \bdd. It is well--known that the conjunction of two BDDs
$\alpha$ and $\beta$ can be easily computed by connecting the
$1$-sink of $\alpha$ to the root of $\beta$ (see proof of
Lemma~\ref{lem:bdd}). The size of the resulting BDD is just the
{\em sum} of the sizes of the respective BDDs of $\alpha$ and
$\beta$. Accordingly, we can repeat this operation $n$ times in
time polynomial in the input size.

\item \fnnf. Direct from the fact that \fnnf\ does not
satisfy \(\bac\).
%3Pierre: new proof. I pu the old one in comments.
%Let us prove that \fnnf\ does not satisfy \(\ac\). Let us consider
%$n$ CNF formulas $\alpha_1$, ..., $\alpha_n$ where $\alpha_i =
%\bigvee_{j=0}^{m-1} (x_{i, 2j} \wedge x_{i, 2j+1})$. Each
%$\alpha_i$, $i \in 1 .. n$, is an \fnnf\ formula. Now the formula
%$\Sigma = \bigwedge_{i=1}^n \alpha_i$ does not have neither a
%polysize CNF representation nor a polysize DNF representation
%because $\Sigma$ has both exponentially many essential prime
%implicates and exponentially many essential prime implicants.
%Specifically, each $\alpha_i$, $i \in 1 .. n$, has $2^m$ essential
%prime implicates; since $\vars(\alpha_i) \cap \vars(\alpha_j) =
%\emptyset$ whenever $i \neq j$, $\Sigma$ has $n.(2^m)$ essential
%prime implicates. As to prime implicants, each $\alpha_i$, $i \in
%1 .. n$, has $m$ essential prime implicants (every term occurring
%in it is such a prime implicant); since $\vars(\alpha_i) \cap
%\vars(\alpha_j) = \emptyset$ whenever $i \neq j$, $\Sigma$ has
%$m^n$ essential prime implicants. Since every \fnnf\ formula can
%be turned into a CNF formula or a DNF formula equivalent to it in
%polynomial time (Lemma~\ref{lem:f-nnf}), it cannot be the case
%that an \fnnf\ formula equivalent to $\Sigma$ can be generated in
%polynomial time from the $n$ \fnnf\ formulas $\alpha_1, \ldots,
%\alpha_n$ (actually, even polynomial space would not be
%sufficient).

\item \fbdd, \uobdd, \obdd, \dnf, \pi\ and \ip.
It is straightforward to convert a clause into an equivalent
formula in any of these languages in polynomial time. In the proof
of Proposition~\ref{prop:succinctness}, we show specific CNF
formulas which cannot be turned into an equivalent \fbdd\ (resp.
\uobdd, \obdd, \dnf, \pi\ and \ip) formulas in polynomial space (see
Tables~\ref{tab:s2} and~\ref{tab:s3}). Hence, such conversion
cannot be accomplished in polynomial time either. This implies
that none of \fbdd, \uobdd, \obdd, \dnf, \pi\ and \ip\ satisfies \(\ac\).

\item \Dnnf, \dDnnf\ and \sdDnnf.
Direct from the fact that none of these languages satisfy \(\bac\)
unless \\
{\sf P} = {\sf NP}.

\item \mods. Let $\Sigma = \bigwedge_{i=1}^n \Sigma_i$, where
$\Sigma_i = (x_{i,1} \vee x_{i,2})$, $i \in 1 .. n$. Each
$\Sigma_i$ has $3$ models over $\vars(\Sigma_i)$. Since $\Sigma$
has $3^n$ models, it does not have a \mods\ representation of size
polynomial in the input size.
\end{itemize}


\item \(\bac\).
\begin{itemize}
\item \nnf, \snnf, \dnnf, \bdd\ and \cnf.
Immediate since each of these languages satisfy \(\ac\) (see
above).

\item \Dnnf, \dDnnf, \sdDnnf, \fbdd\ and \uobdd.
%4Pierre
Checking whether the conjunction of two \obdd\ formulas
$\alpha_1$ and $\alpha_2$ (w.r.t. two different
variable orderings $<$) is consistent is {\sf NP}-complete
(see Lemma 8.14 in \cite{MeinelTheobald98}).
%3Pierre: I changes the key here.
Since \uobdd\ satisfies \co, it cannot
satisfy \(\bac\) unless {\sf P} = {\sf NP}. Since \uobdd\ $\subseteq$ \fbdd\
$\subseteq$ \dDnnf\ $\subseteq$ \Dnnf, and \dDnnf\ and \Dnnf\
satisfy \co, none of them can satisfy \(\bac\) unless {\sf P} =
{\sf NP}. Finally, since every \dDnnf\ formula can be turned in
polynomial time into an equivalent smoothed \dDnnf\ formula and
since \sdDnnf\ satisfies \co, it cannot be the case that \sdDnnf\
satisfy \(\bac\) unless {\sf P} = {\sf NP}.

\item \obdd. Well-known fact \cite{Bryant86}.

\item \fnnf.
Let $\alpha_1 = \bigwedge_{i=0}^{n-1} (x_{2i} \vee x_{2i+1})$ be a
\cnf\ formula and $\alpha_2 = \bigvee_{i=0}^{n-1} (x'_{2i} \wedge
x'_{2i+1})$ a \dnf\ formula. $\alpha_1$ has $2^n$ essential prime
implicants and $n$ essential prime implicates (see the proof of
Proposition \ref{prop:succinctness}, Table \ref{tab:s2}). By
duality, $\alpha_2$ has $n$ essential prime implicants and $2^n$
essential prime implicates. Now, $\alpha_1$ and $\alpha_2$ are
two \fnnf\ formulas. By Lemma \ref{lem:f-nnf}, we know that every
\fnnf\ formula $\beta$ can be turned in polynomial time into a
\cnf\ formula or a \dnf\ formula. If \fnnf\ would satisfy
\(\bac\), then a \fnnf\ formula $\beta$ s.t. $\beta \equiv
\alpha_1 \wedge \alpha_2$ could be computed in time polynomial in
the input size. Hence, either a \cnf\ formula equivalent to
$\alpha_1 \wedge \alpha_2$ or a \dnf\ formula equivalent to
$\alpha_1 \wedge \alpha_2$ could be computed in polytime. But
this is impossible since $\alpha_1 \wedge \alpha_2$ has $n+2^n$
essential prime implicates and $n*2^n$ essential prime implicants.
Hence every \cnf\ (resp. \dnf\ ) formula equivalent to $\alpha_1
\wedge \alpha_2$ has a size exponential in
$|\alpha_1|+|\alpha_2|$.

Note that in the case where the two \fnnf\ formulas \(\alpha_1\)
and \(\alpha_2\) into
consideration can be turned in polynomial time into either
two \cnf\ formulas or two \dnf\ formulas, then a \fnnf\
formula equivalent to \(\alpha_1\wedge\alpha_2\) can be computed
in time polynomial in the input size (this is obvious when
two \cnf\ formulas are considered and the next item of the
proof shows how this can be achieved when two \dnf\ formulas
are considered).
%(** Pierre: I am unable to follow the above proof. Could
%place rephrase or refine? **)
%3Pierre: I'm very sorry, I guess my previous proof was wrong.
%Fortunately, I guess this has no impact on the other proofs.
%I updated Table table:transformations accordingly (two \y replaced
%by two \bn).

\item \dnf\ and \mods. If \(\alpha_1\) and \(\alpha_2\) are
sentences in one of these languages \L, then we can construct a
sentence in \L\ which is equivalent to \(\alpha_1\wedge\alpha_2\)
by simply taking all the conjunctions of one term from
\(\alpha_1\) and one term from \(\alpha_2\), while removing
redundant literals in the resulting terms and removing any
inconsistent terms in the result. The disjunction of all the
resulting terms is a sentence from \L\ equivalent to
\(\alpha_1\wedge\alpha_2\) and it has been computed in polynomial
time.
%(** Pierre: Should this be refined? **)
%3Pierre: I've made a slight change because Cartesian product is
%not defined over terms (but over their sets of models).

\item \pi. Let $\alpha_1 = \bigvee_{i=1}^k p_i$ and $\alpha_2 = \bigwedge_{i=1}^k
\bigwedge_{j=1}^m (\neg p_i \vee q_{i,j})$. Sentence $\alpha_1$
has one prime implicate and $\alpha_2$ has $m*k$ prime
implicates. But $\alpha_1 \wedge \alpha_2$ has $(m+1)^k +m*k$
prime implicates \cite{ChandraMarkowsky78}.
%(** Pierre: check the definition of \(\alpha_1\) **)
%3Pierre: done.

%4Pierre
\item \ip. Let \({\it IP}(\alpha)\) be the set of prime implicants for
\(\alpha\).
%6Pierre: I changed the notation here to keep something similar
%to what was used previously (Table 9).
We have ${\it IP}(\alpha_1 \wedge \alpha_2) =
\max( \{\beta_1 \wedge \beta_2 \ | \ \beta_1 \in {\it
IP}(\alpha_1), \beta_2 \in {\it IP}(\alpha_2)\}, \models)$ (up to logical
equivalence). See e.g., (dual of) Proposition~40 in
\cite{Marquis00}.
\end{itemize}

\newpage

\item \(\oc\).
\begin{itemize}
\item \nnf, \snnf, \Dnnf\ and \dnf. The property is trivially
satisfied by these languages since decomposability is only
concerned with and-nodes, and since every \nnf\ formula can be
turned in polynomial time into an equivalent smoothed \nnf\
formula.

%4Pierre: updated
\item \dnnf\ and \bdd. Direct consequence from the fact that \dnnf\
and \bdd\
%6Pierre: I replaced ``satisfies'' by ``satisfy''.
satisfies both \(\ac\) and \(\nc\). Especially, it is well-known
that the disjunction of two BDDs $\alpha$ and $\beta$ can be
easily computed by connecting the $0$-sink of $\alpha$ to the
root of $\beta$ (see the proof of Lemma~\ref{lem:bdd}). The size
of the resulting BDD is just the {\em sum} of the sizes of the
respective BDDs of $\alpha$ and $\beta$. Accordingly, we can
repeat this operation $n$ times in time polynomial in the input
size.

\item \fnnf. Since \fnnf\ does not satisfy \(\ac\)
but satisfies \(\nc\), it cannot satisfy
\(\oc\) (due to De Morgan's laws).
%(** Pierre: are the (unless {\sf P} = {\sf NP}) needed? Note that
%we have a black dot in both this and in \(\ac\). **)
%3Pierre: no, they are useless. I updated the text accordingly.

%4Pierre
\item \fbdd, \uobdd, \obdd, \cnf, \pi, \ip\ and \mods.
It is straightforward to convert any term into an equivalent
formula from any of the previous languages in polynomial time. In
the proof of Proposition~\ref{prop:succinctness}, we show
specific \dnf\ formulas which cannot be turned into equivalent
\fbdd\ (resp. \uobdd, \obdd, \cnf\ , \pi, \ip\ and \mods) formulas in
polynomial space (see Tables~\ref{tab:s2},~\ref{tab:s3}
and~\ref{tab:s8}). Hence, the conversion cannot be accomplished in
polynomial time either. This implies that none of \fbdd, \uobdd, \obdd,
\cnf, \pi, \ip\ and \mods\ satisfies \(\oc\).

\item \dDnnf\ and \sdDnnf.
Immediate form the fact that none of these classes satisfies
\(\boc\) unless {\sf P} = {\sf NP} (see below).

%4Pierre
%\item \dnnf. Unknown.
\end{itemize}



\item \(\boc\).
\begin{itemize}
%4Pierre: updated
\item \nnf, \dnnf, \Dnnf, \snnf, \bdd\ and \dnf.
Immediate since each of these languages satisfies \(\oc\).

%\item \dnnf. Unknown.

\item \obdd. Well-known fact \cite{Bryant86}.

\item \uobdd, \fbdd, \dDnnf\ and \sdDnnf.
%4Pierre
Checking whether the conjunction of two \obdd\ formulas
$\alpha_1$ and $\alpha_2$ (w.r.t. two different
variable orderings $<$) is consistent is {\sf NP}-complete
(see Lemma 8.14 in \cite{MeinelTheobald98}).
%3Pierre: I changes the key here.
%We know that checking whether
%the conjunction of two \fbdd\ formulas $\alpha_1$ and $\alpha_2$
%is consistent is {\sf NP}-complete \cite{GergovMeinel94b}.
%3Pierre: I updated the key.
Now, $\alpha_1 \wedge \alpha_2$ is inconsistent
%3Pierre: I changed ``consistent'' by ``inconsistent''.
iff $\neg \alpha_1 \vee
\neg \alpha_2$ is valid. Since \uobdd\ satisfies \(\nc\), an
\uobdd\ formula equivalent to $\neg \alpha_1$ (resp. $\neg
\alpha_2$) can be computed in time polynomial in $|\alpha_1|$
(resp. $|\alpha_2|$). Since \uobdd\ $\subseteq$ \fbdd\ $\subseteq$ \dDnnf, the
resulting formulas are also \fbdd\ and \dDnnf\ formulas. If \uobdd\ (resp. \fbdd,
\dDnnf) would satisfy \(\boc\), then an \uobdd\ (resp. \fbdd, \dDnnf)
formula equivalent to $\neg \alpha_1 \vee \neg \alpha_2$ could be
computed in time polynomial in $|\alpha_1|+|\alpha_2|$. But since
\dDnnf\ satisfies \va, this is impossible unless {\sf P} = {\sf
NP}. Finally, since every \dDnnf\ formula can be turned in
polynomial time into an equivalent \sdDnnf\ formula, \sdDnnf\
cannot satisfy \(\boc\) unless {\sf P} = {\sf NP}.

\item \fnnf. Since \fnnf\ does not satisfy \(\bac\)
but satisfies \(\nc\), it cannot satisfy
\(\boc\) (due to De Morgan's laws).
%3Pierre: the proof becomes easier here.
% and \cnf. Every \fnnf\ formula
%can be turned in polynomial time into a DNF or a CNF formula. If
%two \fnnf\ formulas $\alpha_1$ and $\alpha_2$ can be turned in
%polynomial time into DNF formulas, we are done. Otherwise, we
%just have to distribute $\vee$ over $\wedge$ (if the and-node of
%$\alpha_1$ (resp. $\alpha_2$ has $n$ (resp. $m$) outgoing edges,
%the resulting formula is a CNF formula where the and-node has
%$n*m$ outgoing edges).
%(** Pierre: This is symmetric to the proof for \(\bac\). Please
%redo this too when you cleanup the first. **)

%3Pierre: new proof here.
\item \cnf. If \(\alpha_1\) and \(\alpha_2\) are
two \cnf\ sentences, then we can construct a
\cnf\ sentence which is equivalent to \(\alpha_1\vee\alpha_2\)
by simply taking all the disjunctions of one clause from
\(\alpha_1\) and one clause from \(\alpha_2\), while removing redundant literals
inside the resulting clauses and removing any valid clause
in the result. The conjunction of
all the resulting clauses is a \cnf\ sentence
equivalent to \(\alpha_1\vee\alpha_2\), and it
has been computed in polynomial time.

\item \pi. Let \({\it PI}(\alpha)\) be the set of prime implicates for
sentence \(\alpha\).
%6Pierre: I changed the notation here to keep something similar
%to what was used previously (Table 9).
We have ${\it PI}(\alpha_1 \vee \alpha_2) =
\min(\{\beta_1 \vee \beta_2 \ | \ \beta_1 \in {\it
PI}(\alpha_1), \beta_2 \in {\it PI}(\alpha_2)\}, \models)$. See
Proposition~40 in \cite{Marquis00}.

\item \ip. Let $\alpha_1 = \bigwedge_{i=1}^k p_i$ and $\alpha_2 = \bigvee_{i=1}^k
\bigvee_{j=1}^m (\neg p_i \wedge q_{i,j})$. Sentence $\alpha_1$
has one prime implicant and $\alpha_2$ has $m*k$ prime
implicants. But $\alpha_1 \vee \alpha_2$ has $(m+1)^k +m*k$ prime
implicants \cite{ChandraMarkowsky78}.
%(** Pierre: Please check the definition of \(\alpha_1\). **)
%3Pierre: done.


\item \mods. Let $\alpha_1 = \bigwedge_{i=1}^n x_i$ and $\alpha_2 = y$.
Sentence $\alpha_1$ has $1$ model over $\vars(\alpha_1)$ and
$\alpha_2$ has $1$ model over $\vars(\alpha_2)$. But $\alpha_1
\vee \alpha_2$ has $2^n + 1$ models over $\vars(\alpha_1) \cup
\vars(\alpha_2)$.
\end{itemize}


\item \(\nc\).
\begin{itemize}
%4Pierre
\item \nnf, \snnf, \fnnf, \bdd, \fbdd, \uobdd\ and \obdd. The
property is obviously satisfied by \nnf. \snnf\ also satisfies
\(\nc\) since every \nnf\ formula can be turned in polynomial
time into an equivalent \snnf\ formula. \fnnf\ satisfies \(\nc\)
since applying De Morgan's laws on a \fnnf\ formula results in a
\fnnf\ formula. Finally, for all the forms of BDDs, it is
sufficient to switch the labels of the sinks to achieve negation
\cite{Bryant86}.

\item \cnf. Because the negation of a \dnf\ formula is a \cnf\
formula that can be computed in polynomial time, if \cnf\ would
satisfy \(\nc\), then it would be possible to turn any \dnf\
formula into an equivalent \cnf\ formula in polynomial time (by
involution of negation). But we know that it is not possible in
polynomial space since \cnf\ \nas\ \dnf (see the proof of
Proposition~\ref{prop:succinctness}). Hence, \cnf\ does not
satisfy \(\nc\).

\item \dnf. Dual of the proof just above (just replace \cnf\ by
\dnf\ and {\it vice-versa}).

\item \pi. The formula $\Sigma_n = \bigwedge_{i=0}^{n-1} (x_{2i} \vee x_{2i+1})$
is in prime implicates form (see the proof of Proposition \ref{prop:succinctness},
Table \ref{tab:s2}).
%(** Pierre: ref? **)
%3Pierre: done.
This formula has
exponentially many prime implicants, that are just the negations
of the prime implicates of $\neg \Sigma_n$. Since $\neg \Sigma_n$
has exponentially many prime implicates, it cannot be the case
that \pi\ satisfies \(\nc\).

\item \ip. We just have to take the dual of the above proof
(prime implicates case). The formula\\
$\Sigma_n =
\bigvee_{i=0}^{n-1} (x_{2i} \wedge x_{2i+1})$ is in prime
implicants form. This formula has exponentially many prime
implicates, that are just the negations of the prime implicants of
$\neg \Sigma_n$. Since $\neg \Sigma_n$ has exponentially many
prime implicants, it cannot be the case that \ip\ satisfies
\(\nc\).

\item \Dnnf. The negation of any \cnf\ formula can be computed
in polynomial time as a \dnf\ formula, hence as a \Dnnf\ formula.
If \Dnnf\ would satisfy \(\nc\), then it would be possible to
turn a \cnf\ formula into an equivalent \Dnnf\ one (by involution
of negation). Because \Dnnf\ satisfies \co, we would have {\sf P}
= {\sf NP}.

%4Pierre
\item \dnnf.
Following is a procedure for negating a \dnnf\ sentence
\(\Delta\):\footnote{Mark Hopkins pointed us to this procedure.}
\begin{itemize}
\item Traverse nodes in the DAG of \(\Delta\), visiting
the children of a node before you visit the node itself. When
visiting a node, construct its negation as follows:
\begin{itemize}
\item \(\true\) is the negation of \(\false\).
\item \(\false\) is the negation of \(\true\).
\item \(\wedge(N_1^\prime,\ldots,N_k^\prime)\) is the negation of
\(\vee(N_1,\ldots,N_k)\). Here, \(N_i^\prime\) is the node
representing the negation of \(N_i\).
\item \(\vee(\wedge(N_1^\prime,M_1),\ldots,\wedge(N_k^\prime,M_k))\) is the negation of
\(\wedge(N_1,\ldots,N_k)\). Here, \(N_i^\prime\) is the node
representing the negation of \(N_i\), and \(M_i\) is a node
representing the conjunction \(N_1\wedge\ldots\wedge N_{i-1}\).
\end{itemize}
\item Return the negation of the root of \dnnf\ \(\Delta\).
\end{itemize}

We can implement the above four steps so that we when we visit a
node with \(k\) children, we only construct \(O(k)\) nodes and
\(O(k)\) edges.\footnote{We assume that any or-node (resp.
and-node) with less than two children is removed and replaced by
its unique child or by $false$ (resp. $true$) if it has no
children. This simplification process is equivalence-preserving
and it can be achieved in time linear in the size of the input
DAG.} Hence, the procedure complexity is linear in the size of the
original \dnnf. It is easy to check that the result is equivalent
to the negation of the given \dnnf\ sentence and is also in \dnnf.


\item \sdDnnf\ and \dDnnf. Unknown.

\item \mods. $\Sigma =\bigwedge_{i=1}^n x_i$ has only one model over
$\bigcup_{i=1}^n \{x_i\}$ but its negation $\neg \Sigma$ has $2^n
- 1$ models over $\bigcup_{i=1}^n \{x_i\}$. Hence \mods\ cannot
satisfy \(\nc\).~\qed
\end{itemize}
\end{itemize}


\begin{thebibliography}{}

\bibitem[\protect\BCAY{A.~Cimmati\ \BBA\ Traverso}{A.~Cimmati\ \BBA\
  Traverso}{1997}]{Cimattietal97}
A.~Cimmati, E.~Giunchiglia, F.~G.\BBACOMMA\  \BBA\ Traverso, P.
\BBOP1997\BBCP.
\newblock \BBOQ Planning via model checking: a decision procedure for {${\cal
  AR}$}\BBCQ\
\newblock In {\Bem Proceedings of the $4^{th}$ European Conference on Planning
  (ECP'97)}, \BPGS\ 130--142.

\bibitem[\protect\BCAY{Blum, Chandra,\ \BBA\ Wegman}{Blum
  et~al.}{1980}]{Blumetal80}
Blum, M., Chandra, A.~K., \BBA\ Wegman, M.~N. \BBOP1980\BBCP.
\newblock \BBOQ Equivalence of free {Boolean} graphs can be decided
  probabilistically in polynomial time\BBCQ\
\newblock {\Bem Information Processing Letters}, {\Bem 10\/}(2), 80--82.

\bibitem[\protect\BCAY{Boole}{Boole}{1854}]{Boole54}
Boole, G. \BBOP1854\BBCP.
\newblock {\Bem An investigation of the laws of thought}.
\newblock Walton and Maberley, London.

\bibitem[\protect\BCAY{Boufkhad, Gr\'egoire, Marquis, Mazure,\ \BBA\
  Sa\"{\i}s}{Boufkhad et~al.}{1997}]{Boufkhadetal97}
Boufkhad, Y., Gr\'egoire, E., Marquis, P., Mazure, B., \BBA\
Sa\"{\i}s, L.
  \BBOP1997\BBCP.
\newblock \BBOQ Tractable cover compilations\BBCQ\
\newblock In {\Bem Proc. of the $15^{th}$ International Joint Conference on
  Artificial Intelligence (IJCAI'97)}, \BPGS\ 122--127, Nagoya.

\bibitem[\protect\BCAY{Bryant}{Bryant}{1986}]{Bryant86}
Bryant, R.~E. \BBOP1986\BBCP.
\newblock \BBOQ Graph-based algorithms for {Boolean} function
  manipulation\BBCQ\
\newblock {\Bem IEEE Transactions on Computers}, {\Bem C-35}, 677--691.

\bibitem[\protect\BCAY{Bryant}{Bryant}{1992}]{Bryant92}
Bryant, R.~E. \BBOP1992\BBCP.
\newblock \BBOQ Symbolic {Boolean} manipulation with ordered binary decision
  diagrams\BBCQ\
\newblock {\Bem ACM Computing Surveys}, {\Bem 24\/}(3), 293--318.

\bibitem[\protect\BCAY{Cadoli\ \BBA\ Donini}{Cadoli\ \BBA\
  Donini}{1997}]{CadoliDonini97}
Cadoli, M.\BBACOMMA\  \BBA\ Donini, F. \BBOP1997\BBCP.
\newblock \BBOQ A survey on knowledge compilation\BBCQ\
\newblock {\Bem AI Communications}, {\Bem 10}, 137--150.
\newblock (printed in 1998).

\bibitem[\protect\BCAY{Cadoli, Donini, Liberatore,\ \BBA\ Schaerf}{Cadoli
  et~al.}{1996}]{Cadolietal96b}
Cadoli, M., Donini, F., Liberatore, P., \BBA\ Schaerf, M.
\BBOP1996\BBCP.
\newblock \BBOQ Comparing space efficiency of propositional knowledge
  representation formalisms\BBCQ\
\newblock In {\Bem Proc. of the $5^{rd}$ International Conference on Knowledge
  Representation and Reasoning (KR'96)}, \BPGS\ 364--373.

\bibitem[\protect\BCAY{Chandra\ \BBA\ Markowsky}{Chandra\ \BBA\
  Markowsky}{1978}]{ChandraMarkowsky78}
Chandra, A.\BBACOMMA\  \BBA\ Markowsky, G. \BBOP1978\BBCP.
\newblock \BBOQ On the number of prime implicants\BBCQ\
\newblock {\Bem Discrete Mathematics}, {\Bem 24}, 7--11.

\bibitem[\protect\BCAY{Darwiche}{Darwiche}{1999}]{darwicheIJCAI99a}
Darwiche, A. \BBOP1999\BBCP.
\newblock \BBOQ Compiling knowledge into decomposable negation normal
  form\BBCQ\
\newblock In {\Bem Proceedings of International Joint Conference on Artificial
  Intelligence (IJCAI'99)}, \BPGS\ 284--289. Morgan Kaufmann, California.

\bibitem[\protect\BCAY{Darwiche}{Darwiche}{2001a}]{darwicheJACM-DNNF}
Darwiche, A. \BBOP2001a\BBCP.
\newblock \BBOQ Decomposable negation normal form\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 48\/}(4), 608--647.

\bibitem[\protect\BCAY{Darwiche}{Darwiche}{2001b}]{darwicheJANCL}
Darwiche, A. \BBOP2001b\BBCP.
\newblock \BBOQ On the tractability of counting theory models and its
  application to belief revision and truth maintenance\BBCQ\
\newblock {\Bem Journal of Applied Non-Classical Logics}, {\Bem 11\/}(1-2),
  11--34.

\bibitem[\protect\BCAY{Darwiche\ \BBA\ Huang}{Darwiche\ \BBA\
  Huang}{2002}]{darwicheD123}
Darwiche, A.\BBACOMMA\  \BBA\ Huang, J. \BBOP2002\BBCP.
\newblock \BBOQ Testing equivalence probabilistically\BBCQ\
\newblock \BTR\ D--123, Computer Science Department, UCLA, Los Angeles, Ca
  90095.

\bibitem[\protect\BCAY{de~Kleer}{de~Kleer}{1992}]{deKleer92}
de~Kleer, J. \BBOP1992\BBCP.
\newblock \BBOQ An improved incremental algorithm for generating prime
  implicates\BBCQ\
\newblock In {\Bem Proc. of the $10^{th}$ National Conference on Artificial
  Intelligence (AAAI'92)}, \BPGS\ 780--785, San Jose, California.

\bibitem[\protect\BCAY{Dechter\ \BBA\ Rish}{Dechter\ \BBA\
  Rish}{1994}]{DechterRish94}
Dechter, R.\BBACOMMA\  \BBA\ Rish, I. \BBOP1994\BBCP.
\newblock \BBOQ Directional resolution: the {Davis}-{P}utnam procedure,
  revisited\BBCQ\
\newblock In {\Bem Proceedings of the Fourth International Conference on
  Principles of Knowledge Representation and Reasoning (KR'94)}, \BPGS\ 134--145,
  Bonn.

\bibitem[\protect\BCAY{del Val}{del Val}{1994}]{delvalKR94}
del Val, A. \BBOP1994\BBCP.
\newblock \BBOQ Tractable databases: How to make propositional unit resolution
  complete through compilation\BBCQ\
\newblock In {\Bem Proceedings of the International Conference on Principles of
  Knowledge Representation and Reasoning (KR'94)}, \BPGS\ 551--561. Morgan
  Kaufmann Publishers, Inc., San Mateo, California.

\bibitem[\protect\BCAY{Gergov\ \BBA\ Meinel}{Gergov\ \BBA\
  Meinel}{1994a}]{GergovMeinel94}
Gergov, J.\BBACOMMA\  \BBA\ Meinel, C. \BBOP1994a\BBCP.
\newblock \BBOQ Efficient analysis and manipulation of obdds can be extended to
  fbdds\BBCQ\
\newblock {\Bem IEEE Transactions on Computers}, {\Bem 43\/}(10), 1197--1209.

\bibitem[\protect\BCAY{Gergov\ \BBA\ Meinel}{Gergov\ \BBA\
  Meinel}{1994b}]{GergovMeinel94b}
Gergov, J.\BBACOMMA\  \BBA\ Meinel, C. \BBOP1994b\BBCP.
\newblock \BBOQ On the complexity of analysis and manipulation of {Boolean}
  functions in terms of decision diagrams\BBCQ\
\newblock {\Bem Information Processing Letters}, {\Bem 50}, 317--322.

\bibitem[\protect\BCAY{Gogic, Kautz, Papadimitriou,\ \BBA\ Selman}{Gogic
  et~al.}{1995}]{Gogicetal95}
Gogic, G., Kautz, H., Papadimitriou, C., \BBA\ Selman, B.
\BBOP1995\BBCP.
\newblock \BBOQ The comparative linguistics of knowledge representation\BBCQ\
\newblock In {\Bem Proc. of the $14^{th}$ International Joint Conference on
  Artificial Intelligence (IJCAI'95)}, \BPGS\ 862--869, Montreal.

\bibitem[\protect\BCAY{Herzig\ \BBA\ Rifi}{Herzig\ \BBA\
  Rifi}{1999}]{HerzigRifi99}
Herzig, A.\BBACOMMA\  \BBA\ Rifi, O. \BBOP1999\BBCP.
\newblock \BBOQ Propositional belief base update and minimal change\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 115\/}(1), 107--138.

\bibitem[\protect\BCAY{Karp\ \BBA\ Lipton}{Karp\ \BBA\
  Lipton}{1980}]{KarpLipton80}
Karp, R.\BBACOMMA\  \BBA\ Lipton, R. \BBOP1980\BBCP.
\newblock \BBOQ Some connections between non-uniform and uniform complexity
  classes\BBCQ\
\newblock In {\Bem Proc. of the $12^{th}$ ACM Symposium on Theory of Computing
  (STOC'80)}, \BPGS\ 302--309.

\bibitem[\protect\BCAY{Khardon\ \BBA\ Roth}{Khardon\ \BBA\
  Roth}{1997}]{KhardonRo97l}
Khardon, R.\BBACOMMA\  \BBA\ Roth, D. \BBOP1997\BBCP.
\newblock \BBOQ Learning to reason\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 44\/}(5), 697--725.

\bibitem[\protect\BCAY{Lang, Liberatore,\ \BBA\ Marquis}{Lang
  et~al.}{2000}]{LangLiberatoreMarquis00a}
Lang, J., Liberatore, P., \BBA\ Marquis, P. \BBOP2000\BBCP.
\newblock \BBOQ Propositional independence---{Part I}: formula--variable
  independence and forgetting\BBCQ\
\newblock Submitted.

\bibitem[\protect\BCAY{Madre\ \BBA\ Coudert}{Madre\ \BBA\
  Coudert}{1992}]{MadreCoudert92}
Madre, J.~C.\BBACOMMA\  \BBA\ Coudert, O. \BBOP1992\BBCP.
\newblock \BBOQ A new method to compute prime and essential prime implicants of
  boolean functions\BBCQ\
\newblock In {\Bem Advanced research in VLSI and parallel systems, Proceedings
  of the Brown/MIT conference}, \BPGS\ 113--128.

\bibitem[\protect\BCAY{Marquis}{Marquis}{2000}]{Marquis00}
Marquis, P. \BBOP2000\BBCP.
\newblock {\Bem Consequence finding algorithms}, \lowercase{\BVOL}~5 of {\Bem
  Handbook of Defeasible Reasoning and Uncertainty Management Systems:
  Algorithms for Uncertain and Defeasible Reasoning}.
\newblock Kluwer Academic Publishers.

\bibitem[\protect\BCAY{Marquis}{Marquis}{1995}]{marquis95}
Marquis, P. \BBOP1995\BBCP.
\newblock \BBOQ Knowledge compilation using theory prime implicates\BBCQ\
\newblock In {\Bem Proc. International Joint Conference on Artificial
  Intelligence (IJCAI'95)}, \BPGS\ 837--843. Morgan Kaufmann Publishers, Inc., San
  Mateo, California.

\bibitem[\protect\BCAY{Meinel\ \BBA\ Theobald}{Meinel\ \BBA\
  Theobald}{1998}]{MeinelTheobald98}
Meinel, C.\BBACOMMA\  \BBA\ Theobald, T. \BBOP1998\BBCP.
\newblock {\Bem Algorithms and Data Structures in VLSI Design: {OBDD}
  Foundations and Applications}.
\newblock Springer.

\bibitem[\protect\BCAY{Papadimitriou}{Papadimitriou}{1994}]{Papadimitriou94}
Papadimitriou, C. \BBOP1994\BBCP.
\newblock {\Bem Computational complexity}.
\newblock Addison--Wesley.

\bibitem[\protect\BCAY{Quine}{Quine}{1955}]{Quine55}
Quine, W. \BBOP1955\BBCP.
\newblock \BBOQ A way to simplify truth functions\BBCQ\
\newblock {\Bem American Mathematical Monthly}, {\Bem 52}, 627--631.

\bibitem[\protect\BCAY{Quine}{Quine}{1959}]{Quine59}
Quine, W. \BBOP1959\BBCP.
\newblock \BBOQ On cores and prime implicants of truth functions\BBCQ\
\newblock {\Bem American Mathematical Monthly}, {\Bem 66}, 755--760.

\bibitem[\protect\BCAY{Reiter\ \BBA\ {de Kleer}}{Reiter\ \BBA\ {de
  Kleer}}{1987}]{reiter87}
Reiter, R.\BBACOMMA\  \BBA\ {de Kleer}, J. \BBOP1987\BBCP.
\newblock \BBOQ Foundations of assumption-based truth maintenance systems:
  Preliminary report\BBCQ\
\newblock In {\Bem Proceedings of the Fifth National Conference on Artificial
  Intelligence (AAAI)}, \BPGS\ 183--188.

\bibitem[\protect\BCAY{Roth}{Roth}{1996}]{Roth96}
Roth, D. \BBOP1996\BBCP.
\newblock \BBOQ On the hardness of approximate reasoning\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 82\/}(1-2), 273--302.

\bibitem[\protect\BCAY{Schrag}{Schrag}{1996}]{Schrag96}
Schrag, R. \BBOP1996\BBCP.
\newblock \BBOQ Compilation for critically constrained knowledge bases\BBCQ\
\newblock In {\Bem Proc. of the $13^{th}$ National Conference on Artificial
  Intelligence (AAAI'96)}, \BPGS\ 510--515, Portland, Oregan.

\bibitem[\protect\BCAY{Selman\ \BBA\ Kautz}{Selman\ \BBA\
  Kautz}{1996}]{SelmanKautz96}
Selman, B.\BBACOMMA\  \BBA\ Kautz, H. \BBOP1996\BBCP.
\newblock \BBOQ Knowledge compilation and theory approximation\BBCQ\
\newblock {\Bem Journal of the Association for Computing Machinery}, {\Bem 43},
  193--224.

\bibitem[\protect\BCAY{Simon\ \BBA\ del Val}{Simon\ \BBA\ del
  Val}{2001}]{SimondelVal01}
Simon, L.\BBACOMMA\  \BBA\ del Val, A. \BBOP2001\BBCP.
\newblock \BBOQ Efficient consequence finding\BBCQ\
\newblock In {\Bem Proc. of the $17^{th}$ International Joint Conference on
  Artificial Intelligence (IJCAI'01)}, \BPGS\ 359--365, Seattle (WA).

\bibitem[\protect\BCAY{Wegener}{Wegener}{1987}]{Wegener87}
Wegener, I. \BBOP1987\BBCP.
\newblock {\Bem The complexity of boolean functions}.
\newblock Wiley-Teubner, Stuttgart.

\end{thebibliography}

%\newpage

%\bibliography{c:/adnan/latex/adam,c:/adnan/latex/change,biblio}
%\bibliographystyle{theapa}

\end{document}




\begin{thebibliography}{10}

\bibitem{Blumetal80}
M. Blum, A.~K. Chandra, and M.~N. Wegman.
\newblock Equivalence of free {Boolean} graphs can be decided probabilistically
  in polynomial time.
\newblock {\em Information Processing Letters}, 10(2):80--82, 1980.

\bibitem{Boole54}
G. Boole.
\newblock {\em An investigation of the laws of thought}.
\newblock Walton and Maberley, London, 1854.

\bibitem{Boufkhadetal97}
Y.~Boufkhad, E.~Gr\'egoire, P.~Marquis, B.~Mazure, and
L.~Sa\"{\i}s.
\newblock Tractable cover compilations.
\newblock In {\em Proc. of the $15^{th}$ International Joint Conference on
  Artificial Intelligence (IJCAI'97)}, pages 122--127, 1997.

\bibitem{Bryant86}
R.~E. Bryant.
\newblock Graph-based algorithms for {Boolean} function manipulation.
\newblock {\em IEEE Transactions on Computers}, C-35:677--691, 1986.

\bibitem{Bryant92}
R.~E. Bryant.
\newblock Symbolic {Boolean} manipulation with ordered binary decision
  diagrams.
\newblock {\em ACM Computing Surveys}, 24(3):293--318, 1992.

\bibitem{CadoliDonini97}
M.~Cadoli and F.M. Donini.
\newblock A survey on knowledge compilation.
\newblock {\em AI Communications}, 10:137--150, 1997.
\newblock (printed in 1998).

\bibitem{Cadolietal96b}
M.~Cadoli, F.M. Donini, P.~Liberatore, and M.~Schaerf.
\newblock Comparing space efficiency of propositional knowledge representation
  formalisms.
\newblock In {\em Proc. of the $5^{th}$ International Conference on Knowledge
  Representation and Reasoning (KR'96)}, pages 364--373, 1996.

\bibitem{ChandraMarkowsky78}
A.~K. Chandra and G.~Markowsky.
\newblock On the number of prime implicants.
\newblock {\em Discrete Mathematics}, 24:7--11, 1978.

%4Pierre
\bibitem{Cimattietal97}
A.~Cimmati, E. Giunchiglia, F. Giunchiglia and P. Traverso.
\newblock Planning via model checking: a decision procedure for ${\cal AR}$.
\newblock In {\em Proc. of the $4^{th}$ European  Conference on Planning (ECP'97)},
pages 130--142, 1997.

\bibitem{darwicheIJCAI99a}
A. Darwiche.
\newblock Compiling knowledge into decomposable negation normal form.
\newblock In {\em Proc. of the $16^{th}$ International Joint Conference on Artificial
  Intelligence (IJCAI'99)}, pages 284--289, 1999.

%5Pierre
\bibitem{darwicheJACM-DNNF}
A. Darwiche.
\newblock Decomposable negation normal form.
%\newblock Technical Report D--109, Cognitive Systems Laboratory, Computer
% Science Department, UCLA, Los Angeles, Ca 90095, 1999.
\newblock {\em Journal of ACM} 48(4): 608--647, 2001.

%5Pierre: I guess it has been published. Do you have the full reference?
\bibitem{darwicheJANCL}
A. Darwiche.
\newblock On the tractable counting of theory models and its application to
  belief revision and truth maintenance.
%\newblock Technical Report D-113, Cognitive Systems Laboratory, Computer
%  Science Department, UCLA, Los Angeles, Ca 90095, 2000.
\newblock {\em Journal of Applied Non-Classical Logics} 11(1-2): 11--34, 2001.

\bibitem{DechterRish94}
R.~Dechter and I.~Rish.
\newblock Directional resolution: the {Davis}-{P}utnam procedure, revisited.
\newblock In {\em Proc. of the $4^{th}$ International Conference on Knowledge
  Representation and Reasoning (KR'94)}, pages 134--145, 1994.

%4Pierre
\bibitem{deKleer92}
J.~de Kleer.
\newblock An improved incremental algorithm for generating prime implicates.
\newblock In {\em Proc. of the $10^{th}$ National Conference on
Artificial Intelligence (AAAI'92)}, pages 780--785, 1992.

\bibitem{delvalKR94}
A.~del Val.
\newblock Tractable databases: How to make propositional unit resolution
  complete through compilation.
\newblock In {\em Proc. of the $4^{th}$ International Conference on Knowledge
  Representation and Reasoning (KR'94)}, pages 551--561, 1994.

\bibitem{GergovMeinel94}
J.~Gergov and C.~Meinel.
\newblock Efficient analysis and manipulation of {OBDDs} can be extended to
  {FBDDs}.
\newblock {\em IEEE Transactions on Computers}, 43(10):1197--1209, 1994.

\bibitem{GergovMeinel94b}
J.~Gergov and C.~Meinel.
\newblock On the complexity of analysis and manipulation of {Boolean} functions
in terms of decision diagrams.
\newblock {\em Information Processing Letters}, 50:317-322, 1994.

%\bibitem{FBDDMeinel}
%J.~Gergov and C.~Meinel.
%\newblock Efficient analysis and manipulation of {OBDDs} can be extended to
%  {FBDDs}.
%\newblock {\em IEEE Transactions on Computers}, 43(10):1197--1209, 1994.

%\bibitem{MeinelFBDD92}
%J.~Gergov and Ch. Meinel.
%\newblock Efficient analysis and manipulation of {OBDD}'s can be extended to
%  {FBDD}'s.
%\newblock {\em IEEE Transactions on Computers}, 43(10):1197--1209, 1994.

\bibitem{Gogicetal95}
G.~Gogic, H.~Kautz, Ch. Papadimitriou, and B.~Selman.
\newblock The comparative linguistics of knowledge representation.
\newblock In {\em Proc. of the $14^{th}$ International Joint Conference on
  Artificial Intelligence (IJCAI'95)}, pages 862--869, 1995.

\bibitem{HerzigRifi99}
A.~Herzig and O.~Rifi.
\newblock Propositional belief base update and minimal change.
\newblock {\em Artificial Intelligence}, 115(1):107--138, 1999.

\bibitem{KarpLipton80}
R.M. Karp and R.J. Lipton.
\newblock Some connections between non-uniform and uniform complexity classes.
\newblock In {\em Proc. of the $12^{th}$ ACM Symposium on Theory of Computing
  (STOC'80)}, pages 302--309, 1980.

\bibitem{KhardonRo97l}
R.~Khardon and D.~Roth.
\newblock Learning to reason.
\newblock {\em Journal of ACM}, 44(5):697--725, 1997.

%6Pierre: I rectify the title here.
\bibitem{LangLiberatoreMarquis00a}
J.~Lang, P.~Liberatore, and P.~Marquis.
\newblock Propositional independence - Formula-variable independence
  and forgetting, 2002.
\newblock (submitted).

\bibitem{LinReiter94}
F.~Lin and R.~Reiter.
\newblock Forget it!
\newblock In {\em Proc. of the AAAI Fall Symposium on Relevance}, pages
  154--159, New Orleans, 1994.

%4Pierre
\bibitem{MadreCoudert92}
J.-C.~Madre and O. Coudert.
\newblock A new method to compute prime and essential prime implicants of boolean functions.
\newblock In {\em Advanced research in VLSI and parallel systems, Proc. of the 1992
Brown/MIT conference}, pages 113--128, 1992.

\bibitem{Marquis00}
P.~Marquis.
\newblock {\em Consequence finding algorithms}, volume 5, "Algorithms for
  Uncertain and Defeasible Reasoning" of {\em Handbook of Defeasible Reasoning
  and Uncertainty Management Systems}.
\newblock Kluwer Academic Publishers, pages 41-145, 2000.
%\newblock (to appear).

\bibitem{marquis95}
P. Marquis.
\newblock Knowledge compilation using theory prime implicates.
\newblock In {\em Proc. of the $14^{th}$ International Joint Conference on
  Artificial Intelligence (IJCAI'95)}, pages 837--843, 1995.

%4Pierre
\bibitem{MeinelTheobald98}
Ch.~Meinel and Th. Theobald.
\newblock Algorithms and Data Structures in VLSI Design:
OBDD - Foundations and Applications.
\newblock Springer-Verlag, 1998.

\bibitem{Papadimitriou94}
Ch. Papadimitriou.
\newblock {\em Computational complexity}.
\newblock Addison--Wesley, 1994.

\bibitem{Quine55}
W.V.O. Quine.
\newblock A way to simplify truth functions.
\newblock {\em American Mathematical Monthly}, 52:627-631, 1955.

\bibitem{Quine59}
W.V.O. Quine.
\newblock On cores and prime implicants of truth functions.
\newblock {\em American Mathematical Monthly}, 66:755-760, 1959.

\bibitem{reiter87}
R. Reiter and J. {de Kleer}.
\newblock Foundations of assumption-based truth maintenance systems:
  Preliminary report.
\newblock In {\em Proc. of the $6^{th}$ National Conference on Artificial
  Intelligence (AAAI'87)}, pages 183--188, 1987.

\bibitem{Roth96}
D.~Roth.
\newblock On the hardness of approximate reasoning.
\newblock {\em Artificial Intelligence}, 82(1-2):273--302, 1996.

\bibitem{Schrag96}
R.~Schrag.
\newblock Compilation for critically constrained knowledge bases.
\newblock In {\em Proc. of the $13^{th}$ National Conference on Artificial
  Intelligence (AAAI'96)}, pages 510--515, 1996.

\bibitem{SelmanKautz96}
B.~Selman and H.A. Kautz.
\newblock Knowledge compilation and theory approximation.
\newblock {\em Journal of ACM}, 43:193--224, 1996.

%\bibitem{selmanACM}
%B. Selman and H. Kautz.
%\newblock Knowledge compilation and theory approximation.
%\newblock {\em Journal of ACM}, 43(2):193--224, 1996.

%4Pierre
\bibitem{SimondelVal01}
L.~Simon and A. del Val.
\newblock Efficient consequence finding.
\newblock In {\em Proc. of the $17^{th}$ International Joint Conference on Artificial
  Intelligence (IJCAI'01)}, pages 359--365, 2001.

\bibitem{Wegener87}
I.~Wegener.
\newblock {\em The complexity of {Boolean} functions}.
\newblock Wiley-Teubner, Stuttgart, 1987.

\end{thebibliography}
