New Canonical Representations by Augmenting OBDDs with Conjunctive Decomposition (Extended Abstract)

1 Introduction

Canonicity, an important property of knowledge compilation (KC) languages, provides equivalence tests with constant time complexity and plays a critical role in the performance of compiling methods [Darwiche, 2011; Van den Broeck and Darwiche, 2015]. The reduced ordered binary decision diagram (ROBDD) [Bryant, 1986] is one of the most influential canonical languages in the KC literature.

Despite its current success, ROBDD has a well-known weakness in succinctness, which reflects the explosion in size for many types of knowledge bases in practice. Deterministic, decomposable negation normal form (d-DNNF) [Darwiche, 2001] is a strict non-canonical superset of ROBDD, and most efficient compilers (e.g., OBDD compilers) can be seen as special d-DNNF compilers [Huang and Darwiche,

∗This paper is an extended abstract of an article in the Journal of Artificial Intelligence Research [Lai et al., 2017], and was supported by the National Natural Science Foundation of China under grants 61402195 and 61370156, the China Postdoctoral Science Foundation under grant 2014M561292, and Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education.

Minghao Yin

Department of Computer Science Northeast Normal University, China ymh@nenu.edu.cn

2007]. A recent trend in the KC field is to identify new canonical representations in d-DNNF to mitigate the size explosion problem of ROBDD without sacrificing its main advantages. Researchers has proposed many canonical languages, including AND/OR BDD (AOBDD) [Mateescu et al., 2008], compressed and trimmed SDD over a fixed vtree V (CSDDV ) [Darwiche, 2011], ROBDD with as many implied literals as possible (ROBDD-L∞) [Lai et al., 2013]. However, the corresponding compilers cannot yet compile many problems that the state-of-the-art d-DNNF compiler DSHARP can compile [Muise et al., 2012]. Furthermore, the relationships between these canonical representations, which are indispensable for choosing appropriate representations in practical applications, are not well studied.

Decomposability is an important factor behind the strong succinctness and tractability of d-DNNF. The ideas of ROBDD-L∞ and AOBDD are to use two special types of conjunctive decomposability to relax the linear variable ordering of ROBDD. We generalize these two types of ∧-decompositions to propose bounded ∧-decomposition parameterized by integer i (∧i-decomposition), and ∧idecomposition respecting tree T (∧T ,i-decomposition). Then we identify a family of canonical languages in dDNNF called ROBDD[∧̂i ]C by imposing reducedness, the finest ∧i-decomposability, and ordered decision respecting a chain C; and another family of canonical languages called ROBDD[∧ ̂ T ,i ]T by imposing reducedness, the finest ∧T ,idecomposability, and ordered decision respecting T . We demonstrate that these two families of languages cover the three previous languages ROBDD, AOBDD and ROBDDL∞, as depicted in Figure 1.

We evaluate the theoretical properties of the two families of canonical languages from four aspects, and the obtained results significantly extend the current KC map:

• (a) We analyze the expressivity and demonstrate that ROBDD[∧̂i ]C is complete while ROBDD[∧̂ T ,i ]T is incomplete. We also demonstrate that if i ≤ j, ROBDD[∧̂ T ,i ]T is not more expressive than ROBDD[∧ ̂ T ,j ]T (resp. CSDDV).
• (b) We analyze the succinctness and demonstrate that ROBDD[∧̂i ]C (resp. MODS) is strictly less succinct than ROBDD[∧̂j ]C if i < j. We also demonstrate that ROBDD[∧ ̂ T ,i ]T is at most as succinct as ROBDD[∧̂i ]C.

• (c) We analyze the time efficiency in terms of tractability. We demonstrate that ROBDD[∧̂ T ,i ]T is not less tractable than ROBDD. We also demonstrate that ROBDD[∧̂i ]C (i ≥ 2) maintains the same tractability as ROBDD-L∞, which is more tractable than d-DNNF.
• (d) We also analyze the time efficiency in terms of a new notion called rapidity. We prove that each operation on ROBDD[∧̂i ]C (resp. ROBDD[∧̂ T ,j ]T and MODS) is at most as rapid as the same operation on ROBDD[∧̂j ]C.

For practical purposes, we developed an ROBDD[∧̂∞]C compiler with high efficiency. Preliminary experimental results indicate that our compiler is significantly more efficient than the state-of-the-art compilers of ROBDD-L∞ and CSDDV; moreover, only our compiler is comparable to DSHARP in both compiling time and resulting sizes.

2 Basic Concepts

This paper uses x to denote a propositional or Boolean variable, and PV = {x1, . . . , xn, . . .} to denote a countably infinite set of variables. A formula ϕ is constructed from constants true, false and variables in PV using negation operator ¬, conjunction operator ∧, disjunction operator ∨, equality operator ↔ and decision operator ψ ⋄x ψ′ = (¬x ∧ ψ) ∨ (x ∧ ψ′ ), and we use V ars(ϕ) to denote the set of variables appearing in ϕ.

We assume that PV is associated with some strict (partial) order ≺. We focus on the tree-structured orders which are defined as the ancestor-descendant relationships on trees of variables. Given a tree T over variables, we denote its depth by dep(T ), and the corresponding order by ≺T .

Definition 1 (∧-decomposition, ∧i-decomposition and ∧T -decomposition). Given a formula ϕ, a formula set Ψ is its ∧-decomposition, iff ϕ ≡ ∧ψ∈Ψ ψ and {V ars(ψ) : ψ ∈ Ψ} partitions V ars(ϕ). Ψ is bounded by an integer 0 ≤ i ≤ ∞ (∧i-decomposition) iff there exists at most one ψ ∈ Ψ with |V ars(ψ)| > i. Ψ respects a tree T over variables (∧T - decomposition), iff any two formulas ψ, ψ′ ∈ Ψ satisfy that V ars(ψ) and V ars(ψ′ ) are from two disjoint subtrees.

[Lai et al., 2013] and [Mateescu et al., 2008] implicitly discussed ∧1-decomposition and ∧T -decomposition, respectively. Given two ∧-decompositions Ψ and Ψ′ of a formula,

Ψ is strict iff |Ψ| > 1; and Ψ is finer than Ψ′ iff {V ars(ψ) : ψ ∈ Ψ} is a finer partition than {V ars(ψ) : ψ ∈ Ψ′ }.

Proposition 1. From the viewpoint of equivalence, each nontrivial formula has exactly one finest ∧i-decomposition (resp. ∧T -decomposition).

The finest ∧i-decomposition (resp. ∧T -decomposition) is hereafter denoted by ∧̂i -decomposition (resp. ∧̂ T - decomposition), and a ∧̂ T -decomposition bounded by integer i is denoted by ∧̂ T ,i -decomposition.

3 ROBDD[∧̂i ]C and ROBDD[∧̂ T ,i ]T

We first define binary decision diagram with conjunctive decomposition (BDD[∧]):

Definition 2 (BDD[∧]). A BDD[∧] is a rooted DAG. Each vertex v is labeled with a symbol sym(v). If v is a leaf, sym(v) = ⊥ or ⊤; otherwise, sym(v) is a variable or operator ∧. Each internal vertex v has a set of children Ch(v). For a vertex labeled with variable, Ch(v) = {lo(v), hi(v)}, where lo(v) and hi(v) are called low and high children, and are connected by dashed and solid arcs, respectively; for a ∧- vertex, {ϑ(w) : w ∈ Ch(v)} is a strict ∧-decomposition of ϑ(v). Each vertex represents a formula defined as follows:

The formula represented by the BDD[∧] is defined as the one represented by its root.

Given two vertices, we say that they are identical with each other, if they are leaf vertices with the same symbol, or they are internal vertices with the same symbol and children. Next we define some constraints on BDD[∧]:

Definition 3 (constraints on BDD[∧]). Given an integer i, a partial order ≺ over variables, and a tree T over variables,

• A BDD[∧] is ordered over ≺ (OBDD[∧]≺) iff each ⋄- vertex u and its ⋄-descendant v satisfy sym(u) ≺ sym(v);
• A BDD[∧] is reduced (RBDD[∧]) iff no two vertices are identical and no ⋄-vertex has two identical children;
• A BDD[∧] is, respectively, ∧i-decomposable and ∧T ,idecomposable (BDD[∧i] and BDD[∧T ,i]) iff each ∧- vertex is a ∧i-decomposition and a ∧T ,i-decomposition;
• A BDD[∧] is, respectively, ∧̂i -decomposable and ∧̂ T ,i - decomposable (BDD[∧̂i ] and BDD[∧̂ T ,i ]) iff each ∧- vertex is a ∧̂i -decomposition and a ∧̂ T ,i -decomposition, and the ∧̂i -decomposition and ∧̂ T ,i -decomposition of each ⋄-vertex v are {ϑ(v)}.

In the subsequent sections, we focus on OBDD[∧]≺ where ≺ is tree-structured: the ancestor-descendant relationship ≺T on a tree T and particularly ≺C over a chain C. We assume that C and T always satisfy ≺T ⊂≺C, and we sometimes use C and T to denote ≺C and ≺T , respectively. We will analyze the canonicity, expressivity, and space-time efficiency of ROBDD[∧̂i ]C and ROBDD[∧̂ T ,i ]T . Note that each ROBDD over C is an ROBDD[∧̂0 ]C, and the mutual transformation between an ROBDD-L∞ over C (resp. AOBDD over T ) and the equivalent ROBDD[∧̂1 ]C (resp. ROBDD[∧̂ T ,∞]T ) can be performed in linear time.

4 Canonicity and Expressivity

We first state that ROBDD[∧̂i ]C is canonical and complete:

Theorem 1. Fixing integer i and chain C over PV , there is exactly one ROBDD[∧̂i ]C representing a given formula.

ROBDD[∧ ̂ T ,i ]T is also canonical, but incomplete:

Theorem 2. Fixing tree T over PV , there is at most one ROBDD[∧̂ T ,i ]T to represent a given formula, and ROBDD[∧ ̂ T ,i ]T is incomplete when T is not a chain.

Due to the incompleteness of ROBDD[∧̂ T ]T , we draw the expressivity relation between different ROBDD[∧̂ T ,i ]T :

Theorem 3. Given a tree T over variables and two integers i and j, ROBDD[∧̂ T ,i ]T is at most as expressive as ROBDD[∧ ̂ T ,j ]T if i ≤ j.

Given a vtree V corresponding to T , ROBDD[∧̂ T ,i ]T is at most as expressive as CSDDV, because the former is a subset of the latter.

5 Succinctness

In this section, we first analyze the succinctness relationship between ROBDD[∧̂i ]C and ROBDD[∧̂j ]C, and we then analyze the succinctness relationship between ROBDD[∧̂i ]C and ROBDD[∧ ̂ T ,i ]T . Note that the standard definition of succinctness in the KC map only applies to complete languages. We can extend it to handle the case of incomplete languages by only comparing the sizes of formulas that can be represented in both languages.

We can present an algorithm (see Algorithm DECOMPOSE in [Lai et al., 2017]) to transform an OBDD[∧i]C into the equivalent ROBDD[∧̂i ]C. Along with some counter-examples, we can state the following succinctness results:

Theorem 4. ROBDD[∧̂i ]C is at most as succinct as ROBDD[∧̂j ]C iff i ≤ j.

The above theorem indicates that ROBDD[∧̂i ]C can further mitigate the size explosion problem of ROBDD from a theoretical perspective. We then analyze the succinctness relationship between ROBDD[∧̂ T ,i ]T and ROBDD[∧̂i ]C:

Theorem 5. ROBDD[∧̂ T ,i ]T is as succinct as ROBDD[∧̂i ]C if i = 0 or dep(T ) < ∞, and ROBDD[∧̂ T ,i ]T is strictly less succinct than ROBDD[∧̂i ]C otherwise.

The succinctness relationship between ROBDD[∧̂i ]C (resp. ROBDD[∧ ̂ T ,i ]T ) and the ones in {ROBDD, ROBDD-L∞, AOBDD} is immediate from Theorems 4-5. The succinctness relationship between ROBDD[∧̂i ]C (i ≥ 1) and CSDDV is incomparable, because some class of circular bit-shift functions can be represented in ROBDD[∧̂i ]C but not in CSDDV in polysize [Pipatsrisawat, 2010]. Finally, ROBDD[∧̂ T ,i ]T is strictly more succinct than MODS if some variable in T has an infinite number of disjoint subtrees each of which has at least two vertices.

Table 1: Polytime queries and transformations of ROBDD[∧̂i ]C and

ROBDD[∧ ̂ T ,i ]T , where C and T are over PV , √ means "satisfies", · means "does not satisfy", and ◦ means "does not satisfy unless P = NP"

6 Operating Efficiency

We now analyze the time efficiency of operating ROBDD[∧̂i ]C and ROBDD[∧̂ T ,i ]T in terms of tractability and a new notion called rapidity. We can write an operation as a set of triples with the form (ϕ1, . . . , ϕn, α, β), where ϕ1, . . . , ϕn represent the input formulas, α represents the supplementary input, and β represents the output.

6.1 Tractability Evaluation

We examine the tractability of ROBDD[∧̂i ]C and ROBDD[∧ ̂ T ,i ]T with respect to the criteria proposed in [Darwiche and Marquis, 2002] in Table 1.

According to the results in Table 1, we know that ROBDD[∧̂i ]C (i ≥ 2) is as tractable as ROBDD-L∞. In other words, compared with ROBDD-L∞ over C, ROBDD[∧̂i ]C indeed improves the succinctness under the premise of maintaining the same tractability. Moreover, we know that ROBDD[∧ ̂ T ,i ]T is at least as tractable as ROBDD; in particular, ROBDD[∧̂ T ,i ]T even has more tractability than ROBDD if dep(T ) < ∞. Finally, we know that ROBDD[∧̂i ]C is more tractable than d-DNNF, and ROBDD[∧̂ T ,i ]T is more tractable than CSDDV [Van den Broeck and Darwiche, 2015].

6.2 New Perspective on Time Efficiency

Due to distinct succinctness, it can sometimes be insufficient to compare the time efficiency of two languages solely by comparing their tractability. Consider an operation OP, and two languages L and L′ such that L does not satisfy OP but L′ satisfy OP. Assume that the number of basic arithmetic operations involved in performing OP on (ϕ1, . . . , ϕn, α) (resp. (ϕ′1 , . . . , ϕ′n , α)) be 2m (resp. n), where ϕi ∈ L (resp. ϕ′i ∈ L′ ), and m = |α| + ∑1≤i≤n |ϕi| (resp. n = |α| + ∑1≤i≤n |ϕ′i |). Then, performing OP on (ϕ1, . . . , ϕn, α) can be exponentially (in m) more timeconsuming than performing OP on (ϕ′1 , . . . , ϕ′n , α) when n = 2m2 . To overcome this problem, we define a new notion to compare time efficiency from a different perspective, supplementing the concept of tractability:

Definition 4 (rapidity). An operation OP on a canonical language L1 is at most as rapid as OP on another canonical language L2 (L1 ≤OP r L2), iff for each algorithm ALG

performing OP on L1, there exists some polynomial p and some algorithm ALG′ performing OP on L2 such that for every valid input (ϕ1, . . . , ϕn, α) of OP on L1 and every valid input (ϕ′1 , . . . , ϕ′n , α) of OP on L2 satisfying ϕi ≡ ϕ′i , ALG′ (ϕ′1 , . . . , ϕ′n , α) can be done in time p(t + |ϕ1| + · · · + |ϕn| + |α|), where α is any element of supplementary information and t is the running time of ALG(ϕ1, . . . , ϕn, α).

Assume that an operation OP satisfies L1 ≤OP r L2. Let (ϕ1, . . . , ϕn, α) be a valid input of OP on L1 and (ϕ′1 , . . . , ϕ′n , α) be a valid input of OP on L2, where ϕi ≡ ϕ′i for 1 ≤ i ≤ n. We know that if performing OP on (ϕ1, . . . , ϕn, α) can be done in polytime, then performing OP on (ϕ′1 , . . . , ϕ′n , α) can also be done in polytime in |α| + ∑1≤i≤n |ϕi|. Therefore, for applications needing canonical languages, we suggest that users choose a language by the following steps rather than by the traditional viewpoint of the KC map: first, identify the set L of canonical languages meeting the expressivity requirement; second, identify the set OP of necessary operations and identify the subset L′ of L meeting the tractability requirement; third, add each language L ∈ L satisfying ∃L′ ∈ L′∀OP ∈ OP.L′ ≤OP r L to L′ ; and finally, choose one of the most succinct languages in L′ .

We can propose algorithms (see Algorithms CONVERTDOWN and CONVERTTREE in [Lai et al., 2017]) which respectively transform ROBDD[∧̂j ]C and ROBDD[∧̂i ]C into ROBDD[∧̂i ]C and ROBDD[∧̂ T ,i ]T (i ≤ j) and whose time complexities are polynomial in the sizes of outputs. Then we can obtain the following rapidity results:

Theorem 6. Given two integers i and j, a chain C and a tree T over variables, and an operation OP, MODS ≤OP r ROBDD[∧̂i ]C ≤OP r ROBDD[∧̂j ]C if i ≤ j; and ROBDD[∧ ̂ T ,i ]T ≤OP r ROBDD[∧̂i ]C.

It was mentioned that for the operation OP corresponding to SE, SFO, ∧BC or ∨BC, OP on ROBDD[∧̂0 ]C can be performed in polytime but OP on ROBDD[∧̂i ]C (i > 0) cannot be performed in polytime unless P = NP. Therefore, if we only consider the tractability of OP, it may create the illusion that the time efficiency of performing OP on ROBDD[∧̂i ]C is pessimistically lower than that of performing OP on ROBDD[∧̂0 ]C. Actually, OP on ROBDD[∧̂i ]C can also be performed in polytime in the sizes of equivalent ROBDD[∧̂0 ]Cs. According to this new perspective, an application requiring OP prefers ROBDD[∧̂i ]C to ROBDD[∧̂0 ]C.

7 Preliminary Experimental Results

We developed an ROBDD[∧̂∞]C compiler, and compare it with three compilers of two canonical languages ROBDDL∞ and CSDDV and a non-canonical language d-DNNF. The three canonical languages can be seen as subsets of dDNNF. The state-of-the-art ROBDD-L∞, CSDDV and dDNNF compilers are reported in [Lai et al., 2013; Oztok and Darwiche, 2015; Muise et al., 2012], and called BDDjLu, miniC2D and DSHARP, respectively. Individual runs were limited to a one-hour time-out. Table 2 shows the overall performance of the four compilers over the eight domains. The experimental results show that the ROBDD[∧̂∞]C compiler outperformed both BDDjLu and miniC2D on three domains; and it succeeded in 18 (resp. 30) instances more than BDDjLu (resp. miniC2D). The ROBDD[∧̂∞]C compiler and DSHARP outperformed each other on two domains. However, DSHARP succeeded in six more instances than the ROBDD[∧̂∞]C compiler, since the latter was relatively inefficient in sortnet. The reason behind the inefficiency of ROBDD[∧̂∞]C compiler in sortnet is that the ordering heuristic has a negative effect on this domain. Specifically, the ROBDD[∧̂∞]C compiler succeeded in all instances in sortnet when we used the lexicographical order of variables.

Figure 2 analyzes the detailed compiling time and resulting size performance between our ROBDD[∧̂∞]C compiler and DSHARP across the eight domains in Table 2. The experimental results show that the performance of the ROBDD[∧̂∞]C compiler is comparable with that of DSHARP.

8 Conclusions

We proposed two families of canonical languages, and analyzed their theoretical properties in terms of the existing criteria of expressivity, succinctness and tractability, as well as the new criterion rapidity. These results provide an important complement to the existing KC map, and the notion of rapidity sheds new light on identifying more succinct canonical representations without the worry of losing the tractability of KC languages. We also developed an efficient ROBDD[∧̂∞]C compiler, which significantly advances the state-of-the-art of compiling efficiency of canonical representations, and has compiling efficiency even comparable with that of DSHARP.