On CNF Encodings of Decision Diagrams

Abstract

Decisions diagrams such as Binary Decision Diagrams (BDDs), Multi-valued Decision Diagrams (MDDs) and Negation Normal Forms (NNFs) provide succinct ways of representing Boolean and other finite functions. Hence they provide a powerful tool for modelling complex constraints in discrete satisfaction and optimization problems. Generic propagators for these global constraints exist, but they are complex and hard to implement. An alternative approach to making use of them for solving is to encode them to CNF, using SAT style solving technology to implement them efficiently. This may also have advantages since it is naturally incremental and exposes intermediate literals which may well be useful as search decisions for solving the problem.

In this paper we explore different ways that we can map these constraints to CNF, and the different properties these mappings maintain. Surprisingly the most used encoding of BDDs does not maintain domain consistency in arbitrary BDDs. We also consider the strength of propagation with respect to the intermediate literals. We give experiments which compare the performance of the different encodings.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Decisions diagrams such as Binary Decision Diagrams (BDDs), Multi Decision Diagrams (MDDs) and Negation Normal Forms (NNFs) provide succinct ways of representing Boolean and other finite functions. Hence they provide a powerful tool for modelling complex constraints in discrete satisfaction and optimization problems.

Constraint programming solvers include generic propagators for propagating constraints represented by BDDs [16], MDDs [8] and NNFs [15], since they are highly flexible, and hence useful in many different models. But these propagators are complex and hard to implement.

An alternative approach to making use of them for solving is to encode them to CNF, using SAT style solving technology to implement them efficiently. If the remainder of the problem is naturally modelled in CNF then this allows a SAT solver to tackle the problem.

A SAT encoding may also be preferable within a CP solver, as it avoids the need for implementing complex propagators, is naturally incremental, and exposes intermediate literals as candidates for search and learning. A good encoding is critical in lazy decomposition approaches [1], where a propagator that participates in many conflicts is replaced by a CNF decomposition during runtime.

In this paper we explore different approaches for encoding decision diagrams to CNF.¹ The contributions of this paper are:

• An investigation of a large design space for encoding decision diagrams.

• We clarify the picture of BDD/MDD/NNF encodings, analyse their propagation strength and correct some misunderstandings in the literature.

• We introduce an encoding of BDDs and MDDs where unit propagation implements propagation completeness.

• Experiments which compare the performance of the different encodings.

2 Preliminaries

2.1 SAT Solving

We denote the Boolean value true by $\top$ and false by $\bot$.

Let $\mathcal{Y}=\{y_1,y_2,\ldots \}$ be a fixed set of propositional variables. If $y\in \mathcal{Y}$ then y and $\lnot y$ are positive and negative literals, respectively. The negation of a literal l, written $\lnot l$, denotes $\lnot y$ if l is y, and y if l is $\lnot y$. A clause is a disjunction of literals $\lnot y_1 \vee \cdots \vee \lnot y_p \vee y_{p+1} \vee \cdots \vee y_n$, sometimes written as $y_1 \wedge \cdots \wedge y_p \rightarrow y_{p+1} \vee \cdots \vee y_n$. A CNF formula F is a conjunction of clauses.

A set of literals A is contradictory if $\exists y. \{y, \lnot y\} \subset A$. A (partial) assignment A is a set of literals which is not contradictory. A literal l is true in A if $l \in A$, is false in A if $\lnot {l} \in A$, and is undefined in A otherwise. An extension of an assignment A is an assignment $A'$ where $A' \supset A$. A complete assignment is an assignment with no undefined literals. Given a partial assignment A, a completion of A is an extension of A which is a complete assignment.

A complete assignment A satisfies formula $\phi$ if replacing each y in $\phi$ which is true in A with $\top$ and replacing each y in $\phi$ which is false in A with $\bot$ gives an expression which evaluates to $\top$. A partial assignment A satisfies formula $\phi$, written $A\,\models \,\phi$ if every completion of A satisfies $\phi$.

Systems that decide whether a CNF formula F has any model are called SAT solvers, and the main inference rule they implement is unit propagation: given a CNF F and an assignment A, find a clause in F such that all its literals are false in A except at most one, say l, which is undefined, add l to A and repeat the process until reaching a fix-point. See e.g. [21] for more details.

For some set of clauses C, we shall use $UP _C(A)$ to denote the set of literals inferred by unit propagation on C starting from assignment A. We will omit the C subscript when clear from the context. Note that $UP _C(A)$ may be contradictory, in which case unit propagation has detected unsatisfiability.

2.2 Propositional Encodings

Problems of interest rarely (if ever) begin in CNF form. Boolean formulae $\phi$ must be first converted into some equisatisfiable conjunction of clauses $F_\phi$. The seminal work here is the Tseytin transformation [25], later refined by Plaisted and Greenbaum [22], which introduces a variable for each sub-formula and adds clauses to enforce the semantics of each connective.

While equisatisfiability is sufficient for correctness, the choice of decomposition can have a great impact on solver performance. A major consideration here is propagation strength – that is, given some partial assignment A and formula $\phi$, what can be said of $UP _{F_\phi }(A)$.

There are a number of properties we may wish of $F_\phi$.

• An encoding $F_\phi$ for a formula $\phi$ is correct if any complete assignment A on $vars(\phi )$ where $A\,\models \,\phi$, then A has an extension satisfying $F_\phi$, and any complete assignment $A\,\models \,\lnot \phi$ has no extension satisfying $F_\phi$.

• An encoding $F_\phi$ for a formula $\phi$ implements consistency if for every assignment A over $vars(\phi )$ where $A\,\models \,\lnot \phi$, then $UP _{F_\phi }(A)$ is contradictory.

• An encoding $F_\phi$ for a formula $\phi$ implements domain consistency when for each literal l over $vars(\phi )$, if $A\,\models \,\phi \rightarrow l$ then $l \in UP _{F_\phi }(A)$.

• An encoding $F_\phi$ for a formula $\phi$ implements unit refutation completeness [26] (also called SLUR [19]) when for assignment B over $vars(F_\phi )$ where $B\,\models \,\lnot F_\phi$, then $UP _{F_\phi }(B)$ is contradictory.

• An encoding $F_\phi$ for a formula $\phi$ implements propagation completeness [6, 19] when for each literal l over $vars(F_\phi )$, $B\,\models \,F_{\phi } \rightarrow l$ then $l \in UP _{F_\phi }(B)$.

Another important consideration is the encoding size. In general, smaller encodings are more efficient than larger ones, if both have the same propagation strength.

2.3 At-most-one and Exactly-one Constraints

Given a set of literals $l_1, \ldots , l_n$, the At-most-one (${{\mathrm{AMO}}}$) constraint over these literals is defined as $l_1 + l_2 + \ldots + l_n \le 1$.

There are several ways to encode AMO into SAT [3, 7, 14]. Here, we consider the ladder encoding. It introduces variables $\{ a_i := l_1 \vee \ldots \vee l_i \ \vert \ 1 \le i < n \}$ and clauses $\{ a_i \rightarrow a_{i+1}, l_i \rightarrow a_i, l_{i+1} \rightarrow \lnot a_i \}$. It is easy to see that this encoding is propagation complete.

Given a set of literals $l_1, \ldots , l_n$, the Exactly-one (${{\mathrm{EO}}}$) constraint over these literals is defined as $l_1 + l_2 + \ldots + l_n = 1$. Notice that

$${{\mathrm{EO}}}(\{l_1, \ldots , l_n\}) = {{\mathrm{AMO}}}(\{l_1, \ldots , l_n\}) \wedge (l_1 \vee \ldots \vee l_n)$$

This defines a propagation complete encoding for ${{\mathrm{EO}}}$ given a propagation complete encoding of ${{\mathrm{AMO}}}$.

2.4 Direct Encoding for Integer Variables

There are different methods for encoding integer variables into SAT (see for instance [18, 27]). In this paper we use the direct encoding.

Let x be an integer variable with domain [a, b]. The direct encoding introduces Boolean variables $\mathbf {[\![}{x = i}\mathbf {]\!]}$ for $a \le i \le b$. A variable $\mathbf {[\![}{x=i}\mathbf {]\!]}$ is true iff $x = i$. The encoding also introduces the constraint ${{\mathrm{EO}}}(\{ \mathbf {[\![}{x=i}\mathbf {]\!]} ~|~ a \le i \le b\})$.

We will sometimes treat Boolean variables b as integers with domain [0,1].

We will implicitly assume that the direct encoding clauses ${{\mathrm{EO}}}(\{ \mathbf {[\![}{x=i}\mathbf {]\!]} \ \vert \ a \le i \le b \})$ are part of any encoding of formula using integers x. We also assume all assignments A are closed under unit propagation of these clauses.

We extend the notion of satisfaction to formulae involving integer variables, as follows. A complete assignment A satisfies $\phi$ if replacing each Boolean variable as before, and each integer variable $x_i$ by j if $\mathbf {[\![}{x_i = j}\mathbf {]\!]} \in A$ (since $A\,\models \,{{\mathrm{EO}}}(\{ \mathbf {[\![}{x_i=j}\mathbf {]\!]} \ \vert \ a \le j \le b \})$ there must be exactly one) and evaluating the resulting ground expression gives $\top$. We extend the notation $A \models \phi$ as before.

2.5 Multi-valued Decision Diagrams

A directed acyclic graph $\mathcal M$ is called an ordered Multi-valued Decision Diagram (MDD) if it satisfies the following properties:

• It has two terminal nodes, namely $\mathcal T$ (true) and $\mathcal F$ (false).

• Each non-terminal node is labeled by an integer variable $\{x_1, x_2, \cdots , x_n\}$. This variable is called selector variable.

• Every node labeled by $x_i$ has the same number of outgoing edges, namely $b_i-a_i+1$, where $[a_i,b_i]$ is the domain of $x_i$.

• If an edge connects a node with a selector variable $x_i$ and a node with a selector variable $x_j$, then $j > i$.

The MDD is quasi-reduced if no isomorphic subgraphs exist. It is reduced if, moreover, no nodes with only one child exist. A long edge is an edge connecting two nodes with selector variables $x_i$ and $x_j$ such that $j > i+1$. In the following we only consider quasi-reduced ordered MDDs without long edges, and we just refer to them as MDDs for simplicity.² We refer to [24] for further details about MDDs.

Given an MDD $\mathcal M$ we use $\rho$ to refer to its root node. Given a node $\nu \in \mathcal M$, we write ${{\mathrm{var}}}(\nu ) = x_j$ when node $\nu$ is labelled by $x_j$. Given an edge $\varepsilon \in \mathcal M$, we write $\varepsilon = {{\mathrm{edge}}}(\nu , \mu , \mathbf {[\![}{x_i=j}\mathbf {]\!]})$ if $\varepsilon$ joins the node $\nu$ and $\mu$ when $x_i =j$.

An MDD represents a formula over integer variables: a MDD node $\nu$ with selector x with domain [a, b] and children $\nu _a, \nu _{a+1}, \ldots , \nu _b$ represents the formula $\phi _\nu$ where

$$ \phi _\nu \equiv \bigvee _{i \in [a,b]} x = i \wedge \phi _{\nu _i} $$

where $\phi _{\nu _i}$ is the formula represented by node $\nu _i$, and $\phi _\mathcal{T}= \top$ and $\phi _\mathcal{F}= \bot$.

Fig. 1.

(a) MDD of $x_2=0 \vee (x_3= 0 \wedge x_2 - x_1 =1)$ and (b) BDD of $x_2 \wedge (x_1 \vee x_3)$

Example 1

Let us consider the MDD encoding of $x_2=0 \vee ( x_3= 0 \wedge x_2 - x_1~=1)$, with $x_1, x_3 \in \{0,1\}$ and $x_2 \in \{0,1,2\}$, shown in Fig. 1(a). In this case $\rho = \nu _1$, ${{\mathrm{var}}}(\nu _3) = x_2$, and the rightmost edge from $\nu _3$ is ${{\mathrm{edge}}}(\nu _3, \nu _6, x_2 = 1)$. $\phi _{\nu _4} \leftrightarrow \top$, $\phi _{\nu _5} \leftrightarrow x_3 = 0$, $\phi _{\nu _6} \leftrightarrow \bot$, and hence $\phi _{\nu _2} \leftrightarrow (x_2 = 0 \wedge \top ) \vee (x_2 = 1 \wedge x_3 = 0) \vee (x_2 = 2 \wedge \bot )$ or equivalently $\phi _{\nu _2} \leftrightarrow x_2 = 0 \vee (x_2 = 1 \wedge x_3 = 0)$.   $\square$

A binary decision diagram (BDD) is an MDD with only Boolean variables. For a BDD $\mathcal M$ we can consider a non-terminal node $\nu$ as a triple $(x, t, f)$ where there are two outgoing edges ${{\mathrm{edge}}}(\nu , t, x)$ and ${{\mathrm{edge}}}(\nu , f, \lnot x)$. The BDD node $\nu$ represents the formula $\phi _\nu \equiv ITE(x,\phi _t,\phi _f)$ or equivalently $(x \wedge \phi _t) \vee (\lnot x \wedge \phi _f)$.

2.6 Negation Normal Form Formulae

A negation normal form formula (NNF) is a rooted, directed acyclic graph (DAG) where each leaf node is labeled with x or $\lnot x$ and each internal node is labeled with $\wedge$ or $\vee$ and can have arbitrarily many children.

NNFs are a more general form of decision diagram than BDDs, and can be exponentially more compact to represent the same formula [11]. We can use NNFs to express formulae over finite domain integer variables using the direct encoding.

But NNFs in general are too expressive, so usually we require some additional properties, such as:

• Decomposable. An NNF $\mathcal N$ is decomposable if for each conjunction $\phi$ in $\mathcal N$, the conjuncts of $\phi$ do not share variables. That is, if $\phi _1, \ldots , \phi _n$ are the children of and-node $\phi$, then $vars(\phi _i) \cap vars(\phi _j) = \emptyset$ for $i \ne j$.

• Deterministic. An NNF $\mathcal N$ is deterministic if for each disjunction $\phi$ in $\mathcal N$, each two disjuncts of $\phi$ are logically contradictory. That is, if $\phi _1, \ldots , \phi _n$ are the children of or-node $\phi$, then $\phi _i \wedge \phi _j\,\models \,\bot$ for $i \ne j$.

• Smooth. An NNF $\mathcal N$ is smooth if for each disjunction $\phi$ in $\mathcal N$, each disjunct of $\phi$ mentions the same variables. That is, if $\phi _1, \ldots , \phi _n$ are the children of or-node $\phi$, then $vars(\phi _i) = vars(\phi _j)$ for $i \ne j$.

3 Encoding MDDs

3.1 Encoding BDDs

The BDD encoding of MiniSat+ [13] is defined as follows: For each non-terminal BDD node $\nu = (x,t,f)$ we generate a Boolean variable $\nu$ which represents the truth value of the BDD rooted at $\nu$.

For each non-terminal node $\nu = (x,t,f)$, we generate the following clauses:

Define encoding MiniSAT as B1–B6, together with the terminal and root clauses: $\mathcal{T}$ (the true terminal is true), $\lnot \mathcal{F}$ (the false terminal is false) and $\rho$ (the root of the tree must be true).

Note while Een and Sorensen [13] refer to this as a Tseytin encoding, it is not since Tseytin [25] does not include an ITE constructor, so in the Tseytin encoding ITE(x, t, f) needs to be encoded as $(x\wedge t) \vee (\lnot x\wedge f)$.

The encoding contains O(s) variables and clauses, where s is the size of the BDD.

Een and Sorensen [13] show that this encoding maintains domain consistency when used to encode (sorted) pseudo-Boolean constraints.

Theorem 1

([13]). Unit propagation on the MiniSAT encoding for a BDD for pseudo-Boolean constraint $\sum _{i=1}^n c_i x_i \ge d$ maintains domain consistency, assuming the coefficients $c_i$ are in non-increasing order.   $\square$

This theorem does not hold without the ordering criterion. Consider the BDD encoding $x_1 + 2 x_2 + x_3 \ge 3$ (or equivalently $x_2 \wedge (x_1 \vee x_3)$) shown in Fig. 1(b). Any solution of the BDD requires $x_2$ is $\top$. Unit propagation on the MiniSAT encoding generates $\lnot \mathcal{F}, \mathcal{T}, \nu _1, \lnot \nu _4, \nu _6$ and nothing else.

Theorem 2

Unit propagation on the clauses (B2), (B4), (B6), $\lnot \mathcal{F}$, $\rho$ for a BDD maintains consistency.    $\square$

All in all, the encoding is compact (especially if only clauses (B2), (B4), (B6), $\lnot \mathcal{F}$ and $\rho$ are used), but the propagation strength is low.

3.2 Encodings MDDs with One Variable Per Node

The first set of encodings for MDDs, used for example in [2], are generalizations of the MiniSat+ encoding. This is natural since they are also used to encode pseudo-Boolean and linear constraints.

For each node $\nu$ at level i, with children $\nu _{a_i}, \nu _{a_i+1}, \ldots , \nu _{b_i}$, where the domain of $x_i$ is $[a_i, b_i]$.

• M1 $\lnot \nu _j \wedge \mathbf {[\![}{x_i=j}\mathbf {]\!]} \rightarrow \lnot \nu$ (generalizes B2 and B4).

• M2 $\nu _j \wedge \mathbf {[\![}{x_i=j}\mathbf {]\!]} \rightarrow \nu$ (generalizes B1 and B3).

• M3 $\nu _{a_i} \wedge \nu _{a_i+1} \wedge \cdots \wedge \nu _{b_i} \rightarrow \nu$ (weakly generalizes B5).

• M4 $\lnot \nu _{a_i} \wedge \lnot \nu _{a_i+1} \wedge \cdots \wedge \lnot \nu _{b_i} \rightarrow \lnot \nu$ (weakly generalizes B6).

With these clauses, we can define different encodings:

• Minimal: Clauses M1, $\lnot \mathcal{F}$, $\rho$.

• GenMiniSAT: Clauses M1–M4, $\mathcal{T}$, $\lnot \mathcal{F}$, $\rho$.

Minimal is very compact, but its propagation strength is low, moreover when the original variables are fixed it does not necessarily fix all the node variables, and hence does not preserve solution counts. GenMiniSAT is the natural generalization of the BDD encoding from [13] to MDDs. Again, it is not the Tseytin encoding [25] of the MDD. Both encodings use O(s) variables and O(sd) clauses, where s is the MDD size and d is the maximum domain size of variables x.

Proposition 1

Let $A = \{ \mathbf {[\![}{x_i = v_i}\mathbf {]\!]} ~|~ 1 \le i \le n \}$ be a complete assignment on variables x satisfying the MDD $\mathcal M$. Then, there exists a complete assignment $B \supset A$ over the variables $x, \nu$ satisfying clauses GenMiniSAT.   $\square$

Proposition 2

Let $A = \{ \mathbf {[\![}{x_i = v_i}\mathbf {]\!]} ~|~ 1 \le i \le n \}$ be a complete assignment on variables x not satisfying the MDD $\mathcal M$, then clauses $\rho$ and M1 propagate $\mathcal{F}$.   $\square$

Corollary 1

Minimal and GenMiniSAT are correct.    $\square$

These two encodings, however, do not detect inconsistencies:

Example 2

Consider again the MDD of $x_2=0 \vee ( x_3= 0 \wedge x_2 - x_1 =1)$, with $x_1, x_3 \in \{0,1\}$ and $x_2 \in \{0,1,2\}$ shown in Fig. 1(a).

After simplification, GenMiniSAT consists of the following clauses:

$$\begin{array}{llll} \lnot \mathbf {[\![}{x_1=0}\mathbf {]\!]} \vee \nu _2, &{} \lnot \mathbf {[\![}{x_1=1}\mathbf {]\!]} \vee \nu _3, &{} \nu _2 \vee \nu _3, &{} \lnot \mathbf {[\![}{x_2=0}\mathbf {]\!]} \vee \nu _2, \\ \lnot \nu _4 \vee \lnot \mathbf {[\![}{x_2=1}\mathbf {]\!]} \vee \nu _2, &{} \nu _4 \vee \lnot \mathbf {[\![}{x_2=1}\mathbf {]\!]} \vee \lnot \nu _2, &{} \lnot \mathbf {[\![}{x_2=2}\mathbf {]\!]} \vee \lnot \nu _2 &{} \lnot \mathbf {[\![}{x_2=0}\mathbf {]\!]} \vee \nu _3, \\ \lnot \nu _4 \vee \lnot \mathbf {[\![}{x_2=2}\mathbf {]\!]} \vee \nu _3, &{} \nu _4 \vee \lnot \mathbf {[\![}{x_2=2}\mathbf {]\!]} \vee \lnot \nu _3, &{} \lnot \mathbf {[\![}{x_2=1}\mathbf {]\!]} \vee \lnot \nu _3 &{} \lnot \mathbf {[\![}{x_3=0}\mathbf {]\!]} \vee \nu _4, \\ \lnot \mathbf {[\![}{x_3=1}\mathbf {]\!]} \vee \lnot \nu _4. \end{array}$$

Consider the partial assignment $A = \{ \lnot \mathbf {[\![}{x_2=0}\mathbf {]\!]}, \lnot \mathbf {[\![}{x_3=0}\mathbf {]\!]}, \mathbf {[\![}{x_3=1}\mathbf {]\!]} \}$. It cannot be extended to a complete assignment satisfying the MDD. However, unit propagation does not fail.

The same happens with Minimal, since it is a subset of GenMiniSAT.   $\square$

3.3 Tseytin Encoding of an MDD

In this section we describe an alternative encodings for an MDD, the Tseytin encoding [25]. It detects inconsistencies with respect to the original variables but does not enforce domain consistency.

The Tseytin encoding introduce Boolean variables representing the formula of each edge. Let $\nu$ be a node at level i, with outgoing edges $\{ \varepsilon _j \ \vert \ j \in J \}$. Let $\varepsilon = {{\mathrm{edge}}}(\nu , \mu , \mathbf {[\![}{x_i=j}\mathbf {]\!]})$ be an edge of $\mathcal M$, then the Boolean variable $\varepsilon$ encoding the edge represents the formula $\mathbf {[\![}{x_i=j}\mathbf {]\!]} \wedge \phi _\mu$.

The clauses of the Tseytin encoding are, for each node $\nu$ and edge $\varepsilon$

• T1 $\nu \rightarrow \bigvee _j \varepsilon _j$.

• T2 $\varepsilon \rightarrow \nu$.

• T3 $\varepsilon \rightarrow \mu$.

• T4 $\varepsilon \rightarrow \mathbf {[\![}{x_i=j}\mathbf {]\!]}$.

• T5 $\mu \wedge \mathbf {[\![}{x_i=j}\mathbf {]\!]} \rightarrow \varepsilon$.

The Tseytin encoding, Tseytin, consists of clauses T1–T5, $\mathcal{T}$, $\lnot \mathcal{F}$ and $\rho$. Therefore, it consists in O(sd) variables and clauses, where s is the MDD size and d the maximum domain size of variables x.

Proposition 3

Let $A = \{ \mathbf {[\![}{x_i = v_i}\mathbf {]\!]} \ \vert \ 1 \le i \le n \}$ be a complete assignment on variables x satisfying the MDD $\mathcal M$. Then, there exists a complete assignment $B \supset A$ over the variables $x, \nu , \varepsilon$ satisfying clauses Tseytin.   $\square$

Proposition 4

Let A be a partial assignment on variables $\{x_i, x_{i+1}, \ldots , x_n\}$, and let $\nu$ be a node of $\mathcal M$ at level i. Assume that there is no completion $A'$ of A satisfying the MDD rooted at $\nu$. Then, unit propagation on clauses Tseytin and A enforces $\lnot \nu$.   $\square$

As a corollary, we can prove:

Theorem 3

Tseytin is correct; i.e., given a complete assignment of the input variables, this encoding finds an inconsistency if and only if the assignment does not satisfy $\mathcal M$. Moreover, it implements consistency.   $\square$

However, Tseytin does not preserve domain consistency.

Example 3

Let us consider the BDD of $x_2 \wedge (x_1 \vee x_3)$, shown in Fig. 1(b). Tseytin, once simplified, generates the following clauses:

$$\begin{array}{llll} \varepsilon _{1,0} \vee \varepsilon _{1,1}, &{} \lnot \nu _2 \vee x_1 \vee \varepsilon _{1,0}, &{} \lnot \varepsilon _{1,0} \vee \lnot x_1, &{} \lnot \varepsilon _{1,0} \vee \nu _2, \\ \lnot \nu _3 \vee \lnot x_1 \vee \varepsilon _{1,1}, &{} \lnot \varepsilon _{1,1} \vee x_1, &{} \lnot \varepsilon _{1,0} \vee \nu _3, &{} \lnot \nu _2 \vee \varepsilon _{2,1}, \\ \lnot \nu _5 \vee \lnot x_2 \vee \varepsilon _{2,1}, &{} \lnot \varepsilon _{2,1} \vee \nu _2, &{} \lnot \varepsilon _{2,1} \vee x_2, &{} \lnot \varepsilon _{2,1} \vee \nu _5, \\ \lnot \nu _3 \vee \varepsilon _{3,1}, &{} \lnot x_2 \vee \varepsilon _{3,1}, &{} \lnot \varepsilon _{3,1} \vee \nu _3, &{} \lnot \varepsilon _{3,1} \vee x_2, \\ \lnot \nu _5 \vee \varepsilon _{5,1}, &{} \lnot x_3 \vee \varepsilon _{5,1}, &{} \lnot \varepsilon _{5,1} \vee \nu _5, &{} \lnot \varepsilon _{5,1} \vee x_3. \\ \end{array} $$

Consider the partial assignment $A = \emptyset$. Notice that $x_2$ is not propagated even though that there is no solution of $\mathcal M$ with $\lnot x_2$. Clause $x_2 \vee \varepsilon _{2,0} \vee \varepsilon _{3,0}$ would propagate $x_2$.    $\square$

Also, Tseytin does not implement unit refutation completeness:

Example 4

Consider the BDD of the constraint ${{\mathrm{XOR}}}(x_1, x_2, x_3, x_4)$ shown in Fig. 2. Node $\nu _2$ represents the constraint ${{\mathrm{XOR}}}(x_2, x_3, x_4)$, and node $\nu _3$ represents $\lnot {{\mathrm{XOR}}}(x_2, x_3, x_4)$. It is clear, therefore, that the partial assignment $B = \{\nu _2, \nu _3\}$ cannot be extended to a complete assignment satisfying $\mathcal M$. However, Tseytin does not find any conflict.   $\square$

3.4 Path-Based Encodings

Under the encodings described in Sects. 3.2 and 3.3, the semantics of variables match the Boolean formula they represent – a node/edge variable is true (in a complete assignment) iff the corresponding formula is true.

In this section, we describe a set of path-based encodings. Like the Tseytin encoding these introduce one variable per node and per edge, but the interpretation of these variables is different. Under a path-based encoding, $\nu$ (or $\varepsilon$) is true iff the path from the root r to $\mathcal{T}$ defined by the selector variables passes through $\nu$ (resp. $\varepsilon$).

Unlike the previous encodings, the variables introduced here cannot be re-used if a sub-formula occurs in multiple constraints. However, we shall see that this interpretation allows us to make much stronger inferences.

A related treatment of path-based encodings of the regular constraint to CNF can be found in Bacchus work in [4] and by Quimper and Walsh in [23] in context of the grammar constraint. Our study provides a complete analysis of such encodings for decision diagrams and introduces a novel encoding with stronger propagation properties.

We generate clauses for each node $\nu$ and connecting it to each of its outgoing edge $\varepsilon _j$ and each of it incoming edges $\delta _j$, as well as clauses for each edge $\varepsilon = {{\mathrm{edge}}}(\nu ,\mu ,\mathbf {[\![}{x_i=j}\mathbf {]\!]})$.

• P1 $\nu \wedge \mathbf {[\![}{x_i=j}\mathbf {]\!]} \rightarrow \varepsilon _j$.

• P2 $\nu \rightarrow \bigvee _j \delta _j$ where $\nu \ne \rho$.

• P3 $\mathbf {[\![}{x_i=j}\mathbf {]\!]} \rightarrow \bigvee \{ \varepsilon ' \ \vert \ \varepsilon ' = {{\mathrm{edge}}}(\nu , \mu , \mathbf {[\![}{x_i=j}\mathbf {]\!]})$ for some $\nu , \mu \in \mathcal M \}$.

• P4 ${{\mathrm{EO}}}(\{ \nu ' \in \mathcal M \ \vert \ {{\mathrm{Level}}}(\nu ') = i \})$.

Clauses P1 enforce that a node on the path puts its outgoing edge on the path. Clauses P2 require each node on the path (except the root) has an incoming edge. Clauses P3 require that each integer value has an edge that supports it. Clauses P4 require that exactly one node on each level is $\top$.

With these clauses, we can define different encodings:

• BasicPath: Clauses P1–P2, T1–T4, $\mathcal{T}$, $\lnot \mathcal{F}$, $\rho$.

• NNFPath: BasicPath and clauses P3.

• LevelPath: BasicPath and clauses P4.

• CompletePath: BasicPath and clauses P3–P4.

All the encodings require O(sd) variables and clauses, where s is the MDD size and d the maximum domain size of variables x.

A complete assignment A over the variables $x_i$ defines a path in $\mathcal M$ in the obvious way. This path is denoted by $\nu _1 = \rho$, $\varepsilon _1$, $\nu _2$, $\varepsilon _2$, $\ldots$ By definition of the MDD, the assignment is compatible with $\mathcal M$ if and only if $\nu _{n+1} = \mathcal{T}$.

A complete assignment B over variables $x_i, \nu , \varepsilon$ is compatible with $\mathcal M$ if

• $A := B \cap (\{ \mathbf {[\![}{x_i=j}\mathbf {]\!]} \ \vert \ 1 \le i \le n, j \in [a_i,b_i]\} \{ \lnot \mathbf {[\![}{x_i=j}\mathbf {]\!]} \ \vert \ 1 \le i \le n, j \in [a_i,b_i]\})$ is compatible with $\mathcal M$.

• $\nu \in B$ iff $\nu = \nu _i$ for some i on the path defined by A.

• $\varepsilon \in B$ iff $\varepsilon = \varepsilon _i$ for some i on the path defined by A.

Proposition 5

Given a complete assignment A on the variables x compatible with $\mathcal M$, there exists a complete assignment $B \supset A$ over the variables $x, \nu , \varepsilon$ satisfying clauses CompletePath.   $\square$

Proposition 6

Let A be a partial assignment on variables x. Let $UP (A)$ be the set of propagated literals with BasicPath. Let $\nu$ be a node of $\mathcal M$, and $\varepsilon$ be an edge of $\mathcal M$. Then:

• $\lnot \nu \in UP (A)\;if\;A\wedge \nu \,\models \,\lnot \mathcal M$.

• $\lnot \varepsilon \in UP (A)\;if\;A\wedge \varepsilon \,\models \,\lnot \mathcal M$.    $\square$

Let us explain the idea behind the proof. If $\nu$ has not been propagated to false, we can create a path from $\rho$ to $\mathcal{T}$ passing through $\nu$, where all the nodes of this path have not been propagated to false. This path will define a completion B satisfying $\mathcal M$ with $\nu \in B$.

To build this path, we start from $\nu$. Since $\lnot \nu \not \in UP (A)$, $\nu$ must have a parent that has also not been propagated to false. This node, again, has a parent that has not been propagated to false, etc. That gives a path from $\rho$ to $\nu$. In the same way, $\nu$ has a child that has not been propagated to false, and this child has a child that has not been propagated to false, etc. That gives a path from $\nu$ to $\mathcal{T}$. Concatenating both paths, we obtain the desired path from $\rho$ to $\mathcal{T}$.

Theorem 4

BasicPath maintains consistency by unit propagation.   $\square$

BasicPath, however, does not maintain domain consistency. For that we need clauses P3.

Example 5

Let us consider the BDD of $x_2 \wedge (x_1 \vee x_3)$, shown at Fig. 1(b). BasicPath, once simplified, generates the following clauses:

$$\begin{array}{llll} x_1 \vee \varepsilon _{1,0}, &{} \lnot x_1 \vee \varepsilon _{1,1}, &{} \lnot \nu _2 \vee x_2, &{} \lnot \nu _3 \vee x_2, \\ \lnot \nu _5 \vee x_3, &{} \varepsilon _{1,0} \vee \varepsilon _{1,1}, &{} \lnot \nu _2 \vee \varepsilon _{2,1}, &{} \lnot \nu _3 \vee \varepsilon _{3,1},\\ \lnot \nu _5 \vee \varepsilon _{5,1}, &{} \lnot \nu _2 \vee \varepsilon _{1,0}, &{} \lnot \nu _3 \vee \varepsilon _{1,1}, &{} \lnot \nu _5 \vee \varepsilon _{2,1}, \\ \varepsilon _{3,1} \vee \varepsilon _{5,1} &{} \lnot \varepsilon _{2,1} \vee \nu _2, &{} \lnot \varepsilon _{3,1} \vee \nu _3, &{} \lnot \varepsilon _{5,1} \vee \nu _5, \\ \lnot \varepsilon _{1,0} \vee \nu _2, &{} \lnot \varepsilon _{1,1} \vee \nu _3, &{} \lnot \varepsilon _{2,1} \vee \nu _5, &{} \lnot \varepsilon _{1,0} \vee \lnot x_1,\\ \lnot \varepsilon _{1,1} \vee x_1, &{} \lnot \varepsilon _{2,1} \vee x_2, &{} \lnot \varepsilon _{3,1} \vee x_2, &{} \lnot \varepsilon _{5,1} \vee x_3. \end{array}$$

Consider the partial assignment $A = \emptyset$. Then, unit propagation does not propagate $x_2$ even though that there is no solution of $\mathcal M$ with $\lnot x_2$. Clause $x_2 \vee \varepsilon _{2,0} \vee \varepsilon _{3,0}$, from P3, would propagate $x_2$.    $\square$

As Corollary of Proposition 5 and Theorem 4, it follows that

Theorem 5

Encodings BasicPath, NNFPath, LevelPath and CompletePath are correct; i.e., given a complete assignment of the input variables, these encodings find an inconsistency if and only if the assignment does not satisfy $\mathcal M$.   $\square$

Theorem 6

NNFPath maintains domain consistency by unit propagation.   $\square$

NNFPath maintains domain consistency with respect to the original variables. However, since a SAT solver will not differentiate between original variables and auxiliary ones, partial assignments, in general, contain both type of variables. And, without clauses P4, the encodings are not propagation complete:

Fig. 2.

BDD of ${{\mathrm{XOR}}}(x_1, x_2, x_3, x_4)$

Example 6

Consider the MDD shown in Fig. 2, representing the constraint ${{\mathrm{XOR}}}(x_1, x_2, x_3, x_4)$. Consider the partial assignment $B = \{ \nu _4, \nu _5 \}$. It is clear that B cannot be extended to a complete assignment satisfying $\mathcal M$, since no path can contain two nodes on the same level. However, NNFPath does not find any conflict.   $\square$

To maintain consistency with respect to all variables, clauses P4 are needed. In that case, we can generalize the previous results to assignments containing auxiliary variables:

Proposition 7

Let B be a partial assignment on all the variables. Let $UP (B)$ be the set of propagated literals with LevelPath. Let $\nu$ be a node of $\mathcal M$, and $\varepsilon$ be an edge of $\mathcal M$. Then:

• 1. $\lnot \nu \in UP (B)\;if\;B \wedge \nu \,\models \,\lnot \mathcal M$.

• 2. $\lnot \varepsilon \in UP (B)\;if\;B \wedge \varepsilon \,\models \,\lnot \mathcal M$.

• 3. $\nu \in UP (B)\;if\;B \wedge \lnot \nu \,\models \,\lnot \mathcal M$.

• 4. $\varepsilon \in UP (B)\;if\;B \wedge \lnot \varepsilon \,\models \,\lnot \mathcal M$.

Theorem 7

LevelPath is unit refutation complete.   $\square$

LevelPath does not maintain domain consistency on all variables, though. Example 5 shows a counterexample. To obtain domain consistency we once more need the clauses P3.

Theorem 8

CompletePath is propagation complete.   $\square$

The path based encoding do have one weakness compared to the Tseytin encoding. Since they require only a single path throught the MDD, we cannot allow different MDD constraints that share a sub-MDD to reuse the same encoding, we need a different copy of the encoding for each constraint. This is not the case for Tseytin encdings where the node variable $\nu$ just represents the truth value of the sub-formula encoded by the MDD rooted at $\nu$. To our knowledge this restriction is not very significant in the CP context. No such sharing exists in any of our benchmarks. The bulk of nodes in an MDD are in the middle and unlikely to be shared. Moreover, separating MDDs per constraint for translation allows us to use different variable orderings for each MDD and thus reduce the number of nodes required. On the other hand, if substantial sharing of nodes among the different MDDs happens then a Tseytin encoding could be beneficial, since it translates this sharing to the CNF level.

The table below shows the sizes and propagation strength of the different encodings. As before, s is the size of the MDD, d is the maximum domain size of variables x and n is the number of variables x. Notice that usually $n \ll s$.

	Minimal	GMinisat	Tseytin	BasicP	NNFP	LevelP	ComplP
Variables	s	s	$s(d+1)$	$s(d+1)$	$s(d+1)$	$s(d+2)$	$s(d+2)$
Clauses	sd	$s(2d+2)$	$s(4d+1)$	$s(4d+2)$	$s(4d+2)$ $+nd$	$s(4d+5)$	$s(4d+5)+nd$
Consisistent
Dom. Consis.
Ref. Compl.
Prop. Compl

4 Encoding NNFs

BDDs are a special case of NNFs and hence NNF encodings provide an alternate approach to encoding BDDs. There is an existing encoding for NNFs given by [20]. When applied correctly to MDDs it results in the NNFPath (hence the name). But care has to be taken in NNF encodings, without the right restrictions on the form of the NNF the encodings are incorrect!

An encoding of an NNF $\mathcal N$ to clauses is given by [20]. Each node $\nu$ is associated with a literal, also called $\nu$. For leaf nodes the literal is just the label of the node. For non-leaf nodes the literal is a new Boolean variable. The clauses we make use of are

• N1 $\nu \rightarrow \nu _1 \vee \cdots \vee \nu _k$ for each $\vee$-node $\nu$ with children $\nu _1, \ldots , \nu _k$

• N2 $\nu \rightarrow \nu _i, 1 \le i \le k$ for each $\wedge$-node $\nu$ with children $\nu _1, \ldots , \nu _k$

• N3 $\nu \rightarrow p_1 \vee \cdots \vee p_m$ for each node $\nu$ with incoming edges from nodes $p_1, \ldots , p_m$.

We consider two encodings: BaseNNF Clauses N1–N2 and $\rho$, and ExtNNF Clauses N1–N3 and $\rho$ as defined in [20].

Theorem 9

Given an NNF $\mathcal N$ then BaseNNF is a correct encoding.    $\square$

Note that this correctness result does not apply to ExtNNF unless the NNF is smooth and decomposable. Jung [20] also claim that ExtNNF enforces domain consistency for decomposable NNFs, but this too is incorrect.

Fig. 3.

NNF for formula (a) $(x \wedge (p \vee q)) \vee (\lnot x \wedge (\lnot p \vee \lnot q))$ and (b) $(\lnot q \wedge p) \vee (p \wedge q)$

Example 7

The NNF shown in Fig. 3(a) is decomposable, deterministic but not smooth (e.g. the two children of node $\nu _4$ do not mention the same variables). The ExtNNF encoding is

$$ \begin{array}{rl@{~~~}l@{~~~}l@{~~~}l@{~~~}l} N1:&{} \nu _1 \rightarrow \nu _2 \vee \nu _3 &{} \nu _4 \rightarrow p \vee q &{} \nu _5 \rightarrow \lnot p \vee \lnot q \\ N2:&{} \nu _2 \rightarrow x &{} \nu _2 \rightarrow \nu _4 &{} \nu _3 \rightarrow \lnot x &{} \nu _3 \rightarrow \nu _5 \\ N3:&{} \nu _2 \rightarrow \nu _1 &{} \nu _3 \rightarrow \nu _1 &{} x \rightarrow \nu _2 &{} \nu _4 \rightarrow \nu _2 &{} \lnot x \rightarrow \nu _3 \\ &{} \nu _5 \rightarrow \nu _3 &{} p \rightarrow \nu _4 &{} q \rightarrow \nu _4 &{} \lnot p \rightarrow \nu _5 &{} \lnot q \rightarrow \nu _5 \\ \rho : &{} \nu _1 &{} \\ \end{array} $$

Consider the assignment $A = \{ x, \lnot q \}$ unit propagation determines $\nu _1, \nu _2, \nu _4, p, \nu _5$, $\nu _3, \lnot x$ and hence a contradiction. This is wrong since there is a model of the NNF $\{ x, \lnot q, p\}$.   $\square$

Example 8

Consider the smooth, decomposable and deterministic NNF for $(\lnot q \wedge p) \vee (p \wedge q)$ shown in Fig. 3(b). Then the clauses of ExtNNF are

$$ \begin{array}{rl@{~~~}l@{~~~}l@{~~~}l@{~~~}l} \rho : &{} \nu _1 &{} N1:&{} \nu _1 \rightarrow \nu _2 \vee \nu _3 \\ N2:&{} \nu _2 \rightarrow \lnot q &{} \nu _2 \rightarrow p &{} \nu _3 \rightarrow p &{} \nu _3 \rightarrow q \\ N3:&{} \nu _2 \rightarrow \nu _1 &{} \nu _3 \rightarrow \nu _1 &{} \lnot q \rightarrow \nu _2 &{} p \rightarrow \nu _2 \vee \nu _3 &{} q \rightarrow \nu _3 \end{array} $$

Any model of the formula must make p true, but unit propagation on these clauses derives only $\nu _1$. What is missing is information that $\lnot p$ does not appear in the NNF. This means p must hold!    $\square$

Table 1. Results on nurse rostering, shift scheduling and pentominoes.

To fix Jung’s encoding we add the following clauses

• N4 $\lnot l$ for each literal l for $vars(\mathcal{N})$ which does not appear in $\mathcal N$.

We denote by FullNNF Clauses N1–N4 and $\rho$.

Theorem 10

Given a smooth decomposable NNF $\mathcal N$ then FullNNF is a correct encoding.

Theorem 11

Given a smooth decomposable NNF $\mathcal N$, then unit propagation on FullNNF enforces domain consistency.    $\square$

It follows that FullNNF is equivalent to NNFPath if applied to MDDs rewritten as NNF. To summarise the results in this section we provide the following table.

	BaseNNF	ExtNNF	FullNNF
Clauses	N1–N2	N1–N3	N1–N4
Correctness	Always	Smooth and Decomposable	Smooth and Decomposable
Domain consistent

5 Experiments

We show results on three benchmarks: nurse rostering, shift scheduling and pentominoes (Nurse, Shift and Pent).³ The MDD encodings are implemented as eager translations of MDDs within the LCG solver Chuffed [9, 10] and compared with a native MDD propagator with learning [17]. We use SAT branching heuristics (VSIDS) and the programmed search as specified in the models (prog). We omit instances not solved by any solver using that search. For each model we show: (#sol) the number of instances solved (SAT and UNSAT for Nurse, to optimality for Shift, all solutions for Pent); (com) the mean solving time in seconds for all benchmarks solved by all solvers (except Minimal); and (all) the mean solving time of all benchmarks using timeout (1200 s) for unsolved instances. The results on the encoding Minimal are omitted for com and for Pent since it does not preserve solution counting. Best results are in bold, and second best are underlined (Table 1).

In case of satisfiable instances of Nurse the results show that encodings do not compete with the native propagator. This is not surprising as the search quickly finds the solutions without being disturbed by the complete CNF model generated by the eager encodings. For the UNSAT instances decompositions and their intermediate literals show their strength and beat the propagator. GenMiniSAT shows best performance for these UNSAT instances with VSIDS. The encodings also have an advantage over the propagator when programmed search is used, but it is unclear which one dominates.

For Shift the results show that when using activity based search and branching takes place on auxiliary variables, the path based approaches are generally superior.

The main advantage of the native propagator is that its explanations are built in a more deterministic fashion and hence tend to be more reusable. Furthermore, since the propagator only generates a fraction of the variables of the eager encoding, the search is less likely get trapped in an unfruitful search space using VSIDS. The difference in results on SAT and UNSAT instances of Nurse clearly indicate that a combination of the propagator and a lazy encoding as in [1] would be a strong approach.

6 Conclusion and Future Work

This paper resulted from discussions that uncovered our own misunderstanding of the strength of decision diagram encodings. We were surprised to discover that the usual BDD encoding is not domain consistent. In this paper we seek to remove this confusion, and demonstrate a wealth of different encoding possibilities, with different properties.

The experimental results show that there is unlikely to be one single best encoding for MDDs, and hence an important direction of future work is to determine when each encoding is best. Possibly a portfolio approach varying over encodings of each constraint is a fruitful and pragmatic technique to solve hard problems in practice.

Another interesting direction of future work is to determine a propagation complete encoding for NNFs. It appears the result may require restricting to Sentential Decision Diagrams [12] a form of NNF with a uniform V-tree.

The literature on CNF encodings focuses on consistencies wrt. primary variables of the constraint, whereas we have shown that consistency on auxiliary variables are worthwhile to look at. Our work concentrated on translations of decision diagrams and we would like to extend this research to other constraints like linear and sequence. State-of-the-art CNF encodings of cardinality are the next candidate for this investigation.

In case of theoretical results, an interesting direction is to establish lower bounds on the size of encodings implementing certain consistencies for concrete constraints. The strong relationship between CNF encodings and monotone circuits established in [5, 19] demonstrates a powerful tool for this purpose.