On Valued Negation Normal Form Formulas

1 Introduction

For the past few years, several frameworks specializing the standard propositional one have been developed. Such frameworks are centered on fragments which are proper subsets of a full propositional language. Among them is the influential DNNF fragment [Darwiche, 2001], and its subsets d-DNNF, FBDD and OBDD, which have been successfully applied to a number of AI tasks, including diagnosis, reasoning under uncertainty, and planning. The success of such languages comes from the fact that they support a number of queries and transformations in polynomial time and are quite spatially succinct. The sources of their efficiency have been identified as formal properties on the corresponding structures, e.g. decomposability for DNNF, while d-DNNF asks also for determinism [Darwiche and Marquis, 2002].

On the other hand, in the recent years, many algebraic frameworks generalizing the standard CSP one have been pointed out; among them are VCSP [Schiex et al., 1995], valuation algebra [Shenoy and Shafer, 1988; Kohlas and Shenoy,

∗The authors would like to thank Sylvie Coste-Marquis for her help. The second author has been partly supported by the R´egion Nord/Pas-de-Calais, the IRCICA Consortium and by the European Community FEDER Program.

Pierre Marquis

CRIL-CNRS, Universit´e d'Artois, Lens email: marquis@cril.univ-artois.fr

2000] and semiring CSP [Bistarelli et al., 1995]; PFU [Pralet et al., 2006]. In such frameworks, satisfaction is a more gradual notion than in the standard CSP one; valuations range over some ordered scale (which can e.g. be interpreted as a utility/uncertainty scale) and can be aggregated using some operators. These frameworks consider a number of queries which extend the ones considered in the standard framework (mainly, the consistency query); especially, optimization is an important query in such settings.

At the intersection of those two research lines are a few approaches, where DAGs are used to represent functions ranging over an ordered scale. Let us mention SLDD [Wilson, 2005], AADD [Sanner and McAllester, 2005], ADD [Bahar et al., 1993], and arithmetic circuits [Darwiche, 2002].

This work can be viewed as a further, yet more systematic attempt to bridge the gap between both research streams. We present a general framework, called VNNF (for "Valued NNFs"), suited for the representation of a much more general class of functions than just Boolean ones. This framework supports a larger family of queries and transformations than in the NNF case, including variable elimination, suited to optimization issues and encompasses a number of existing representation settings, e.g. NNF, semiring CSP, mixed CSP, SLDD, ADD, and AADD. We show how the properties imposed on NNFs to define "tractable" fragments (decomposability, determinism, decision, read-once) can be extended to give rise to subsets of VNNF, for which a number of queries and transformations can be achieved in polynomial time.

2 The VNNF Framework

The VNNF framework gathers the family of VNNF languages, and the queries and transformations they support. Each VNNF language allows the representation of some functions ranging over an ordered scale; such a language is fully characterized by a representation context 〈E,X, F〉 consisting of a valuation structure E, a set X of variables and a set F of primitive or "local" functions (the word is taken from [Pralet et al., 2006] where local functions represent preferences or plausibility degrees over assignments). Let us first make precise the notion of valuation structure:

Definition 1 (valuation structure) A valuation structure is a triple E = 〈E, ⪰, OP 〉 where:

• (E,⪰) is a set ordered by a relation ⪰ (which is thus

reflexive, antisymmetric and transitive) and such that E has a greatest element ⊤ and a least element ⊥;

• OP is a subset of OPE, the set of all binary operators ⊗ on E such that each ⊗ is associative, commutative, monotonic (∀a, b, c ∈ E, if a ⪰ b then a ⊗ c ⪰ b ⊗ c) and has a neutral element e⊗.

When E is totally ordered by ⪰, elements of OPE are generally called uninorms. When ⊥ (resp. ⊤) is the neutral element of ⊗, ⊗ is usually called a t-conorm (resp. a t-norm) on E. We shall use the same terminology here, neglecting the fact that E is not necessarily totally ordered. For instance, t-conorms on E = [0, 1] include the operations max(a, b), a + b - a.b, min(a + b, 1). T-norms include the operations min(a, b), a.b. Max and ∑ are also t-conorms on E = R+ ∪{+∞}. ∑ is a uninorm on E = R∪{+∞, -∞}.

We assume that OP contains the following operators ∧ and ∨, which can be viewed as generalizations of the well-known Boolean connectives:

When ⪰ is a total order, min and max are alternative generalizations of the Boolean connectives. Interestingly, ∧ and ∨ are admissible in any valuation structure (hence our assumption is harmless), while min and max are admissible in any valuation structure with a totally ordered domain:

Proposition 1 1 Let E be any valuation structure. OPE contains ∧ (resp. ∨) which is a t-norm (resp. a t-conorm) on E. Furthermore, if ⪰ is a total order, OPE contains min (resp. max) which is a t-norm (resp. a t-conorm) on E.

The last two elements of a representation context are much simpler notions:

• X = {x1, . . . , xn} is a finite set of variables ranging on finite domains. dom(x) denotes the domain of variable x ∈ X. When Y ⊆ X, we note dom(Y ) = Πx∈Y dom(x) and call Y -assignments the elements ⃗y ∈ dom(Y ). If Y and Z are disjoint subsets of X, then ⃗y+⃗z is the Y ∪Z-assignment obtained by ordering the values given in the two tuples in an increasing way w.r.t. the indexes of the associated variables.
• F is a set of functions f ranging over E (the "local functions"). When f is a function from Y ⊆ X to E, scope(f) = Y is called the scope of f. Constant functions are identified with elements of E without loss of generality. We assume that F contains all functions f such that card(scope(f)) ≤ 1, i.e. F contains all "literals" (cf. Section 5.3) and constants from E.

Let f ∈ F such that scope(f) = Y . Let Z s.t. Y ⊆ Z ⊆ X and ⃗z be any Z-assignment. We consider that f(⃗z) is equal to f(⃗y) where ⃗y is the Y -assignment which coincides with ⃗z for every variable from Y .

Now, let f, f ′ ∈ F; let ⊗ ∈ OP and x ∈ X; let ⃗z be any Z-assignment s.t. Z ⊆ scope(f). We shall use the following notations:

1 Due to space reasons, proofs are omitted.

• f⃗z denotes the restriction (or conditioning) of f by ⃗z, i.e. the function given by scope(f⃗z) = scope(f) \ Z and for any scope(f⃗z)-assignment ⃗t, f⃗z(⃗t) = f(⃗z +⃗t). Clearly enough, the conditioning of f by ⃗z where Z is any subset of X (and not necessarily of scope(f)) can also be defined, and considered equal to f⃗y where ⃗y is the Z ∩scope(f )-assignment which coincides with ⃗z for every variable from Z ∩ scope(f ).
• f⊗f ′ is the⊗-combination of f and f ′ , i.e. the function given by scope(f ⊗ f ′ ) = scope(f ) ∪ scope(f ′ ) and for any scope(f⊗f ′ )-assignment ⃗t, f⊗f ′ (⃗t) = f (⃗t)⊗f ′ (⃗t).
• f[x,⊗] is the [x,⊗]-projection of f (or ⊗-elimination of variable x), i.e. the function given by scope(f[x,⊗]) = scope(f) \ {x} and for any scope(f[x,⊗])-assignment ⃗t, f[x,⊗](⃗t) = ⊗⃗x∈dom(x) f⃗x(⃗t).

We shall typically consider tractable representation contexts:

Definition 2 (tractable representation context) A representation context 〈E,X, F〉 where E = 〈E,⪰,OP〉 is tractable iff each element of F ∪ OP is in linear time, 2 and this is also the case for the characteristic function of ⪰.

If a function f is in linear time, then every conditioning of f and every ⊗-combination of f with another linear time function are in linear time as well, provided that ⊗ is in linear time. and any ⃗z, f⃗z ∈ F). We are now ready to define in a formal way the family of VNNF languages:

Definition 3 (VNNF) Given a representation context 〈E,X, F〉 where E = 〈E,⪰,OP〉, VNNF is the set of all finite, rooted directed acyclic graphs (DAGs) where each internal node is labeled by the name of an operator of OP and can have many arbitrarily children and where each leaf node is labeled by the name of an element of F and by a Z-assignment where Z ⊆ X.

It is important to observe that such DAGs are not concerned by the representation of local functions (or operators): they are just given by their names, and can be represented as data structures or algorithms, but outside the DAG.

Each leaf node N of a VNNF φ labeled by f and ⃗z actually represents f⃗z: ⃗z grounds some of the variables of scope(f). Let vars(N) = scope(f) \ Z denote the set of free variables of the function associated to N. For any internal node M, let op(M) denote the label of M, and Children(M) the set of its children. The set of free variables occurring in the VNNF φ rooted at node M is thus vars(φ) = vars(M) = ⋃N∈Children(M) vars(N). φ is said to be grounded when vars(φ) = ∅.

Definition 4 (semantics of a VNNF) Let φ be a VNNF w.r.t. 〈E,X, F〉. The semantics val(φ) of φ is the function from scope(val(φ)) = vars(φ) to E recursively defined by:

• If φ is a leaf node labeled by f ∈ F and a Z-assignment ⃗z, then val(φ) = f⃗z;
• Otherwise φ = ⊗(φ1, . . . , φn), and val(φ) = val(φ1)⊗ . . . ⊗ val(φn).

2 A function is said to be polytime (resp. in linear time) when there exists a polynomial (resp. linear) time algorithm computing it.

A VNNF is thus simply the structured representation of a function (val(φ)) that does not necessarily belong to the set of primitives F. Importantly if 〈E,X, F〉 is tractable, then val(φ) is a polytime function.

Obviously, a given function over a valuation structure can be represented by many distinct but equivalent VNNFs. Since VNNFs are defined as DAGs, subformulas that would have several occurrences in tree-like representations do not need to be duplicated. But they can. It is always possible to simplify a VNNF by merging identical subgraphs. This reduction does not change the semantics and can be achieved by an algorithm similar to the one used for OBDDs. However, it does not lead to a canonical form in the general case (i.e., we do not necessarily have val(φ) = val(ψ) only if the reduced form of φ coincides with the reducd form of ψ).

Let us now "quantify" VNNFs. In classical logic, two quantifiers are used: ∃ and ∀. In the VNNF framework, every operator of OP can be used as a quantifier:

Definition 5 (Q-VNNF) A (prenex) quantified VNNF (QVNNF) is a sentence of the form Φ = ⊗1xi1 , . . . ⊗j xij φ where φ is a VNNF, each variable xij belongs to X, 3 and each ⊗i belongs to OP (i ∈ 1 . . . j). ⊗1xi1 , . . . ⊗j xij is called the prefix of Φ and φ its matrix.

The semantics of Φ, denoted val(Φ) is the function from scope(val(Φ)) = vars(φ) \ {xi1 , . . . , xij } to E recursively defined as follows:

• If the prefix of Φ is empty, then val(Φ) = val(φ).
• Otherwise, Φ is of the form ⊗yΨ and val(Φ) = ⊗⃗y∈dom(y) val(Ψ)⃗y.

Clearly enough, quantified VNNFs are convenient for representing at the syntactic level projections of functions. When xi1 , . . . , xij are pairwise distinct, Φ is said to be polite. When vars(φ) ⊆ {xi1 , . . . , xij }, the Q-VNNF Φ is said to be closed. Its semantics is an element of E. Computing it is what is called the evaluation of a (closed) Q-VNNF.

3 Generality of the VNNF Framework

Let us now show how the VNNF framework encompasses various representation settings pointed out so far.

Negation Normal Forms (NNFs) The propositional language NNF (Negation Normal Form formulas) is a wellknown fragment for representing Boolean functions. For recovering it as a VNNF language, it is enough to set E = {0, 1}, ⪰ is such that 1 ⪰ 0, dom(x) = E for each x ∈ X, F is the set of all Boolean functions of arity at most 1 (such functions can be represented by literals and Boolean constants), OP = {min,max} (min nodes correspond to conjunctions of formulas and max nodes to disjunctions). Then val(φ)(⃗x) is simply the truth value taken by the boolean function which is the semantics of φ when applied to ⃗x. Quantified Boolean formulas in negation normal form are also easily recovered as Q-VNNFs: minx (resp. maxx) stands for the universal (resp. existential quantification) on variable x.

3 If Y = {y1, . . . , yk} ⊆ X and ⊗ ∈ OP, then we abbreviate ⊗y1 . . . ⊗ yk by ⊗Y ; this is harmless since each ⊗ ∈ OP is associative and commutative.

CSPs Recovering the standard CSP framework is also easy, considering the same valuation structure as for the NNF framework. No restriction is put on X (it can be any set of discrete variables), but for getting a CSP as a VNNF language we must add some restrictions on VNNF formulas. First of all, the root node has to be a min node. In general CSPs, each child of the root is a local function f : scope(f) → {0, 1}. In table-defined CSPs, each child of the root is a max node, whose children are themselves min nodes connecting functions of the form x == a, that take value 1 if satisfied and value 0 otherwise. Quantified CSPs can also be viewed as specific Q-VNNFs, where min x (resp. max x) stands for the universal (resp. existential quantification) on variable x.

Semiring CSPs and valuation algebras E is equipped with two operators: OP = {∨, ⊗} and ⪰ is defined by a ⪰ b iff a ∨ b = a. It is moreover assumed that 〈E,⪰, ∨,⊗〉 is a commutative semiring and ∨ is idempotent. In a semiring CSP viewed as a VNNF, the root node of the DAG is a ⊗ node and each of its children is a local function. Interestingly, the definition of quantified semiring CSPs follows from our framework. In particular, if ⪰ is complete, then computing the best value of a semiring CSP φ is equivalent to compute maxXφ (note that min can also be added to OP and used as a quantifier). Valuation algebras [Shenoy and Shafer, 1988; Kohlas and Shenoy, 2000] can be more general than VNNF since valuations can bear on subsets of assignment, e.g. for representing commonality functions. When restricted to the distributional case they can be recovered in way similar to the one used for semiring CSPs.

Other frameworks for decision making under uncertainty

The VNNF framework subsumes many of the constraintbased frameworks for decision making under uncertainty, e.g. mixed CSPs (they can be represented by disjunctions of a conjunction of constraints Ci, i ∈ 1 . . . n representing what is satisfying and, with a disjunction of constraints Ki, i ∈ 1 . . .m representing the knowledge about the state variables) and possibilistic mixed CSPs (each such CSP can be represented by a VNNF whose root is labeled by max and has two children: a min-rooted VNNF and a max-rooted one). Stochastic or more generally expected utility CSP networks can be represented as well by products between a VNNF φp representing the probability density over the state variables (e.g. a bayesian net) and a semiring CSP φu over E = [0, 1] synthesizing the utility function. Denoting X the set of decision variables and Y the set of state variables, maximizing expected utility amounts to compute maxX ∑ Y φp . φu. In the qualitative cases (mixed and possibilistic) a standard quantifying sequence is rather maxXminY . PFU generic networks [Pralet et al., 2006]) are not stricto sensu subsumed by the VNNF framework, since they may involve a noncommutative combination of utility degrees and plausibility degrees. Nevertheless, non-commutativity is not a compulsory condition and most of the practical instances of PFU consider a commutative aggregator. Arithmetic circuits, as considered in [Darwiche, 2002], for the factored representation of belief networks can also be recovered as VNNFs.

Finally, we shall see in Section 5.3 that VNNFs also encompass decision diagrams like AADDs (and thus ADDs)

4 Queries and Transformations

The VNNF framework includes a number of algorithms for answering queries about functions represented as VNNFs, and related functions which can be characterized via the application of transformations on functions represented by VNNFs. A fundamental difference between the NNF setting and the VNNF one is that in the VNNF framework, the underlying valuation structure does not necessarily reduce to the Boolean one. Especially, since E may contain more than two elements, the equivalences a ≻ ⊥ iff a = ⊤ and a ≺ ⊤ iff a = ⊥ do not hold anymore. In the NNF framework, the key queries include consistency (CO), validity (VA), and model counting (CT), while the key transformations are conditioning (CD), conjunction (∧C), disjunction (∨C) and forgetting (FO). Let us explain how to state related queries and transformations in the VNNF framework, and point out some additional ones which make sense in this more general setting.

Full consistency/validity If we consider ⊤ as the norm, we get very strong notions of consistency/validity: φ is fully consistent iff there exists ⃗x s.t. val(φ)(⃗x) = ⊤ and φ is fully valid iff for each ⃗x, val(φ)(⃗x) = ⊤.

Partial consistency/validity On the contrary, onemay consider every value of E except ⊥ as the norm, and this leads to the following notions of partial consistency and partial validity: φ is partially consistent iff there exists ⃗x s.t. val(φ)(⃗x) ≻ ⊥ and φ is partially valid iff for each ⃗x, val(φ)(⃗x) ≻ ⊥.

Optimal satisfaction More interesting in practice is the notion of optimal satisfaction, that looks for best assignments; this query is typically useful when VNNFs encode preferences or plausibility degrees and calls for optimization: given a VNNF φ, find ⃗x and a ∈ E such that val(φ)(⃗x) = a and such that there is no ⃗y such that val(φ)(⃗y) ≻ a. We thus search for a non-dominated solution. When ⪰ is a total order, this is equivalent to classical maximization. The associated decision problem (deciding whether a value is optimal) consists in determining whether, given a ∈ E and a VNNF φ, a is the value taken by φ for some non-dominated solution.

Counting extends easily fromNNF toVNNF: Given a ∈ E and a VNNF φ, how many ⃗x are such that val(φ)(⃗x) = a?

Evaluation of a quantified form The extended notion of quantification naturally leads to the problem of evaluating a (closed and polite) Q-VNNF. As a decision problem, this can be written as determining whether val(Φ) ⪰ a. This query is of great importance in many settings: in the NNF one, this query generalizes the famous PSPACE-complete problem called QBF. Quantification also makes sense when E ̸= {0, 1}. When ⪰ is a total order, evaluating a Q-VNNF is a way to achieve optimization (find the best value of φ amounts to evaluating maxXφ). The relationship between optimization and quantified forms is less obvious when partial orders are considered (the identification of an operator encoding non-domination is not an easy problem and may have no solution; for instance, computing a non-dominated value for a semiring CSP represented by a VNNF φ is not equivalent to evaluate the quantified one ∨Xφ).

We have obtained the following complexity results for VNNF assuming that the underlying representation context is tractable (which is a reasonable assumption that we make from now on up to the end of the paper):

Proposition 2

• Partial and full consistency are NP-complete.
• Partial and full validity are coNP-complete.
• Optimization is NP-hard
• Optimal value is DP-complete.
• Counting is #P-hard.
• Evaluation of a closed Q-VNNF is PSPACE-complete.

Observe that, though VNNF is a much more general framework than the NNF one, the generalization does not lead to a complexity shift w.r.t. the basic queries under consideration in [Darwiche and Marquis, 2002]. Note that we could also define notions of full entailment and full equivalence and show the corresponding decision problems coNP-complete.

Let us now focus on transformations. Three transformations are mainly to be considered; conditioning (compute a VNNF representing val(φ)⃗z), ⊗-combination (compute a VNNF representing val(φ1)⊗val(φ2)) and ⊗-variable elimination (compute a VNNF representing val(φ)[y,⊗] = val(⊗yφ), or more generally val(⊗Y φ)).

The case of ⊗-combination is obvious since φ1 ⊗ φ2 is a VNNF and represents val(φ1) ⊗ val(φ2). If the representation context is tractable, then each ⊗-combination is in linear time. If φ is a VNNF, then a VNNF representing val(φ)⃗z can also be obtained in linear time in the size of φ. It is enough to revise the assignment associated to φ:

Definition 6 (conditioning a VNNF) Given a VNNF φ, we denote φ⃗z the VNNF obtained by replacing in the label of each leaf, the Y -assignment ⃗y by ⃗y ◦⃗z, the Y ∪Z-assignment which coincides with ⃗y on each variable from Y and with ⃗z on each variable from Z \ Y .

It can be easily checked that φ⃗z represents the restriction of val(φ) by ⃗z, i.e. that val(φ⃗z) = val(φ)⃗z. That is why we call φ⃗z the conditioning of φ by ⃗z.

⊗-variable elimination generalizes the transformation known as forgetting in the NNF case. In contrast to the previous transformations, it can be very expensive: at each elimination step, the size of the current VNNF φ may increase in a non-constant way (the size of ⊗⃗x∈dom(x) φ⃗x can be |dom(x)| larger than the size of φ). Thus, applying the definition directly would lead to an exponentially larger VNNF, unless a bounded number of variables has to be eliminated.

5 Determinism, Decomposability, Decision and Read-Once

The previous sections have shown the VNNF framework quite general. However, every query under consideration, if it is no more difficult than in the Boolean case, is intractable under the standard assumptions of complexity theory. An important issue is thus to define restrictions on the VNNF languages allowing efficient queries and transformations.

In the NNF framework, a few properties, namely decomposability, determinism, decision and read-once are sufficient to achieve many of them in polynomial time. We shall see that a third one is valuable in the VNNF framework, namely distributivity. The key point is that it enables efficient ⊗-variable elimination, which is an important transformation for several issues, including the optimization one.

5.1 Distributivity and decomposability

The space explosion inherent to a direct application of ⊗- variable elimination in the general case does not necessarily occur; especially, it can be limited when some of the children of φ do not depend on the variable x to be eliminated. Thus, in the DNNF case, at most one child of each ∧ node may depend on the variable to be forgotten. Actually, in addition to independence, a further property is implicitly used in the NNF framework for ensuring polytime forgetting, and it has to be made explicit in order to be extended to VNNF: the distributivity of ∧ over ∨. The impact of distributivity on variable elimination in valuation algebras is known for a while (see e.g. [Shenoy and Shafer, 1988]) and requiring it is not so demanding in many representation contexts.

Definition 7 (⊗-distributivity) A VNNF φ ensures ⊗- distributivity iff for any ⊙ labelling an internal node in φ, ⊙ distributes over ⊗: ∀a, b, c ∈ E : a ⊙ (b ⊗ c) = (a ⊙ b) ⊗ (a ⊙ c).

Proposition 3

• Any VNNF w.r.t. any representation context ensures ⊗- distributivity for ⊗ = ∨ and for ⊗ = ∧.
• Any VNNF w.r.t. any representation context where ⪰ is a total order ensures ⊗-distributivity for ⊗ = max and for ⊗ = min.

We are now ready to define the fragment of ⊗- decomposable VNNFs:

Definition 8 (⊗-decomposability) Let φ be a VNNF:

• A node N of φ is simply decomposable iff for each Ni,Nj ∈ Children(N), vars(Ni) ∩ vars(Nj) = ∅ when i ̸= j.
• A node N of φ is ⊗-decomposable iff it is simply decomposable and op(N) is distributive over ⊗.
• φ is ⊗-decomposable iff each of its (internal) nodes N is ⊗-decomposable when op(N) ̸= ⊗. ⊗-DVNNF is the class of all the ⊗-decomposable VNNFs.

As to ⊗-decomposability, the main result is:

Proposition 4 ⊗-DVNNF is linearly closed for ⊗-variable elimination, i.e., there exists a linear time algorithm for computing a ⊗-DVNNF equivalent to ⊗Y φ when φ ∈ ⊗-DVNNF and Y ⊆X.

This generalizes the result of tractability of DNNF for the forgetting operation. It moreover implies that the optimization of any VNNF the nodes of which are either max nodes or decomposable nodes is tractable.

Proposition 5 The restrictions of full consistency, partial consistency and optimisation on max-DVNNF are in P.

5.2 Determinism

A second important property in the NNF framework is determinism. More than a property of logical exclusion, it is linked to the existence of a neutral element for ⊗:

Definition 9 (determinism) An internal node N in a VNNF φ is deterministic iff for each ⃗y ∈ dom(vars(N)), there is at most one M ∈ Children(N) such that val(ψ)(⃗y) ̸= eop(N), where ψ is the VNNF rooted at M.

Definition 10 (d-DVNNF) d-DVNNF is the class of all VNNFs in which each internal node is either simply decomposable or deterministic.

As to d-DVNNF, the main result is:

Proposition 6 The restrictions of full validity and partial validity on d-DVNNF are in P. If φ is a d-DVNNF, then counting can be achieved in time O(|E| + |φ|).

5.3 Decision diagrams

Let us now focus on other properties that prove useful for defining another interesting fragment of VNNF: the set of all decision diagrams. We first need a number of definitions:

Definition 11 (literals) A literal on x ∈ X is a function f whose scope is {x}. LX is the set of all the literals that can be built on variables from X.

By extension, we shall also call literals the leaves labeled by literals.

Definition 12 (assignment nodes) An assignment node N on x ∈ X in a VNNF φ is a node of the form l ⊗α, where l is a literal on x and ⊗ is a t-norm on E.

Two assignment nodes N1 and N2 on x ∈ X are exclusive iff their respective literals f1 and f2 are exclusive, i.e., ∀⃗x ∈ dom(x), either f1(⃗x) = ⊥ or f2(⃗x) = ⊥.

In any assignment node N of the form l ⊗ α where l is a literal on x one may assume without loss of generality that α is not a literal (a literal f can always be replaced by the assignment node f ∧⊤). Then dvar(N) can denote the variable x and tail(N) the formula α in a non-ambiguous way.

Definition 13 (decision nodes) A decision node N on x in a VNNF φ is a node of the form N1 ⊙ . . . ⊙Nm where all the Ni are assignment nodes on the same variable x and ⊙ is a t-conorm on E. N is exclusive iff its assignment nodes are pairwise exclusive.

Definition 14 (linear node) A node N is linear iff at most one of its children is not grounded.

Note that leaves are linear nodes. We are now ready to define the language of decision diagrams:

Definition 15 (decision diagrams) A decision diagram is a VNNF in which each internal node is either an exclusive decision node or a linear node.

Two particular subclasses of decision diagrams are worthwhile noticing, the read-once ones and the ordered ones:

Definition 16 (read-once and ordered decision diagrams)

• A decision diagram φ is read-once iff for any assignment node N in φ, dvar(N) does not occur in tail(N).

• A decision diagram φ is ordered w.r.t. a strict order < on X iff for every pair of decision nodes M and N in φ, if M is an ancestor of N in φ, then dvar(M) < dvar(N).

The second property obviously implies the first one. Interestingly, AADDs and SLDDs are specific decision diagrams:

AADD For recovering algebraic decision diagrams, let us set E = R ∪ {-∞, -∞}, ⪰=≥, OP = {min, max, +, .}, ∀x ∈ X, dom(x) = {0, 1}, F = LX. The decision nodes of such decision diagrams are of the form Nx = max(min(fh, ch + bh.Nh), min(fl, cl + bl.Nl)), where:

• fh (resp. fl) is the literal on x that valuates to -∞ for x = 0 (resp. x = 1) and to +∞ for x = 1 (resp. x = 0);
• ch, bh, cl, bl are constants of E;
• Nh and Nl are either decision nodes or constant nodes.

The root of an AADD is a linear formula c+b.Nk. The reader can check that min(fh, ch + bh.Nh) and min(fl, cl + bl.Nl) are exclusive assignment nodes whose tails are linear ones.

SLDD A SLDD is an ordered decision diagram built on some set E ordered by some ⪰ and equipped with two operators ⊕ and ⊗, where ⊗ is a t-norm and ⊕ is a t-conorm. It is moreover required that ⊗ distributes over ⊕: 〈E, ⊥, ⊤, ⊕, ⊗〉 is a commutative semiring. For recovering SLDD, it is sufficient to set F to the subset of literals of LX ranging over {⊥, ⊤}.

and to consider ordered decision diagrams whose decision nodes are of the form N = ∨(∧(l1, c1 ⊗N1), . . . , ∧(lk, ck ⊗ Nk)), where the ci are constants of E.

SLDDs and AADDs are obviously read-once. This is important enough, since one can prove that the read-once property on decision diagrams ensure that they are not only decomposable but also deterministic:

Proposition 7 Read-once decision diagrams are d-DVNNFs. As a consequence of Propositions 5, 6 and 7, we get:

Proposition 8 The restrictions of full and partial consistency, optimization, full and partial validity on read-once (and thus on ordered) decision diagrams are in P. Counting can be achieved in time O(|E| + |φ|).

Now, it can be shown that the ⊗-elimination of a variable x can be performed in an efficient way on a decision diagram φ for which distributivity w.r.t. ⊗ is ensured, provided that x is final in φ (i.e., for any assignment node N on x in φ, tail(N) is grounded).

Definition 17 (distributive Q-VNNF) A Q-VNNF is said to be distributive iff each operator of its matrix distributes over each operator of its prefix.

For instance, when E is totally ordered, any quantified decision diagram (e.g. a quantified AADD or a quantified ADD) is distributive for a prefix composed of existential (max) and universal (min) quantifiers.

Proposition 9 Let < be the total ordering on X defined by the prefix of a (closed and polite) Q-VNNF Φ, i.e. xi1 < . . . < xij iff Φ = ⊗1xi1 , . . . ,⊗jxij φ. The evaluation problem for a distributive, closed and polite Q-VNNF the matrix of which is a decision diagram ordered by < is in P.

6 Conclusion

In this paper, we have presented a new framework, VNNF, which encompasses many representation settings pointed out so far. We have shown how some properties imposed on NNFs to define more "tractable" fragments (namely, decomposability, determinism, decision, read-once) can be extended to VNNFs.

This work calls for a number of perspectives. The more immediate ones are of algorithmic nature: we need algorithms for compiling VNNFs into ⊗-DVNNFs, d-DVNNFs, or (ordered) decision diagrams. From a more theoretical (but not less important) point of view, a number of issues need to be addressed as well, including the succinctness one (how do the VNNF fragments w.r.t. a given representation context relate w.r.t. spatial efficiency?) and the canonicity one (under which requirements can we guarantee that two VNNFs represent the same function iff they are identical?).