Hélène Fargier
email: fargier@irit.fr

Pierre Marquis
email: marquis@cril.univ-artois.fr

Disjunctive closures for knowledge compilation ✩

Keywords:

 can be viewed as a multi-criteria evaluation of a number of target classes of representations for propositional KC. Using this map, the choice of a class for a given application can be made, considering both the space efficiency of it (i.e., its ability to represent information using little space), and its time efficiency, i.e., the queries and transformations which can be achieved in polynomial time, among those of interest for the application under consideration. When no class of propositional representations offers all the transformations one would expect, some of them can be left implicit. This is the key idea underlying the concept of closure introduced here: instead of performing computationally expensive transformations, one just remembers that they have to be done. In this paper, we investigate the disjunctive closure principles, i.e., disjunction, existential quantification, and their combinations. We provide several characterization results concerning the corresponding closures. We also extend the KC map with new propositional languages obtained as disjunctive closures of several incomplete propositional languages, including the well-known KROM (the CNF formulae containing only binary clauses), HORN (the CNF formulae containing only Horn clauses), and AFF (the affine language, which is the set of conjunctions of XOR-clauses). Each introduced language is evaluated along the lines of the KC map.

Introduction

Knowledge compilation (KC) consists of a family of approaches which aim at improving the efficiency of some computational tasks -typically, saving on-line computation time -via pre-processing. The pre-processing step consists in turning some pieces of available information into a compiled form, during an off-line compilation phase.

KC gathers a number of research lines focusing on different problems, [START_REF] Cadoli | A survey on knowledge compilation[END_REF][START_REF] Boufkhad | Tractable cover compilations[END_REF][START_REF] Selman | Knowledge compilation and theory approximation[END_REF][START_REF] Schrag | Compilation for critically constrained knowledge bases[END_REF][START_REF] Marquis | Knowledge compilation using theory prime implicates[END_REF][START_REF] Del Val | Tractable databases: how to make propositional unit resolution complete through compilation[END_REF][START_REF] Dechter | Directional resolution: the Davis-Putnam procedure, revisited[END_REF][START_REF] Darwiche | Decomposable negation normal form[END_REF], ranging from theoretical ones, where the key question is the compilability issue, i.e., determining whether pre-processing can lower the computational complexity of some tasks, to more practical ones, especially the design of compilation algorithms for some specific tasks like clausal entailment. An important research line [START_REF] Gogic | The comparative linguistics of knowledge representation[END_REF][START_REF] Darwiche | A knowledge compilation map[END_REF] is concerned with the issue of choosing a target class of representations for KC. In [START_REF] Darwiche | A knowledge compilation map[END_REF], the authors argue that the choice of a target class for a compilation purpose must be based both on its time efficiency, defined as the set of queries and transformations which can be achieved in polynomial time when the pieces of data to be exploited are represented in the class, as well as the space efficiency of the class, i.e., its ability to represent data using little space. Thus, the KC map [START_REF] Darwiche | A knowledge compilation map[END_REF] is an evaluation of a dozen of significant propositional classes L, also called propositional fragments, w.r.t. several dimensions: the space efficiency (aka succinctness) of the fragment and its time efficiency (aka tractability), i.e., the class of queries and transformations it supports (or not) in polynomial time, often under standard assumptions from complexity theory. The KC map is intended to serve as a guide for selecting the "right" target class given the requirements imposed by the application under consideration.

The KC map reported in [START_REF] Darwiche | A knowledge compilation map[END_REF] has already been extended to other propositional classes, queries and transformations in a number of subsequent papers, including [START_REF] Wachter | Propositional DAGs: a new graph-based language for representing Boolean functions[END_REF][START_REF] Fargier | On the use of partially ordered decision graphs in knowledge compilation and quantified Boolean formulae[END_REF][START_REF] Subbarayan | Knowledge compilation properties of tree-of-BDDs[END_REF][START_REF] Mateescu | AND/OR multi-valued decision diagrams (AOMDDs) for graphical models[END_REF][START_REF] Pipatsrisawat | New compilation languages based on structured decomposability[END_REF][START_REF] Fargier | Extending the knowledge compilation map: Krom, Horn, affine and beyond[END_REF][START_REF] Fargier | Extending the knowledge compilation map: closure principles[END_REF][START_REF] Fargier | Knowledge compilation properties of trees-of-BDDs, revisited[END_REF][START_REF] Pipatsrisawat | A lower bound on the size of decomposable negation normal form[END_REF][START_REF] Darwiche | SDD: a new canonical representation of propositional knowledge bases[END_REF][START_REF] Marquis | Existential closures for knowledge compilation[END_REF][START_REF] Bordeaux | Knowledge compilation with empowerment[END_REF]. In all those papers, queries and transformations are also viewed as properties of classes of propositional representations L. One says that L offers or satisfies a given query or a transformation when there exists a polynomial-time algorithm to achieve it, provided that the input representations are from L. When such an algorithm does not exist for sure or unless P = NP, one says that L does not offer the query or the transformation.

When no class of propositional representations offers all the transformations one would expect, an approach consists in leaving some of them implicit. This is the key idea underlying closure principles as introduced in this paper: instead of performing some computationally expensive transformations on representations, one just remembers in the representations that the transformations have to be done. This leads to extend the previous classes to new ones, which are at least as succinct, and for which implicit transformations are for free. Another nice effect of some implicit transformations on incomplete propositional languages is to recover completeness, i.e., the ability to represent any Boolean function.

In this paper, we investigate the disjunctive closure principles, i.e., disjunction [∨], existential quantification [∃], and their combinations. The disjunction principle [∨] when applied to a class L of representations leads to a class L[∨], the disjunction closure of L, which qualifies disjunctions of representations from L, while the existential quantification principle [∃] applied to a class L leads to a class L[∃], the existential closure of L, which qualifies existentially quantified representations from L. L[∨, ∃], the full disjunctive closure of L, is obtained by applying both disjunctive closure principles to L. We provide a number of characterization results concerning the corresponding closures. Especially, we show that applying at most once each disjunctive closure principle on L is enough, in the sense that applying one of them twice or more leads to classes polynomially equivalent to L. We also identify the queries and transformations which are preserved by applying disjunctive closure principles.

In addition, we extend the KC map with new classes of propositional representations obtained as disjunctive closures of several incomplete propositional languages, namely the well-known Krom CNF fragment KROM (also known as the bijunctive fragment) [START_REF] Krom | The decision problem for formulas in prenex conjunctive normal form with binary disjunctions[END_REF] the Horn CNF fragment HORN [START_REF] Horn | On sentences which are true of direct unions of algebras[END_REF], and the affine fragment AFF (also known as the biconditional fragment) [START_REF] Schaefer | The complexity of satisfiability problems[END_REF], as well as K/H (Krom or Horn CNF formulae) and renH, the language of renamable Horn CNF formulae [START_REF] Lewis | Renaming a set of clauses as a Horn set[END_REF]. Each of these languages is a well-known polynomial class for the satisfiability problem sat (i.e., it offers CO), but none of them is fully expressive w.r.t. propositional logic (there exist propositional formulae which cannot be represented in any of them), which drastically restricts their attractiveness for the KC purpose. Importantly, switching from any of those languages to its disjunction closure or to its full disjunctive closure leads to recover a fully expressive propositional language. This is crucial for many applications. The rest of the paper is organized as follows. In Section 2, some formal preliminaries about graph-based, quantified, propositional representations are provided. In Section 3, we make precise the queries and transformations of interest, and extend the notions of expressiveness, succinctness and polynomial translations to any subsets of the class of graph-based, quantified, propositional representations. In Section 4, the concepts of disjunctive closures of a class of propositional representations are defined and we derive a number of characterization results about them. In Section 5, the disjunctive closures of KROM, HORN, K/H, renH, and AFF are considered and we analyze them along the lines of the KC map. Finally, Section 6 concludes the paper by discussing the results, pointing out the disjunctive closures which appear as the best target classes for the KC purpose; it also gives some perspectives for further research.

Quantified propositional representations

Syntax

In this paper, we consider subsets of the class C -QDAG of quantified propositional representations over a countably infinite set PS of propositional variables, given a finite set C of propositional connectives. Each connective c ∈ C is supposed to have a fixed, finite arity. Leaf nodes of such DAGs are labeled by literals, where a literal (over V ⊆ PS) is an element x ∈ V (a positive literal) or a negated one ¬x (a negative literal), or a Boolean constant (⊤ and ⊥). L V is the set of all literals over V . Literal l is the complementary literal of literal l, so that ⊤ = ⊥, ⊥ = ⊤, x = ¬x and ¬x = x. For a literal l different from a Boolean constant, var(l) denotes the corresponding variable: for x ∈ PS, we have var(x) = x and var(¬x) = x.

Formally, C -QDAG is given by: Definition 1 (C -QDAG). C -QDAG is the set of all finite, single-rooted DAGs (also referred to as "representations") α where:

• each leaf node of α is labeled by a literal l over PS, • each internal node of α is labeled by a connective c ∈ C and has as many children as required by c (it is then called a c-node), or is labeled by a quantification ∃x or ∀x (where x ∈ PS) and has a single child.1 The size |α| of a C -QDAG representation α is the number of nodes plus the number of arcs in the DAG. Var(α) denotes the set of free variables of α, i.e., those variables x for which there exists a leaf node N x of α labelled by a literal l such that var(l) = x and there is a path from the root of α to N x such that no node from it is labelled by ∃x or ∀x. Clearly enough, determining whether a given x ∈ PS belongs to Var(α) can be done in time polynomial in the size of α 2 ; similarly, computing Var(α) can also be achieved in time polynomial in the size of α.

Fig. 1 presents a C -QDAG representation α with C = {∧, ∨, ¬, ⊕}. Its set of free variables is Var(α) = {q, r}.

As Fig. 1 exemplifies it, a C -QDAG mainly corresponds to a Quantified Boolean Circuit [START_REF] Kleine-Büning | Transformations into normal forms for quantified circuits[END_REF]. Abusing words, such DAGbased representations are also referred to as "formulae" in the KC literature, and classes of such representations are called "languages". In the following, we will only use the term "formula" for designating a tree-shaped representation of a Boolean function, and the term "language" for sets of formulae. Fig. 2 gives a C -QDAG formula with C = {∧, ∨, ¬, ⊕}.

Many classes of propositional representations considered so far as target classes for KC are subsets of C -QDAG with C = {∧, ∨, ¬, ⊕}, and typically subsets of C -DAG, the subset of C -QDAG with C = {∧, ∨, ¬, ⊕} where no node labeled by a quantification is allowed. Especially, the propositional DAGs considered in [14] are C -DAG representations with C = {∧, ∨, ¬}, and the classes considered in [START_REF] Darwiche | A knowledge compilation map[END_REF] are subsets of DAG-NNF (the non-quantified DAGs with C = {∧, ∨}). Clearly enough, for each non-quantified representation α from C -DAG, Var(α) coincides with the set of variables occurring in α.

In Fig. 1, the DAG rooted at the ∧ node is a C -DAG representation with C = {∧, ∨, ¬} and the DAG rooted at the ∨ node is a DAG-NNF representation. DNNF is the subset of DAG-NNF consisting of DAGs where each ∧-node ∧(α 1 , . . . , α k ) is decomposable, which means that ∀i, j ∈ {1, . . . , k}, if i = j then Var(α i ) ∩ Var(α j ) = ∅. d-DNNF is the subset of DNNF where every ∨-node ∨(α 1 , . . . , α k ) is deterministic, which means that ∀i, j ∈ {1, . . . , k}, if i = j then α i ∧ α j is inconsistent. BDD is the subset of C -DAG with C = {ite} which consists of DAGs α such that every leaf node is labelled by a Boolean constant, ⊤ or ⊥. ite is a ternary connective ("ite" stands for "if ... then ... else ..."). Usually, instead of labeling a decision node N = x, N + , N -of a BDD formula by the name of the connective used (i.e., "ite") and considering three children for it 2 The algorithm consists in labeling each node N of α by a set of variables V N ; the nodes are considered in inverse topological ordering, V N = var (l) when N is a leaf node labeled by l, V N = V M \ {x} when N is an internal node labeled by ∃x or ∀x and M is the child of N, V N = M i child of V N V M i when N is an internal node labeled by a connective c ∈ C ; Var(α) is equal to V Nα where N α is the root of α.

(one for x, one for N + and one for N -), N is labelled by x and has only two children (one for N + and one for N -). Given a total, strict ordering < over PS, the class OBDD < is the subset of BDD which consists of DAGs α such that every path from the root of α to a leaf node is compatible with <.

As usual, a clause (resp. a term) is a finite disjunction (resp. conjunction) of literals. CLAUSE is the subset of DAG-NNF consisting of all clauses, and TERM is the subset of DAG-NNF consisting of all terms. NNF is the subset of DAG-NNF consisting of formulae (i.e., tree-shaped representations). CNF is the subset of NNF consisting of all conjunctions of clauses, while DNF is the subset of NNF consisting of all disjunctions of terms. PI is the subset of CNF consisting of prime implicates formulae (also known as Blake formulae); a PI formula is a CNF formula, the conjunction of all clauses from the set PI(α) for some C -QDAG representation α; PI(α) contains the prime implicates of α, i.e., the logically strongest clauses which are implied by α (one representative per equivalence class is considered, only). An essential prime implicate of α is a prime implicate δ of α such that if the clause equivalent to δ is removed from PI(α), the conjunction of the clauses from the resulting set is no longer equivalent to α. For instance, if α = (p ⇒ q) ∧ (q ⇒ r) ∧ (p ⇒ (r ∨ s)), then PI(α) = {¬p ∨ q, ¬q ∨ r, ¬p ∨ r}. ¬p ∨ q and ¬q ∨ r are essential prime implicates of α, while ¬p ∨ r is not. An important point is that any CNF formula equivalent to a propositional representation α contains (up to logical equivalence) every essential prime implicate of α.

For space reasons, we do not provide hereafter the definitions of the propositional classes of representations DNNF T and IP (see [START_REF] Darwiche | A knowledge compilation map[END_REF][START_REF] Pipatsrisawat | New compilation languages based on structured decomposability[END_REF] for formal definitions).

Semantics

Let us recall that an interpretation (or world) over V ⊆ PS is a mapping ω from V to BOOL = {0, 1}. Interpretations are sometimes viewed as subsets of PS, consisting of all the variables that are set to 1 by the interpretations. When a total, strict ordering < over PS is considered, the restriction of an interpretation ω over a finite subset {x 1 , . . . , x n } of PS can also be represented as a bit vector; for instance, the restriction of ω over {a, b, c} such that ω(a) = 1, ω(b) = 0, and ω(c) = 0 can be represented as 100 when a, b, c are such that a < b < c. For any x ∈ V , ω -x is the interpretation over V which coincides with ω on every variable of V , except on x; formally, ω -x (y) = ω(y

) if y = x, = 1 -ω(x) if y = x.
We are now ready to define the semantics of C -QDAG representations in an interpretation ω over PS:

Definition 2 (Semantics of C -QDAG representations).
The semantics of a C -QDAG representation α in an interpretation ω over PS is the truth value ❏α❑(ω) from BOOL defined inductively as follows:

• If α = ⊤, then ❏α❑(ω) = 1. • If α = ⊥, then ❏α❑(ω) = 0.
• If α is a positive literal x, then ❏α❑(ω) = ω(x).

• If α is a negative literal ¬x, then ❏α❑(ω) = 1 -ω(x).

• If α = c(β 1 , . . . , β n ), where c ∈ C has arity n, then ❏α❑(ω) = ❏c❑(❏β 1 ❑(ω), . . . , ❏β n ❑(ω)), where ❏c❑ is the Boolean function from BOOL n to BOOL, which is the semantics of c.

• If α = ∃x.β, then ❏α❑(ω) = 1 iff ❏β❑(ω) = 1 or ❏β❑(ω -x ) = 1. • If α = ∀x.β, then ❏α❑(ω) = 1 iff ❏β❑(ω) = 1 and ❏β❑(ω -x ) = 1. An interpretation ω over PS is said to be a model of α ∈ C -QDAG, noted ω | α, if and only if ❏α❑(ω) = 1. If α has a model, then it is consistent; if every interpretation over PS is a model of α, then α is valid. If every model of α is a model of β ∈ C -QDAG, then β is a logical consequence of α, noted α | β. Mod(α)
denotes the set of models of α over Var(α). Furthermore, when both α | β and β | α hold, α and β are logically equivalent, noted α ≡ β.

For instance, with C = {∧, ∨, ¬, ⊕}, the C -QDAG representation given in Fig. 1 is equivalent to the C -QDAG formula given in Fig. 2.

By structural induction one can easily show that the semantics of any C -QDAG representation α depends only on its free variables, in the sense that, for any interpretation ω ′ over PS which coincides with a given interpretation ω on all the free variables of α, ω is a model of α if and only if ω ′ is a model of α. Accordingly, the semantics of a C -QDAG representation α in an interpretation ω over PS is fully determined by α and the restriction of ω over Var(α).

Clearly enough, renaming at the same time a quantified occurrence of a variable x in a quantification ∃x or ∀x occurring in a C -QDAG formula α, and every occurrence of x in α which depends on the quantification leads to a C -QDAG formula equivalent to α. Furthermore, such a renaming process can be achieved in time linear in the size of α.

However, things are much more tricky when general C -QDAG representations (not reduced to formulae) are considered. Consider for instance the quantification ∃q occurring in the C -QDAG representation α reported at Fig. 1, where C = {∧, ∨, ¬, ⊕}. The occurrence of variable q in the leaf of α labelled with literal q depends on this quantification. Replacing q by the fresh variable s in ∃q and at this occurrence would not lead to a representation equivalent to α since s would be a free variable of the resulting representation. Indeed, there exist four paths from the root of α to that leaf, and three of them do not contain any quantified occurrence of q. This is salient on the C -QDAG formula equivalent to α reported at Fig. 2, and obtained by "unfolding" α. Thus, when some variable occurrence can be both free and bound, renaming quantified variables while preserving equivalence can be a computationally demanding task (the unfolding process may easily lead to an exponential blow-up of the input representation). Actually, when C ⊇ {∧, ∨}, the possibility of having some variable occurrences both free and bound (or to depend on different existential quantifications) in C -QDAG representations not containing universal quantifications is enough to simulate universal quantifications in them (see [START_REF] Kleine-Büning | Transformations into normal forms for quantified circuits[END_REF]). As a consequence, the corresponding class of DAGs is strictly more succinct than the corresponding language of formulae. On the other hand, some problems are computationally easier when formulae (and not DAGs) are considered; for instance, when universal quantifications are disabled, the model checking problem for C -QDAG formulae with C ⊇ {∧, ∨} is "only" NP-complete, while it is PSPACE-complete when the full class of C -QDAG representations without universal quantifications is considered.

Conventionally, the representation α N rooted at a decision node N = x, N + , N -over x ∈ PS in the standard repre- sentation of an ordered binary decision diagram (i.e., an OBDD < representation) is such that α

N ≡ ite(x, α N + , α N -) ≡ (x ∧ α N + ) ∨ (¬x ∧ α N -). α N + (resp. α N -)
, the representation associated with node N + (resp. N -), is the conditioning of α by x (resp. ¬x), i.e., the representation obtained by replacing every occurrence of x in α N by ⊤ (resp. ⊥).

Finally, we consider the following notations. If α ∈ C -QDAG and X = {x 1 , . (these notations are well-founded since whatever the chosen ordering on X , the resulting representations are logically equivalent).

KROM, HORN, AFF, K/H, and renH

In the following, we will focus on several well-known propositional languages, namely the Krom CNF language KROM (also known as the bijunctive fragment) [START_REF] Krom | The decision problem for formulas in prenex conjunctive normal form with binary disjunctions[END_REF], the Horn CNF language HORN [START_REF] Horn | On sentences which are true of direct unions of algebras[END_REF], and the affine language AFF (also known as the biconditional fragment) [START_REF] Schaefer | The complexity of satisfiability problems[END_REF], as well as K/H (Krom or Horn CNF formulae) and renH, the language of renamable Horn CNF formulae [START_REF] Lewis | Renaming a set of clauses as a Horn set[END_REF].

The languages KROM, HORN, AFF, K/H, and renH are formally defined as follows:

Definition 3 (KROM, HORN, AFF, K/H, and renH).

• The language KROM is the subset of all CNF formulae in which each clause is binary, i.e., it contains at most two literals.

• The language HORN is the subset of all CNF formulae in which each clause is Horn, i.e., it contains at most one positive literal.

• The language K/H is the union of KROM and HORN.

• The language renH is the subset of all CNF formulae α for which there exists a subset V of Var(α) (called a Horn renaming for α) such that the formula noted V (α) obtained by substituting in α every literal l of L V by its complementary literal l is a HORN formula. • The language AFF is the subset of C -DAG with C = {∧, ¬, ⊕}, consisting of conjunctions of XOR-clauses where a XORclause is a finite XOR-disjunction of literals (the XOR connective is denoted by ⊕).

Here are some examples of formulae from KROM, HORN, renH, and AFF:

• (x ∨ y) ∧ (¬y ∨ z) is a KROM formula. • (¬x ∨ ¬y ∨ z) ∧ (¬y ∨ z) is a HORN formula. • (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ z) is a renH formula. V = {x, z} is a Horn renaming for it. • (x ⊕ ¬y ⊕ ⊤) ∧ (¬x ⊕ y ⊕ z) is an AFF formula.
Clearly enough, determining whether a given C -QDAG representation α (for any fixed C ) is a KROM (resp. HORN, K/H, AFF) formula can be easily achieved in time polynomial in the size of α. Note also that there exists linear time algorithms for recognizing renH formulae (see e.g. [START_REF] Hébrard | A linear algorithm for renaming a set of clauses as a Horn set[END_REF][START_REF] Del Val | On 2-sat and renamable Horn[END_REF]); furthermore, such recognition algorithms typically give a Horn renaming when it exists. KROM, HORN, AFF, K/H, and renH are known as polynomial classes for the sat problem (i.e., the restriction of sat to any of them is in polynomial time -stated otherwise, each of them satisfies CO). However, none of them is fully expressive w.r.t. propositional logic (there exist propositional formulae, like (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z), which cannot be represented in any of them); this severely restricts their attractiveness for the KC purpose.

Interestingly, KROM, HORN, and AFF have semantical characterizations in terms of closures of sets of models:

• A set S of interpretations over a finite V ⊆ PS is the set of models of a HORN formula α such that Var(α) = V if and only if it is closed for the bitwise AND connective [START_REF] Mckinsey | The decision problem for some classes of sentences without quantifiers[END_REF][START_REF] Dechter | Structure identification in relational data[END_REF], i.e., ∀ω 1 , ω 2 ∈ S, the interpretation and(ω 1 , ω 2 ) over V belongs to S. Here and(ω 1 , ω 2 ) is defined by ∀x ∈ V , and(ω

1 , ω 2 )(x) = 1 if ω 1 (x) = ω 2 (x) = 1.
• A set S of interpretations over a finite V ⊆ PS is the set of models of an AFF formula α such that Var(α) = V if and only if S is closed for the ternary ⊕ connective [START_REF] Post | The two-valued iterative systems of mathematical logic[END_REF][START_REF] Schaefer | The complexity of satisfiability problems[END_REF], i.e., ∀ω 1 , ω 2 , ω 3 ∈ S, the interpretation ⊕(ω 1 , ω 2 , ω 3 ) over V belongs to S. Here ⊕(ω

1 , ω 2 , ω 3 ) is defined by ∀x ∈ V , ⊕(ω 1 , ω 2 , ω 3 )(x) = ω 1 (x) ⊕ ω 2 (x) ⊕ ω 3 (x).
These characterization results can be exploited to show that some propositional formulae cannot be expressed as KROM (resp. HORN, AFF) formulae.

Queries, transformations, expressiveness and succinctness

Let us now briefly recall the sets of queries and transformations used for comparing propositional languages in [START_REF] Darwiche | A knowledge compilation map[END_REF], as well as the notions of expressiveness and succinctness; their importance is discussed in depth in [START_REF] Darwiche | A knowledge compilation map[END_REF], so we refrain from recalling it here.

Queries

The basic queries considered in [1] and subsequent papers concern DAG-NNF representations; they include tests for consistency (CO), validity (VA), clausal entailment (CE), implicants (IM), equivalence (EQ), sentential entailment (SE), counting (CT) and enumerating theory models (ME). We extend them to C -QDAG representations and add to them MC, the model checking query, which is trivially offered by unquantified representations, but not by quantified representations in the general case. Definition 4 (Queries). Let L denote any subset of C -QDAG.

• L satisfies CO, the consistency query (resp. VA, the validity query) if there exists a polynomial-time algorithm that maps every representation α from L to 1 if α is consistent (resp. valid), and to 0 otherwise. • L satisfies CE, the clausal entailment query, if there exists a polynomial-time algorithm that maps every pair α, δ , where α is a representation from L and δ is a clause, to 1 if α | δ holds, and to 0 otherwise.

• L satisfies EQ, the equivalence query (resp. SE, the sentential entailment query) if there exists a polynomial-time algorithm that maps every pair α, β of representations from L to 1 if α ≡ β (resp. α | β) holds, and to 0 otherwise. • L satisfies IM, the implicant query, if there exists a polynomial-time algorithm that maps every pair α, γ , where α is a representation from L and γ is a term, to 1 if γ | α holds, and to 0 otherwise. • L satisfies CT, the model counting query, if there exists a polynomial-time algorithm that maps every representation α from L to a nonnegative integer that represents the number of models of α over Var(α) (in binary notation).

• L satisfies ME, the model enumeration query, if there exists a polynomial p(., ). and an algorithm that outputs all models of an arbitrary representation α from L in time p(n, m), where n is the size of α and m is the number of its models over Var(α).

• L satisfies MC, the model checking query, if there exists a polynomial-time algorithm that maps every pair α, ω , where α is a representation from L and ω is an interpretation over Var(α), to 1 if I is a model of α, and to 0 otherwise.

Transformations

The basic transformations considered in [START_REF] Darwiche | A knowledge compilation map[END_REF] are conditioning (CD), (possibly bounded) closures under the connectives3 ∧, ∨, and ¬ (∧C, ∧BC, ∨C, ∨BC, ¬C) and (possibly bounded) forgetting which can be viewed as a closure operation under existential quantification (FO, SFO). Forgetting is an important transformation as it allows us to focus/project a representation on a set of variables, which proves helpful in many applications, including model-based diagnosis [START_REF] Darwiche | Model-based diagnosis using structured system descriptions[END_REF], reasoning about actions [START_REF] Herzig | Updates, actions, and planning[END_REF], and reasoning under inconsistency [START_REF] Lang | Resolving inconsistencies by variable forgetting[END_REF][START_REF] Lang | Reasoning under inconsistency: a forgetting-based approach[END_REF]. All those transformations concern DAG-NNF representations.

We extend them to C -QDAG representations and enrich the list with two additional transformations, which are dual to (FO, SFO), namely "ensuring" (EN) and the bounded restriction of it (SEN). Ensuring amounts to eliminating universal quantifications and allows us to project a representation on a set of variables in a robust way, i.e., independently of the values of the removed variables. This transformation is central in decision making under uncertainty and non-deterministic planning, see e.g. [START_REF] Fargier | Propositional logic and one-stage decision making[END_REF].

Definition 5 (Transformations). Let L denote any subset of C -QDAG.

• L satisfies CD, the conditioning transformation, if there exists a polynomial-time algorithm that maps every pair α, γ , where α is a representation from L and γ is a consistent term, to a representation from L that is logically equivalent to ∃Var(γ ).(α ∧ γ ). • L satisfies FO, the forgetting transformation, if there exists a polynomial-time algorithm that maps every pair α, X , where α is a representation from L and X is a set of variables from PS, to a representation from L equivalent to ∃X.α.

If the property holds for each singleton X, we say that L satisfies SFO (singleton forgetting).

• L satisfies EN, the ensuring transformation, if there exists a polynomial-time algorithm that maps every pair α, X , where α is a representation from L and X is a set of variables from PS, to a representation from L equivalent to ∀X.α.

If the property holds for each singleton X, we say that L satisfies SEN (singleton ensuring). • L satisfies ∧C, the closure under conjunction transformation (resp. ∨C, the closure under disjunction transformation) if there exists a polynomial-time algorithm that maps every finite set of representations α 1 , . . . , α n from L to a represen- tation of L that is equivalent to α 1 ∧ . . . ∧ α n (resp. α 1 ∨ . . . ∨ α n ).

• L satisfies ∧BC, the bounded closure under conjunction transformation (resp. ∨BC, the bounded closure under disjunction transformation), if there exists a polynomial-time algorithm that maps every pair of representations α and β from L to a representation of L that is equivalent to α ∧ β (resp. α ∨ β).

• L satisfies ¬C, the closure under negation transformation, if there exists a polynomial-time algorithm that maps every representation α from L to a representation of L which is equivalent to ¬α.

When α is a C -DAG representation (i.e., a non-quantified representation), the conditioning of α by γ can be defined in an equivalent, yet simpler way, as the representation α |γ obtained by replacing in α every occurrence of variable x by ⊤ (resp. ⊥) when x (resp. ¬x) is a literal of γ . Such a characterization cannot be extended to C -QDAG representations in the general case. Especially, considering only those variables x occurring free in α as candidates for the replacement is not enough. Indeed, since DAG-based representations are considered, it can be the case that in α one can find a leaf node N labeled by x such that one path from the root of α to this leaf node does not contain any node labeled by a quantification on x, while other paths from the root to N contain such quantifications (see [START_REF] Kleine-Büning | Transformations into normal forms for quantified circuits[END_REF]).

Expressiveness, succinctness, and polynomial translations

We consider three notions of translations on classes of propositional representations (here, subsets of C -QDAG), starting from the less demanding one, namely expressiveness: Definition 6 (Expressiveness). Let L 1 and L 2 be two subsets of C -QDAG. L 1 is at least as expressive as L 2 , denoted L 1 ≤ e L 2 , if for every representation α ∈ L 2 , there exists an equivalent representation β ∈ L 1 .

A first refinement of such a notion of translatability consists in considering only polynomial-space translations, i.e., the size of the translated representation must remain polynomial in the size of the input representation: Definition 7 (Succinctness). Let L 1 and L 2 be two subsets of C -QDAG. L 1 is at least as succinct as L 2 , denoted L 1 ≤ s L 2 , if there exists a polynomial p such that for every representation α ∈ L 2 , there exists an equivalent representation β ∈ L 1 where |β| ≤ p(|α|).

Finally, we consider still more demanding translations, namely polynomial-time translations: Definition 8 (Polynomial translation). Let L 1 and L 2 be two subsets of C -QDAG. L 2 is said to be polynomially translatable into L 1 , noted L 1 ≤ p L 2 , if there exists a (deterministic) polynomial-time algorithm f such that for every α ∈ L 2 , we have f (α) ∈ L 1 and f (α) ≡ α. We also say that α is polynomially translatable into f (α).

Clearly enough, ≤ e , ≤ s , and ≤ p are pre-orders (i.e., reflexive and transitive relations) over the subsets of C -QDAG. Furthermore, we have the inclusions:

≤ p ⊂ ≤ s ⊂ ≤ e
For each relation ≤ * among ≤ e , ≤ s , and ≤ p , the relation ∼ * denotes the symmetric part of ≤ * , defined by L 1 ∼ * L 2 if L 1 ≤ * L 2 and L 2 ≤ * L 1 . By construction, each ∼ * is an equivalence relation (i.e., a reflexive, symmetric and transitive relation). On the other hand,the relation < * denotes the asymmetric part of ≤ * , defined by L 1 < * L 2 if L 1 ≤ * L 2 and L 2 * L 1 . By construction, each < * is a strict order (i.e., an irreflexive and transitive relation).

In the following, L 1 * s L 2 means that L 1 s L 2 unless the polynomial hierarchy PH collapses (which is considered very unlikely in complexity theory).

When L 1 ≤ e L 2 holds, every representation from L 2 can be translated into an equivalent representation from L 1 . The minimal elements w.r.t. ≤ e (i.e., the most expressive elements) of the set of all subsets of C -QDAG when C is any functionally complete set of connectives (especially, as soon as C contains ∨ and ∧ since leaf nodes of C -QDAG representations are labeled by literals) are called complete propositional classes: they can provide a representation (up to logical equivalence) of any Boolean function.

When L 1 ∼ e L 2 (resp. L 1 ∼ s L 2 , L 1 ∼ p L 2 ), L 1 and L 2 are said to be equally expressive (resp. equally succinct, polynomially equivalent).

Whenever L 1 is polynomially translatable into L 2 , every query which can be answered in polynomial time in L 2 can also be answered in polynomial time in L 1 ; and conversely, every query which cannot be answered in polynomial time in L 1 unless P = NP cannot be answered in polynomial time in L 2 , unless P = NP. Furthermore, polynomially equivalent classes are equally efficient in the sense that they possess the same set of tractable queries and transformations.

On closures of propositional representations

Intuitively, a closure principle applied to a class L of propositional representations defines a new class, called a closure of L, through the (implicit) application of "operators" (i.e., connectives from C or quantifications) to the representations from L. Formally: Definition 9 (Closure). Let L ⊆ C -QDAG and △ ⊆ C ∪ {∀, ∃}. The closure L[△] of L by △ is the subset of C -QDAG inductively defined as follows 4 :

1. if α ∈ L, then α ∈ L[△],
2. if c ∈ △ is an n-ary connective and α 1 , . . . , α n are elements of L[△] such that ∀i, j ∈ {1, . . . , n}, if i = j then α i and α j do not share any common (nonempty) subgraphs, then c(α 1 , . . . , α n

) ∈ L[△], 3. if c ∈ △ is a quantifier, x ∈ PS, and α ∈ L[△], then cx.α ∈ L[△].
Each element of L[△] can be viewed as a "tree" which "internal nodes" are labeled by connectives from C or quantifications and its "leaf nodes" correspond to "independent" representations from L. Accordingly, the representations α i considered in item 2. of Definition 9 do not share any common subgraphs.

Clearly, if there exists a polynomial-time algorithm for determining whether a given representation α ∈ C -QDAG belongs or not to L, then there also exists a polynomial-time algorithm for determining whether a given representation α ∈ C -QDAG belongs or not to the closure L[△] of L by △.

We have derived the following (easy) proposition, which rules the inclusions between closures depending on the way their sets of connectives are related by set inclusion: Proposition 1. For every subset L, L ′ of C -QDAG and every subset △ 1 , △ 2 of C ∪ {∃, ∀}, we have:

0. L ⊆ L[△ 1 ], and if L ⊆ L ′ , then L[△ 1 ] ⊆ L ′ [△ 1 ]. 1. (L[△ 1 ])[△ 2 ] ⊆ L[△ 1 ∪ △ 2 ]. 2. (L[△ 1 ])[△ 1 ] = L[△ 1 ]. 3. If △ 1 ⊆ △ 2 then L[△ 1 ] ⊆ L[△ 2 ]. 4. If △ 1 ⊆ △ 2 then (L[△ 1 ])[△ 2 ] = L[△ 2 ] and (L[△ 2 ])[△ 1 ] = L[△ 2 ].
Some additional properties stating how some closures of a class L can be composed, can be derived when bound variables can be "freely" renamed in the L representations. The property of stability by uniform renaming, given at Definition 10, characterizes the subsets of C -QDAG for which, intuitively, the choice of variable names in the L representations does not really matter: Definition 10 (Stability by uniform renaming). Let L be any subset of C -QDAG. L is stable by uniform renaming if for every α ∈ L, for every non-empty subset V of variables occurring in α, there exist arbitrarily many distinct bijections r i (i ∈ N) from V to subsets V i of fresh variables from PS (i.e., for each i, j ∈ N with i = j, we have

V i ∩ V j = V i ∩ V = ∅) such
that the representation r i (α) obtained by replacing in α (in a uniform way) every occurrence of x ∈ V (either quantified or non-quantified) by r i (x) belongs to L as well. This condition is not very demanding: all the "standard" classes of propositional representations (quantified or not) are stable by uniform renaming (when based on a countably infinite set PS as this is the case here). Special attention must nevertheless be paid to the OBDD < language, and more generally to every class based on an ordered set of propositional variables. For the OBDD < case where < is a strict and complete ordering over PS we may assume the ordered set (PS, <) to be of order type η (η is the order type of the set of rational numbers equipped with its usual ordering [START_REF] Cantor | Beiträge zur Begründung der Transfiniten Mengenlehre[END_REF]). This restriction is harmless since the set of variables occurring in any OBDD < representation is finite. In a nutshell, whatever the way the variables occurring in a given OBDD < representation α are ordered w.r.t. <, one must be able to "insert" in this ordering arbitrarily many fresh variables between two variables of α while preserving the way other variables are ordered. Order type η clearly allows it (between two distinct rational numbers one can find countably many rationals). To make things clearer, let us give a counter-example: let PS = {x i | i ∈ N} ordered in such a way that for every i ∈ N, x i < x i+1 . Consider an OBDD < representation of x 0 ∨ x 1 as given in Fig. 3. < is not of type η. Take V = {x 0 }: x 0 cannot be renamed into a different variable from PS without questioning the ordering requirement over OBDD < , which shows that OBDD < is not stable by uniform renaming in this case.

Straightforwardly, the closure by any set of connectives/quantifiers of any class of propositional representations, which is stable by uniform renaming, also is stable by uniform renaming.

We are now ready to present more specific results. The following polynomial (dual) equivalences, showing that existential quantifications (resp. universal quantifications) when viewed as "operators" "distribute" over disjunctions (resp. conjunctions), are well-known:

∃x.(α 1 ∨ . . . ∨ α n ) ≡ (∃x.α 1 ) ∨ . . . ∨ (∃x.α n ), ∀x.(α 1 ∧ . . . ∧ α n ) ≡ (∀x.α 1 ) ∧ . . . ∧ (∀x.α n ).
It can then be shown that: Proposition 2. Let L be any subset of C -QDAG s.t. L is stable by uniform renaming. We have: Proposition 1 and Proposition 2 show together that when △ = {∨, ∃} (resp. {∧, ∀}) closing L[△] by subsets of △ in an iterative fashion does not lead to a "new" class, i.e., a class which is not polynomially equivalent to L. Especially, we have

• (L[∃])[∨] ∼ p (L[∨])[∃] ∼ p L[∨, ∃]. • (L[∀])[∧] ∼ p (L[∧])[∀] ∼ p L[∧, ∀].
L[∨, ∃] [∃] ∼ p L[∨, ∃] [∨] ∼ p L[∨, ∃].
This shows, so to say, that the "sequential" closure of a propositional class, stable by uniform renaming, by a set of operators among {∨, ∃} (resp. among {∧, ∀}) is polynomially equivalent to its "parallel" closure. No similar result can be systematically guaranteed for arbitrary choices of classes and operators. For instance, if L is the set of literals over PS, then the "sequential"

closure (L[∨])[∧] is the set of all CNF formulae, the "sequential" closure (L[∧])[∨]
is the set of all DNF formulae, and the "parallel" closure L[∨, ∧] is the set of all NNF representations. It is well-known that those three languages are not pairwise polynomially equivalent (indeed, we have CNF s DNF, DNF s CNF, NNF < s CNF, and NNF < s DNF, see e.g. [START_REF] Hastad | Almost optimal lower bounds for small depth circuits[END_REF]). Similarly,

if L = CLAUSE, then (L[∧])[∃] and L[∧, ∃] are polynomially equivalent to CNF[∃], but (L[∃])[∧] is polynomially equivalent to CNF, which is not polynomially equivalent to CNF[∃]. Indeed, whatever C , C -DAG is polynomially translatable into CNF[∃]
using Tseitin's extension principle [START_REF] Tseitin | On the complexity of derivation in propositional calculus[END_REF], while CNF is not at least as succinct as C -DAG as soon as C ⊇ {∧, ∨, ¬} (indeed, CNF is not at least as succinct as the subset DNF of NNF, which is itself a subset of C -DAG in this case).

We have derived the following proposition, which relates the queries and the transformations offered by L, with the queries and transformations offered by its disjunctive closures L[∨] (the disjunction closure of L), L[∃] (the existential closure of L), and L[∨, ∃] (the full disjunctive closure of L). • If L satisfies FO (resp. SFO), then L[∨] satisfies FO (resp. SFO).

• If L satisfies ∧C (resp. ∧BC, ∨C, ∨BC), then L[∃] satisfies ∧C (resp. ∧BC, ∨C, ∨BC).

Note that applying disjunctive closures do not preserve other queries or transformations in the general case. Thus:

• If L satisfies VA (resp. IM, CT, EQ, and SE), then it can be the case that L[∨] does not satisfy it. For instance, TERM satisfies each of VA, IM, CT, EQ, and SE, but TERM[∨] = DNF does not satisfy any of them unless P = NP [START_REF] Darwiche | A knowledge compilation map[END_REF]. • If L satisfies VA (resp. IM, CT, EQ, and SE), then it can be the case that L[∃] does not satisfy it. Thus, L = CNF satisfies VA and IM but CNF[∃] does not satisfy any of them unless P = NP; indeed, DNF (which does not offer any of them) is polynomially translatable into CNF[∃] using Tseitin's transformation [START_REF] Tseitin | On the complexity of derivation in propositional calculus[END_REF]. Similarly, L = HORN satisfies both EQ and SE, but HORN[∃] does not offer any of them (see Proposition 5). Finally, the subset L = d-DNF of DNF consisting of deterministic DNF formulae (i.e., the DNF formulae α = n i=1 γ i such that for each i, j ∈ 1, . . . , n, if i = j, then the terms γ i and γ j are such that

γ i ∧ γ j is inconsistent) satisfies CT, but d-DNF[∃] does not. Indeed, DNF is polynomially translatable into d-DNF[∃]: with each DNF formula α = n i=1 γ i we can associate in polynomial time the equivalent d-DNF[∃] formula ∃{y 1 , . . . , y n }. n i=1 (y i ∧ i-1 j=1 ¬y j ∧ γ i ),
where {y 1 , . . . , y n } is a set of fresh variables (disjoint from Var(α)).

• If L satisfies ∧C, then it can be the case that L[∨] does not satisfy it. Thus, L = TERM satisfies ∧C, but TERM[∨] = DNF does not, unless P = NP [START_REF] Darwiche | A knowledge compilation map[END_REF]. • If L satisfies ¬C, then it can be the case that none of L[∨] and L[∃] satisfies it. Thus, L = OBDD < satisfies ¬C, but none of OBDD < [∨] and OBDD < [∃] satisfies ¬C unless P = NP. As to OBDD < [∨], this comes from the fact that TERM ≥ p OBDD < , which implies that DNF ≥ p OBDD < [∨]. Since every CNF formula α is polynomially translatable into the negation of a DNF formula β, if OBDD < [∨] would satisfy ¬C, then the consistency of α could be tested in polynomial time by computing first an OBDD < [∨] representation equivalent to β, then "negating" it to reach an OBDD < [∨]

representation equivalent to α. Indeed, since OBDD < satisfies CO, OBDD < [∨] also satisfies CO (see Proposition 3). As to OBDD < [∃], we can make a rather similar proof given that OBDD < [∃] also satisfies CO (see again Proposition 3). To get the proof, it is enough to show that OBDD < [∨] ≥ p OBDD < [∃]: let α = n i=1 α i be an OBDD < [∨] representation; let y 1 , . . . , y n be variables from PS \ Var(α) such that each y i (i ∈ 1, . . . , n) precedes every variable from Var(α). From α, we can generate in polynomial time the OBDD < representation β = y 1 , α 1 , y 2 , α 2 , . . . , y n , α n , ⊥, . . . .

To conclude the proof it is enough to observe that α is equivalent to the OBDD < [∃] representation ∃{y 1 , . . . , y n }.β.

• If L satisfies EN, then it can be the case that L[∨] does not satisfy it. Thus, L = TERM satisfies EN, but TERM[∨] = DNF does not, unless P = NP, since a DNF formula α is valid iff its universal closure ∀Var(α).α is valid iff ∀Var(α).α is consistent (since ∀Var(α).α has no free variable, it is equivalent to ⊤ or to ⊥, hence it is consistent precisely when it is valid), and DNF satisfies CO.

• If L satisfies EN, then it can be the case that L[∃] does not satisfy it. Thus, L = CNF satisfies EN, but CNF[∃] does not, unless PH collapses. This comes easily from the fact that the validity problem for CNF[∃] formulae of the form ∃X.α is Π p 2 -complete. Indeed, ∃X.α is valid iff the (closed) quantified Boolean formula ∀Var(α) \ X.(∃ X.α) is valid.

On the disjunctive closures of KROM, HORN, AFF, K/H, and renH

Let us now focus on the disjunctive closures of KROM, HORN, AFF, K/H, and renH.

First of all, it is obvious that the four languages KROM, HORN, K/H, and AFF are stable by uniform renaming. This is also the case for renH: if V is a Horn renaming for a renH formula α, and if α ′ X is the CNF formula obtained by substituting in a uniform way in α every occurrence of a variable v from X ⊆ PS by the fresh variable v ′ , then α ′ X also is a renH formula and

V ′ = {v ∈ Var(α ′ ) | v ∈ V \ X} ∪ {v ′ ∈ Var(α ′ ) | v ∈ V ∩ X} is a Horn renaming for it.
Now, thanks to Propositions 1 and 2, it is enough to consider the three disjunctive closures L[∃], L[∨], and L[∨, ∃] with L being any on the five above languages. Clearly enough, the disjunction (resp. existential, full disjunctive) closure of any language among KROM, HORN, K/H, renH, and AFF is also stable by uniform renaming.

Applying the disjunctive closure principles [∨], [∃], and [∨, ∃] to the five languages KROM, HORN, K/H, renH, and AFF leads to consider fifteen additional languages. The following easy result shows that some of the resulting languages do not need to be considered separately, because they are polynomially equivalent.

Proposition 4.

• KROM ∼ p KROM[∃]. • KROM[∨] ∼ p KROM[∨, ∃]. • AFF ∼ p AFF[∃]. • AFF[∨] ∼ p AFF[∨, ∃].
As a direct consequence, we have that KROM and KROM[∃] (resp. AFF and AFF[∃], KROM[∨] and KROM[∨, ∃], AFF[∨] and AFF[∨, ∃]) are both (pairwise) equally succinct and equally expressive.

Accordingly, we focus in the following on the sixteen languages: KROM, HORN, K/H, renH, AFF, HORN

[∃], K/H[∃], renH[∃], KROM[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃], and renH[∨, ∃].
From Proposition 1, we get that:

KROM ⊆ KROM[∨] ⊆ KROM[∨, ∃] HORN ⊆ HORN[∃] ⊆ HORN[∨, ∃] HORN ⊆ HORN[∨] ⊆ HORN[∨, ∃] K/H ⊆ K/H[∃] ⊆ K/H[∨, ∃] K/H ⊆ K/H[∨] ⊆ K/H[∨, ∃] renH ⊆ renH[∃] ⊆ renH[∨, ∃] renH ⊆ renH[∨] ⊆ renH[∨, ∃] AFF ⊆ AFF[∨]
Obviously enough, from the definitions of the languages KROM, HORN, K/H, and renH, we also have the following inclusions:

KROM ⊆ K/H HORN ⊆ K/H HORN ⊆ renH Table 1
KROM, HORN, K/H, AFF, renH, their disjunction, existential and full disjunctive closures and the corresponding polynomial-time queries.

√ means "satisfies" and • means "does not satisfy unless P = NP".

CO VA CE IM EQ SE CT ME MC renH[∨, ∃] √ • √ • • • • √ √ K/H[∨, ∃] √ • √ • • • • √ √ HORN[∨, ∃] √ • √ • • • • √ √ AFF[∨] √ • √ • • • • √ √ renH[∨] √ • √ • • • • √ √ K/H[∨] √ • KROM[∨] ⊆ K/H[∨] HORN[∨] ⊆ K/H[∨] HORN[∨] ⊆ renH[∨] HORN[∃] ⊆ K/H[∃] HORN[∃] ⊆ renH[∃] HORN[∨, ∃] ⊆ K/H[∨, ∃] HORN[∨, ∃] ⊆ renH[∨, ∃]
In addition, since every consistent KROM formula is a renH formula 5 and since KROM satisfies CO, with every K/H formula we can associate in polynomial time an equivalent renH formula, i.e., K/H ≥ p renH. As a consequence, we also get that

K/H[∨] ≥ p renH[∨] K/H[∃] ≥ p renH[∃] K/H[∨, ∃] ≥ p renH[∨, ∃] Finally, since for every subset L of C -QDAG, L ⊆ L[∨] ⊆ L[∨, ∃], ⊆ is included into ≥ p ,
and both ⊆ and ≥ p are transitive relations, a number of additional inclusions/polynomial translatability results can be directly obtained from the results above; they will be exploited in some forthcoming proofs.

Queries and transformations

As to queries, we have obtained the following results:

Proposition 5. The results in Table 1 hold.

As to transformations, we have obtained the following results: Proposition 6. The results in Table 2 hold. √ means "satisfies," • means "does not satisfy," while • means "does not satisfy unless P = NP." ! means that the transformation is not always feasible within the language.

CD FO SFO EN SEN ∧C ∧BC ∨C ∨BC ¬C renH[∨, ∃] √ √ √ • • • • √ √ • K/H[∨, ∃] √ √ √ • √ • •

Expressiveness

It is well-known that none of the languages KROM, HORN, K/H, renH, or AFF is complete for propositional logic. For instance, there is no formula from any of these languages which is equivalent to the CNF formula (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z). This is problematic for many applications; indeed, what can be done when the available information cannot be represented in the targeted language? Approximating it is not always an option, especially because the best approximation of the available information can be rough and the missing pieces of information in the approximation can be crucial ones for reasoning and/or decision making. In the following, we are going to prove that while considering the existential closure of any of those languages does not increase its expressiveness, switching to its disjunction closure (or to its full disjunctive closure) is enough to recover a complete propositional language, thus escaping from the above mentioned expressiveness problem.

Let us start with the existential closures of KROM, HORN, K/H, renH, and AFF. First, since KROM (resp. AFF) is polynomially equivalent to KROM[∃] (resp. AFF[∃]), it turns out that those languages are (pairwise) equally expressive: KROM[∃] ∼ e KROM, and AFF[∃] ∼ e AFF. Similarly, we have derived the following expressiveness results, showing that the existential closure of any language L among HORN, K/H, and renH is not more expressive than L itself.

Proposition 7.

• HORN

[∃] ∼ e HORN. • K/H[∃] ∼ e K/H. • renH[∃] ∼ e renH.
Now, from the definitions of KROM, HORN, K/H, renH, the fact that K/H ≥ p renH, and the fact that x ∨ y is a KROM formula, which is not equivalent to a HORN one, ¬x ∨ ¬y ∨ ¬z is a HORN formula which is not equivalent to a KROM one, x ∨ y ∨ z is a renH formula which is not equivalent to a K/H one, we easily get that: KROM e HORN and HORN e KROM renH < e K/H < e HORN K/H < e KROM In addition, AFF and any of KROM, HORN, K/H, renH are incomparable w.r.t. ≤ e . Indeed, there is no renH formula equivalent to the AFF formula x ⊕ y ⊕ z. This comes from the fact that every CNF formula equivalent to x ⊕ y ⊕ z must contain the four clauses x ∨ y ∨ z, ¬x ∨ ¬y ∨ z, x ∨ ¬y ∨ ¬z, ¬x ∨ y ∨ ¬z since those clauses are essential prime implicates of x ⊕ y ⊕ z, plus the fact that by construction, every CNF formula containing the clauses x ∨ y ∨ z, ¬x ∨ ¬y ∨ z, x ∨ ¬y ∨ ¬z, ¬x ∨ y ∨ ¬z is not renamable Horn (renaming at least two variables in the first clause to make it a Horn clause also changes one of the remaining three clauses into a non-Horn one). Conversely, there is no AFF formula equivalent to ¬x ∨ ¬y, which is both in KROM and in HORN. This is a direct consequence of the semantical characterization result concerning AFF recalled in Section 2.3: with x < y, ω 1 = 00, ω 2 = 01, and ω 3 = 10 are models of ¬x ∨ ¬y, but ⊕(ω 1 , ω 2 , ω 3 ) = 11 is not a model of ¬x ∨ ¬y. Fig. 5. The expressiveness picture for disjunctive closures. An arrow from L 1 to L 2 means that L 1 is strictly more expressive than L 2 , so that a lack of arrow means that the expressiveness of L 1 and the expressiveness of L 2 are incomparable. Fig. 6. The succinctness picture for incomplete languages. An arrow from L 1 to L 2 means that L 1 is strictly more succinct than L 2 , i.e., L 1 < s L 2 . The arrow is thick in the specific case when the fact that L 2 s L 1 comes from the fact that L 2 e L 1 . A lack of arrow means that the succinctness of L 1 and the succinctness of L 2 are incomparable.

Let us finally switch to the disjunction closures and the full disjunctive closures of KROM, HORN, K/H, renH, or AFF; interestingly, the eight languages defined as such are equally, and fully, expressive:

Proposition 8. KROM[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃] are complete propositional languages.
Fig. 5 depicts the expressiveness relationships identified in the above propositions.

Succinctness

As to incomplete languages, since KROM (resp. AFF) is polynomially equivalent to KROM[∃] (resp. AFF[∃]), those languages are (pairwise) equally succinct: KROM[∃] ∼ s KROM, and AFF[∃] ∼ s AFF. More interestingly, we have obtained the following succinctness results, showing that the existential closure of any language L among HORN, K/H, and renH is strictly more succinct than L itself. Proposition 9.

• HORN[∃] < s HORN.

• K/H[∃] < s K/H. • renH[∃] < s renH. • renH and K/H[∃] are incomparable w.r.t. ≤ s . • K/H and HORN[∃] are incomparable w.r.t. ≤ s .
Fig. 6 summarizes the succinctness relationships among incomplete languages identified in Proposition 9. We observe that it does not coincide with the corresponding expressiveness picture, restricted to incomplete languages (see Fig. 5).

Table 3

The relative succinctness of the full disjunctive closures of KROM, HORN, AFF, K/H, and renH.

AFF[∨] renH[∨, ∃] K/H[∨, ∃] HORN[∨, ∃] KROM[∨] AFF[∨] ∼ s s s s s renH[∨, ∃] s ∼ s ≤ s ≤ s ≤ s K/H[∨, ∃] s s ∼ s ≤ s ≤ s HORN[∨, ∃] s s s ∼ s s KROM[∨] s s s s ∼ s
As to complete languages, our succinctness results mainly focus on the five languages KROM

[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃], AFF[∨],
the full disjunctive closures of the incomplete languages KROM, HORN, K/H, renH, AFF considered at start. 6There are several reasons for this focus: • HORN

• KROM[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃],
[∨, ∃] < s HORN[∨]. • K/H[∨, ∃] < s K/H[∨]. • renH[∨, ∃] < s renH[∨].
Thus, the full disjunctive closures of the incomplete languages KROM, HORN, K/H, renH, AFF are either equally succinct as the corresponding disjunction closures (this is the case for the closures of KROM and of AFF), or strictly more succinct than them (for the three remaining languages).

Let us now provide the remaining succinctness results we got. We split our results into two propositions (and two tables). In the first table, we compare KROM

[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃], AFF[∨] w.r.t. spatial efficiency ≤ s .
Proposition 11. The results in Table 3 hold.

As a direct consequence of Proposition 11, we have that

renH[∨, ∃] < s K/H[∨, ∃] < s HORN[∨, ∃] K/H[∨, ∃] < s KROM[∨, ∃]
One can observe that the resulting succinctness picture is similar to the expressiveness picture for the corresponding incomplete fragments AFF, renH, K/H, HORN, KROM. The succinctness picture for complete classes. An arrow from L 1 to L 2 means that L 1 is strictly more succinct than L 2 , so that a lack of arrow means that the succinctness of L 1 and the succinctness of L 2 are incomparable for sure (or, under the assumption that the polynomial hierarchy does not collapse when d-DNNF is concerned). For a clarity sake, there are two exceptions to this notation, which also concern d-DNNF: it is unknown whether d-DNNF ≤ s PI, and whether d-DNNF ≤ s IP [1].

Discussion

Let us now compare in more details the five languages KROM, HORN, K/H, renH, and AFF, with their closures and with other classes of propositional representations considered so far for knowledge compilation.

We start with the existential closures. Since applying the existential closure principle to any of KROM, HORN, K/H, renH, and AFF does not change its expressiveness, the existential closures of KROM, HORN, K/H, renH, and AFF are incomplete languages as well. KROM[∃] (resp. AFF[∃]) is polynomially equivalent to KROM (resp. AFF) since KROM and AFF satisfy FO. As a consequence, KROM[∃] and AFF[∃] satisfy the same queries and transformations as their underlying language, and KROM[∃] and AFF[∃] are equally succinct as KROM and AFF, respectively. For the remaining existential closures (namely,

HORN[∃], K/H[∃], renH[∃]
), all the transformations already offered by HORN, K/H, renH, are preserved and FO is obtained "for free". However, some queries offered by HORN, K/H, and renH (EQ, SE) are not preserved. This seems to be the price to be paid for the gain in succinctness the existential closures offer. Indeed, we have HORN[∃] < s HORN, K/H[∃] < s K/H, and renH[∃] < s renH. Thus, for applications where their expressiveness proves enough and EQ and SE are not expected but FO is, renH[∃] (resp. HORN[∃]) appears as a better choice than renH (resp. HORN) as a target language for KC.

Unlike existential closures, the disjunction closures and the full disjunctive closures of KROM, HORN, K/H, renH, and AFF are complete propositional languages, i.e., fully expressive ones. Furthermore, switching from any of KROM, HORN, K/H, renH, or AFF to its disjunction closure or its full disjunctive closure leads to get ∨C (hence ∨BC) "for free" and FO, when it was not already offered. Conversely, some queries and transformations primarily offered are then lost; as to queries, this is the case for VA, IM, EQ, SE for the five languages, plus CT satisfied by AFF but not by any of its disjunction closure or its full disjunctive closure; as to transformations, this is the case for EN and ∧C (and even SEN, which is satisfied by renH but not satisfied by renH[∨] or renH[∨, ∃], unless P = NP). Just like considering the existential closures of HORN, K/H, renH leads to strictly more succinct languages, considering the existential closures of HORN[∨], K/H[∨], renH[∨] leads as well to strictly more succinct languages since HORN

[∨, ∃] < s HORN[∨], K/H[∨, ∃] < s K/H[∨], and renH[∨, ∃] < s renH[∨].
Thus, it turns out that the full disjunctive closures of KROM, HORN, K/H, renH, and AFF are always at least as interesting as the corresponding disjunction closures from a KC perspective: as to KROM and AFF, those closures are polynomially equivalent, hence equally interesting; as to HORN, K/H, renH, both closures satisfy the same queries, while each full disjunctive closure offers FO (not satisfied by the corresponding disjunction closure) and is strictly more succinct than the underlying language.

Comparing now one another the full disjunctive closures of KROM, HORN, K/H, renH, AFF it turns out that none of them is strictly dominated by another one from the KC point of view. All of them are equally expressive, and they satisfy precisely Finally, it is interesting to compare the full disjunctive closures of KROM, HORN, K/H, renH, AFF, with previous complete classes of representations for propositional logic, which have been considered as target classes for KC. One focuses on IP, DNF, PI, OBDD < , DNNF T , and d-DNNF:

• IP satisfies all the queries but CT, and no transformation but CD, EN, SEN and ∧BC. • OBDD < satisfies all the queries and the transformations CD, SFO, SEN, ∧BC, ∨BC, and ¬C. Thus, none of the full disjunctive closures of KROM, HORN, K/H, renH, and AFF is strictly dominated by any of IP, DNF, PI, OBDD < , DNNF T , and d-DNNF, viewing the set of queries, the set of transformations and the succinctness relation as comparison criteria.

Conclusion and perspectives

Conclusion

In the light of the results reported in the previous sections, the following conclusions can be drawn.

Generally speaking, the disjunctive closures of classes L of propositional representations appear as interesting target classes for KC when the application under consideration expects tractability for the queries and transformations CO, CD and their consequences (e.g., CE, ME), as well as FO and/or ∨C (depending on the type of closure which is considered). Especially, as soon as L is stable by uniform renaming, the transformations FO, ∨C are offered "for free" by the full disjunctive closure L[∨, ∃] (even if the underlying class L does not offer any of them), while CO, CD are preserved by the closure. The other queries and transformations considered in the KC map are not guaranteed to be offered or to survive a disjunctive closure operation in the general case.

Considering specific disjunctive closures may allow for preserving additional queries or transformations, and for increasing the expressiveness of the underlying language. Thus, the disjunction closure and the full disjunctive closure of any language L containing TERM are complete propositional languages, even if L is not (KROM, HORN, K/H, renH, and AFF are such languages). Clearly enough, fully expressive propositional languages are highly expected by many applications.

Of course, it cannot be guaranteed in the general case that the size of a compiled form remains "small enough" when a disjunctive closure is targeted. Nevertheless, every disjunctive closure of a class L includes L as a subset, hence applying a disjunctive closure principle to a class L decreases neither the expressiveness nor the succinctness of L. Now, from the application point of view, there are many important problems in AI and in other fields of Computer Science, where one is interested in encoding some pieces of information using representations for which CO, CD, FO and ME are computationally easy.

For instance, in model-based diagnosis, it makes sense to compile the description of the system to be diagnosed (during an off-line phase) in order to be able to generate efficiently consistency-based diagnoses, for a number of observations available on-line only [START_REF] Darwiche | Model-based diagnosis using structured system descriptions[END_REF][START_REF] Huang | On compiling system models for faster and more scalable diagnosis[END_REF][START_REF] Torasso | Model-based diagnosis through OBDD compilation: a complexity analysis[END_REF]. Such diagnoses are the models of the system description, once conditioned by the given observation and then projected onto the variables expressing the components statuses (in the simplest case, faulty or not). Accordingly, if the system description has been compiled first into a representation which satisfies CO, CD, FO and ME, then the diagnoses can be computed in input-output polynomial time. Our results thus show full disjunctive closures of languages L satisfying the stability by uniform renaming condition as valuable target languages for the compilation, as soon as L satisfies CO and CD (which is the case for KROM, HORN, K/H, renH, and AFF).

In product configuration and interactive recommendation, it is also important to offer some response-time guarantees to the front-end user, especially when the interaction is Web-based. In order to achieve this goal, an approach consists in compiling the product catalog into a propositional representation (the models of it representing the feasible products). Among the operations required by the configuration process are propagating the user's choices (the CD transformation), testing whether at least one feasible product is compatible with the user's choices (the CO query), and listing a fixed number of feasible products compatible with the user's choices (see e.g. [START_REF] Astesana | Constraint-based vehicle configuration: a case study[END_REF][START_REF] Felfernig | Developing constraint-based recommenders[END_REF]). Often, the feasible products are described using two types of variables (or "codes" [START_REF] Zengler | Boolean quantifier elimination for automotive configuration -a case study[END_REF]): the customer variables -the variables the user controls -and the manufacturer control variables -which express some information related to the factory or to the distribution of the product, and are not available to the user. Thus, the manufacturer control variables must be forgotten from the representation before listing the solutions. Our results show that those operations can be achieved efficiently when the catalog has been compiled into a full disjunctive closure of a class L of propositional representations, stable by uniform renaming, and satisfying CO and CD.

In particular, the task of enumerating a preset number of solutions is feasible in polynomial time in this case (Algorithm 1 given in Appendix A is a polynomial delay enumeration procedure).

Beyond AI applications, enumerating models once projected on a given set of variables appears as a fundamental issue for a number of problems considered in software engineering and formal methods. Thus, in the setting of automatic case generation based on propositional logic, such models correspond to test cases [START_REF] Khurshid | A case for efficient solution enumeration[END_REF]. The problem all-sat (or "all-solutions" sat) which consists in enumerating the assignments to "important" variables of a propositional representation, which can be extended to models, turns out to be very significant in symbolic model checking [START_REF] Grumberg | Memory efficient all-solutions SAT solver and its application for reachability analysis[END_REF], which explains that dedicated algorithms have been developed for solving it [START_REF] Gebser | Solution enumeration for projected Boolean search problems[END_REF]. Indeed, this problem is considered for predicate abstraction [START_REF] Lahiri | A symbolic approach to predicate abstraction[END_REF], and re-parameterization in symbolic simulation [START_REF] Chauhan | A SAT-based algorithm for reparameterization in symbolic simulation[END_REF]. In reachability analysis, one is interested in computing the set of states reachable from (resp. leading to) a given set of states under a transition relation; this is called the image (resp. pre-image) computation problem. The transition relation T can be modeled as a Boolean function T over X ∪ Y ∪ X ′ , complete terms γ X over X (resp. X ′ ) are used to denote states before (resp. after) a transition and complete terms γ Y over Y represent inputs making precise the transition. By construction, the models of ∃Y .T |γ X (resp. ∃Y .T |γ X ′ ) represent the image of γ X (resp. the pre-image of γ X ′ ) by T . The "important" variables are those of X ′ (resp. X ). Accordingly, many sat solvers have been customized into all-sat solvers precisely for computing images or pre-images (see e.g. [START_REF] Gupta | SAT-based image computation with application in reachability analysis[END_REF][START_REF] Kang | SAT-based unbounded symbolic model checking[END_REF]) from CNF representations of transition relations. In practice, such sat-based approaches to symbolic model checking can prove much more efficient than OBDD < -based approaches on some instances, which coheres with the fact that the succinctness of OBDD < and the succinctness of CNF are incomparable [53]. Interestingly, when T is represented as a full disjunctive closure of a class L of propositional representations, stable by uniform renaming, and satisfying CO and CD, both the computation of ∃Y .T |γ X (resp. ∃Y .T |γ X ′ ) and the enumeration of its models can be achieved in polynomial time (in the size of the input plus the size of the output). Contrastingly, no response-time guarantee can be ensured in the general case for computing a single model when T is represented as a CNF formula.

Thus, for each of the applications above, considering full disjunctive closures for the representation purpose can prove to be a reasonable choice.

Perspectives

This work calls for several perspectives.

One of them concerns the problem of closed-world reasoning. Indeed, the disjunction covers of HORN and renH are known as interesting target languages when propositional formulae are to be interpreted under some form of the closed-world assumption, like the extended closed-world assumption (ECWA) [START_REF] Gelfond | On the relationship between circumscription and negation as failure[END_REF], the extended generalized closed-world assumption (EGCWA) [START_REF] Yahya | Deduction in non-Horn databases[END_REF], the generalized closed-world assumption (GCWA) [START_REF] Minker | On indefinite databases and the closed world assumption[END_REF] or the careful closed-world assumption (CCWA) [START_REF] Gelfond | Negation as failure: careful closure procedure[END_REF]. To be more precise, though inference from a propositional formula interpreted under ECWA, EGCWA, GCWA or CCWA is Π p 2 -hard, its complexity is at most at the first level of the polynomial hierarchy when the formula belongs to HORN[∨] or to renH[∨] [START_REF] Coste-Marquis | Knowledge compilation for closed world reasoning and circumscription[END_REF]. Furthermore, the complexity of inference under EGCWA falls down to P when HORN[∨] formulae are considered, or when GCWA is considered and queries are limited to CNF formulae. Finally, it turns out that the complexity of closed-world reasoning is the same one for HORN[∨] formulae and for DNF formulae, despite the fact that DNF is strictly less succinct than HORN[∨]. It would be interesting to identify the complexity of closed-world reasoning for full disjunctive closures, especially those of HORN and renH.

Another important issue for further research is the design and the evaluation of compilers targeting the disjunctive closures introduced in the paper. Actually, compilers targeting some of those closures considered here do exist. Thus, Boufkhad et al. [START_REF] Boufkhad | Tractable cover compilations[END_REF] present some compilation algorithms targeting KROM[∨], HORN[∨], K/H[∨], and renH[∨], and evaluate them on a number of benchmarks. While the obtained results show the feasibility of computing disjunction closure compilations, we can hardly use them to compare the practical significance of the corresponding closures with OBDD < and DNNF T for which some experimental results are also available. Indeed, the compilation algorithms given in [START_REF] Boufkhad | Tractable cover compilations[END_REF] are based on an old-style DPLL sat solver, and the performances of such solvers are dramatically overtaken by those of modern sat solvers, based on a CDCL architecture.

Interestingly, Nishimura et al. [START_REF] Nishimura | Detecting backdoor sets with respect to Horn and binary clauses[END_REF] have shown that the problem of determining whether a given CNF formula α has a strong KROM-backdoor set (resp. a strong HORN-backdoor set) containing at most k variables is fixed-parameter tractable with parameter k. Similarly, Samer and Szeider [START_REF] Samer | Backdoor trees[END_REF] have shown that the problem of determining whether a given CNF formula α has a KROM-backdoor tree (resp. a HORN-backdoor tree) containing at most k leaves is fixed-parameter tractable with parameter k. The algorithm given in [START_REF] Samer | Backdoor trees[END_REF] can be used to determine "efficiently" (i.e., for sufficiently "small" k) whether a KROM[∨] compilation or a HORN[∨] compilation of "reasonable" size (i.e., linear in k and the size of α) exists. As mentioned in [START_REF] Samer | Backdoor trees[END_REF]: "There is some empirical evidence that real-world instances actually have small backdoor sets". Such instances also have "small" HORN[∨] representations (hence, "small" K/H[∨] and "small" renH[∨] representations). 7 This explains why it makes sense to develop new compilation algorithms targeting disjunction closures.

Incorporating existentially quantified variables in the representations during the compilation phase in order to generate full disjunctive closures also appears as an interesting perspective. Indeed, new variables can be introduced as "names" given to arbitrarily complex subformulae of the input formula (using equivalences); the point is that equivalence w.r.t. the input formula is preserved when such variables are existentially quantified. Taking advantage of it can dramatically reduce the size of the compiled forms (our succinctness results show that exponential gaps in the representation size can be achieved thanks to existential closure); the difficulty is to determine when introducing new variables (this is reminiscent to the general problem of lemmatization in automated reasoning).

Finally, the fact that each of KROM[∨], HORN[∨, ∃], and AFF[∨] satisfies ∧BC paves the way for bottom-up compilation algorithms for those classes. As noted in [START_REF] Pipatsrisawat | New compilation languages based on structured decomposability[END_REF], this is important for applications from formal verification based on unbounded model checking which require bottom-up, incremental compilation of formulae, where pieces of information are compiled independently and then conjoined together. This explains why HORN[∨, ∃], and AFF[∨] which offers CD, FO, ∧BC, and ME appear as valuable candidates for the image/pre-image computation problem considered in reachability analysis, as discussed above. Indeed, OBDD < , which offers CD, FO, ∧BC, and ME as well, has been extensively used for the purpose of symbolic model checking [START_REF] Clarke | Model Checking[END_REF]; furthermore, we have shown that the succinctness of HORN[∨, ∃], and of AFF[∨] are incomparable with the succinctness of OBDD < . Since each of KROM[∨], HORN[∨, ∃], and AFF[∨] satisfies CO and includes CLAUSE, getting ∧BC is optimal in the sense that no class of propositional representations containing CLAUSE can satisfy both ∧C and CO, unless P = NP.

(L[△

1 ])[△ 1 ] = L[△ 1 ]: considering the inclusion reported at item 1. in this proof with △ 2 = △ 1 , we get (L[△ 1 ])[△ 1 ] ⊆ L[△ 1 ]; the converse inclusion L[△ 1 ] ⊆ (L[△ 1 ])[△ 1 ] follows from the inclusion at item 0. in this proof. 3. If △ 1 ⊆ △ 2 then L[△ 1 ] ⊆ L[△ 2 ]: the inclusion at item 0. in this proof shows that L[△ 1 ] ⊆ (L[△ 1 ])[△ 2 ], and item 1. in this proof shows that (L[△ 1 ])[△ 2 ] ⊆ L[△ 1 ∪ △ 2 ]. The fact that L[△ 1 ∪ △ 2 ] is equal to L[△ 2 ] when △ 1 ⊆ △ 2 completes
the proof.

4. Suppose that △ 1 ⊆ △ 2 . Then, from the equality reported at item 2. in this proof, since △ 1 ∪ △ 2 = △ 2 , we have

(L[△ 1 ])[△ 2 ] ⊆ L[△ 2 ] and (L[△ 2 ])[△ 1 ] ⊆ L[△ 2 ]. Conversely, the inclusion at item 0. in this proof shows that L[△ 2 ] ⊆ (L[△ 2 ])[△ 1 ]; finally, L[△ 2 ] ⊆ (L[△ 1 ])[△ 2 ] derives from the fact that L ⊆ L[△ 1 ]
(which is again ensured the inclusion at item 0. in this proof), and the implication reported at item 0. as well. ✷ Proposition 2. Let L be any subset of C -QDAG s.t. L is stable by uniform renaming. We have:

• (L[∃])[∨] ∼ p (L[∨])[∃] ∼ p L[∨, ∃]. • (L[∀])[∧] ∼ p (L[∧])[∀] ∼ p L[∧, ∀].
Proof. We just prove the first point of the proposition; the second one is similar (by duality). The facts that L

[∨, ∃] ≤ p (L[∨])[∃] and L[∨, ∃] ≤ p (L[∃])[∨] come immediately from the inclusions L[∨, ∃] ⊇ (L[∨])[∃] and L[∨, ∃] ⊇ (L[∃])[∨] (see item 1. in Proposition 1). It remains to show that L[∨, ∃] ≥ p (L[∨])[∃] and L[∨, ∃] ≥ p (L[∃])[∨]. • L[∨, ∃] ≥ p (L[∨])[∃].
β ′′ i ∈ L[∨] such that β ′ i ≡ ∃X i .β ′′ i (es- pecially, if β ′ i is an L[∨]
representation, then we take X i = ∅). For i ∈ 1, . . . , n, let X ′ i be a set of variables of PS which is disjoint with the set of variables occurring in α and such that there exists a bijection between X ′ i and X i . One can always find such a bijection since each β i (i ∈ 1, . . . , n) belongs to L[∨, ∃], which is stable by uniform renaming since L is so. Furthermore, since PS is countably infinite, we can always find sets

X ′ i so that for i, j ∈ 1, . . . , n, if i = j then X ′ i ∩ X ′ j = ∅. Now, for i ∈ 1, . . . , n, let β ′′ i [X i ← X ′ i ]
be the representation obtained by replacing in a uniform way in β ′′ i every occurrence of x ∈ X i by the corresponding variable x ′ ∈ X ′ i . Clearly enough, such representations can be computed in polynomial time. Since quantified variables are dummy ones, we have ∃X i .

β ′′ i ≡ ∃X ′ i .β ′′ i [X i ← X ′ i ].
Hence, we have α -If α = ∨(β 1 , . . . , β n ) with β i ∈ L[∨, ∃] (i ∈ 1, . . . , n), then by induction hypothesis, one can compute in polynomial

≡ ∨(β ′ 1 , . . . , β ′ n ) ≡ ∨(∃X 1 .β ′′ 1 , . . . , ∃X n .β ′′ n ) ≡ ∨(∃X ′ 1 .β ′′ 1 [X 1 ← X ′ 1 ], . . . , ∃X ′ n .β ′′ n [X n ← X ′ n ]). Since for each i ∈ 1, . . . , n, we have Var(β ′′ i [X i ← X ′ i ]) ∩ j=1,...,n| j =i X ′ j = ∅, each ∃X ′ i .β ′′ i [X i ← X ′ i ] is equivalent to ∃ n j=1 X ′ j .β ′′ i [X i ← X ′ i ]. Thus we get that α ≡ ∨(∃ n j=1 X ′ j .β ′′ 1 [X 1 ← X ′ 1 ], . . . , ∃ n j=1 X ′ j .β ′′ n [X n ← X ′ n ]) ≡ ∃ n j=1 X ′ j . ∨ (β ′′ 1 [X 1 ← X ′ 1 ], . . . , β ′′ n [X n ← X ′ n ]). Since ∨(β ′′ 1 [X 1 ← X ′ 1 ], . . . , β ′′ n [X n ← X ′ n ]) is an L[∨] representation,
time n representations β ′ i ∈ (L[∃])[∨] (i ∈ 1, . . . , n) such that for each i ∈ 1, . . . , n, β ′ i ≡ β i . Since ∨(β ′ 1 , . . . , β ′ n ) is an (L[∃])[∨] representation equivalent to α, the conclusion follows. -If α = ∃x.β with β ∈ L[∨, ∃],
then by induction hypothesis, one can compute in polynomial time a representation input : an L representation α, and a set γ of literals over Var(α) • If L satisfies FO (resp. SFO), then L[∨] satisfies FO (resp. SFO).

β ′ ∈ (L[∃])[∨] such that β ′ ≡ β. If β ′ is an L[∃] representation, then ∃x.β ′ also is an L[∃] representation; since it is equivalent to α and since (L[∃])[∨] ⊇ L[∃] (see item 0. in
1 if α is consistent then 2 if Var(α) = ∅ then
• If L satisfies ∧C (resp. ∧BC, ∨C, ∨BC), then L[∃] satisfies ∧C (resp. ∧BC, ∨C, ∨BC).

Proof.

• As to CO, since L[∨] ⊆ L[∨, ∃] and L[∃] ⊆ L[∨, ∃], it is enough to show that L[∨, ∃] satisfies CO. Let α be any repre- sentation from L[∨, ∃]; since L[∨, ∃] ∼ p (L[∨])[∃] (cf.
Proposition 2), we can compute in time polynomial in the size of α an equivalent representation β = ∃X. ∨ (β 1 , . . . , β n ) where X is a finite subset of PS and each β i (i ∈ 1, . . . , n) is an L representation. We have that α is consistent iff β is consistent iff ∨(β 1 , . . . , β n ) is consistent iff at least one β i (i ∈ 1, . . . , n) is consistent. Since the latter can be decided in polynomial time, the conclusion follows.

As to CD, let γ be any consistent term. Let α be an L[∨] representation; we have α = ∨(β 1 , . . . , β n ) where each β i (i ∈ 1, . . . , n) is an L representation. Since ∧ distributes over ∨ and existential quantifications "distribute" over ∨ as well, we have ∃Var(γ

).(α ∧ γ ) ≡ ∃Var(γ ).(∨(β 1 , . . . , β n ) ∧ γ ) ≡ ∃Var(γ ). ∨ (β 1 ∧ γ , . . . , β n ∧ γ ) ≡ ∨(∃Var(γ ).(β 1 ∧ γ ), . . . , ∃Var(γ ).(β n ∧ γ )). If L satisfies CD, then each ∃Var(γ ).(β i ∧ γ ) (i ∈ 1, . . . , n) can be associated in polynomial time with an equivalent L representation β ′ i . Hence ∃Var(γ ).(α ∧ γ ) is equivalent to the L[∨] representation ∨(β ′ 1 , . . . , β ′ n )
which can be computed in time polynomial in the size of the input. Now let α be an L[∃] representation; we have α = ∃X.β where X is a finite subset of PS and β is an L representation.

We have ∃Var(γ

).(α ∧ γ ) ≡ ∃Var(γ [X ← X ′ ]).((∃X.β) ∧ γ [X ← X ′ ]) where γ [X ← X ′ ]
is the representation obtained by replacing in γ every variable x ∈ Var(γ ) ∩ X by a fresh variable x ′ , not occurring in . . , β n ) where X is a finite subset of PS and each β i (i ∈ 1, . . . , n) is an L representation. Then it is enough to combine the two previous proofs to get the desired result.

β or γ . Since Var(γ [X ← X ′ ]) ∩ X = ∅, we have that ∃Var(γ [X ← X ′ ]).((∃X.β) ∧γ [X ← X ′ ]) ≡ ∃Var(γ [X ← X ′ ]) ∪ X.(β ∧γ [X ← X ′ ]) ≡ ∃X.(∃Var(γ [X ← X ′ ]).(β ∧ γ [X ← X ′ ])). If L satisfies CD, then ∃Var(γ [X ← X ′ ]).(β ∧ γ [X ← X ′ ]) can
• We generalize some easy lemmata from [START_REF] Darwiche | A knowledge compilation map[END_REF] to the C -QDAG case. As to CE, it is enough to observe that for any C -QDAG representation α and any non-valid clause δ, we have α | δ iff α ∧ ¬δ is inconsistent iff ∃Var(¬δ).(α ∧ ¬δ) is inconsistent.

As to ME, let α be any L representation. Procedure 1 enumerates the models of α over Var(α). It amounts to searching a decision tree T in a depth-first manner. Each branch of T corresponds either to a model of α over Var(α), or to an implicant of ¬α. Each model is represented as a set of literals over Var(α). The procedure is called with γ = ∅. Given a total, strict ordering over the variables of Var(α), the function first(α) at Line 4 returns the first variable of α w.r.t. this ordering.

Procedure 1 first consists in testing whether α is consistent (Line 1). If α is inconsistent, then the procedure stops; otherwise, one checks whether Var(α) is empty or not (Line 2). If this set is empty, then one returns the model of α stored in the accumulator γ (Line 3). In the remaining case, one computes the first variable x of α (Line 5). Afterwards, the procedure enumerates recursively all the models of α |x by adding x to the accumulator γ (Line 6), then all the models of α |¬x by adding ¬x to the accumulator γ (Line 7). In both cases, a variable is removed (since x / ∈ Var(α |x ) ∪

Var(α |¬x )), hence the number of recursive calls for each branch of T cannot exceed the number of variables of α.

Furthermore, since L satisfies CO and CD, the time spent between two successive calls is polynomial in the input size.

Procedure 1 is thus a polynomial delay model enumeration algorithm: a first model of α (when it exists) is generated in time polynomial in the size of the input, and after each model generation, the time needed to generate a further model (or to determine that no more models exist) also is polynomial in the size of the input. As a consequence, it runs in time polynomial in the size of the input plus the size of the output.

• Due to the inclusions L ⊆ L[∨], L ⊆ L[∃] ⊆ L[∨, ∃] (see Proposition 1), it is enough to show that L[∨, ∃] satisfies MC. Let α be any L[∨, ∃] representation. Since L[∨, ∃] ∼ p (L[∨])[∃] (cf.
Proposition 2), we can compute in time polynomial in the size of α an equivalent representation β = ∃X. ∨ (β 1 , . . . , β n ) where X is a finite subset of PS and each β i (i ∈ 1, . . . , n) is an L representation. Furthermore, we have Var(β) = Var(α). Let ω be any interpretation over Var(α) and let γ be the consistent term (unique up to logical equivalence) such that Var(γ ) = Var(α) and ω is a model of γ . We have ω | α iff γ ∧ β is consistent iff γ ∧ ∨(β 1 , . . . , β n ) is consistent iff there exists i ∈ 1, . . . , n such that γ ∧ β i is consistent iff there exists i ∈ 1, . . . , n such that ∃Var(γ ).(β i ∧ γ ) is consistent. Since L satisfies CO and CD, the conclusion follows.

• The fact that L[∨] and L[∨, ∃] satisfy ∨C and L[∃] and L[∨, ∃] satisfy FO is obvious (by construction).

• We prove the FO case (for SFO just take X as a singleton). Let α be a representation from L[∨] and X ⊆ PS. By construction, α = ∨(β 1 , . . . , β n ) where each β i (i ∈ 1, . . . , n) is an L representation. Since existential quantifications "distribute" over ∨, we have ∃X.α ≡ ∨(∃X.β 1 , . . . , ∃X.β n ).

∃X i i .β i [X i ← X i i ]
obtained by renaming in a uni- form way every occurrence of variable x ∈ X i by the fresh variable x i . Whenever β i belongs to L, β i [X i ← X i i ] belongs to L as well (due to the stability condition). From the replacement metatheorem, we get that n

i=1 α i ≡ n i=1 (∃X i .β i ) ≡ n i=1 (∃X i i .β i [X i ← X i i ])
. By construction, we have X i i ∩ X j j = ∅ when i = j. As a consequence, we have

n i=1 (∃X i i .β i [X i ← X i i ]) ≡ ∃ n i=1 X i i .( n i=1 β i [X i ← X i i ]
) Since L satisfies ∧C, we can turn in polynomial time the repre-

sentation n i=1 β i [X i ← X i i ] into an equivalent representation β from L. Since n i=1 α i ≡ ∃ n i=1 X i i .β and n i=1 X i i .
β is an L[∃] representation, the conclusion follows. The proof is similar for the remaining cases (∧BC, ∨C, ∨BC). ✷ Proposition 4.

• KROM ∼ p KROM[∃]. • KROM[∨] ∼ p KROM[∨, ∃]. • AFF ∼ p AFF[∃]. • AFF[∨] ∼ p AFF[∨, ∃].
Proof. These polynomial equivalences come easily from the fact that each of KROM and AFF satisfies FO (cf. Proposition 6), plus the fact that existential quantifications "distribute" over disjunctions. ✷ Proposition 5. The results in Table 1 hold.

CO VA CE IM EQ SE CT ME MC renH[∨, ∃] √ • √ • • • • √ √ K/H[∨, ∃] √ • √ • • • • √ √ HORN[∨, ∃] √ • √ • • • • √ √ AFF[∨] √ • √ • • • • √ √ renH[∨] √ • √ • • • • √ √ K/H[∨] √ • Proof.
CO It is well-known that each of KROM, HORN, renH, AFF satisfies CO (cf. [64-67,25]). Since deciding whether a C -QDAG representation is in KROM (resp. HORN) can be done in polynomial time, we get that K/H satisfies CO. Then point 1. of Proposition 3 allows to conclude that each of the [∨], [∃], and [∨, ∃] closures of those languages satisfies CO as well. VA KROM, HORN, K/H and renH satisfy VA since they are subsets of CNF and CNF satisfies VA. AFF satisfies VA since it satisfies CT (indeed, an AFF formula α is valid if and only if it has 2 n models where n is the cardinality of Var(α)).

As to renH[∃], K/H[∃] and HORN[∃], the results hold since each of these languages satisfies IM. Obviously, every subset L of C -QDAG which satisfies IM satisfies VA as well (indeed, α ∈ L is valid iff it is implied by the term ⊤). Since the proof that each of renH[∃], K/H[∃] and HORN[∃] satisfies IM relies on the fact that HORN[∃] satisfies VA, it just remains to show it. This is easy since a formula α from HORN[∃] is valid if and only if its universal closure is valid. The fact that the validity problem for closed, prenex quantified Boolean formulae with a HORN matrix is in P [68] concludes the proof. formula such that α is a renH formula, and let γ be a term. Let V be any Horn renaming for α. We have γ | ∃X.α iff γ ⇒ (∃X.α) is valid. Now, viewing V as a substitution, one can take advantage of the substitution metatheorem for propositional logic.

Finally, none of KROM[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃],
This theorem (see e.g., [START_REF] Kleene | Mathematical Logic[END_REF]) states that for any propositional formula Σ and any substitution σ (a mapping which replaces each variable by a formula), if Σ is valid, then σ (Σ) is valid. With Σ = γ ⇒ (∃X.α) and σ = V , we get that if γ ⇒ (∃X.α) is valid, then V (γ ⇒ (∃X.α)) is valid. Since for every formula β, V (V (β)) ≡ β, we also get that if

V (γ ⇒ (∃X.α)) is valid, then γ ⇒ (∃X.α) is valid. Altogether, we get that γ ⇒ (∃X.α) is valid iff V (γ ⇒ (∃X.α)) is valid. Now, V (γ ⇒ (∃X.α)) is valid iff V (γ ) ⇒ V (∃X.α) is valid iff V (γ ) | V (∃X.α).
Let ω be any interpretation over Var(α) ∪ X . Since for every variable x, V (x) is equal to x or is equal to ¬x, V (ω) can be viewed as well as an interpretation over Var(α) ∪ X . We have ω | V (∃X.α) iff V (ω) | ∃X.α (using the substitution theorem and the fact that for every formula β, V (V (β)) ≡ β) iff there exists an interpretation ω ′ over Var(α) ∪ X such that ω ′ | α and ∀y ∈ (Var(α) ∪ X) \ X , V (ω)(y) = ω ′ (y) (by definition of ∃X.α) iff there exists an interpretation V (ω ′ ) over Var(α) ∪ X such that V (ω ′ ) | V (α) and ∀y ∈ (Var(α) ∪ X) \ X , V (V (ω))(y) = V (ω ′ )(y). Since V (V (ω)) = ω, this is equivalent to state that ω is a model of ∃X.V (α). As a consequence, we have V (∃X.α) ≡ ∃X.V (α).

Accordingly, γ is an implicant of the renH[∃] formula ∃X.α iff the term V (γ ) is an implicant of the HORN[∃] formula ∃X.V (α). As explained above (see the VA point in the proof), the fact that HORN[∃] satisfies CD and VA shows that it satisfies IM as well. Given that a Horn renaming V for α can be computed in polynomial time given α, and that V (γ ) (resp. V (α)) can be computed in polynomial time from γ (resp. α) once V has been computed, the fact that HORN[∃]

satisfies IM shows that renH[∃] satisfies IM as well.

Finally, none of KROM ] satisfies IM unless P = NP, since none of them satisfies VA unless P = NP. SE Determining whether a KROM (resp. HORN, K/H, renH) formula β is a logical consequence of a KROM (resp. HORN, K/H, renH) formula α amounts to determining whether every clause of β is a logical consequence of α. The fact that each of KROM, HORN, K/H and renH satisfy CE completes the proof for those four languages. As to AFF, determining whether an AFF formula β is a logical consequence of an AFF formula α amounts to determining whether every XOR-clause of β is a logical consequence of α. Now, a XOR-clause l 1 ⊕ . . . ⊕ l n is a logical consequence of an AFF formula α if and only if the AFF formula α ∧ (l 1 ⊕ . . . ⊕ l n ⊕ ⊤) is inconsistent. The fact that AFF satisfies CO concludes the proof for

[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃

AFF.

As to renH[∃], K/H[∃] and HORN[∃], it is enough to prove the result for HORN[∃] since this language is included in the two remaining ones. Let α be a CNF formula over n variables x 1 , . . . , x n . Let α ′ be the HORN formula obtained by replacing every positive literal x i in α by the negative literal ¬x ′ i (where each x ′ i is a fresh variable), conjoined with n

additional clauses ¬x i ∨ ¬x ′ i (i ∈ 1, . . . , n). Let β ′ be the KROM formula n i=1 (x i ∨ x ′ i ). By construction, α is inconsistent iff α ′ ∧ β ′ is inconsistent iff α ′ | ¬β ′ . ¬β ′ is equivalent to n i=1 (¬x i ∧ ¬x ′ i ), which in turn is equivalent to the formula γ ′ = ∃{y 1 , . . . , y n }((¬y 1 ∨ . . . ∨ ¬y n ) ∧ n i=1 ((y i ∨ ¬x i ) ∧ (y i ∨ ¬x ′ i ))) (
where each y i is a fresh variable). The fact that α ′ and γ ′ are HORN[∃] formulae which can be computed in time polynomial in the size of α shows the coNP-hardness of the sentential entailment problem for HORN[∃] formulae and concludes the proof. ] satisfies SE unless P = NP since none of them satisfies VA unless P = NP; the fact that ⊤ is a formula from each of these languages and that α ∈ C -QDAG is valid iff ⊤ | α concludes the proof.

Finally, none of KROM[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃
EQ Each of KROM, HORN, K/H, renH, and AFF satisfies EQ since it satisfies SE.

As to renH[∃], K/H[∃] and HORN[∃]: for every formulae α ′ and γ ′ from C -QDAG we have that α ′ | γ ′ iff α ′ ∧ γ ′ ≡ α ′ . Consider now the formulae α ′ and γ ′ used for proving that none of renH[∃], K/H[∃] and HORN[∃] satisfies SE unless P = NP (see the item SE in this proof). Since none of the y i variables occurs in α ′ , the formula α ′ ∧ γ ′ can be turned in linear time into the equivalent formula ∃{y 1 , . . . , ] satisfies EQ unless P = NP since none of them satisfies VA unless P = NP; the fact that ⊤ is a formula from each of these languages and that α ∈ C -QDAG is valid iff ⊤ ≡ α concludes the proof.

y n }.(α ′ ∧ ((¬y 1 ∨ . . . ∨ ¬y n ) ∧ n i=1 ((y i ∨ ¬x i ) ∧ (y i ∨ ¬x ′ i )))), which is a HORN[∃] formula. This concludes the proof. Finally, none of KROM[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃
CT The result for AFF is proven in [69]. The results for all the remaining languages come from the fact that the language of negative Krom formulae (i.e., the set of all conjunctions of negative, binary clauses) is included into each language among KROM, HORN, K/H, renH, KROM

[∨], HORN[∨], K/H[∨], renH[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃]; further- more, DNF is included in AFF[∨]
since each term is an AFF formula. The fact that none of the language of negative Krom formulae and DNF satisfies CT [START_REF] Roth | On the hardness of approximate reasoning[END_REF] concludes the proof. MC The results come directly from the third item of Proposition 3, given that each of KROM, HORN, K/H, renH, and AFF satisfies both CO and CD. ✷ Proposition 6. The results in Table 2 hold. √ means "satisfies," • means "does not satisfy," while • means "does not satisfy unless P = NP." ! means that the transformation is not always feasible within the language.

CD FO SFO EN SEN ∧C ∧BC ∨C ∨BC ¬C renH[∨, ∃] √ √ √ • • • • √ √ • K/H[∨, ∃] √ √ √ • √ • • AFF √ √ √ √ √ √ √ ! ! ! renH √ • √ √ √ ! ! ! ! ! K/H √ • √ √ √ ! ! ! ! ! HORN √ • √ √ √ √ √ ! ! ! KROM √ √ √ √ √ √ √ ! ! ! KROM,

Proof.

CD When α is a CNF formula and γ is a term, a CNF formula β equivalent to α |γ can be computed in time polynomial in the size of α plus the size of γ by removing from α every clause containing a literal l from γ while removing the complementary literal l from every clause of α containing it. Obviously enough, removing clauses and shortening clauses are two internal laws in the languages KROM and HORN. This shows that KROM, HORN and K/H satisfy CD.

Similarly, when α is an AFF formula and γ is a term (viewed as a set of literals), an AFF formula β equivalent to α |γ can be computed in time polynomial in the size of α plus the size of γ by replacing in α every occurrence of a literal l by ⊤ when l belongs to γ and by ⊥ when l belongs to γ . As to renH, it is not hard to see that if V is a Horn renaming for a renH formula α then for any term γ , V also is Horn renaming for the formula β as defined above.

Hence renH also satisfies CD.

Then As to KROM, it is well-known that the set of prime implicates of a KROM formula α can be computed in time polynomial in the size of α and that each such prime implicate is a binary clause (see [START_REF] Marquis | Handbook on Defeasible Reasoning and Uncertainty Management Systems[END_REF]). Furthermore, the prime implicates of ∃X.α with X ⊆ PS are the prime implicates of α which do not contain any atom from X (Proposition 55 in [START_REF] Marquis | Handbook on Defeasible Reasoning and Uncertainty Management Systems[END_REF]), showing in particular that PI satisfies FO. Together, this shows that KROM satisfies FO.

The fact that AFF satisfies FO is given by Lemma 1 from [72].

Now, taking advantage of the fact that for any C -QDAG representation of the form ∨(α 1 , . . . , α n ) and any finite subset X of PS ∃X. ∨ (α 1 , . . . , α n ) is logically equivalent to ∨(∃X.α 1 , . . . , ∃X.α n ), we get that each of KROM[∨] and AFF [∨] satisfies FO.

It remains to consider the cases of HORN, K/H, renH and of their disjunction closures. Consider the HORN formula

α n = ( n i=1 ¬x i ) ∧ n i=1 (x i ∨ ¬y i ) ∧ (x i ∨ ¬z i )
and the set X n = {x 1 , . . . , x n } of atoms. Every clause of the form n i=1 ¬l i where l is y or z is an essential prime implicate of ∃X n .α n and there are 2 n such clauses. This shows that ∃X n .α n has only exponential size CNF representations. Thus HORN does not satisfy FO. Since α n also is a K/H formula and a renH formula, we also get that none of K/H and renH satisfies FO. Finally, the fact that HORN SFO Obviously, every language satisfying FO satisfies SFO as well. Hence it is enough to consider the cases of HORN, K/H, renH and of their disjunction closures.

[∨] (resp. K/H[∨], renH[∨]) does not satisfy FO comes from the fact that HORN[∨, ∃] < s HORN[∨] (resp. K/H[∨, ∃] < s K/H[∨], renH[∨, ∃] < s renH[∨]).
Let us consider first the HORN and renH cases. For any CNF formula α (viewed as a set of clauses) and a propositional variable x ∈ PS, one can compute from α in polynomial time the following three sets of clauses α * , α + , and α -: first remove from α every valid clause to get a set of clauses α ′ ; now, compute α * as the set of clauses of α ′ not containing x as a variable, α + as the set of clauses of α ′ containing x as a (positive) literal, from which x is removed, and compute α -as the set of clauses of α ′ containing ¬x as a (negative) literal from which ¬x is removed. By construction, the conjunction

β of clauses from α * ∪ {δ + ∨ δ -| δ + ∈ α + , δ -∈ α -} is a CNF formula equivalent to (α | ¬x) ∨ (α | x),
hence equivalent to ∃x.α. Since none of α + and α -can contain more clauses or more literals than α, it comes that β can be computed in time polynomial in the size of α. It remains to show that if α is HORN (resp. renH) then the corresponding β is HORN (resp. renH). Assume that α is HORN. Then every clause from α * is a Horn clause; furthermore, by construction every clause δ + ∈ α + is a negative clause and every clause δ -∈ α -is a Horn clause; hence, every clause of the form δ + ∨ δ -is a Horn clause. Similarly, if α is renH and V is any Horn renaming for it, then V also is a Horn renaming for the corresponding β. Hence HORN and renH satisfy SFO.

Since both KROM and HORN satisfy SFO, K/H satisfies SFO as well.

Finally, given that for any C -QDAG representation α and any atom x ∈ PS, we have ∃x.α ≡ (∃x.(α ∧ ¬x) ∨ ∃x.(α ∧ x)), the results for HORN[∨], K/H[∨], and renH[∨] come that each of these languages satisfies CD and ∨BC.

EN For any C -QDAG representations α and β and any finite subset X of PS we have the equivalence ∀X.(α ∧ β) ≡ (∀X.α) ∧ (∀X.β). Furthermore, when δ is a clause, ∀X.δ is equivalent to the clause obtained by removing from δ every literal l such that var(l) ∈ X . Since removing literals from a KROM (resp. HORN) clause leads to a KROM (resp. HORN) clause, altogether we get that each of KROM and HORN satisfies EN, and this shows that K/H satisfies EN as well. Now, if α is a renH formula and V is a Horn renaming for it, then the formula obtained by removing in every clause of α every literal built up from a variable of X still is a renH formula (indeed, V is still a Horn renaming for it). Hence, renH also satisfies EN. Let us consider now the case of an AFF formula α. We assume w.l.o.g. that α is simplified, i.e., for every XOR-clause δ = l 1 ⊕ . . . ⊕ l k of α, either δ reduces to ⊥, or every literal in δ is positive or equal to ⊤ and δ does not contain more than one occurrence of any variable and of ⊤ (if this is not the case it is sufficient to exploit the equivalences ¬x ≡ x ⊕ ⊤, β ⊕ β ≡ ⊥, β ⊕ ⊥ ≡ β to render α simplified while preserving logical equivalence); it is easy to check that if α is a simplified AFF formula containing a variable from X , then ∀X.α is equivalent to ⊥, otherwise ∀X.δ is equivalent to α. Hence, AFF satisfies EN.

The fact that HORN[∃] satisfies EN is a consequence of Corollary 11 from [START_REF] Bubeck | Models and quantifier elimination for quantified Horn formulas[END_REF]. Since KROM[∃] ∼ p KROM and KROM satisfies EN, as a consequence, we also have that K/H[∃] satisfies EN.

As to the case of renH[∃], let us consider a renH[∃] formula α = ∃X.β. Let V be a Horn renaming for β. Since

HORN[∃]

satisfies EN, for every finite subset Y of PS, the formula ∀Y .(∃X.V (β)) can be turned in polynomial time into an equivalent formula ∃Z .γ from HORN[∃]. From the substitution metatheorem, we have

V (∀Y .(∃X.V (β))) ≡ V (∃Z .γ ). Hence, we have ∀Y .(∃X.V (V (β))) ≡ ∃Z .V (γ ). Since V (V (β)) = β, we get that ∀Y .(∃X.β) ≡ ∃Z .V (γ ). Clearly, ∃Z .V (γ ) is a renH[∃] formula; indeed, V (γ ) is a renH formula since V (V (γ )) = γ is a HORN formula. Since ∃Z .V (γ ) can be computed in polynomial time from ∀Y .(∃X.β), we get that renH[∃] satisfies EN.
Finally, for any C -QDAG representation α and any finite subset X of PS we have that α is valid iff ∀Var(α).α is valid iff ∀Var(α).α is consistent (since ∀Var(α).α has no free variable, it is equivalent to ⊤ or to ⊥, hence it is consistent precisely when it is valid). Hence every language satisfying CO but not satisfying VA unless P = NP cannot satisfy EN unless P = NP. This is the case for each language among Finally, as to renH[∨] and renH[∨, ∃], let α be a CNF formula over n variables x 1 , . . . , x n . Let α ′ be the HORN formula obtained by replacing every positive literal x i in α by the negative literal ¬x ′ Finally, let us consider the case of HORN[∃]: let ∃X 1 .α 1 , ..., ∃X n .α n be nHORN [∃] formulae where each α i (i ∈ 1, . . . , n) is a HORN formula. For each i ∈ 1, . . . , n, let α i i be the HORN formula obtained by replacing in α i every occurrence of x ∈ X i by a fresh variable x i , and let X i i be the set of all the variables x i generated in the construction of α i i . By construction, every variable from X i i does not occur in any α j j when j = i. Hence, n i=1 ∃X i .α i is equivalent to Similarly, consider the AFF formula α = ¬x ∧ ¬y. No AFF formula is equivalent to ¬α, hence the ¬C transformation is not always feasible in AFF. • HORN[∃] ∼ e HORN.

∃ n i=1 X i i . n i=1 α i i . Clearly enough, ∃ n i=1 X i i . n i=1 α i i is a HORN[∃]
As to KROM[∨], HORN[∨], K/H[∨], let us consider the DNF formula α n = n i=1 (¬x i ∧ ¬y i ∧ ¬z i ); α n is a KROM[∨]
• K/H[∃] ∼ e K/H. • renH[∃] ∼ e renH.
Proof.

• HORN, K/H: Every prime implicate of a HORN formula (resp. a KROM formula) α is a Horn clause (resp. a binary clause). Since the prime implicates of ∃X.α for a finite subset X of PS and a C -DAG representation α are the prime implicates δ of α such that Var(δ) ∩ X = ∅, we get that ∃X.α is equivalent to a HORN formula (resp. a KROM formula) when α is a HORN formula (resp. a KROM formula).

• renH: Let α be a renH formula. A PI formula equivalent to ∃X.α is given by the conjunction β of all prime implicates of α not containing any variable from X . If V is a Horn renaming for α, then V (α) is a HORN formula. Since V (β) is equivalent to ∃X.V (α) and since HORN[∃] ∼ e HORN, V (β) is equivalent to a HORN formula. This shows that β is a renH formula (V is a Horn renaming for it) and this concludes the proof. ✷ Proof. This comes easily from the fact that TERM is included in each of KROM, HORN and AFF; as a consequence, its disjunction closure TERM[∨] is included into each of eight closures above; the fact that DNF = TERM[∨] is complete ends up the proof. ✷ Proposition 9.

• HORN[∃] < s HORN. in order to prove that renH s K/H[∃] and K/H s HORN[∃], it is enough to consider again the horn[∃] formula α n = ∃{y 1 , . . . , y n }.(( n i=1 ¬y i ) ∧ n i=1 ((¬x i ∨ y i ) ∧ (¬z i ∨ y i ))). We have shown above that this formula also is a K/H[∃] formula but that it does not have a representation of size of polynomial in n as a renH formula or as a K/H formula. This concludes the proof. ✷ Proposition 10.

• HORN

[∨, ∃] < s HORN[∨]. • K/H[∨, ∃] < s K/H[∨]. • renH[∨, ∃] < s renH[∨].
Proof. We focus on AC3, the class of propositional representations containing all disjunctions of CNF formulae and all conjunctions of DNF formulae. Since every formula from HORN The proof is based on a theorem due to Sipser [START_REF] Sipser | Borel sets and circuit complexity[END_REF]. This theorem can be expressed as follows: consider any Boolean function α n k over n 2k-2 variables, represented by a NNF formula of depth k > 1 and such that all the leaves are labeled by variables occurring once in the formula, the ith level (i ∈ 1, . . . , k -1) from the bottom consists of nodes labeled by ∧ (resp. ∨) when i is even (resp. odd), the outdegree of the root node and the deepest internal nodes (those at depth k -1) is equal to n > 1 and the outdegree of every other internal node is equal to n 2 . Sipser showed that such an α n k cannot be represented by a polynomial-sized circuit over {¬, ∨, ∧} of depth at most k -1.

Consider the Boolean function α n 4 over n 6 variables. By construction, it can be represented by a disjunction of n conjunctions β 1 , . . . , β n of DNF formulae, where each β i (i ∈ 1, . . . , n) is the conjunction of n 2 DNFγ i, j ( j ∈ 1, . . . n 2 ), each DNFγ i, j ( j ∈ 1, . . . n 2 ) consists of the disjunction of n 2 terms δi, j, k (k ∈ 1, . . . n 2 ), and finally each term δi, j, k (k ∈ 1, . . . n 2 ) consists of the conjunction of n negated variables ¬x i, j,k,l (l ∈ 1, . . . , n) occurring only once in α n 4 . For each i ∈ 1, . . . , n and j ∈ 1, . . . n 2 , consider now the HORN formula h i, j such that )). First of all, since existential quantifications "distribute" over disjunctions and since each y

h i, j = n 2 k=1 ¬y i, j,k ∧ n 2 k=1 n l=1 (y i, j,k ∨ ¬x i, j,k,l
i, j,k (i ∈ 1, . . . , n, j ∈ 1, . . . , n 2 k ∈ 1, . . . , n 2 ) does not occur in h i ′ , j ′ (i ′ ∈ 1, . . . , n, j ∈ 1, . . . , n 2 ) unless i ′ = i and j ′ = j, we have that ∃Y .( n i=1 ( n 2 j=1 h i, j )) is equivalent to n i=1 ( n 2 j=1 ∃ n 2 k=1 {y i, j,k }.h i, j
). Finally, by construction, for each i ∈ 1, . . . , n and j ∈ 1, . . . , n 2 , γ i, j = n 2 k=1 δ i, j,k is the IP representation of ∃ n 2 k=1 {y i, j,k }.h i, j , hence it is equivalent to it. The replacement metatheorem for propositional logic concludes the proof. ✷ Proposition 11. The results in Table 3

hold. AFF[∨] renH[∨, ∃] K/H[∨, ∃] HORN[∨, ∃] KROM[∨] AFF[∨] ∼ s Table 5
The relative succinctness of the full disjunctive closures of KROM, HORN, AFF, K/H, and renH.

AFF[∨] renH[∨, ∃] K/H[∨, ∃] HORN[∨, ∃] KROM[∨] AFF[∨] ∼ s renH[∨, ∃] ∼ s ≤ s K/H[∨, ∃] ∼ s ≤ s ≤ s HORN[∨, ∃] ∼ s KROM[∨] ∼ s Table 6
The relative succinctness of the full disjunctive closures of KROM, HORN, AFF, K/H, and renH.

AFF[∨] renH[∨, ∃] K/H[∨, ∃] HORN[∨, ∃] KROM[∨] AFF[∨] ∼ s renH[∨, ∃] ∼ s ≤ s ≤ s ≤ s K/H[∨, ∃] ∼ s ≤ s ≤ s HORN[∨, ∃] ∼ s KROM[∨]
∼ s

Table 7

The relative succinctness of the full disjunctive closures of KROM, HORN, AFF, K/H, and renH.

AFF[∨] renH[∨, ∃] K/H[∨, ∃] HORN[∨, ∃] KROM[∨] AFF[∨] ∼ s renH[∨, ∃] ∼ s ≤ s ≤ s ≤ s K/H[∨, ∃] ∼ s ≤ s ≤ s HORN[∨, ∃] s ∼ s s KROM[∨, ∃] ∼ s
Proof. The proof is broken into six steps, where we prove some succinctness relationships between languages, and then apply transitivity of ≤ s to possibly infer new relationships. Associated with each step of the proof is a table in which we mark all relationships proved at the step.

[∨, ∃] ⊆ K/H[∨, ∃], HORN[∨, ∃] ⊆ renH[∨, ∃], KROM[∨] ⊆ K/H[∨, ∃],
we get the results given in Table 5. Since KROM satisfies CO, we can easily determine in polynomial time which β i are consistent. All the β i (i ∈ 1, . . . , n) which are inconsistent can be removed from the disjunction without questioning equivalence (if they are all inconsistent, the input formula is associated with ⊥, which is a renH[∨, ∃] formula). In the remaining case, since every consistent KROM formula is a renH formula, the resulting disjunction is a renH[∨, ∃] formula equivalent to the input formula. Hence we get the results given in Table 6. α n and whose size is polynomial in n. Especially, m must remain polynomial in n. We also know that HORN[∃] ∼ e HORN (cf. Proposition 7). Hence, if β exists, then there also exists a HORN[∨] formula γ = m i=1 γ i equivalent to α n and with m polynomial in n. Note that the size of γ i (i ∈ 1, . . . , m) can be exponential in the size of β i (this does not matter for the remaining part of the proof).

By construction, α n has 2 n minimal models ω over Var(α n ), where for each i ∈ 1, . . . , n, exactly one of the two variables x i and y i are set to 1 by ω. Consider now any pair ω, ω ′ of distinct minimal models of α n ; by construction, and(ω, ω ′ ) maps each variable to 0, hence it is not a model of α n . Thus, as a consequence of the characterization of HORN by closure of models, ω and ω ′ cannot be models of the same formula γ i . Therefore, every HORN[∨] formula γ = m i=1 γ i equivalent to α n must be such that m ≥ 2 n . This shows that there is no HORN[∨, ∃] formula equivalent to α n and whose size is polynomial in n. Thus, we get the results given in Table 7. KROM[∨] s HORN. Consider the HORN formula α n = n i=1 (¬x i ∨ ¬y i ∨ ¬z i ) for any n. Towards a contradiction, suppose that there exists in KROM[∨] a formula γ = m i=1 γ i equivalent to α n and whose size is polynomial in n; then m must remain polynomial in n.

Table 8

The relative succinctness of the full disjunctive closures of KROM, HORN, AFF, K/H, and renH.

AFF[∨] renH[∨, ∃] K/H[∨, ∃] HORN[∨, ∃] KROM[∨] AFF[∨] ∼ s renH[∨, ∃] ∼ s ≤ s ≤ s ≤ s K/H[∨, ∃] ∼ s ≤ s ≤ s HORN[∨, ∃] s s ∼ s s KROM[∨] s s s ∼ s Table 9
The relative succinctness of the full disjunctive closures of KROM, HORN, AFF, K/H, and renH.

AFF[∨] renH[∨, ∃] K/H[∨, ∃] HORN[∨, ∃] KROM[∨] AFF[∨] ∼ s renH[∨, ∃] ∼ s ≤ s ≤ s ≤ s K/H[∨, ∃] s ∼ s ≤ s ≤ s HORN[∨, ∃] s s ∼ s s KROM[∨] s s s ∼ s
By construction, α n has 7 n models over Var(α n ). How many models of α n can be models of the same γ i (i ∈ 1, . . . , m)? Let us consider any ω 1 , ω 2 , ω 3 ∈ Mod(γ i ), it cannot be the case that for any i ∈ 1, . . . , n, we have ω 1

(x i ) = 0, ω 1 (y i ) = 1, ω 1 (z i ) = 1, ω 2 (x i ) = 1, ω 2 (y i ) = 0, ω 2 (z i ) = 1, ω 3 (x i ) = 1, ω 3 (y i ) = 1, ω 3 (z i ) = 0. Indeed, if this were the case, we would have maj(ω 1 , ω 2 , ω 3 )(x i ) = maj(ω 1 , ω 2 , ω 3 )(y i ) = maj(ω 1 , ω 2 , ω 3 )(z i ) = 1. If γ i is a KROM formula, then maj(ω 1 , ω 2 , ω 3 )
should also be a model of γ i . But maj(ω 1 , ω 2 , ω 3 ) is not a model of α n . Thus, each γ i cannot have more than 6 n models of α n over Var(α n ). Subsequently, the pigeon/hole principle shows that at least ⌈( 76 ) n ⌉KROM formulae γ i are required to cover the models of α n . The fact that ⌈( 76 ) n ⌉ is exponential in the size of α n concludes the proof. By transitivity of ≤ s , we get the results given in Table 8. to α n and whose size is polynomial in n. Especially, m must remain polynomial in n. We also know that K/H[∃] ∼ e K/H (cf. Proposition 7). Hence, if β exists, then there also exists a K/H[∨] formula γ = m i=1 γ i equivalent to α n and with m polynomial in n.

Let us now prove that if such a γ exists, then there also exists a KROM[∨] formula δ = m i=1 δ i equivalent to α n and with m polynomial in n. Consider any K/H formula γ i (i ∈ 1, . . . , m) and suppose that it is a HORN formula. Then γ i is equivalent to an implicant of α n . This is obvious if γ i is inconsistent. In the remaining case, every clause x i ∨ y i ∨ z i (i ∈ 1, . . . , n) of α n must be implied by a prime implicate of γ i , which must be a Horn clause; hence this prime implicate must be equivalent to x i , y i or z i . Accordingly, γ i must be equivalent to a term, hence to a KROM formula.

It remains to show that α n has no polyspace representation in KROM[∨]. The proof is similar to the one used for showing that KROM[∨, ∃] s HORN (this is not surprising since α n is a reverse Horn CNF formula). We get the results given in Table 9. Let α n = n i=1 (x i ⊕ y i ⊕ z i ⊕ ⊤). By construction α n is an AFF formula. Furthermore, the restriction of any model of α n over any {x i , y i , z i } (i ∈ 1, . . . , n) is of the form 000, 011, 101 or 110. Thus, α n has 4 n models over Var(α n ). Since each γ i (i ∈ 1, . . . , m) is a renH formula which entails α n , from [START_REF] Boufkhad | Algorithms for propositional KB approximation[END_REF], there exists a model V i of α n such that V i is a Horn renaming for γ i , and V i (γ i ) | V i (α n ). As explained above, the restriction of V i over any {x i , y i , z i } (i ∈ 1, . . . , n) is of the form 000, 011, 101 or 110. Since applying V i leads to renaming an even number of variables in each set {x i , y i , z i } (i ∈ 1, . . . , n), we necessarily have V i (x i ⊕ y i ⊕ z i ⊕ ⊤) ≡ x i ⊕ y i ⊕ z i ⊕ ⊤, and subsequently V i (α n ) ≡ α n . We are now going to prove that this is not the case, i.e., the number of disjoints in any HORN[∨] formula m i=1 δ i equivalent to α n actually is exponential in n. Consider the subset S of models ω of α n over Var(α n ) such that for each i ∈ 1, . . . , n the restriction of ω over {x i , y i , z i } is of the form 011, 101 or 110. Every pair of distinct models ω and ω ′ from S is such that and(ω, ω ′ ) is not a model of α n ; indeed, there must exist i ∈ 1, . . . , n such that the restrictions of ω and ω ′ over {x i , y i , z i } differ, and and(ω, ω ′ ) is not a model of x i ⊕ y i ⊕ z i ⊕ ⊤ (its restriction over {x i , y i , z i } is of the form 001, 010 or 100). Thus, because of the closure property of HORN formulae, every pair of distinct models in S cannot be models of the same HORN formula δ i . Since S contains 3 n models, the number m of disjoints in m i=1 δ i is lower bounded by 3 n .

This shows that α n has no polynomial-sized representation as a renH[∨, ∃] formula.

Conversely, let us show that AFF[∨] is not at least as succinct as any of renH[∨, ∃], K/H[∨, ∃], HORN[∨, ∃] and KROM[∨].

Consider the formula α n = n i=1 (¬x i ∨ ¬y i ) for any n. It is a KROM formula and a HORN formula. Hence, it is also a K/H formula and a renH formula. Since Var(α n ) contains 2n atoms, 4 n interpretations over Var(α n ) have to be considered. Among them, one can find 3 n models of α n , only, since for each i ∈ 1, . . . , n, there are only 3 truth assignments of x i and y i (over the four possible assignments of those two variables) which satisfy ¬x i ∨ ¬y i . Now, there is no AFF formula β implying α n and with strictly more than 2 n models (taken in the set of models of α n since β | α n must hold). By reductio ad absurdum: if this were the case, then one could find i ∈ 1, . . . , n and ω 1 , ω 2 , ω 3 ∈ Mod(α n ) such that ω 1 (x i ) = 0, ω 1 (y i ) = 0, ω 2 (x i ) = 0, ω 2 (y i ) = 1, ω 3 (x i ) = 1, ω 3 (y i ) = 0. If ω 1 , ω 2 , ω 3 ∈ Mod(β) and β is an AFF formula, then the affine closure property requires ⊕(ω 1 , ω 2 , ω 3 ) to be a model of β, hence a model of α n . But ⊕(ω 1 , ω 2 , ω 3 ) falsifies ¬x i ∨ ¬y i . Subsequently, from the pigeon/hole principle, every AFF[∨] formula equivalent to α n must contain at least ⌈( 32 ) n ⌉AFF formulae as disjuncts. The fact that ⌈( 32 ) n ⌉ is exponential in the size of α n concludes the proof. ✷ Proposition 12. The results in Table 4 Proof. Again, the proof is broken in a number of steps, where we prove some succinctness relationships between languages, and then apply transitivity of ≤ s to possibly infer new relationships. Associated with each step of the proof is a table in which we mark all relationships proved at the step. equivalent to it. Similarly, the AFF formula β n = n i=1 x i (which is also an AFF[∨] formula) has 2 n-1 essential prime implicants, hence there is no polynomial-sized IP formula and no polynomial-sized DNF formula equivalent to it. We get the results given in Table 12.

Table 13:

In the proof of Proposition 11, we have shown that the AFF formula α n = n i=1 (x i ⊕ y i ⊕ z i ⊕ ⊤) has no polynomially-sized renH[∨, ∃] representation. The point is that α n has a polynomially-sized PI representation (consisting in 4n clauses: ¬x i ∨ ¬y i ∨ ¬z i , ¬x i ∨ y i ∨ z i , x i ∨ ¬y i ∨ z i , x i ∨ y i ∨ ¬z i for each i ∈ 1, . . . , n), and a polynomially-sized OBDD < representation for every ordering < which is such that x i , y i , z i (i ∈ 1, . . . , n) are successive elements. Indeed, for each i ∈ 1, . . . , n, one can generate in constant time an OBDD < representation equivalent to each x i ⊕ y i ⊕ z i ⊕ ⊤ and then, starting with the OBDD < representation of x 1 ⊕ y 1 ⊕ z 1 ⊕ ⊤, in an iterative way, replace the ⊤ sink of the current OBDD < representation by the root of the next OBDD < representation. Furthermore, in the proof of Proposition 11, we proved that the formula α n = n i=1 (¬x i ∨ ¬y i ) (for any n) does not have a polynomial-size AFF[∨] representation. The point is that α n is a PI formula, and it also has a polynomially-sized OBDD < representation for every ordering < which is such that x i , y i (i ∈ 1, . . . , n) are successive elements. Indeed, for each i ∈ 1, . . . , n, one can generate in constant time an OBDD < representation equivalent to each ¬x i ∨ ¬y i and then, starting with the OBDD < representation of ¬x 1 ∨ ¬y 1 , in an iterative way, replace the ⊤ sink of the current OBDD < representation by the root of the next OBDD < representation.

Given that PI ≥ p CNF, OBDD < ≥ p d-DNNF, OBDD < ≥ p DNNF T , and the succinctness relationships given in Proposition 11, by transitivity of ≤ s , we get the results given in Table 13.

Table 14:

As to DNNF T , it is enough to show that the family of circular bit shift functions cbs m have polynomially-sized representations in KROM[∨], HORN[∨], K/H[∨], and AFF[∨]. Indeed, it has been proven that such functions do not have polynomially-sized SDNNF representations, where SDNNF is the union of DNNF T for all vtrees T [START_REF] Pipatsrisawat | A lower bound on the size of decomposable negation normal form[END_REF].

For any positive integer m, consider the following Boolean function over 2 m+1 + m variables cbs m (x 0 , . . . , x 2 m -1 , y 0 , . . . , y 2 m -1 , i 0 , . . . , i m-1 ) which is the semantics of the formula whose size is linear in the number of variables of cbs m . In this formula, i b j j denotes the literal i j when b j = 0 and the literal ¬i j when b j = 1; num is the mapping from {0, 1} m to the set of natural numbers which gives the integer represented by the binary string b 0 . . . b m-1 . Thus, the variables i 0 , . . . , i m-1 make precise how the bits of the binary string y 0 . . . y 2 m -1 must be (circularly) shifted, and cbs m (x 0 , . . . , x 2 m -1 , y 0 , . . . , y 2 m -1 , i 0 , . . . , i m-1 ) = 1 exactly when the variables x 0 , . . . , x 2 m -1 and the shifted variables y 0 , . . . , y 2 m -1 are pairwise equal. As to d-DNNF, the result comes easily from the fact that d-DNNF is not at least as succinct as DNF, unless the polynomial hierarchy collapses [START_REF] Darwiche | A knowledge compilation map[END_REF], plus the fact that DNF is polynomially translatable into the disjunction closure and into the full disjunctive closure of each of KROM, HORN, K/H, and renH.

We finally get the results given in Table 14. ✷

Fig. 1 .

 1 Fig. 1. A C -QDAG representation with C = {∧, ∨, ¬, ⊕}.

Fig. 2 .

 2 Fig. 2. A C -QDAG formula with C = {∧, ∨, ¬, ⊕}.

Fig. 3 .

 3 Fig. 3. An OBDD < representation of x 0 ∨ x 1 .

Fig. 4

 4 Fig.4illustrates the polynomial equivalences between disjunctive closures given at Proposition 2.

Proposition 3 .

 3 Let L be any subset of C -QDAG s.t. L is stable by uniform renaming. • If L satisfies CO (resp. CD), then L[∨], L[∃] and L[∨, ∃] satisfy CO (resp. CD). • If L satisfies CO and CD, then L satisfies CE and ME. • If L satisfies CO and CD, then L, L[∨], L[∃] and L[∨, ∃] satisfy MC. • L[∨] and L[∨, ∃] satisfy ∨C (hence ∨BC) and L[∃] and L[∨, ∃] satisfy FO (hence SFO).

Fig. 4 .

 4 Fig. 4. Polynomial equivalences between disjunctive closures. The representation α at the top of the picture belongs to L[∨, ∃]. β 1 [X, Y , Z , T ] and β 2 [X, Y , Z , T ] denote propositional representations (not necessarily tree-structured ones) from L such that Var(β 1 ) = Var(β 2 ) = X ∪ Y ∪ Z ∪ T , where X , Y , Z , and T are pairwise disjoint, finite subsets of PS. The representation α ∃∨ at the bottom, left-hand side of the picture is an (L[∨])[∃] representation into which α can be polynomially translated. The representation α ∨∃ at the bottom, right-hand side of the picture is an (L[∃])[∨] representation into which α can be polynomially translated.

Fig. 7

 7 Fig. 7 depicts the succinctness relationships reported mainly in Proposition 11 and Proposition 12. The closure languages considered in this paper are underlined.

Fig. 7 .

 7 Fig. 7.The succinctness picture for complete classes. An arrow from L 1 to L 2 means that L 1 is strictly more succinct than L 2 , so that a lack of arrow means that the succinctness of L 1 and the succinctness of L 2 are incomparable for sure (or, under the assumption that the polynomial hierarchy does not collapse when d-DNNF is concerned). For a clarity sake, there are two exceptions to this notation, which also concern d-DNNF: it is unknown whether d-DNNF ≤ s PI, and whether d-DNNF ≤ s IP[1].

  the same queries CO, CE, ME, MC. As to transformations, KROM[∨], HORN[∨, ∃], and AFF[∨] satisfy CD, FO, SFO, SEN, ∧BC, ∨C and ∨BC. They are pairwise incomparable w.r.t. succinctness. While K/H[∨, ∃] is strictly more succinct than each of KROM[∨], or HORN[∨, ∃], it does not offer SEN, and while renH[∨, ∃] is strictly more succinct than K/H[∨, ∃], it does not offer ∧BC.

  the conclusion follows. Note that the set of free variables of α is preserved by the translation. -If α is not an L representation and α = ∃x.β with β ∈ L[∨, ∃], then by induction hypothesis, one can compute in polynomial time a representation β ′ ∈ (L[∨])[∃] such that β ′ ≡ β. Since ∃x.β ′ is an (L[∨])[∃] representation equivalent to α, the conclusion follows. Again, the set of free variables of α is preserved by the translation. • L[∨, ∃] ≥ p (L[∃])[∨]. Again, the proof is by structural induction. Let α be any representation from L[∨, ∃]: -If α is an L representation, then it is also an (L[∃])[∨] representation due to the inclusion (L[∃])[∨] ⊇ L which comes from item 0. in Proposition 1.

3 write(γ ) 4 else 5 x

 345 ← first(Var(α)) 6 enumerate(α |x , γ ∪ {x}) 7 enumerate(α |¬x , γ ∪ {¬x}) • If L satisfies CO and CD, then L, L[∨], L[∃] and L[∨, ∃] satisfy MC. • L[∨] and L[∨, ∃] satisfy ∨C (hence ∨BC) and L[∃] and L[∨, ∃] satisfy FO (hence SFO).

  be associated in polynomial time with an equivalent L representation β ′ . Hence ∃Var(γ ).(α ∧ γ ) is equivalent to the L[∃] representation ∃X.β ′ which can be computed in time polynomial in the size of the input. Finally, let α be an L[∨, ∃] representation; since L[∨, ∃] ∼ p (L[∨])[∃] (cf. Proposition 2), we can compute in time polynomial in the size of α an equivalent representation β = ∃X. ∨ (β 1 , .

  HORN, K/H, AFF, renH, their disjunction, existential and full disjunctive closures and the corresponding polynomial-time transformations.

FO

  point 1. of Proposition 3 allows to conclude that each of the [∨], [∃], and [∨, ∃] closures of those languages satisfies CD as well. Each of HORN[∃], K/H[∃], renH[∃], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃] obviously satisfies FO since such a transformation can be done in an implicit way in each of those languages.

  Let us consider the HORN case (the other cases are similar): forgetting a set of variables X in a HORN[∨] formula α amounts to computing a HORN[∨] formula equivalent to the HORN[∨][∃] formula ∃X.α. If HORN[∨] would satisfy FO, then every HORN[∨][∃] formula ∃X.α could be turned in polynomial time into an equivalent HORN[∨] formula. Since HORN[∨][∃] ∼ p HORN[∨, ∃], we would have HORN[∨, ∃] ≥ p HORN[∨]. But this conflicts with the fact that HORN[∨] s HORN[∨, ∃] (in a nutshell, if no polynomialspace translation exists, then no polynomial-time translation exists).

  KROM[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃]. SEN Every language satisfying EN also satisfies SEN. Hence, each of KROM, HORN, K/H, renH, HORN[∃], K/H[∃], renH[∃], AFF satisfies SEN. Furthermore, since for any C -QDAG representation α and a variable x ∈ PS, we have ∀x.α ≡ α |x ∧ α |¬x , every language satisfying both CD and ∧BC also satisfies SEN. Hence each of HORN[∨], KROM[∨], HORN[∨, ∃] satisfies SEN. Since each of HORN[∨], KROM[∨] satisfies SEN, we also have that K/H[∨] satisfies SEN. Similarly, since each of HORN[∨, ∃], KROM[∨, ∃] (∼ p KROM[∨]) satisfies SEN, we have that K/H[∨, ∃] satisfies SEN.

Proposition 8 .

 8 KROM[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃] are complete propositional languages.

Table 7 :

 7 Let us now show that HORN[∨, ∃] s KROM[∨, ∃], HORN[∨, ∃] s K/H[∨, ∃], and HORN[∨, ∃] s renH[∨, ∃]. To do so, it is enough to prove that HORN[∨, ∃] s KROM. Consider the KROM formula α n = n i=1 (x i ∨ y i ) for any n. Towards a contradiction, suppose that there exists in HORN[∨, ∃] a formula equivalent to α n and whose size is polynomial in n; since HORN[∨, ∃] ∼ p HORN[∃][∨] (cf. Proposition 1), there exists as well a HORN[∃][∨] formula β = m i=1 ∃X i .β i equivalent to

  Let β be a renH[∨, ∃] formula equivalent to α n . Since renH[∨, ∃] ∼ p renH[∃][∨] (cf. Proposition 1), β is polynomially translatable into a formula m i=1 β i from renH[∃][∨]. Therefore, if β is a polynomial-sized representation of α n , then m i=1 β i also is apolynomial-sized representation of α n , which implies that m must not be exponential in n.Since renH[∃] ∼ e renH (cf. Proposition 7), each β i (i ∈ 1, . . . , m) can be translated into an equivalent renH formula γ i (which size can be exponential in the size of β i , but this does not matter). The point is that if β has a renH[∃][∨] representation as a disjunction of mrenH[∃] formulae, then it also has a renH[∨] representation as a disjunction of mrenH formulae.

  α m = b 0 ,...,b m-1 ∈{0,1} ⇔ y ( j+num(b 0 ,...,b m-1 ))mod2 m ,

1 j=0(

 1 For each b 0 , . . . , b m-1 ∈ {0, 1}, the formulaβ b 0 ,...,b m-1 = y ( j+num(b 0 ,...,b m-1 ))mod2 m is equivalent to the KROM formula γ b 0 ,...,b m-1 = ¬x j ∨ y ( j+num(b 0 ,...,b m-1 ))mod2 m ) ∧ 2 m -1 j=0 (x j ∨ ¬y ( j+num(b 0 ,...,b m-1 ))mod2 m ). Clearly enough, γ b 0 ,...,b m-1 also is a HORN formula, hence it is a K/H formula and a renH formula. Similarly, β b 0 ,...,b m-1 is also equivalent to the AFF formula δb 0 , . . . , b m-1 = m-1 j=0 lit(i j , b j ) ∧2 m -1 j=0 x j ⊕ y ( j+num(b 0 ,...,b m-1 ))mod2 m ⊕ ⊤ where lit(i j , b j ) = i j when b j = 0 and lit(i j , b j ) = i j ⊕ ⊤ when b j = 1. Both γ b 0 ,...,b m-1 and δ b 0 ,...,b m-1 can be computed in time linear in the size of β b 0 ,...,b m-1 , hence linear in the number of variables of cbs m . As a consequence, b 0 ,...,b m-1 ∈{0,1} γ b 0 ,...,b m-1 is a KROM[∨] (and a HORN[∨], a K/H[∨], a renH[∨]) formula equivalent to α m , and b 0 ,...,b m-1 ∈{0,1} δ b 0 ,...,b m-1 is an AFF[∨] formula equivalent to α m . The fact that the size of any of b 0 ,...,b m-1 ∈{0,1} γ b 0 ,...,b m-1 and b 0 ,...,b m-1 ∈{0,1} δ b 0 ,...,b m-1 is linear in the number of variables of cbs m completes the proof.

  . . , x n } ⊆ PS, then ∃X.α is a short for ∃x 1 . ∃x 2 .(...∃x n .α)...

and ∀X.α is a short for ∀x 1 . ∀x 2 .(...∀x n .α)...

Table 2

 2 KROM, HORN, K/H, AFF, renH, their disjunction, existential and full disjunctive closures and the corresponding polynomial-time transformations.

  AFF[∨] are complete languages, while KROM, HORN, K/H, renH, AFF and their existential closures are not (see Proposition 7 and Proposition 8 above).

• HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃] satisfy the same queries as the corresponding disjunction closures, namely HORN[∨], K/H[∨], renH[∨] (see Proposition 5), and more transformations than them (see Proposition 6), since they offer FO "for free". • due to the obvious inclusion HORN[∨] ⊆ HORN[∨, ∃], we have that HORN[∨, ∃] is at least as succinct as HORN[∨]; and similarly for K/H[∨, ∃] and renH[∨, ∃]. Actually, we can strengthen this point by proving that the full disjunctive closure of HORN (resp. K/H, renH) is strictly more succinct than the corresponding disjunction closure: Proposition 10.

  In Proposition 12, we compare w.r.t. ≤ s the languages KROM[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃] and AFF[∨] with several classes of propositional representations for KC which have been introduced so far, and with CNF. We specifically focus on those target classes for which compilers have been developed, i.e., PI, IP, DNF, OBDD < , d-DNNF, and DNNF T .

	Proposition 12. The results in Table 4 hold.

Table 4

 4 Comparing w.r.t. succinctness the full disjunctive closures of KROM, HORN, K/H, renH, and AFF, with OBDD < , IP, DNF, d-DNNF, DNNF T , PI, and CNF. * means that the result holds unless the polynomial hierarchy collapses.

	CNF	AFF[∨] s , s	renH[∨, ∃] s , s	K/H[∨, ∃] s , s	HORN[∨, ∃] s , s	KROM[∨, ∃] s , s
	PI	s , s	s , s	s , s	s , s	s , s
	DNNF T	s , s	s , s	s , s	s , s	s , s
	d-DNNF	* s , s	* s , s	* s , s	* s , s	* s , s
	DNF IP OBDD <	s , ≥ s s , ≥ s s , s	s , ≥ s s , ≥ s s , s	s , ≥ s s , ≥ s s , s	s , ≥ s s , ≥ s s , s	s , ≥ s s , ≥ s s , s

  Hence each of the full disjunctive closures of KROM, HORN, AFF satisfies less queries than IP but they are incomparable w.r.t. transformations. Furthermore, IP is strictly less succinct than any of the full disjunctive closures of KROM, HORN, K/H, renH, AFF. • DNF satisfies the same queries as any of the full disjunctive closures of KROM, HORN, K/H, renH, AFF, and the same transformations as KROM[∨], HORN[∨, ∃], and AFF[∨]. Since it is strictly less succinct than any of the full disjunctive closures of KROM, HORN, K/H, renH, AFF, it appears as dominated by KROM[∨], HORN[∨, ∃], and AFF[∨]. • PI satisfies all the queries but CT, and the transformations CD, FO, SFO, ∨BC. Hence, any of the full disjunctive closures of KROM, HORN, K/H, renH, AFF satisfies more transformations than PI. In addition, PI is incomparable w.r.t.

succinctness with any of them.

  Hence it offers more queries than the full disjunctive closures of KROM, HORN, K/H, renH, AFF, but it is incomparable with any of them when transformations are considered. OBDD < is also incomparable w.r.t. succinctness with any of the full disjunctive closures of KROM, HORN, K/H, renH, AFF.• DNNF T satisfies the same queries as any of the full disjunctive closures of KROM, HORN, K/H, renH, AFF, and the same transformations as KROM[∨], HORN[∨, ∃], and AFF[∨]. It is incomparable w.r.t. succinctness with any of them. • d-DNNF satisfies all the queries but SE, and it is unknown whether it offers EQ. As to transformations, it offers only CD

(it is unknown whether it satisfies EN, SEN, or ¬C, but it is known that it does not satisfy the other transformations). Thus, the full disjunctive closures of KROM, HORN, K/H, renH, AFF satisfy less queries than d-DNNF but offer additional transformations. Furthermore, d-DNNF is incomparable w.r.t. succinctness with any of the full disjunctive closures of KROM, HORN, K/H, renH, AFF (unless the polynomial hierarchy collapses).

  (resp. K/H[∨, ∃], renH[∨, ∃]) is strictly more succinct than the corresponding disjunction closure HORN[∨] (resp. K/H[∨], renH[∨]).

Actually, applying any/both of those two principles may lead to new classes, which can prove strictly more expressive and strictly more succinct than the underlying class L. Thus, each of the disjunction closure and the full disjunctive closure of any of KROM, HORN, K/H, renH, and AFF is strictly more expressive than the underlying language. Furthermore, the full disjunctive clo-sure HORN[∨, ∃]

  Let L be any subset of C -QDAG s.t. L is stable by uniform renaming.

	Proposition 1), the conclusion follows. Otherwise
	we have β ′ = ∨(β ′ 1 , . . . , β ′ n ) where β ′ i is an L[∃] representation (i ∈ 1, . . . , n). By replacement, α is equivalent to ∃x. ∨ (β ′ 1 , . . . , β ′ n ), which is equivalent to ∨((∃x.β ′ n )). Since the latter representation is an (L[∃])[∨] rep-1 ), . . . , (∃x.β ′ resentation, the conclusion follows. ✷
	Proposition 3.

• If L satisfies CO (resp. CD), then L[∨], L[∃] and L[∨, ∃] satisfy CO (resp. CD).

• If L satisfies CO and CD, then L satisfies CE and ME. Algorithm 1: enumerate(α, γ ).

  Now, since L satisfies FO, with each ∃X.β i (i ∈ 1, . . . , n) we can associate in polynomial time an equivalent L representation β ′ Since the L[∨] representation ∨(β ′ 1 , . . . , β ′ n ) can be computed in polynomial time in the size of α plus the size of X , the conclusion follows.• We prove the ∧C case. Let us consider n representations α 1 , ..., α n from L[∃] where L satisfies ∧C. By construction, for each i ∈ 1, . . . , n, α i is of the form ∃X i .β i where X i is a finite subset of PS and β i ∈ L. With each ∃X i .β i we can associate in polynomial time the equivalent representation

	that ∃X.α ≡ ∨(β ′ 1 , . . . , β ′	i . Applying the replacement metatheorem, 9 we get

n ).

  renH[∨, ∃] satisfies VA unless P = NP since each of those languages includes DNF as a subset and DNF does not satisfy VA unless P = NP. CE, ME The results come directly from the second item of Proposition 3, given that each of the sixteen languages considered here satisfies both CO and CD. IM As to KROM, HORN, K/H, renH, and AFF, the results come from the fact that if a subset of C -QDAG satisfies VA and Since each of K/H[∃] and HORN[∃] is polynomially translatable into renH[∃], it is enough to prove the result for renH[∃]. We first show that the implicant problem for renH[∃] formulae can be reduced in polynomial time into the implicant problem for HORN[∃] formulae. Let ∃X.α be a renH[∃]

CD, then it satisfies IM (this slightly extends Lemma A.7 from

[START_REF] Darwiche | A knowledge compilation map[END_REF]

to C -QDAG representations).

Consider now the case of renH[∃], K/H[∃] and HORN[∃].

  (where each x ′ i is a fresh variable), conjoined with n additional clauses ¬x i ∨ ¬x ′ i (i ∈ 1, . . . , n). Let β ′ be the KROM formulan i=1 (x i ∨ x ′ i ). By construction, α is inconsistent iff α ′ ∧ β ′ is inconsistent. Now,we associate α in polynomial time with the renH[∨] formula γ = (α ′ ∧ ¬y) ∨ (β ′ ∧ y) where y is a fresh variable. γ also is a renH[∨, ∃] formula. We can easily check that ∀y.γ is equivalent to α ′ ∧ β ′ . If renH[∨] (resp. renH[∨, ∃]) would satisfy SEN, then we could compute in time polynomial in the size of α a renH[∨] (resp. renH[∨, ∃]) formula equivalent to ∀y.γ . Since each of renH[∨] and renH[∨, ∃] satisfies CO, we would have a polynomial time algorithm for deciding the satisfiability of α, hence we would have P = NP. ∧C It is obvious that each of KROM, HORN, and AFF satisfies ∧C. ∃], renH[∨, ∃], the results comes from the fact that none of these languages satisfies ∧BC, unless P = NP. Consider now the cases of KROM[∨], HORN[∨], AFF[∨] and HORN[∨, ∃]. Observe that every clause is a formula from any of those languages since every literal is a KROM formula, a HORN formula, and an AFF formula. Determining whether a conjunction of clauses is consistent cannot be achieved in (deterministic) polynomial time unless P = NP (this is the famous sat problem). Since each of KROM[∨], HORN[∨], AFF[∨] and HORN[∨, ∃] satisfies CO, none of them can also satisfy ∧C unless P = NP.

	For K/H, renH, K/H[∃], renH[∃], the non-representability results (!) holds already in the bounded case (∧BC).
	For K/H[∨], renH[∨], K/H[∨,

i

  formula, and it can be generated in polynomial time from ∃X 1 .α 1 , ..., ∃X n .α n . ∧BC Each of KROM, HORN, AFF and HORN[∃] satisfies ∧BC since it satisfies ∧C.As to K/H and K/H[∃], consider the K/H formulae x ∨ y and ¬x ∨ ¬y ∨ ¬z. They are also K/H[∃] formulae. The conjunction of them neither is equivalent to a KROM formula, nor is equivalent to a HORN formula, hence it is not equivalent to a K/H formula. From Proposition 7, we know that K/H ∼ e K/H[∃], hence this conjunction is not equivalent to a K/H[∃] formula. As to renH and renH[∃], consider the two renH formulae α = x ∨ y ∨ z and β = ¬x ∨ ¬y ∨ ¬z. They are also renH[∃] formulae. There is no renH formula logically equivalent to the conjunction α ∧ β. From Proposition 7, we know that renH ∼ e renH[∃], hence this conjunction is not equivalent to a renH[∃] formula. Let us now consider the cases of KROM[∨], HORN[∨], and AFF[∨]. Let α = ∨(α 1 , . . . , α n ) and β = ∨(β 1 , . . . , β m ) be ∧ β j ) can be computed in time polynomial in the size of α plus the size of β, and is a KROM[∨] (resp. HORN[∨], AFF[∨]) formula logically equivalent to the conjunction α ∧ β. Let us focus on the case of HORN[∨, ∃]. Let α and β be two HORN[∨, ∃] formulae. From Proposition 2, since HORN is stable by uniform renaming, one can compute in polynomial time a HORN[∨][∃] formula ∃X.α ′ (resp. ∃Y .β ′ ) equivalent to α (resp. β) where α ′ (resp. β ′ ) is a HORN[∨] formula. Let α ′′ (resp. β ′′ ) be the HORN[∨] formula obtained by replacing in α ′ (resp. β ′ ) every occurrence of x ∈ X (resp. x ∈ Y ) by a fresh variable x ′ and let X ′ (resp. Y ′ ) be the set of all variables x ′ generated in the construction of α ′′ (resp. β ′′ ). By construction α ∧ β is equivalent to (∃X.α ′ ) ∧ (∃Y .β ′ ), which is in turn equivalent to ∃X ′ ∪ Y ′ .(α ′′ ∧ β ′′ ). Now, HORN[∨] satisfies ∧BC. Hence, a HORN[∨] formula γ equivalent to α ′′ ∧ β ′′ can be generated in time polynomial in the size of α ′′ plus the size of β ′′ . Accordingly, ∃X ′ ∪ Y ′ .γ is a HORN[∨, ∃] formula equivalent to α ∧ β, and it can be computed in time polynomial in the size of α plus the size of β. , let us consider the cases ofK/H[∨], renH[∨], K/H[∨, ∃], renH[∨, ∃].Let α be a CNF formula over n variables x 1 , . . . , x n . Let α ′ be the HORN formula obtained by replacing every positive literal x i in α by the negative literal ¬x ′ is a fresh variable), conjoined with n additional clauses ¬x i ∨ ¬x ′ i (i ∈ 1, . . . , n). Let β ′ be the KROM Observe that β ′ is consistent, hence each of α ′ and β ′ is a K/H formula and renH formula. As a consequence, each of them also belongs to K/H[∨], renH[∨], K/H[∨, ∃], and renH[∨, ∃]. Furthermore, both α ′ and β ′ can be computed in time polynomial in the size of α. By construction,α is consistent iff α ′ ∧ β ′ is consistent. If any of K/H[∨], renH[∨], K/H[∨, ∃], or renH[∨, ∃]would satisfy ∧BC, since each of these languages satisfy CO, we would have P = NP. ∨C The non-representability results for KROM, HORN, K/H, renH, AFF, HORN[∃], K/H[∃], renH[∃] come directly from the corresponding non-representability results for ∨BC. The fact that each of KROM[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃] satisfies ∨C is immediate from their definitions. ∨BC Consider the two KROM formulae α = (x ∨ y) ∧ (¬y ∨ ¬z) and β = ¬x ∧ z. Each of α and β belongs as well to K/H, renH, K/H[∃], renH[∃]. Now, α ∨ β is logically equivalent to the formula (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z) for which no equivalent KROM formula (resp. K/H formula, renH formula) exists. From Proposition 7, we know that KROM ∼ e KROM[∃] (resp. K/H ∼ e K/H[∃], renH ∼ e renH[∃]), hence there are no KROM[∃] formula (resp. K/H[∃] formula, renH[∃] As to the HORN case and the AFF case, it is enough to consider α = x and β = y: no HORN formula and no AFF formula is equivalent to α ∨ β. From Proposition 7, we know that HORN ∼ e HORN[∃], hence there is no HORN[∃] formula equivalent to α ∨ β. Finally, the fact that each of KROM[∨], HORN[∨], K/H[∨], renH[∨], AFF[∨], HORN[∨, ∃], K/H[∨, ∃], renH[∨, ∃] satisfies ∨BC comes from the fact that each of them satisfies ∨C. ¬C Consider the KROM formula α = (¬x ∨ y) ∧ (¬x ∨ z) ∧ (x ∨ ¬y) ∧ (¬y ∨ z) ∧ (x ∨ ¬z) ∧ (y ∨ ¬z). α also is a HORN formula, a K/H formula, a renH formula, a HORN[∃] formula, a K/H[∃] formula, and a renH[∃] formula. But ¬α is equivalent to the formula (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z) for which no equivalent KROM formula (resp. HORN formula, K/H formula, renH formula) exists. From Proposition 7, we know that HORN ∼ e HORN[∃], K/H ∼ e K/H[∃], and renH ∼ e renH[∃]. Accordingly, the ¬C transformation is not always feasible in any of KROM, HORN, K/H, renH, HORN[∃], K/H[∃], renH[∃].

	two KROM[∨] (resp. HORN[∨], AFF[∨]) formulae. Then the formula n i=1 j=1 (α i Finallyformula m n i=1 (x i ∨ x ′

i (where each x ′ i i ).

formula) equivalent to α ∨ β.

  formula, a HORN[∨] formula and a K/H[∨] formula. Now, in the proof of Proposition 11 (see Table 9), we show that the renH formula n i=1 (x i ∨ y i ∨ z i ) equivalent to ¬α n has no polynomial-size representation in K/H[∨], hence the conclusion follows. Finally, let us consider the cases of AFF[∨], renH[∨], renH[∨, ∃], K/H[∨, ∃] and HORN[∨, ∃]. DNF is a subset of each of these languages. Now, a DNF formula α is valid iff ¬α is inconsistent. The fact that each of AFF[∨], renH[∨], renH[∨, ∃], K/H[∨, ∃] and HORN[∨, ∃] satisfies CO completes the proof. ✷

	Proposition 7.

  Let us consider first the three first items. For L ∈ {HORN, K/H, renH}, we have to prove that L[∃] < s L, i.e., L[∃] ≤ s L and L s L[∃]. That L[∃] ≤ s L comes immediately from the inclusion L[∃] ⊇ L (cf. item 0. of Proposition 1). The other way around, consider the HORN[∃] formula α n = ∃{y 1 , . . . , y n }.(( n i=1 ¬y i ) ∧ n i=1 ((¬x i ∨ y i ) ∧ (¬z i ∨ y i ))). Since HORN ⊆ K/H and HORN ⊆ renH, this is also a K/H[∃] formula and a renH[∃] formula (cf. item 0. of Proposition 1). Since α n has 2 n essential prime implicates, it does not have a CNF representation of size polynomial in n. Since HORN, K/H, and renH are subsets of CNF, the language CNF is at least as succinct as any of them, so α n does not have a representation of size of polynomial in n as a HORN formula, a K/H formula or a renH formula. For the last two items, we have to prove that renH s K/H[∃], K/H[∃] s renH, K/H s HORN[∃], HORN[∃] s K/H. From Proposition 7, we know that K/H[∃] ∼ e K/H, and that HORN[∃] ∼ e HORN. Furthermore, we know that renH < e K/H < e HORN (cf. Section 5). Altogether, this shows that renH < e K/H[∃] and both < e HORN[∃]. Especially, we have K/H[∃] e renH and HORN[∃] e K/H. Due to the fact that the relation ≤ s is included into the relation ≤ e , we have that for any subsets L 1 and L 1 of C -QDAG, if L 1 e L 2 , then L 1 s L 2 . This shows that K/H[∃] s renH and HORN[∃] s K/H. Finally,

	• K/H[∃] < s K/H. • renH[∃] < s renH. • renH and K/H[∃] are incomparable w.r.t. ≤ s . • K/H and HORN[∃] are incomparable w.r.t. ≤ s .
	Proof.

  [∨], K/H[∨] or renH[∨] is a disjunction of CNF formulae, each of the languages HORN[∨], K/H[∨], and renH[∨] is a subset of AC3, hence we have AC3 ≤ s HORN[∨], AC3 ≤ s K/H[∨], and AC3 ≤ s renH[∨]. In order to prove the proposition, it is thus enough to show that AC3 s HORN[∨, ∃], AC3 s K/H[∨, ∃], and AC3 s renH[∨, ∃]. Since HORN ⊆ K/H and HORN ⊆ renH, we have the inclusions HORN[∨, ∃] ⊆ K/H[∨, ∃] and HORN[∨, ∃] ⊆ renH[∨, ∃] (cf. item 0. of Proposition 1), which imply that K/H[∨, ∃] ≤ s HORN[∨, ∃], and renH[∨, ∃] ≤ s HORN[∨, ∃]. Therefore, in order to show that AC3 s HORN[∨, ∃], AC3 s K/H[∨, ∃], and AC3 s renH[∨, ∃], it is enough to show that AC3 s HORN[∨, ∃]. We do it by exhibiting a HORN[∨, ∃] formula which has no polynomial-sized AC3 representation.

  i, j contains n 3 + 1 clauses of size at most n 2 , hence the HORN formula n 2 j=1 h i, j contains n 5 +n 2 clauses of size at mostn 2 . Let Y = n i=1 ( n 2 j=1 ( n 2 k=1 {y i, j,k })).By construction, the HORN[∨, ∃] formula ∃Y .( n i=1 ( n 2 j=1 h i, j )) can be generated in time polynomial in n. From Sipser theorem, α n 4 has no polynomial-sized AC3 representation. It remains to show that α n

	equivalent to ∃Y .( n i=1 ( n 2 j=1 h i, j	4 is

).

h

Table 5 :

 5 From the obvious equalities and inclusions HORN

Table 6 :

 6 Since

K/H[∨, ∃] ∼ p K/H[∃][∨] (cf. Proposition 1), every K/H[∨, ∃] formula can be associated in polynomial time with an equivalent disjunction n i=1 ∃X i .β i of K/H[∃] formulae.

Table 8 :

 8 Let us now show that KROM[∨] s HORN[∨, ∃], KROM[∨] s K/H[∨, ∃], and KROM[∨] s renH[∨, ∃]. To do so, it is enough to prove that

Table 9 :

 9 We

also have to show that K/H[∨, ∃] s renH[∨, ∃]. To do so, it is enough to prove that K/H[∨, ∃] s renH.

Consider the renH formula α n = n i=1 (x i ∨ y i ∨ z i ) for any n (Var(α n ) is a possible

Horn renaming for it, since if one replaces in α n every literal from L Var(α n ) by its complementary literal, one gets a HORN formula). Towards a contradiction, suppose that there exists in K/H[∨, ∃] a formula equivalent to α n and whose size is polynomial in n; since K/H[∨, ∃] ∼ p K/H[∃][∨] (cf. Proposition 1), there exists as well a K/H[∃][∨] formula β = m i=1 ∃X i .β i equivalent

Table 10 :

 10 Finally, we show that AFF[∨] is incomparable w.r.t. ≤ s w.r.t. any of renH[∨, ∃], K/H[∨, ∃], HORN[∨, ∃] and KROM[∨]. We first show that renH[∨, ∃] s AFF, which proves enough to conclude that renH[∨, ∃] s AFF[∨], K/H[∨, ∃] s AFF[∨], HORN[∨, ∃] s AFF[∨], and KROM[∨] s AFF[∨].

Table 10

 10 The relative succinctness of the full disjunctive closures of KROM, HORN, AFF, K/H, and renH. (γ i ) is a HORN[∨] formula equivalent to α n . At this stage, we have shown that if α n has a polynomial-sized representation as a renH[∨, ∃] formula, then it must also have a HORN[∨] representation with a number of disjoints that is polynomial in n.

		AFF[∨]	AFF[∨] ∼ s	renH[∨, ∃]	K/H[∨, ∃]	HORN[∨, ∃]	KROM[∨]
	Thus, we get that	m i=1 V i

  hold.Comparing w.r.t. succinctness the full disjunctive closures of KROM, HORN, K/H, renH, and AFF, with OBDD < , IP, DNF, d-DNNF, DNNF T , PI, and CNF. * means that the result holds unless the polynomial hierarchy collapses.

	CNF	AFF[∨] s , s	renH[∨, ∃] s , s	K/H[∨, ∃] s , s	HORN[∨, ∃] s , s	KROM[∨, ∃] s , s

Table 11 :

 11 Let L be any language among AFF[∨], renH[∨], K/H[∨], HORN[∨], KROM[∨], and the corresponding existential closures renH[∨, ∃], K/H[∨, ∃], HORN[∨, ∃]. Since TERM ⊆ AFF, TERM ⊆ HORN, TERM ⊆ KROM, HORN ⊆ renH and KROM ≥ p renH, we obviously have DNF ≥ p L, hence we have DNF ≥ s L.In[START_REF] Darwiche | A knowledge compilation map[END_REF], it is proven that PI ≥ s CNF, DNF s CNF, DNF s OBDD < , and IP ≥ s DNF. By transitivity of ≤ s , we get the results given in Table11.

Table 12 :

 12 Consider the following consistent KROM formula α n = n i=1 (¬x i ∨ ¬y i ); it is also a HORN formula, hence it belongs to the disjunction closure and to the full disjunctive closure of each language among KROM, HORN, K/H, and renH. α n has 2 n essential prime implicants, 10 hence there is no polynomial-sized IP formula and no polynomial-sized DNF formula

Table 11

 11 Comparing w.r.t. succinctness the full disjunctive closures of KROM, HORN, K/H, renH, and AFF, with other classes of propositional representations.

	AFF[∨]	renH[∨, ∃]	K/H[∨, ∃]	HORN[∨, ∃]	KROM[∨]

Table 14

 14 Comparing w.r.t. succinctness the full disjunctive closures of KROM, HORN, K/H, renH, and AFF, with other classes of propositional representations.

	CNF	AFF[∨] s , s	renH[∨, ∃] s , s	K/H[∨, ∃] s , s	HORN[∨, ∃] s , s	KROM[∨] s , s
	PI	s , s	s , s	s , s	s , s	s , s
	DNNF T	s , s	s , s	s , s	s , s	s , s
	d-DNNF	* s , s	* s , s	* s , s	* s , s	* s , s
	DNF IP OBDD <	s , ≥ s s , ≥ s s , s	s , ≥ s s , ≥ s s , s	s , ≥ s s , ≥ s s , s	s , ≥ s s , ≥ s s , s	s , ≥ s s , ≥ s s , s

Each binary connective c which is associative (like ∧, ∨, ⊕) corresponds to a family of connectives (with the same name c) of arity i with i ≥

For each i ≥ 2, the connective c of arity i is defined by: for every i-tuple x 1 , . . . , x i of Boolean values, c(x 1 , . . . , x i ) = c(x 1 , c(x 2 , c(. . . , c(x i-1 , x i )) . . .)).

Closures under other connectives could also be easily defined but seem to be less significant.

In order to alleviate the notations, when △ = {δ 1 , . . . , δ n }, we write L[δ 1 , . . . , δ n ] instead of L[{δ 1 , . . . , δ n }].

√ • √ √From such results, we immediately derive that:

This is a direct consequence of the fact that a CNF formula α is renamable Horn precisely when there exists an interpretation ω such that at most one literal per clause of α is false in ω[START_REF] Lewis | Renaming a set of clauses as a Horn set[END_REF]; indeed, when α is a KROM formula, this last statement exactly means that α is consistent.

• √ √ √ !

√ √ √ √

Remember that KROM[∨, ∃] ∼ p KROM[∨] and that AFF[∨, ∃] ∼ p AFF[∨], see Proposition 4.

Note by the way that determining whether "small" renH[∨] representations which are not HORN[∨] representations exist can be computationally demanding since the detection of a strong renH-backdoor set is W[2]-hard[START_REF] Gaspers | Backdoors to satisfaction[END_REF].

A key observation here is that all β i (i ∈ 1, . . . , n) are pairwise independent, i.e., they do not share any node and for i ∈ 1, . . . , n, every arc reaching a node of β i comes from a node of β i ; if this was not the case, such a proof by structural induction would not work.

In classical propositional logic, this metatheorem states that if β is a subformula of a propositional formula α and β ′ is a formula equivalent to β, then the formula obtained by replacing in α the subformula β by β ′ is a formula equivalent to α[START_REF] Kleene | Mathematical Logic[END_REF] (this comes directly from the truth-functionality of the connectives); this metatheorem also holds for quantified formulae and can be generalized to the case of DAG-based representations (under some conditions); more precisely, given any node N of a C -QDAG representation α let β N be the subgraph of α given by the set S N of nodes of α reachable from N; if every arc of α having its extremity in S N \ {N} also has its origin in S N , then for every C -QDAG representation β ′ equivalent to β, the C -QDAG representation obtained by removing in α every node and every arc of β, and redirecting the arcs entering N to the root of β ′ is a representation equivalent to α.

A prime implicant γ of a formula α is essential iff the disjunction of all prime implicants of α except γ (up to logical equivalence) is not equivalent to α.

Acknowledgements

We would like to thank the anonymous reviewers for many helpful comments.

Appendix A. Proofs Proposition 1. For every subset L, L ′ of C -QDAG and every subset △ 1 , △ 2 of C ∪ {∃, ∀}, we have: