J Ér

Ôme Amilhastre
email: jamilhastre@cameleon-software.com

H Él

Ène Fargier
email: fargier@irit.fr

Alexandre Niveau
email: niveau@cril.fr

C Édric Pralet
email: cpralet@onera.fr

COMPILING CSPs: A COMPLEXITY MAP OF (NON-DETERMINISTIC) MULTIVALUED DECISION DIAGRAMS *

Keywords: Knowledge Compilation, CSP, MDD

Constraint Satisfaction Problems (CSPs) offer a powerful framework for representing a great variety of problems. The difficulty is that most of the requests associated with CSPs are NP-hard. When these requests have to be addressed online, Multivalued Decision Diagrams (MDDs) have been proposed as a way to compile CSPs.

In the present paper, we draw a compilation map of MDDs, in the spirit of the NNF compilation map, analyzing MDDs according to their succinctness and to their tractable transformations and queries. Deterministic ordered MDDs are a generalization of ordered binary decision diagrams to non-Boolean domains: unsurprisingly, they have similar capabilities. More interestingly, our study puts forward the interest of non-deterministic ordered MDDs: when restricted to Boolean domains, they capture OBDDs and DNFs as proper subsets and have performances close to those of DNNFs. The comparison to classical, deterministic MDDs shows that relaxing the determinism requirement leads to an increase in succinctness and allows more transformations to be satisfied in polynomial time (typically, the disjunctive ones). Experiments on random problems confirm the gain in succinctness.

Introduction

The powerful framework of Constraint Satisfaction Problems (CSPs) allows the representation a great variety of problems. Different kinds of requests can be posted on a CSP, such as the classical extraction of a solution, but also enforcement of global inverse consistency for the domains, 1 dynamic addition of new constraints, solutions counting, and even combinations of these requests. For instance, the interactive solving of a configuration problem amounts to a sequence of unary constraints additions, while maintaining global inverse consistency. [START_REF] Gelle | Interactive configuration using constraint satisfaction techniques[END_REF][START_REF] Amilhastre | Consistency restoration and explanations in dynamic CSPs-Application to configuration[END_REF] Most of these requests are NP-hard; however, they must sometimes be addressed online. A possible way of solving this contradiction consists in representing the set of solutions of the CSP as a Multivalued Decision Diagram (MDD), [START_REF] Vempaty | Solving constraint satisfaction problems using finite state automata[END_REF][START_REF] Kam | Multi-valued decision diagrams: Theory and applications[END_REF][START_REF] Andersen | A constraint store based on multivalued decision diagrams[END_REF] that is, as a graph the nodes of which are labeled with variables and the edges of which represent assignments of the variables. In such diagrams, each path from the root to the sink represents a solution of the CSP. MDDs allow several operations, like those previously cited, to be achieved in time polynomial in the size of the diagram. This size can theoretically be exponentially higher than the size of the original CSPs, but it remains low in many applications. Indeed, as they are graphs, MDDs can take advantage of the (conditional) interchangeability of values, and save space by merging identical subproblems. As a matter of fact, decision diagrams have been used in various contexts, e.g., in product configuration, [START_REF] Amilhastre | Consistency restoration and explanations in dynamic CSPs-Application to configuration[END_REF] in recommender systems, [START_REF] Cambazard | Knowledge compilation for itemset mining[END_REF] or, in their original Boolean form, in planning [START_REF] Giunchiglia | Planning as model checking[END_REF][START_REF] Hoey | SPUDD: Stochastic planning using decision diagrams[END_REF] and diagnosis [START_REF] Torasso | Model-based diagnosis through OBDD compilation: A complexity analysis[END_REF] .

Up to our knowledge, these applications always consider (syntactically) deterministic MDDs, that is, MDDs in which edges going out of a node have mutually exclusive labels. However, this assumption is probably not compulsory for many operations, notably the aforementioned ones. Non-deterministic structures could thus be appealing, depending on what is lost and gained when assuming or relaxing the determinism assumption. To evaluate the interest of this relaxation, we propose to draw a compilation map of MDDs, in the spirit of the NNF knowledge compilation map. [START_REF] Darwiche | A knowledge compilation map[END_REF] Such a map provides a way to identify the most succinct language supporting in polynomial time the operations needed for a given application. In this purpose, we conducted a general complexity analysis on MDDs with respect to a variety of requests, coming either from reasoning-oriented problems or from CSP (decision-oriented) applications.

The next section presents the framework of multivalued variable diagrams (MVDs), which correspond to "non-deterministic MDDs"; it includes several sublanguages, yielded from the application of the decision and ordering properties. In Section 3, we study the case of Boolean domains, in order to picture MDDs and MVDs in the NNF knowledge compilation map: we show that, beyond ordered MDDs, which somehow correspond to OBDDs, the language of non-deterministic ordered MVDs is strictly more succinct than both OBDDs and DNFs. Section 4 is devoted to the MVD knowledge compilation map, including a succinctness analysis of the different languages of the family of MVDs, as well as a complexity analysis of many queries and transformations. Section 5 then presents our first experimental results about the relative succinctness of deterministic and non-deterministic MDDs. Last, all proofs are gathered in the appendix.

Compiling Constraint Satisfaction Problems

Constraint satisfaction problems

We consider variables with finite domains of values. For a variable x, Dom(x) denotes the domain of x. For a set of variables X = {x 1 , . . . , x k }, Dom(X) denotes the set of assignments of variables from X, or X-assignments, that is to say, Dom(X) = Dom(x 1 ) × • • • × Dom(x k ), and x denotes an X-assignment: x ∈ Dom(X). When X and Y are disjoint sets of variables, x . y is the concatenation of x and y. Last, for an X-assignment x and a set of variables Z, x| Z denotes the restriction of x to the variables in Z, and x| xi the value assigned to x i in x.

Definition 2.1 (Constraint satisfaction problem). A Constraint Satisfaction Problem (CSP) is an ordered pair P = X, C , where X = {x 1 , . . . , x n } is a finite set of finite-domain variables and C is a finite set of constraints. Each constraint c ∈ C has an associated scope, denoted Scope(c) and included in X, and consists of a set of Scope(c)-assignments: these are the assignments allowed by the constraint.

A solution of P is an X-assignment x compatible with every constraint in C, that is, ∀c ∈ C, x| Scope(c) ∈ C. The set of solutions of P is denoted Sol(P ).

In this paper, we study the compilation of the solution set of CSPs. To this end, we consider a solution set as a Boolean function on the CSP's variables X, mapping each X-assignment x to ⊤ if x is a solution, and to ⊥ otherwise. We will consider several target compilation languages representing Boolean functions on finite-domain variables. Definition 2.2 (Target compilation language). Let X be a finite set of finitedomain variables; a target compilation language on X is a set L X of graph structures, together with an interpretation function I L X , mapping each graph φ to a Boolean function I L X (φ) : Dom(X) → {⊤, ⊥}, called its interpretation, and a size function • L X . A subset of a language L X is called a sublanguage of L X .

In the following, we omit the X subscript when there is no ambiguity. We denote languages using a typewriter font, as usual in the knowledge compilation map. [START_REF] Darwiche | A knowledge compilation map[END_REF]

Multivalued variable diagrams

Languages used to compile CSPs have been given various names in the literature; sometimes the same name has been used to denote slightly different languages, yielding ambiguity. We will adopt an explicit terminology here, formally defining one "root" language (that of "multivalued variable diagrams"), and retrieving several sublanguages by the application of structural restrictions. We will discuss in Section 2.3 the other names and forms of the languages we define.

Definition 2.3 (Multivalued variable diagram). A Multivalued Variable Diagram

(MVD) φ on a finite set of finite-domain variables X (denoted Scope(φ)) is a directed acyclic graph φ = N , E where N is a set of nodes containing at most one root and at most one leaf (the sink, denoted Sink(φ)). Each non-sink node N ∈ N is labeled with a variable Var(N ) in X, and each edge going out of N is labeled with a value in the domain of Var(N ).

We denote by Out(N ) (resp. In(N )) the set of outgoing (resp. incoming) edges of N . An edge E ∈ E is often denoted by the triple N, N ′ , a of its source node N , denoted Src(E), its destination node N ′ , denoted Dest(E), and its associated value a, denoted Lbl(E).

Multivalued diagrams constitute a generalization of well-known binary decision diagrams, [START_REF] Bryant | Graph-based algorithms for Boolean function manipulation[END_REF] which represent Boolean functions of Boolean variables. In the same fashion, multivalued diagrams represent Boolean functions of multivalued variables.

Definition 2.4 (Semantics of MVDs

). An MVD φ on X represents a function I(φ) from Dom(X) to {⊤, ⊥}, called the interpretation of φ and defined as follows: for every X-assignment x, I(φ)( x) = ⊤ if and only if there exists a path p from the root to the sink of φ such that for each edge E = N, N ′ , a along p, x| Var(N ) = a.

We say that x is a model of φ whenever I(φ)( x) = ⊤; Mod(φ) denotes the set of models of φ. Figure 1 shows examples of MVDs. To check whether an assignment x = a 1 , . . . , a n ∈ Dom(X) belongs to Mod(φ), one only has to traverse the MDD from the root to the sink and, at every node N labeled with variable x i , to follow an edge labeled with a i , if there exists one; x is a model if and only if the sink is reached.

We define the target compilation language of MVDs using this semantics, together with a size function taking domains into account, since some operations rely on values that are not mentioned in the graph itself.

Definition 2.5 (The MVD language). The MVD X language is the set of all MVDs on X, together with the interpretation function I of Definition 2.4, and the size function associating every MVD φ with the sum of its number of edges and of the cardinalities of all domains of variables from X.

Note that MVDs are non-deterministic, in the sense that edges going out of a node are not necessarily disjoint: starting from the root, choosing a value for each variable does not impose one to follow a single path. In other words, a given assignment can correspond to several complete paths in the graph. This is not the case in existing proposals referring to the compilation of CSPs [START_REF] Vempaty | Solving constraint satisfaction problems using finite state automata[END_REF][START_REF] Amilhastre | Consistency restoration and explanations in dynamic CSPs-Application to configuration[END_REF][START_REF] Andersen | A constraint store based on multivalued decision diagrams[END_REF] : they use multivalued decision diagrams (MDDs), that are (syntactically) deterministic. We define the MDD language as the restriction of MVD to syntactically deterministic graphs; we call this restriction the decision property, 13 refraining from using "determinism" for the sake of consistency with the NNF knowledge compilation map, [START_REF] Darwiche | A knowledge compilation map[END_REF] in which determinism is a semantic property. Definition 2.6 (Decision). A node N in an MVD is a decision node if and only if values labeling edges going out of N are pairwise distinct. An MVD satisfies the

x 3 x 2 x 2 x 2 x 1 x 1 x 1 x 1 x 1 x 1 x 3 x 2 x 2 x 2 x 1 x 1 x 1 x 1 x 2 = x 3 = 1 2 3 1 2 3 1 2 3 1 2 3 2, 3 3 1, 3 2 1 1, 2 1, 2 1, 3 2, 3 1, 2 1, 3 2, 3 3 2 1
Fig. 1. The coloring problem on a star graph (3 variables, 3 colors), an OMVD and a OMDD representing its set of solutions (both for

x 3 < x 2 < x 1 ).
decision property, and is called a multivalued decision diagram (MDD), if and only if all its nodes are decision nodes. The language MDD is the sublanguage of MVD containing all and only MVDs satisfying the decision property.

We also define another syntactic restriction, that of "ordering", which is generally assumed in the literature about CSP compilation, [START_REF] Vempaty | Solving constraint satisfaction problems using finite state automata[END_REF][START_REF] Amilhastre | Consistency restoration and explanations in dynamic CSPs-Application to configuration[END_REF][START_REF] Andersen | A constraint store based on multivalued decision diagrams[END_REF] but was only an option in the original definition of MDDs. [START_REF] Srinivasan | Algorithms for discrete function manipulation[END_REF] Definition 2.7 (Ordering). Let < be a strict total order over a set X of variables. An MVD on X is said to be ordered with respect to < if and only if for every pair of nodes N, M such that N an ancestor of M , Var(N ) < Var(M ) holds.

We call for short "ordered MVD (OMVD) on <", an MVD that is ordered with respect to <. Decision and ordering are the basis for several sublanguages of MVD. Definition 2.8 (Family of OMVDs). We define the following languages:

• OMVD is the sublanguage of MVD containing all and only ordered MVDs; • OMVD < is the sublanguage of OMVD containing all and only MVDs that are ordered with respect to a given <; • OMDD (resp. OMDD < ) is the sublanguage of OMVD (resp. OMVD < ). containing all and only OMVDs that satisfy the decision property.

In other words, OMVD is the union of all OMVD < (for any <), and OMDD (resp. OMDD < ) is the intersection of OMVD (resp. OMVD < ) with MDD. It obviously holds that OMDD < ⊆ OMDD ⊆ MDD and that OMVD < ⊆ OMVD ⊆ MVD.

Similarly to binary decision diagrams, we suppose that MVDs are in reduced form, that is, (i) isomorphic nodes (labeled with the same variable and pointing to the same children with the same labels) have been merged, (ii) redundant nodes (having a unique child and one edge per value in the variable's domain) have been skipped, and (iii) nodes with no parent (except for the root) or no successor (except for the sink) have been removed. Assuming that MVDs are reduced is harmless, because reduction can be done in time polynomial in the size of the diagram. Proposition 2.9 (Reduction). Let L be one of the languages we defined. There exists a polynomial algorithm that transforms any φ in L into a reduced φ ′ in L such that I(φ ′ ) = I(φ) and φ ′ ≤ φ .

Related languages

The MVD framework covers several languages that have been used to compile CSPs; we discuss them in this section and show how they can come down as MVDs.

Finite-state automata

Up to our knowledge, the first paper about CSP compilation is due to Vempaty, 4 who used deterministic finite-state automata (DFAs) from computability theory. The idea is to represent X-assignments as words over an alphabet Σ X = x∈X Dom(x); for example, the word abc corresponds to the {x, y, z}-assignment in which x = a, y = b, and z = c (considering the variable order x < y < z). The solution set of any CSP then corresponds to a set of words, i.e., to a finite formal language; any finite formal language being regular, this solution set can thus be represented by a deterministic finite-state automaton accepting this language.

Remark that the usual notion of DFA is more general than the one used in CSP compilation. For instance, all paths in a DFA representing a CSP must have the same (finite) length; it is obviously not the case for general DFAs, which can recognize even infinite languages. In the context of CSP compilation, [START_REF] Vempaty | Solving constraint satisfaction problems using finite state automata[END_REF][START_REF] Amilhastre | Consistency restoration and explanations in dynamic CSPs-Application to configuration[END_REF][START_REF] Hadzic | On automata, MDDs and BDDs in constraint satisfaction[END_REF] the use of the term "DFA" is metonymic.

These structures are very close to ordered multivalued decision diagrams. Except for the differences in terminology, the main distinction, as shown by Hadzic et al., [START_REF] Hadzic | On automata, MDDs and BDDs in constraint satisfaction[END_REF] is the fact that a path in an OMDD needs not mention all the CSP variables in the scope, whereas automata cannot "skip" a variable, since it would change the formal language they accept. However, this restriction is harmless: in an OMDD φ, the number of "skipped" edges is bounded by e × d × |X| edges, where e is the number of edges and d the cardinal of the largest domain (at worst, we have to add |X| nodes with d edges for each edge already in the graph). This number being bounded by φ

3 , adding all "skipped" edges in φ makes it only polynomially larger.

Deterministic finite-state automata thus correspond to OMDD; similarly, using non-deterministic finite-state automata (NFAs) to compile CSPs would correspond to using OMVD. Finally, note that by using a different kind of alphabet (such as Σ ′ X = { x, a : x ∈ X, a ∈ Dom(x)}), it is possible to cast non-ordered MDDs and MVDs as specific DFAs and NFAs, respectively.

MDDs with two leaves

In their original definition, [START_REF] Srinivasan | Algorithms for discrete function manipulation[END_REF] MDDs are not necessarily ordered, and can have several leaves (to represent functions with several output values). However, in the literature, it is often assumed that MDDs are ordered and that they have exactly two leaves, in the manner of BDDs-a ⊤-leaf, indicating assignments that are models of the function represented, and a ⊥-leaf, indicating countermodels.

Yet, since two-leaf MDDs are syntactically deterministic, each assignment corresponds to exactly one complete path from the root to a leaf; such a path leads either to the ⊤-leaf or to the ⊥-leaf. Consequently, the ⊤-leaf plays the role of the sink in our definition of MDDs, whereas the ⊥-leaf is actually redundant: removing it, and reducing the graph to remove dangling edges and nodes, we get exactly our (single-leaf) MDDs. Moreover, adding a ⊥-leaf to a single-leaf MDD φ is also easy: for each node N , and each value a ∈ Dom(Var(N )) for which N has no outgoing edge, add an edge N, ⊥, a . The number of added edges is bounded by n × d, where n is the number of nodes in φ and d the cardinal of the largest domain. Both n and d being bounded by φ , the number of added edges is at most polynomial.

Consequently, our choice (also made by Hadzic et al. [START_REF] Hadzic | On automata, MDDs and BDDs in constraint satisfaction[END_REF] ) to define the MDD language as containing single-leaf MDDs rather than two-leaf MDDs, is harmless from the point of view of the knowledge compilation map, while offering a consistent notation for non-deterministic structures (in which the ⊥-leaf is meaningless, since a given assignment can be associated with several paths).

MVDs in the Boolean Knowledge Compilation Map

In this section, we study the relationship between MVDs and languages in the Boolean knowledge compilation map, notably BDDs. Let us start by defining concepts allowing a formal comparison of target languages. The first one concerns the "translation" of elements of some language into another language; when this translation is tractable, the first language inherits many properties of the second one. [START_REF] Fargier | Extending the knowledge compilation map: Krom, Horn, affine and beyond[END_REF] Definition 3.1 (Translatability). A target language L 2 is polynomially translatable (resp. linearly translatable) into another target language L 1 , which we denote L 1 ≤ P L 2 (resp. L 1 ≤ L L 2 ), if and only if there exists a polynomial (resp. linear) algorithm A L2 →L1 mapping any element in L 2 to an element in L 1 with the same interpretation.

When translations A L1 →L2 and A L2 →L1 are linear and stable, i.e., when

A L1 →L2 = A -1
L2 →L1 , we say that L 1 and L 2 are linearly equivalent, denoted L 1 ≡ L L 2 . Linearly equivalent languages are so close that they can somehow be considered as identical; the complexity of operations is the same for both languages.

Another important concept is succinctness, that compares languages with respect to their ability to represent data in a compact manner. [START_REF] Gogic | The comparative linguistics of knowledge representation[END_REF][START_REF] Darwiche | A knowledge compilation map[END_REF] Definition 3.2 (Succinctness). A target language L 1 is at least as succinct as another target language L 2 (denoted L 1 ≤ s L 2 ) if and only if there exists a polynomial P (•) such that for each element φ of L 2 , there exists an element ψ of L 1 having the same interpretation and verifying ψ ≤ P ( φ ).

Relation ≤ s is a preorder. We denote ∼ s its symmetric part, and < s its asymmetric part. Of course,

L 1 ≤ L L 2 ⇒ L 1 ≤ P L 2 ⇒ L 1 ≤ s L 2 .
To highlight the relationship between MVDs and the NNF knowledge compilation map, [START_REF] Darwiche | A knowledge compilation map[END_REF] let us consider the Boolean case. For any sublanguage L of MVD, let L B be the sublanguage of L obtained when restricting it to Boolean variables.

The BDD and MDD B languages are linearly equivalent: to transform a BDD into a Boolean MDD, remove the ⊥-leaf and reduce the graph. To transform a Boolean MDD into a BDD, add a ⊥-leaf, and for any node that has only one outgoing edge E, add an edge pointing to the ⊥-leaf, labeled by 0 if Lbl(E) = 1 and by 1 otherwise.

Proposition 3.3. MDD B ≡ L BDD, OMDD B ≡ L OBDD, and OMDD B < ≡ L OBDD < .
As they are not necessarily deterministic, multivalued variable diagrams capture fragments beyond the BDD family. DNFs, for instance, can be represented as OMVDs in linear time, although some DNFs have no polynomial OBDD (and thus OMVD) representation. OMVD can hence be seen as a proper "superset" of DNF. The results of our succinctness analysis are depicted in Table 1 (see also Figure 2 for the Boolean case). Some of these results are not surprising and directly follow from the fact that OMDD and OMDD < collapse into OBDD and OBDD < when domains are Boolean: OMDD < ≤ s OMDD is a straightforward consequence of OBDD < ≤ s OBDD. Some other results are derived from the NNF map in a less immediate way; for instance OMDD ≤ s OMVD < holds since OMVD B < ≤ L DNF and OBDD ∼ s OMDD B : if OMDD ≤ s OMVD < were true, we could derive OBDD ≤ s DNF, which has been proven false. [START_REF] Darwiche | A knowledge compilation map[END_REF] Some results are harder to get. For instance, in order to prove that OMVD ≤ s MDD, we used the n-coloring problem of a clique containing n vertices. On the one hand, it can be shown that the set of solutions Sol of this problem can be represented as an MDD of size polynomial in n. On the other hand, it is possible to prove that any OMVD representing Sol contains at least 2 n nodes. Figure 3 shows the corresponding blow-up on a small instance.

We get OMVD < ≤ s OMDD by generalizing the classical proof of OMDD < ≤ s OBDD: we can show that when compiling the CSP compensate for the exponential blow-up caused by ordering all y i before all z i . We also get a direct proof of OMDD < ≤ s OMVD < by considering another CSP, the problem of n-coloring a star graph with n vertices (see Figure 1 for an example with n = 3). Let x 1 be the center of the star, and consider the order

n i=1 [y i = z i ], non-determinism cannot x 1 x 2 x 2 x 2 x 3 x 3 x 3 x 1 x 2 x 3 = = =
x n < • • • < x 2 < x 1 :
the OMDD on < representing this problem contains at least 2 n nodes and n • 2 n-1 edges, whereas it can be shown that this CSP can be represented by an OMVD on the same order < and of size polynomial in n.

Queries and transformations

As outlined by Darwiche and Marquis, 11 evaluating the suitability of a target compilation language for a particular application consists in balancing its succinctness against the set of requests that it supports in polynomial time. The requests identified by Darwiche and Marquis are oriented towards applications in knowledge management, yet most of them are still meaningful in some applications targeted by the CSP framework. We enrich this set by a few new requests, raised by more decision-oriented applications.

• The most usual requests are checking the consistency of the CSP (CO), extracting one solution (MX), enumerating all solutions (ME), and counting (CT) the number of solutions. • The "context extraction" query (CX) aims at providing the user with all possible values of a variable of interest. • The "conditioning" operation (CD) assigns values to some variables. More generally, the "term restriction" transformation (TR) restricts the possible values of some variables to a subset of their domains. TR, CD and CX are often used in sequence in interactive CSP solving, where users iteratively look for the possible values of the next variables and restrict them according to their preferences. 3 • "Clausal entailment" (CE) is a request coming from reasoning problems: it consists in determining whether all the solutions of a problem satisfy a disjunction of elementary conditions (unary constraints). Reasoning AI applications raise other requests, like VA (is a formula valid?) and ¬C (compute the negation of a given formula). • The equivalence (EQ) and sentential entailment (SE) requests come from model checking. They can be useful for CSP modeling problems: SE corresponds to checking whether a set of constraints is a semantic relaxation of another one (whether the assignments satisfying the latter also satisfy the former); EQ is the equivalence test. • Interactive modeling applications can also involve the manipulation of compiled constraints, with conjunction (∧C), disjunction (∨C) and the aforementioned negation (¬C), so as to build composed constraints from a few operators. This interactive modeling process can also rely on other operations to check the resulting constraint (or problem), e.g., by projecting, through a CX operation, the constraint on one of its variables. • The forgetting operation (FO) allows one to eliminate some (intermediate) variables from the problem-this amounts to an existential projection of the problem. Its dual operation, ensuring (EN), performs a universal variable elimination. The forgetting and ensuring operations are notably relevant for compilation-based approaches of planning, such as the "planning as model checking" paradigm. [START_REF] Giunchiglia | Planning as model checking[END_REF] All these operations are often performed in sequence. Conditioning (CD) followed by model extraction (MX) can for instance be useful in planning under uncertainty: if we suppose that a decision policy π associating decisions with states has already been compiled, CD allows π to be conditioned by the current state, whereas MX allows a valid decision for that state to be extracted. Another example is given by online diagnosis applications: the (compiled) model of the system is first conditioned by the observations (CD), then CX can give the possible failure modes of each component in the system. More complex failure hypotheses can be checked via clausal entailment (CE) queries.

Let us now adopt a more formal stance. In a compilation map, the ability of a language L to efficiently achieve operations defines properties of L, which L can satisfy or not. These properties serve as criteria for deciding whether L is appropriate as a target compilation language for a given problem. More precisely, the operations mentioned above can be partitioned into two sets, viz., the transformations and the queries. Transformations take as input a (compiled) problem and return another one (e.g., the conditioning of a CSP by some assignment produces a CSP with less variables). Queries do not modify the problem, but simply answer a question (e.g., checking the consistency of a CSP).

We formally define the queries and transformations described above; while some are straightforward generalizations of the Boolean case, 11 some others need to be carefully adapted. Let us begin with queries.

i ⊆ Dom(x i ), to 1 if Mod(φ)) ⊆ Mod([x 1 ∈ A 1 ]∨• • •∨[x k ∈ A k ]) (resp. Mod([x 1 ∈ A 1 ] ∧ • • • ∧ [x k ∈ A k ]) ⊆ Mod(φ)
) and to 0 otherwise. • L satisfies SE (resp. EQ) if and only if there exists a polynomial algorithm that maps every pair of MVDs φ, ψ in L such that Scope(φ) = Scope(ψ), to 1 if Mod(φ) ⊆ Mod(ψ) (resp. Mod(φ) = Mod(ψ)), and to 0 otherwise. Before defining transformations, we present the semantic operations on which they are based. • L satisfies CD if and only if there exists a polynomial algorithm that maps every MVD φ in L and every assignment

x of X ⊆ Scope(φ) to an MVD φ ′ in L such that I(φ ′ ) = I(φ)| x . • L satisfies TR if
⊆ Dom(x i ), to an MVD φ ′ in L verifying I(φ ′ ) = I(φ)| [x1∈A1]∧•••∧[x k ∈A k ] . • L satisfies FO (resp. EN) if
MVD φ in L to an MVD φ ′ in L such that I(φ ′ ) = ¬ I(φ).
The results of our analysis of the complexity of queries and transformations are depicted in Tables 2 and3.

Theorem 4.5. The results in Tables 2 and3 hold.

Results for MDD, OMDD, and OMDD < are generally known or follow directly from previous works. [START_REF] Srinivasan | Algorithms for discrete function manipulation[END_REF][START_REF] Kam | Multi-valued decision diagrams: Theory and applications[END_REF][START_REF] Darwiche | A knowledge compilation map[END_REF] OMDDs have almost the same capabilities as OBDDs, which is not surprising, given how strong their relationship is. However, note that single

L CO VA MC CE IM EQ SE MX CX CT ME MVD • • √ • • • • • • • • MDD • • √ • • • • • √ √ √ √

Note:

√ means "satisfies", and • means "does not satisfy, unless P = NP". Most results for DNF, DNNF, d-DNNF, OBDD, and OBDD< are from the NNF map and are given here as a baseline.

Table 3. Results about transformations.

L CD TR FO SFO EN SEN ∨C ∨BC OMVD √ √ √ √ • • ? ? • • • OMDD √ • • • • • • • • • √ OMVD< √ √ √ √ • • √ √ • √ • OMDD< √ • • • • • • √ √ • • • d-DNNF √ √ • • • • • • • • ? OBDD √ • • √ • √ • • • • √ OBDD< √ • • √ • √ • √ • √ √

Note:

√ means "satisfies", • means "does not satisfy", and • means "does not satisfy, unless P = NP". Most results for DNF, DNNF, d-DNNF, OBDD, and OBDD< are from the NNF map and are given here as a baseline.

forgetting and single ensuring, while satisfied by OBDD, are not satisfied by OMDD; this is due to the domain sizes being unbounded. More interestingly, Theorem 4.5 puts forward the attractiveness of nondeterministic OMVDs with respect to transformations. Indeed, OMVD < satisfies more transformations than OMDD < , "losing" only the negation transformation; yet it is strictly more succinct than OMDD < . Similarly, OMVD < is strictly more succinct than DNF, and yet they satisfy the same transformations; the only exception is SEN, but DNF only satisfies it because it is limited to Boolean variables (it does not satisfy it when extended to finite-domain variables).

As for performances with respect to queries, OMVD and OMVD < are less interesting than their deterministic counterparts. However, "only" CT, VA, EQ, IM, and SE are lost when determinism is relaxed (remark that the same requests are lost when comparing DNNF to d-DNNF)-hence the interest of these languages for many applications that do not involve these requests, such as planning, in which one needs to often check consistency, forget variables and extract models, or online configuration, which relies essentially on conditioning and context extraction.

Experimental Results

Table 4 reports some results 18 obtained on randomly generated CSPs containing 15 variables whose domain size is equal to 6. For each line, 50 random problems are generated. For each of these problems, the order < on the variables used in the compiled forms is built via the MCSInv heuristics, [START_REF] Tarjan | Simple linear-time algorithms to test chordality of graphs, test acyclicity of hypergraphs, and selectively reduce acyclic hypergraphs[END_REF] which iteratively chooses a variable connected to the greatest number of remaining variables in the constraint graph. The OMDD compiler we use follows the bottom-up approach 4 : each constraint is compiled as an OMDD, and the elementary OMDDs obtained are then combined by conjunction. The compilation can be pursued by using additional compacting operations, which generalize the merging of isomorphic nodes without preserving determinism [START_REF] Amilhastre | FA minimisation heuristics for a class of finite languages[END_REF] ; in the end, an OMVD is obtained. It appears that the interest of non-deterministic structures is not limited to a few specific problems like those used in proofs: indeed, even on random CSPs, allowing non-deterministic compacting operations can sometimes divide by 2 or more the number of nodes in the graph.

Conclusion

Both theoretical complexity results and experiments show that relaxing the determinism requirement in ordered decision diagrams can improve succinctness. Relaxing determinism also allows more transformations to be achieved in polynomial time: typically, all transformations (except for SEN, which depends on the domain size) satisfied by DNF are also satisfied by OMVD < . This includes forgetting and disjunction, which are not satisfied by deterministic languages. The price to pay when putting determinism away is the loss of the negation transformation, and of the counting, validity, equivalence, and implication queries (note that the same operations are lost when going from deterministic to non-deterministic DNNFs). As a result, OMVD < is especially appealing for applications relying on transformations (with the exception of negation) and on basic consistency queries (CO, MX, ME, CX), such as planning and online configuration. From the theoretical point of view, we also established that, when restricted to Boolean domains, OMVD < is a new fragment in the NNF map, below DNNF and above DNF and OBDD. Moreover, OMVD < satisfies more queries and transformations than DNNF does.

The next step is to introduce decomposable AND nodes in the MVD framework. This should allow AND/OR graphs to be captured, and also new fragments to be defined, such as non-deterministic AND/OR graphs.

Appendix A. Proofs

This appendix gathers all proofs of propositions and theorems in the paper. Note that most results are already known, straightforward, or inherited from the BDD framework; we tried to be exhaustive to save the reader the need to refer to numerous sources while checking proofs. These sources include, as far as we know, the original knowledge compilation map, [START_REF] Darwiche | A knowledge compilation map[END_REF] works about MDDs, [START_REF] Srinivasan | Algorithms for discrete function manipulation[END_REF][START_REF] Kam | Multi-valued decision diagrams: Theory and applications[END_REF] and our knowledge compilation map of set-labeled diagrams [START_REF] Niveau | Representing CSPs with set-labeled diagrams: A compilation map[END_REF] (from which a number of the following proofs are directly taken or lightly adapted).

As usual with compilation maps, several proofs use the fact that all languages presented allow Boolean terms and clauses to be represented in linear time and space. The proof is taken from the Boolean case. [START_REF] Darwiche | A knowledge compilation map[END_REF] Lemma A.1. Given an order < between variables, any term or clause in propositional logic can be expressed in the OMDD B < language in linear time. Proof. In order to represent a term

t = ℓ 1 ∧ • • • ∧ ℓ k or a clause c = ℓ 1 ∨ • • • ∨ ℓ k
as an OMDD, let us order its literals in such a way that i < j if and only if Var(ℓ i ) < Var(ℓ j ). Then, let us build a chain of nodes N 1 , . . . , N k , N k+1 , where for each i ∈ {1, . . . , k}, Var(N i ) = Var(ℓ i ) and where N k+1 is a sink.

For the term, edges are as follows: each non-sink node N i has one child N i+1 , and the edge label is ⊤ if ℓ i is a positive literal and ⊥ ℓ i is a negative literal.

For the clause, edges are as follows: each node N i for i < k has two children, N i+1 and the sink N k+1 . If ℓ i is a positive literal, the edge pointing to N i+1 labeled ⊥ and the one pointing to N k+1 is labeled ⊤. If ℓ i is a negative literal, it is the opposite. Finally, N k has the sink as unique successor, via an edge labeled ⊤ ℓ k is a positive literal, and ⊥ otherwise.

A.1. MVDs in the NNF map

Proof of Proposition 3.4. We first show that OMVD B < ≤ L DNF. Let φ be a DNF, and < a strict total order on Scope(φ). First, let us transform each term in φ into a Boolean-variable OMDD, ordered with respect to <; thanks to Lemma A.1, we know that this process is in linear time, and thus that the term-OMDDs we obtain are of size linear in the size of φ. Let x be the smallest variable (for <) mentioned in any of the term-OMDDs. Note that x can only appear in a root node; merge all the roots labeled with x into a single root node R. Then, for each term-OMDD that does not mention x, denoting N its root, add two edges R, N, ⊤ and R, N, ⊥ .

The resulting graph, denoted ψ, is an element of OMVD B < (it does not satisfy the decision property when φ contains at least two terms), and has been obtained in time linear in the size of φ. We now show that φ and ψ have the same interpretation.

Let y ∈ Mod(φ); y satisfies at least one term in φ. If this term contains x, then the root of the corresponding term-OMDD has been merged into the root of ψ; if it does not contain x, by construction, there exists an edge labeled with y| x between the root of ψ and the root of the corresponding term-OMDD. In both cases, there exists a path from the root to the sink of ψ that is compatible with y.

Reciprocally, let y ∈ Mod(ψ). There exists a path from the root to the sink of ψ that is compatible with y. This path traverses one of the term-OMDDs, so y satisfies one of the terms in φ, therefore it is a model of φ. Proof. Let X be a set of 2n Boolean variables, and let < b be a total strict order on X. We are going to show that there exists a family Γ n of Boolean functions over X, and a total strict order < a on X, such that

• Γ n can be represented as an OMDD on < a of size polynomial in n;

• all representations of Γ n as OMVDs on < b are of size exponential in n.

Let us consider that X is partitioned into two sets, Y {y 1 , . . . , y n } and Z = {z 1 , . . . , z n }, such that the total strict order < b on X verifies

y 1 < b y 2 < b . . . < b y n < b z 1 < b z 2 < b . . . < b z n .
Let Γ n be the Boolean function

n i=1 [y i = z i ].
We consider the total strict order < a on X, defined as

y 1 < a z 1 < a y 2 < a z 2 < a . . . < a y n < a z n .
Γ n can be represented as an OMDD on < a of size polynomial in n: each constraint x i = y i can be represented as an OMDD with only 3 nodes and 4 edges (recall variables in X are Boolean), and since they do not share variables, these small OMDDs can be chained (replacing the sink of each one by the root of the next one) into an OMDD respecting the order < a , which we denote as φ a n . Now, we show that the size of any OMVD on < b representing Γ n is exponential in n. Let φ b n be an OMVD on < b representing Γ n . Consider an edge E N, N ′ , a in φ b n , representing the assignment of some variable y i (that is, an edge in the first half of the graph).

Let us consider a path p from the root the sink of φ b n including E. On this path, the value of z i must be a, by definition of Γ n . Therefore, there can be no path from the root to N on which y i is assigned a different value than a.

More generally, any two paths from the root to N ′ correspond either to identical or to completely disjoint assignments of y 1 , . . . , y i , Each of the possible assignments of variables from Y is thus represented by (at least) one path pointing to a distinct z 1 -node. Since there are 2 n assignments of variables from Y , there are at least 2 n nodes labeled z 1 . Hence φ b n ≥ 2 n : all representations of Γ n as OMVDs on < b are of size in n.

All in all, for any total strict variable order <, there exists a family Γ n of Boolean functions that have polynomial representations as OMDDs but no polynomial representation in OMVD < : OMVD < ≤ s OMDD.

Proposition A.3. OMVD ≤ s MDD.
Proof. Let n ∈ N * . Let Z n be a set of n variables {z 1 , . . . , z n } of domain {1, . . . , n}. Let Σ n be the Boolean function defined as Σ n ≡ alldiff(z 1 , . . . , z n ), or equivalently:

Σ n ≡ n i=1 i-1 j=1 [z i = z j ].
There exists an MDD of size polynomial in n representing Σ n . Indeed, each constraint [z i = z j ] can be represented as an MDD of n 2 edges (n edges for z i , and for each one, a z j -node with n -1 outgoing edges). Chaining these small MDDs (replacing the sink of each one by the root of the next one), we obtain an MDD of size polynomial in n. Now, let φ be an OMVD representing of Σ n ; we consider, without loss of generality, that its variable order < verifies z 1 < • • • < z n . We prove that φ is exponential in n.

Let i ∈ {1, . . . , n -1}; consider two distinct subsets S S ′ of {1, . . . , n} such that |S| = |S ′ | = i. Let a ∈ {1, . . . , n} such that a ∈ S and a / ∈ S ′ . Let z S and z S ′ be two {z 1 , . . . , z i }-assignments that cover all values in S and S ′ , respectively. We consider two paths p S and p S ′ from the root to the sink of φ, compatible with z S and z S ′ , respectively. Suppose they go through a same z i+1 -node N ; p S assigns a to some variable before encountering N , and p S ′ assigns a to some variable after having encountered N . Then, the path obtained by joining the first part of p S (from the root to N ) and the second part of p S ′ (from N to the sink) is a consistent path assigning a to two different variables. Since such a path violates the "alldifferent" constraint, it is impossible, so p S and p S ′ must go through two different z i+1 -nodes.

Hence, there are at least one z i+1 -node for each S ⊆ {1, . . . , n} of cardinal i; since there are n i such subsets, there are at least n i z i+1 -nodes. The number of nodes in φ is thus greater than

n-1 i=1 n i = 2 n -2.
All in all, family Σ n has polynomial representations as MDDs, but only exponential representations as OMVDs, which proves OMVD ≤ s MDD.

Proposition A.4. OMDD ≤ s OMVD < .

Proof. Proposition 3.4 states that OMVD B < ≤ s DNF. If OMDD ≤ s OMVD < , it would hold that OMDD ≤ s DNF. Since the edges in OMDDs representing propositional formulae are only labeled with 0 or 1, this would imply that OMDD B ≤ s DNF. But thanks to Proposition 3.3, it would mean that OBDD ≤ s DNF-yet it is false. [START_REF] Darwiche | A knowledge compilation map[END_REF] Proof of Theorem 4.1. All positive results come directly from simple language inclusions (if L ⊇ L ′ , then surely L ≤ s L ′ ).

All negative results stem from Propositions A.2, A.3 and A.4, and from the fact that if L 1 ≤ s L 2 , then every L such that L 1 ≤ s L verifies L ≤ s L 2 , and every L such that L ≤ s L 2 verifies L 1 ≤ s L, or we could derive L 1 ≤ s L 2 by transitivity.

A.3. First proofs of transformations (Theorem 4.5)

In this section, we prove the satisfaction of several transformations on some languages; these results are used in subsequent proofs.

Lemma A.5. Algorithm 1 runs in time polynomial in the size of its input MVD. When given an MVD ordered with respect to its input order <, the output MVD is also ordered with respect to <.

Proof. Let us consider an MVD φ, a set X = {x 1 , . . . , x k } of variables in Scope(φ), a sequence A = A 1 , . . . , A k of sets of values such that ∀i ∈ {1, . . . , k}, A i ⊆ Dom(x i ), and a strict total order < on Scope(φ). Let d = max 1≤i≤k |A i |.

Complexity. The number of iterations of the loop starting on line 5 is bounded by the number of edges in φ, and thus by φ . Reduction (line 9) is polynomial (Prop. 2.9). On line 10, it is well known that indexing nodes in a DAG in ascending order can be done in time polynomial. Note that r is simply the number of non-sink nodes.

Next, on line 15, it should be noted that the number of incoming edges of a node is always bounded by dr (in the worst case, there is one edge per node and per value); this is independant from the fact that the algorithm adds edges as the loop goes. Moreover, on line 16, the number of children of a node is obviously always bounded by r. All in all, on line 20, we only add at most dr 2 edges to the graph; note that there can be no duplicate edges in a graph (edges having the same source, the same destination, and the same label), so if an edge is already present, it is not "added again". In the loop that starts on line 12, the number of added edges is bounded by dr [START_REF] Amilhastre | Consistency restoration and explanations in dynamic CSPs-Application to configuration[END_REF] .

Finally, the root merging process on line 23 is linear in dr, and the loop starting on line 25 adds at most dr edges to the new root node R.

To conclude, the algorithm runs in time polynomial in φ , d, and r. Since ∀i ∈ {1, . . . , k}, |A i | ≤ |Dom(x i )| ≤ φ , it holds that d ≤ φ , and since there cannot be more non-sink nodes than edges (every non-sink node has at least one outgoing edge), r ≤ φ . Consequently, the algorithm is polynomial in φ .

Ordering. Let us suppose that φ is ordered with respect to <, the order given as input to the algorithm. In the first part (until line 21), edges and nodes are Algorithm 1 Syntactic restriction of an MVD to a "multivalued term".

1: input: an MVD φ 2: input: a set X = {x 1 , . . . , x k } of variables in Scope(φ) 3: input: a sequence A = A 1 , . . . , A k of sets of values, such that ∀i ∈ {1, . . . , k}, A i ⊆ Dom(x i ) 4: input: a strict total order < on Scope(φ) 5: for each edge E = N, N ′ , a in φ such that Var(N ) ∈ X do 6:

let x i := Var(N ) 7: if a / ∈ A i then 8:
remove E from φ 9: reduce φ 10: associate with each node an index i, such that N 0 is the sink, and if there is an edge from N i to N j , then i > j 11: let r be the index of the root 12: for i := 1 to r -1 do if Var(N i ) ∈ X then for each E ∈ In(N i ) do 16: let R be the set of children of the root that are labeled with a variable x minimal for <

for each N ′ ∈ Ch(N i ) do 17: let E ′ := Src(E), N ′ , Lbl(E)

23:

create a new node R that results from the merging of all nodes in R 24:

remove from φ all nodes in R and their incoming and outgoing edges 25:

for each N ′ ∈ Ch(N r ) do 26:
for each a ∈ Dom(x) do 27:

add an outgoing edge R, N ′ , a to R 28:

remove N r and its outgoing edges, and add R as the new root 29: remove from Scope(φ) all variables in X removed from φ, but no nodes are added; the resulting MVD is thus still ordered with respect to <. Now, if the procedure enters the test on line 21, it removes the former root N r and adds a new one R. However, this new root is labeled by the smallest variable x (with respect to <) labeling any child of N r ; and all children of N r labeled with x have been merged into R. Hence, R has no child the label of which is larger or equal to x; and since the remainder of the graph is not modified, the resulting MVD is still ordered with respect to <.

Proposition A.6. MVD and its subclasses satisfy CD.

Proof. We will use Algorithm 1, showing that when the size of each input A i is 1, it computes a conditioning, and moreover maintains the decision property.

Let us consider an MVD φ, a set X = {x 1 , . . . , x k } of variables in Scope(φ), and an X-assignment x. We will show that when given φ, X, the sequence A = { x| xi } 1≤i≤k of the singletons of assigned values in x, and any variable order <, Algorithm 1 outputs an MVD φ ′ such that I(φ

′ ) = I(φ)| x .
Let us denote Z = Scope(φ) \ X = Scope(φ ′ ) (line 29), and let z be any Zassignment. By definition of the conditioning, we must prove that

I(φ ′ )( z) = ⊤ ⇐⇒ I(φ)( x . z) = ⊤.
Sufficient Condition. Suppose I(φ)( x . z) = ⊤; there exists at least one path from the root to the sink of φ that is compatible with x . z. The loop over edges, starting on line 5, only removes X-edges that are not compatible with x, so all compatible paths remain. Let us consider one of these paths p, let us consider two subsequent edges along p, denoted

E 1 = N, N ′ , a 1 and E 2 N ′ , N ′′ , a 2 , such that Var(N ′ ) ∈ X.
In the loop over nodes, N ′ is removed, together with its incoming and outgoing edges-thus E 1 and E 2 are removed. However, a new edge N, N ′′ , a 1 is added; consequently, there still exists at least one path p ′ compatible with x . z.

Finally, if the root of φ is labeled by a variable in X, it is replaced by a new root R. Let N r , N ′ , a be the first edge in p ′ . If Var N ′ is minimal for <, then the new root R is labeled by Var N ′ and all outgoing edges of N ′ are outgoing edges of R: removing the first edge of p ′ , and replacing N ′ by R in the next edge, we get a path from the root to the sink of φ ′ that is compatible with x . z. If Var N ′ is not minimal for <, then the new root R has one outgoing edge leading to N ′ per value in Dom(Var(R)): surely, one is compatible with x. Adding this edge at the beginning of p ′ , we get a path from the root to the sink of φ ′ that is compatible with x . z.

In all cases, there exists in φ ′ a path from the root to the sink that is compatible with x . z; since all X-nodes have been removed, the path is compatible with z.

Hence I(φ ′ )( z) = ⊤.
Necessary Condition. Suppose I(φ ′ )( z) = ⊤; let p be a path from the root to the sink of φ ′ that is compatible with z, and thus with x . z, since φ ′ does not mention any variable from X. Even if the root of φ ′ has been modified (lines 21-28), we know that there was a path compatible with x . z before the modification, since the new root R then was a child of the former root, via an edge compatible with x (all edges incompatible with x have been removed from φ in the loop starting on line 5).

Let E = N, N ′ , a be an edge along p; either E was already in φ, or it has been added on line 20 to bypass an X-node N x (with Var(N x ) = x), in which case it corresponds to two edges in the MVD of the previous loop, N, N x , a and N x , N ′ , a x , with x| x = a x (all edges incompatible with x had been removed). Since it is the case for any E along p, p results from the transformation of at least one path p ′ in φ, that is compatible with x . z. This proves that I(φ)( x . z) = ⊤.

Decision Property. Let us suppose φ is an MDD; we prove that φ ′ also is an MDD. First, remark that removing nodes or edges does not compromise the decision property. Let us study the two moments when the procedure actually adds edges, viz., lines 20 and 25-27. Now, note that the loop over edges (starting from line 5) removes any edge incompatible with x; since φ is an MDD, there can be at most one outgoing edge per node that is compatible with x. Consequently, after this loop, every X-node has at most one outgoing edge-and thus at most one child; and on line 9, reduction removes those that have no child at all. Therefore, on line 20, we simply replace each incoming edge N, N i , a of N i by a single edge N, N ′ , a , with N ′ the unique child of N i . Since no other edge is added at this step, it preserves the decision property.

Finally, in the root replacement step, we know that the former root N r has exactly one child N ′ , and thus the new root R is simply a copy of N ′ . Since N ′ is removed from φ, the procedure does not even enter the loop on line 25. Once again, this step maintains the decision property.

Proposition A.7. OMVD and OMVD < satisfy TR, FO, and SFO.

Proof. We show that Algorithm 1, when given an ordered graph, computes a term restriction. Let us consider an OMVD φ on some variable order <, a set X = {x 1 , . . . , x k } of variables in Scope(φ), and a sequence A = A 1 , . . . , A k of sets of values such that ∀i ∈ {1, . . . , k}, A i ⊆ Dom(x i ). Let φ ′ be the output of Algorithm 1 when given as input φ, X, A, and <. We show that I(φ

′ ) ≡ I(φ)| [x1∈A1]∧•••∧[x k ∈A k ] .
Let us denote Z = Scope(φ) \ X = Scope(φ ′ ) (line 29), and let z be any Zassignment. By definition of restriction and forgetting, we must prove that

I(φ ′ )( z) = ⊤ ⇐⇒ ∃ x ∈ Dom(X), (I(φ) ∧ [x 1 ∈ A 1 ] ∧ • • • ∧ [x k ∈ A k ])( z . x) = ⊤ Sufficient Condition. Suppose that there exists an X-assignment x such that (I(φ) ∧ [x 1 ∈ A 1 ] ∧ • • • ∧ [x k ∈ A k ])( z . x) = ⊤.
Consequently, for any x i ∈ X, it must hold that x| xi ∈ A i ; and there must be at least one path p from the root to the sink of φ that is compatible with x . z. Since the loop over edges, starting on line 5, only removes X-edges that are not compatible with x, p remains.

In a fashion similar to the sufficient condition in the proof of Proposition A.6, we can show that p corresponds to a path from the root to the sink of φ ′ that is compatible with x . z, and since all X-nodes have been removed, compatible with z. Hence I(φ ′ )( z) = ⊤.

Necessary Condition. Suppose I(φ ′ )( z) = ⊤; let p be a path from the root to the sink of φ ′ that is compatible with z. In a fashion similar to the necessary condition in the proof of Proposition A.6, we can show that p to at least one path from the root to the sink of φ that is compatible with z. Let us consider one of these paths, p ′ ; there necessarily exists at least one X-assignment x that is compatible with p ′ , because φ is ordered, and thus, each variable can only be encountered once along p ′ ; each variable can be assigned at most once, there is no contradiction. Moreover, along p ′ , all edges N, N ′ , a such that Var(N ) = x i ∈ X verify a ∈ A i , because edges that do not verify this are removed in the first loop (line 5), and we know that the procedure transforms p ′ into p. Hence, there exists at least one X-assignment x compatible with p ′ and verifying ∀i ∈ {1, . . . , k}

x| xi ∈ A i ; such an assignment is a model of [x 1 ∈ A 1 ]∧• • •∧[x k ∈ A k ],
and p ′ being compatible with both z and x, z . x is a model of I(φ):

(I(φ) ∧ [x 1 ∈ A 1 ] ∧ • • • ∧ [x k ∈ A k ])( z . x) = ⊤.
In conclusion, Algorithm 1 computes a term restriction, and since we know by Lemma A.5 that it runs in polynomial time and maintains the ordering property (but not the decision property), it holds that OMVD and OMVD < satisfy TR, and thus FO (forgetting a variable x amounts to restricting it the term [x ∈ Dom(x)]) and SFO.

Proposition A.8. MDD, OMDD, and OMDD < satisfy ¬C.

Proof. Using the two-leaf form of MDDs (Section 2.3.2), "negating" an MDD is very simple: it is sufficient to swap its two leaves. Since any assignment corresponds to exactly one path from the root to a leaf, an assignment is a model of the original MDD if and only if it is not a model of the resulting MDD. This procedure is done in constant time, and obviously preserves ordering.

Proposition A.9. OMDD < and OMVD < satisfy ∧BC.

Proof. We can use the algorithm in Figure 2, adapted from that on OBDDs. [START_REF] Bryant | Graph-based algorithms for Boolean function manipulation[END_REF] It applies on non-empty OMVDs of a same variable order (if one OMVD is empty, it is trivial to compute the conjunction). A cache is maintained to avoid computing twice the same pair of nodes, thus conjunct step is not called more than φ 1 • φ 2 times. The procedure is polynomial and it maintains determinism when the inputs are deterministic. For each execution of conjunct step, each value of a given variable's domain is explored once, and the size of the domain is lower than either φ 1 or φ 2 (by definition of the size function). The procedure is hence in polynomial time. Proof. Since these languages satisfy CD (Proposition A.6), we can test whether x is a model of φ by conditioning the MVD by x; indeed, we get either the empty MVD (then the assignment is not a model) or the sink-only MVD (then x is a model). Hence all these languages satisfy MC. Algorithm 2 conjunct step(N 1 , N 2 ): returns an OMVD < that is the conjunction of the two OMVDs < of which N 1 and N 2 are roots. Create a node N ′ labeled by x 10:

for each ω ∈ Dom(x), E 1 ∈ Out(N 1 ), E 2 ∈ Out(N 2 ) do 11: if ω = Lbl(E 1 ) = Lbl(E 2 ) then 12:
Let φ ω := conjunct step(Dest(E 1 ), Dest(E 2 )) From CT, we can test in polynomial time whether the number of models is equal to the number of possible assignments of the variables, i.e., whether the OMDD is valid, thus OMDD supports VA.

Proposition A. 18. OMDD and OMDD < satisfy IM.

Proof. Let φ be an MVD; checking whether [ Proof. Let φ and ψ be two MVDs; Checking whether I(φ) entails I(ψ) is equivalent to checking whether I(φ) ∧ ¬ I(ψ) is inconsistent. Since OMDD < satisfies ¬C (Prop. A.8), ∧BC (Prop. A.9), and CO (Prop. A.13), this verification can be done in time polynomial, and OMDD < hence satisfies SE. This implies that it also satisfies EQ, since checking whether I(φ) is equivalent to I(ψ) amounts to checking whether I(φ) entails I(ψ) and I(ψ) entails I(φ).

x 1 ∈ A 1 ] ∧ • • • ∧ [x k ∈ A k ] entails I(φ) is equivalent to checking whether ¬ I(φ) [x 1 ∈ A 1 ] ∧ • • • ∧ [x k ∈ A k ] is inconsistent; now, it is consistent if and only if (¬ I(φ))| [x1∈A1]∧•••∧[x k ∈A k ] consistent.
Proposition A.20. OMDD does not satisfy SE unless P = NP.

Proof. Let φ and ψ be two MVDs; checking whether I(φ) ∧ I(ψ) is consistent is equivalent to checking whether I(φ) does not entail ¬ I(ψ). Since OMDD satisfies ¬C (Prop. A.8), if it also satisfied SE, we would have a polynomial algorithm for checking the consistency of the conjunction of two OMDDs, and in particular, of two OBDDs (possibly on different variable orders), since OMDD B ≡ L OBDD (Prop. 3.3). However, Meinel and Theobald showed in Lemma 8.14 of their book about OBDDs 22 that checking the consistency of the conjunction of two OBDDs is NP-complete. Therefore OMDD cannot satisfy SE unless P = NP.

Proposition A.21. OMDD satisfies EQ. Proof. The procedure described in Algorithm 3 is adapted from the proof of Theorem 8.11 of the OBDD book by Meinel and Theobald. [START_REF] Meinel | Algorithms and Data Structures in VLSI Design: OBDD -Foundations and Applications[END_REF] The procedure is based on the following equation, holding for any variable x ∈ ∪ Scope(Ψ): let ψ be one of the OMDDs such that φ, ψ ∈ L 5:

for each ψ ′ such that φ, ψ ′ ∈ L do 6:

if ψ ′ ≡ ψ then for each a ∈ Dom(x) do 11:

if there exists E ∈ Out(N ) such that Lbl(E) = a then 12:

let φ E be the OMDD rooted at Dest(E) remove the pair φ, ψ from L 17: for each pair φ, ψ ∈ L do return false 20: return true L is initialized with Φ, Ψ , so this is trivially true at the beginning. On line 8, we remove only redundant pairs. On line 16, we have replaced the last pair φ, ψ by a set of pairs according to the decomposition scheme (A.1). Hence, while the procedure runs, we know that I(Φ) ≡ I(Ψ) holds if and only if ∀ φ, ψ ∈ L, I(φ) ≡ I(ψ), q.e.d. (A.2).

We use this equivalence to show that the algorithm is sound and complete. On line 6, we encounter two inconsistent pairs: it is impossible that φ be equivalent to both ψ and ψ ′ . Thus there exists a pair in L such that I(φ) ≡ I(ψ), and hence I(Φ) ≡ I(Ψ). We can return false. At the end of the algorithm, we have tested the equivalence of all pairs in L (lines 17-19), we can thus return true.

Let us now show that the algorithm is polynomial. Each node of Φ is treated once. For a given node N , we add exactly For each node, we make at most d • |Nodes Φ| equivalence tests at line 6; equivalence tests being on OMDDs of the same variable order, they can be done in time polynomial (Prop. A. 19). The traversal of the graph (lines 2-16) is thus polynomial.

Once we have traversed the entire Φ, we know by construction that the only pairs φ, ψ left in L are such that φ is either the sink-only or the empty OMDD, so φ is an OMDD of the same variable order as Ψ: all the equivalence tests of line 18 Proof. The negation of a CNF is a DNF, which is linearly translatable into an OMVD of any order (Proposition 3.4). Thus, if OMVD < or OMVD satisfied ¬C, we would have a polynomial algorithm translating any CNF into an equivalent OMVD (take the negation of the CNF, translate the resulting DNF into an OMVD, and take the negation of the result). As OMVD < and OMVD satisfy CO (Prop. A.13), we would have a polynomial algorithm for deciding whether a CNF is consistent, which is impossible unless P = NP.

Proposition A.23. MVD and MDD satisfy ∧C and ∧BC.

Proof. To make the conjunction of k MVDs φ 1 , . . . , φ k , replace the sink of φ i by the root of φ i+1 , for all i in {1, . . . , k -1}. Then the obtained MVD, rooted at the root of φ 1 and using the sink of φ k , represents k i=1 φ i . This procedure is linear in k, so MVD satisfies ∧C, and thus ∧BC.

Applying the previous procedure on MDDs, the result also is an MDD, since no edge is modified or added: it maintains the decision property. Hence MDD also satisfies ∧C and ∧BC.

Proposition A.24. OMVD and OMDD do not satisfy ∧BC or ∧C unless P = NP.

Proof. Thanks to Proposition 3.3, any OBDD can be turned into an equivalent OMVD in linear time. If OMVD (resp. OMDD) satisfied ∧BC, we would have a polynomial algorithm deciding whether the conjunction of two OBDDs (the variable order being possibly different in each OBDD) is consistent, since OMVD (resp. OMDD) supports CO (Prop. A.13); yet, this problem is NP-complete, as shown by Meinel and Theobald in Lemma 8.14 of their book about OBDDs. [START_REF] Meinel | Algorithms and Data Structures in VLSI Design: OBDD -Foundations and Applications[END_REF] Therefore OMVD (resp. OMDD) does not support ∧BC, and thus ∧C, unless P = NP.

Proposition A.25. OMDD and OMDD < do not satisfy ∧C.

Proof. Lemma A.1 states that any propositional clause can be represented in the form of an OMDD on any order < in linear time; if OMDD (resp. OMDD < ) satisfied ∧C, we could thus translate in polynomial time any propositional CNF into OMDD (resp. OMDD < ). Since the edges in OMDDs representing propositional formulae can only be labeled with 0 or 1, it would mean that OMDD B ≤ P CNF (resp. OMDD B < ≤ P CNF). But thanks to Proposition 3.3, OMDD B ≡ L OBDD (resp. OMDD B < ≡ L OBDD < ); yet we know from the Boolean map 11 that OBDD ≤ s CNF (resp. OBDD < ≤ s CNF). Hence OMDD (resp. OMDD < ) cannot satisfy ∧C.

Proposition A.26. OMVD < does not satisfy ∧C unless P = NP.

Proof. Lemma A.1 states that any propositional clause can be represented in the form of an OMVD on any order < in linear time; if OMVD < satisfied ∧C, we could thus translate any propositional CNF into OMVD < , and it would be possible to check whether it is consistent, as OMVD < satisfies CO (Prop. A. 13). Yet it is impossible, unless P = NP.

Proposition A.27. MVD satisfies ∨C and ∨BC.

Proof. To make the disjunction of k MVDs φ 1 , . . . , φ k , add to the root of φ i an edge per value in the domain of Var(Root(φ), pointing to the root of φ i+1 . Then merge all the sinks into a single one.

Proposition A.28. MDD satisfies ∨C and ∨BC; OMDD and OMDD < do not satisfy ∨C; OMDD does not satisfy ∨BC unless P = NP; and OMDD < satisfies ∨BC.

Proof. Let L be a sublanguage of MVD satisfying ¬C; L verifies ∨C (resp. ∨BC) if and only if it satisfies ∧C (resp. ∧BC). Indeed, to make the disjunction of φ 1 , . . . φ k , it is enough to compute the negation of each disjunct, then build their conjunction, and again compute the negation of the result.

MDD, OMDD, and OMDD < satisfy ¬C (Prop. A.8) so this property applies to them. We get the result since MDD satisfies ∧C and ∧BC (Prop. A.23), OMDD and OMDD < do not satisfy ∧C (Prop. A.25), OMDD does not satisfy ∧BC unless P = NP (Prop. A.24), and OMDD < satisfies ∧BC (Prop. A.9). Proposition A.29. OMVD < satisfies ∨C and ∨BC.

Proof. Implied by the fact that OMVD < satisfies SFO (Prop. A.7): indeed, given k OMVDs φ 1 , . . . , φ k on the same order <, by joining them thanks to a new root node labeled with a new variable and forgetting this variable, we get an OMVD on < that represents k i=1 I(φ i ). The joining algorithm is linear in k, forgetting is polynomial, therefore OMVD < satisfies ∨C and thus ∨BC.

Proposition A.30. MVD and MDD do not satisfy FO or TR unless P = NP.

Proof. Given any MVD φ, φ is consistent if and only if Forget(I(φ), Scope(φ)) ≡ ⊤. The only MVDs that do not mention any variable are the empty and the sinkonly graph, and testing whether an MVD is empty is done is constant time. If MVD (resp. MDD) satisfied FO, we would have a polynomial algorithm for deciding the consistency of any MVD (resp. MDD), yet MVD (resp. MDD) does not satisfy CO unless P = NP (Prop. A.11).

Hence, neither MVD nor MDD satisfies FO unless P = NP, and since TR implies FO (forgetting a variable x amounts to restricting it the term [x ∈ Dom(x)]) we get the result.

Proposition A.31. OMDD and OMDD < do not satisfy SFO, FO, or TR.

Proof. Suppose OMDD satisfied SFO. Then we could obtain in polynomial time an OMDD representing the disjunction of an arbitrary number of OMDDs on the same order <, by joining them thanks to a new root node labeled with a new variable, and forgetting this variable. Since any term can be represented as a polysize OMDD on < (Lemma A.1), we could transform in polynomial time any DNF into an OMDD (possibly on a different order than <). It would hence imply that OMDD B ≤ P DNF, since edges in OMDDs representing propositional formulae can only be labeled with 0 or 1. Since OMDD B ≡ L OBDD (Prop. 3.3), we would have OBDD ≤ P DNF, yet we know from the Boolean map 11 that OBDD ≤ s DNF. Hence, OMDD cannot satisfy SFO.

If OMDD < satisfied SFO, it would also be the case for OMDD, so OMDD < does not satisfy SFO. Finally, since TR implies FO (forgetting a variable x amounts to restricting it the term [x ∈ Dom(x)]) and thus SFO, we get the result. Proof. This is a consequence of the fact that OMDD < (resp. OMDD) supports ¬C and does not support SFO (Prop. A.31). Indeed, for any interpretation function I and any set of variables X ⊆ Scope(I), Forget(I, X) = ¬ Ensure(¬ I, X). If OMDD < (resp. OMDD) satisfied SEN, we would have a polynomial algorithm for performing a forgetting of some variable x in φ: compute a negation of φ, ensure x in this negation, and return a negation of the result. Hence OMDD < (resp. OMDD) does not satisfy SEN, and thus EN. Proposition A.35. OMVD and OMVD < do not satisfy SEN unless P = NP.

Proof. We prove that if OMVD or OMVD < satisfied SEN, we could translate any CNF into one of these languages in polynomial time, and thus check its consistency, which is impossible unless P = NP.

Let φ be a propositional CNF, and let < be a total strict order on Scope(φ). All clauses in φ can be transformed in polynomial time into OMVDs ordered with respect to < (Lemma A.1). If OMVD satisfied SEN, we could obtain in polynomial time an OMVD, possibly on a different order, representing the conjunction of all these OMVDs (that is, the original CNF), by joining them with a new root node labeled with a new variable, and ensuring this variable. Since OMVD satisfies CO (Prop. A.13), we would have a polynomial algorithm for checking the consistency of any CNF, yet this is impossible unless P = We extend the result to OMVD < , since if OMVD < satisfied SEN, then OMVD also would.

A.6. Final proof

Proof of Theorem 4.5. All results from this theorem have been proved in previous propositions. The proposition corresponding to each result is indicated in Table 5.

Proposition 3 . 4 .

 34 It holds that OMVD B < ≤ L DNF and OMVD B < ≥ s DNF. Finally, it holds that OMDD B ⊆ d-DNNF and OMVD B ⊆ DNNF; moreover, d-DNNF < s OMDD B (since OMDD B ≡ L OBDD).

Figure 2 Fig. 2 .

 22 Fig.2. OMVD B and its sublanguages in the DNNF succinctness map. An edge L 1 → L 2 indicates that L 1 is strictly more succinct than L 2 . Dashed edges indicate incomplete results. Relations deducible by transitivity are not represented, which means that two fragments not being ancestors to each other are incomparable with respect to succinctness.

4 .

 4 The Knowledge Compilation Map of MVDs 4.1. Succinctness

Fig. 3 .

 3 Fig.3. The "Alldifferent" coloring problem on a complete graph (3 variables, 3 colors) and an OMDD representing its set of solutions (x 1 < x 2 < x 3 ).

Definition 4 . 2 (

 42 Queries). Let L denote a sublanguage of MVD.

Definition 4 . 3 .

 43 Let I and J be the interpretation functions of some MVDs. • Given a set of variables Y ⊆ Scope(I), the forgetting of Y in I is the function Forget(I, Y ) of scope Z = Scope(I) \ Y , such that Forget(I, Y )( z) = ⊤ if and only if there exists a Y -assignment y verifying I( z . y) = ⊤. • Given a set of variables Y ⊆ Scope(I), the ensuring of Y in I is the function Ensure(I, Y ) of scope Z = Scope(I) \ Y , such that Ensure(I, Y )( z) = ⊤ if and only if for all Y -assignment y, it holds that I( z . y) = ⊤. • The restriction of I to J, denoted I | J , is defined by I | J = Forget(I ∧ J, Scope(J)). • Given an assignment y of some set of variables Y ⊆ Scope(I), the conditioning of I by y is the function I | y of scope Z = Scope(I) \ Y , defined by I | y ( z) = I( y . z). Definition 4.4 (Transformations). Let L denote a sublanguage of MVD.

18 :

 18 let E := E ∪ {E ′ } 19: remove N i , In(N i ), and Out(N i ) from φ 20: add all edges in E to φ 21: if Var(N r ) ∈ X then 22:

A. 4 .

 4 Proofs of queries (Theorem 4.5)Proposition A.10. Every sublanguage of MVD we defined satisfies MC.

1 : 8 :

 18 if the cache contains the key (N 1 , N 2 ) then 2:return the OMVD corresponding to this key in the cache3: if Out(N 1 ) = ∅ (the sink of N 1 is reached) then 4:return a copy of the OMVD rooted atN 2 5: if Out(N 2 ) = ∅ (the sink of N 2 is reached) then 6:return a copy of the OMVD rooted at N 7: if Var(N 1 ) = Var(N 2 ) then Let x := Var(N 1 ) = Var(N 2 ) 9:

13 : 14 : 19 : 20 :

 13141920 Add an edge coming out of N ′ , labeled by ω and pointing to the root of φ ω return the OMVD rooted at N ′ 15:N i = Argmin < (Var(N 1 ), Var(N 2 )), 16: N j = Argmax < (Var(N 1 ), Var(N 2 ))17: Create a node N ′ i labeled by Var(N i ) 18: for each E ∈ Out(N i ) do Let φ E := conjunct step(Dest(E), N j ) Add an edge coming out of N ′ i , labeled by Lbl(E) and pointing to the root of φ E 21: return N ′ Proposition A.11. MVD and MDD do not satisfy any query we defined, besides MC, unless P = NP. Proof. Proposition 3.3 states that BDD ≡ L MDD B , and MDD B ⊆ MDD ⊆ MVD, so MDD and MVD cannot satisfy any query that BDD does not satisfy. We know from the Boolean knowledge compilation map 11 that BDD does not satisfy CO or VA unless P = NP, therefore neither MDD nor MVD satisfies CO or VA unless P = NP. Since the satisfaction of CE, MX, CX, or ME implies the satisfaction of CO, and the satisfaction of IM, EQ, SE, or CT implies the satisfaction of VA, none of these queries can be satisfied by MDD or MVD unless P = NP. A.4.1. Ordered languages Proposition A.12. OMVD and OMVD < do not satisfy VA, IM, EQ, SE, or CT, unless P = NP. Proof. Proposition 3.4 states that OMVD B < ≤ L DNF. If OMVD or OMVD < satisfied VA,

IAlgorithm 3 3 :

 33 (Φ) ≡ I(Ψ) ⇐⇒ ∀a ∈ Dom(x), I(Φ)| x=a ≡ I(Ψ)| x=a . (A.1)Now, the procedure keeps a list L of pairs of subgraphs from Φ and Ψ respectively. We show that this list has the following property:I(Φ) ≡ I(Ψ) ⇐⇒ ∀ φ, ψ ∈ L, I(φ) ≡ I(ψ).(A.2) Given two OMDDs Φ and Ψ, checks whether I(Φ) ≡ I(Ψ) holds.1: let L := { Φ, Ψ } 2:for each node N in Φ, ordered from the root to the sink, except the sink do let φ be the subgraph rooted at N 4:

′ from L 9 :

 9 let x := Var(N ) 10:

18 :

 18 if I(φ) ≡ I(ψ) then 19:

  d N = |Dom(Var(N ))| pairs to L (line 15), d N being bounded by Φ . We also remove one pair (line 16). Hence L contains at most d • |Nodes Φ| pairs, with d = max N d N .

(A. 5 .

 5 there can be at most d • |Nodes Φ| of them) can be done in polynomial time. All in all, OMDD satisfies EQ. Proofs of transformations (Theorem 4.5) Proposition A.22. OMVD < and OMVD do not satisfy ¬C unless P = NP.

  Proposition A.32. MVD and MDD satisfy SFO, SEN. Proof. First, we show that Forget(I, {x}) = x∈Dom({x}) I | x and Ensure(I, {x}) = x∈Dom({x}) I | x . It is straightforward from the definition: let W = X \ {x}. Forget(I, {x}) = I ↓W . Then Forget(I, {x})( w) = ⊤ if and only if there exists x ∈ Dom({x}) such that I( w . x) = ⊤. Hence Forget(I, {x}) = x∈Dom({x}) I | x . Similarly, let W = X \{x}. Ensure(I, {x}) = I ⇓W . Then Ensure(I, {x})( w) = ⊤ if and only if for all x ∈ Dom({x}), it holds that I( w . x) = ⊤. Hence Ensure(I, {x}) = x∈Dom({x}) I | x . Now, let φ be an MVD, and x ∈ Scope(φ). Let d = |Dom(x)|. To obtain an MVD of interpretation Forget(I(φ), {x}) (resp. Ensure(I(φ), {x})), it is sufficient to make d copies of φ, to condition each of them by one of the possible assigment of x to make d -1 disjunctions (resp. conjunctions). Any sublanguage of MVD satisfying CD and ∨C (resp. CD and ∧C) thus satisfies SFO (resp. SEN). Both MVD and MDD satisfy CD (Prop. A.6), ∨C (Prop. A.27, Prop. A.28), and ∧C (Prop. A.23), so they satisfy SFO and SEN. Proposition A.33. MVD, MDD, OMVD, and OMVD < do not satisfy EN unless P = NP.Proof. Given any MVD φ, φ is valid if and only if Ensure(I(φ), Scope(φ)) ≡ ⊤. The only MVDs that do not mention any variable are the empty and the sink-only graphs. If MVD (resp. MDD, OMVD, OMVD < ) satisfed EN, we would have a polynomial algorithm for deciding the validity of any MVD (resp. MDD, OMVD, OMVD on <), yet MVD (resp. MDD, OMVD, OMVD < ) does not support VA unless P = NP (Prop. A.11 and A.12).Proposition A.34. OMDD and OMDD < do not satisfy EN or SEN.

Table 1 .

 1 Results about succinctness.

	L	MVD MDD	OMVD OMDD	OMVD<	OMDD<
	MVD MDD OMVD OMDD OMVD< OMDD<	≤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 ≤s ≤s ≤s

Theorem 4.1. The results in Table

1

hold.

  • L satisfies CO (resp. VA) if and only if there exists a polynomial algorithm that maps every MVD φ in L to 1 if φ has a model (resp. has no countermodel), and to 0 otherwise. • L satisfies MC if and only if there exists a polynomial algorithm that maps every MVD φ in L and any Scope(φ)-assignment x to 1 if x is a model of φ and to 0 otherwise. • L satisfies CE (resp. IM) if and only if there exists a polynomial algorithm that maps any MVD φ in L, any set of variables {x 1 , . . . , x k } ⊆ Scope(φ), and any sequence A 1 , . . . , A k of finite sets of integers such that ∀i ∈ {1, . . . , k}, A

  • L satisfies MX if and only if there exists a polynomial algorithm that maps every MVD φ in L to a model of φ if there exists one, and that stops without returning anything otherwise. • L satisfies CX if and only if there exists a polynomial algorithm that outputs, for any φ in L and any y ∈ Scope(φ), the set of all values taken by y in at least one model of φ. • L satisfies CT if and only if there exists a polynomial algorithm that maps every MVD φ in L to its number of models |Mod(φ)|. • L satisfies ME if and only if there exists a polynomial P (•, •) and an algo-

rithm that enumerates, for every MVD φ in L, its set of models Mod(φ), in time P ( φ , |Mod(φ)|).

  and only if there exists a polynomial algorithm mapping any MVD φ in L, any set of variables {x 1 , . . . , x k } ⊆ Scope(φ) and any sequence A 1 , . . . , A k of finite sets of integers such that ∀i ∈ {1, . . . , k}, A i

  and only if there exists a polynomial algorithm that maps every MVD φ in L and every Y ⊆ Scope(φ) to an MVD φ ′ in L such that I(φ ∧C) if and only if there exists a polynomial algorithm that maps every finite tuple φ 1 , . . . , φ k of MVDs in L to an MVD φ ′ in L such that I(φ ′ ) = satisfies ∨BC (resp. ∧BC) if and only if it satisfies ∨C (resp. ∧C) when limited to a pair of MVDs (i.e., k = 2). • L satisfies ¬C if and only if there exists a polynomial algorithm that maps every

	k i=1 I(φ i ) (resp. I(φ ′ ) =	k i=1 I(φ i )).
	• L

′ ) = Forget(I(φ), Y ) (resp. I(φ ′ ) = Ensure(I(φ), Y )).

• L satisfies SFO (resp. SEN) if and only if it satisfies FO (resp. EN) when limited to a single variable (i.e., |Y | = 1).

• L satisfies ∨C (resp.

Table 2 .

 2 Results about queries.

Table 4 .

 4 Results for randomly generated binary CSPs (15 variables, domain size equal to 6).

	%T	%C	#SOL	#N OMVD	#N OMDD
		10	290888073	80	81
		20	136056826	1338	1558
	70	30	5006576	5662	8132
		40	95131	3315	5005
		50	2367	737	897
		20	1581648506	2572	2932
		30	189551100	12223	16370
	80	40	11557737	20501	35486
		50	1035884	13815	25240
		60	70185	5776	9253
		70	4662	1719	2246
		80	229	54	401
	Note: %T denotes the percentage of tuples satisfying each
	constraint; %C the density of the constraint graph; #SOL

the number of solutions of the CSP; #N the number of nodes in the compiled form.

  All in all, we can translate any DNF into OMVD B < in linear time, hence OMVD B < ≤ L DNF. We now show that OMVD B < ≥ s DNF. It is clear that OMDD B < ≥ s OMVD B < , since any OMDD is an OMVD. If OMVD B < ≥ s DNF held, we could infer that OMDD B < ≥ s DNF, and since OMDD B < ≡ L OBDD (Prop. 3.3), that OBDD ≥ s DNF. However, this is false, 11 hence OMVD B < ≥ s DNF holds.

A.2. Succinctness proofs (Theorem 4.1)

Proposition A.2. OMVD < ≤ s OMDD.

  Since OMDD satisfies ¬C (Prop. A.8), TR (Prop. A.31), and CO (Prop. A.13), this verification can be done in time polynomial, and OMDD hence satisfies IM. By inclusion, OMDD < also satisfies IM. Proposition A.19. OMDD < satisfies SE and EQ.

Table 5 .

 5 Results about queries and transformations.

		MVD	MDD	OMVD	OMDD	OMVD<	OMDD<
	CO VA MC CE IM EQ SE CX MX CT ME CD TR FO SFO EN SEN ∨C ∨BC ∧C ∧BC ¬C	• A.11 • A.11 √ A.10 • A.11 • A.11 • A.11 • A.11 • A.11 • A.11 • A.11 • A.11 √ A.6 • A.30 • A.30 √ A.32 • A.33 √ A.32 √ A.27 √ A.27 √ A.23 √ A.23 ?	• A.11 • A.11 √ A.10 • A.11 • A.11 • A.11 • A.11 • A.11 • A.11 • A.11 • A.11 √ A.6 • A.30 • A.30 √ A.32 • A.33 √ A.32 √ A.28 √ A.28 √ A.23 √ A.23 √ A.8	√ A.13 • A.12 √ A.10 √ A.14 • A.12 • A.12 • A.12 √ A.15 √ A.13 • A.12 √ A.16 √ A.6 √ A.7 √ A.7 √ A.7 • A.33 • A.35 ? ? • A.24 • A.24 • A.22	√ A.13 √ A.17 √ A.10 √ A.14 √ A.18 √ A.21 • A.20 √ A.15 √ A.13 √ A.17 √ A.16 √ A.6 • A.31 • A.31 • A.31 • A.34 • A.34 • A.28 • A.28 • A.25 • A.24 √ A.8	√ A.13 • A.12 √ A.10 √ A.14 • A.12 • A.12 • A.12 √ A.15 √ A.13 • A.12 √ A.16 √ A.6 √ A.7 √ A.7 √ A.7 • A.33 • A.35 √ A.29 √ A.29 • A.26 √ A.9 • A.22	√ A.13 √ A.17 √ A.10 √ A.14 √ A.18 √ A.19 √ A.19 √ A.15 √ A.13 √ A.17 √ A.16 √ A.6 • A.31 • A.31 • A.31 • A.34 • A.34 • A.28 √ A.28 • A.25 √ A.9 √ A.8

Note:

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

Acknowledgements

This work is partially supported by the project BR4CP ANR-11-BS02-008 of the French National Agency for Research.

it would be the case for OMVD B < by inclusion: we could check in time polynomial the validity of any DNF, yet it is impossible unless P = NP.

Since the satisfaction of IM, EQ, SE, or CT implies the satisfaction of VA, OMVD and OMVD < cannot satisfy any of them unless P = NP.

Proposition A. 13. OMVD and its sublanguages satisfy MX and CO.

Proof. In an OMVD, every path from the root to the sink corresponds to at least one model. Indeed, the ordering property imposes that no variable can be encountered twice on a given path. Let φ be an OMVD, and p be a path from the root to the sink of φ. Denoting N 1 , N 2 , a 1 , N 2 , N 3 , a 2 , . . . , N k , N k+1 , a k the edges along this path, any Scope(φ)-assignment x in which Var(N i ) is assigned to a i (for

Consequently, extracting a model of an OMVD boils down to choosing a path, retrieving the associated assignment, and complete it by assigning random values to variables in Scope(φ) that are not mentioned along the chosen path. The only case when it does not work is when there is no path to choose, i.e., when the graph is empty; in this case the OMVD is inconsistent, and there is no model to find. Hence, OMVD MX, and thus CO. Any MVD in a sublanguage of OMVD is obviously an OMVD, so the procedure also works for OMVD < , OMDD, and OMDD < .

Proposition A.14. OMVD and its sublanguages satisfy CE.

Proof. Checking whether I(φ) entails [x

; and using the definition of restriction, we get that

is inconsistent. Since OMVD satisfies TR (Prop. A.7) and CO (Prop. A.13), it satisfies CE. By inclusion, OMVD < , OMDD, and OMDD < also satisfy CE.

Proposition A.15. OMVD and its sublanguages satisfy CX.

Proof. Let φ be an OMVD and X be a set of variables in Scope(φ). The context of a variable x is the set of values that are part of at least one model of I(φ). To check whether a value a is in the context of x in φ, it is thus sufficient to assign x to a, which amounts to a conditioning, and to check whether the result is consistent. Since OMVD satisfies CD (Prop. A.6) and CO (Prop. A.13), this process is polynomial. Applying it for every value in Dom(x), we obtain the context of x; since |Dom(x)| ≤ φ , the process is also polynomial. Last, |X| ≤ |Scope(φ)| ≤ φ , so retrieving the context of all variables in X is polynomial. Hence OMVD satisfies CX, and by inclusion, OMVD < , OMDD, and OMDD < also satisfy CX.

Proposition A. 16. OMVD and its sublanguages satisfy ME.

Proof. This holds because OMVD satisfies CD (Prop. A.6) and CO (Prop. A.13). Enumerating models can be done by exploring the entire assignment tree, as done in the Boolean case [START_REF] Darwiche | A knowledge compilation map[END_REF] (checking consistency after each branching avoids having to backtrack, so the size of the search tree is polynomial in the size of the output).

A.4.2. Decision diagrams

Proposition A.17. OMDD and OMDD < satisfy CT and VA.

Proof. Let φ be an OMDD, and p a path from the root to the sink of φ. Denoting N 1 , N 2 , a 1 , N 2 , N 3 , a 2 , . . . , k , N k+1 , a k the edges along p, any Scope(φ)assignment x in which Var(N i ) is assigned to a i (for 1 ≤ i ≤ k) is compatible with p, by construction, and is thus a model of φ. However, it cannot be compatible with any other path in φ: if it were the case, φ would be non-deterministic.

All in all, each path in φ can be associated with the set of models of φ that are compatible with it, and these models are not compatible with any other path: models are partitioned among all paths. Counting the models of φ thus amounts to counting the models associated with each path.

The number of models associated with a given path p depends on the variables it mentions: if it mentions all variables in Scope(φ), then it is compatible with exactly one model; if it mentions all variables but one, denoted x, then it is associated with |Dom(x)| models; etc.

Given a node N in an OMDD φ on <, let us denote Scope(N ) the set of all variables greater or equal to Var(N ) with respect to <. To count the number of models of we will associate with each node N , the number n N of Scope(N )-assignments that are compatible with any path from N to the sink. We start by noticing that n Sink(φ) = 1: indeed, Scope(Sink(φ)) = ∅, and the unique ∅-assignment is compatible with all paths from the sink to itself (there is none). Then, the outgoing edges of an internal node N cannot be compatible with a same Scope(N )-assignment, (recall that models are partitioned among paths, since φ satisfies the decision property). Hence

with n E the number of Scope(N )-assignments compatible with E. Denoting D = Dest(E), this number is simply n D , multiplied by Var(N )<x<Var(D) |Dom(x)|, to take into account all variables not mentioned in this subgraph.

The number n Root(φ) is then the number of Scope(Root(φ))-assignments that are compatible with some path from the root to the sink of φ; to obtain the number of models of φ, we once again have to multiply it, this time by