key: cord-0046702-74nwwx3m
authors: de Colnet, Alexis
title: A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
date: 2020-06-26
journal: Theory and Applications of Satisfiability Testing - SAT 2020
DOI: 10.1007/978-3-030-51825-7_22
sha: e571f2083485f4116c4f65de4edd1c51503a7253
doc_id: 46702
cord_uid: 74nwwx3m

Two major considerations when encoding pseudo-Boolean (PB) constraints into SAT are the size of the encoding and its propagation strength, that is, the guarantee that it has a good behaviour under unit propagation. Several encodings with propagation strength guarantees rely upon prior compilation of the constraints into DNNF (decomposable negation normal form), BDD (binary decision diagram), or some other sub-variants. However it has been shown that there exist PB-constraints whose ordered BDD (OBDD) representations, and thus the inferred CNF encodings, all have exponential size. Since DNNFs are more succinct than OBDDs, preferring encodings via DNNF to avoid size explosion seems a legitimate choice. Yet in this paper, we prove the existence of PB-constraints whose DNNFs all require exponential size.

Pseudo-Boolean (PB) constraints are Boolean functions over 0/1 Boolean variables x 1 , . . . , x n of the form n i=1 w i x i 'op' θ where the w i are integer weights, θ is an integer threshold and 'op' is a comparison operator <, ≤, > or ≥. PBconstraints have been studied extensively under different names (e.g. threshold functions [14] , Knapsack constraints [13] ) due to their omnipresence in many domains of AI and their wide range of practical applications [3, 7, 9, 15, 21] .

One way to handle PB-constraints in a constraint satisfaction problem is to translate them into a CNF formula and feed it to a SAT solver. The general idea is to generate a CNF, possibly introducing auxiliary Boolean variables, whose restriction to variables of the constraint is equivalent to the constraint. Two major considerations here are the size of the CNF encoding and its propagation strength. One wants, on the one hand, to avoid the size of the encoding to explode, and on the other hand, to guarantee a good behaviour of the SAT instance under unit propagation -a technique at the very core of SAT solving. Desired propagation strength properties are, for instance, generalized arc consistency (GAC) [4] or propagation completeness (PC) [6] . Several encodings to CNF follow the same twosteps method: first, each constraint is represented in a compact form such as BDD (Binary Decision Diagram) or DNNF (Decomposable Negation Normal Form).

Second, the compact forms are turned into CNFs using Tseitin or other transformations. The SAT instance is the conjunction of all obtained CNFs. It is worth mentioning that there are GAC encodings of PB-constraints into polynomial size CNFs that do not follow this two-steps method [5] . However no similar result is known for PC encodings. PC encodings are more restrictive that GAC encodings and may be obtained via techniques requiring compilation to DNNF [17] . Thus the first step is a knowledge compilation task.

Knowledge compilation studies different representations for knowledge [10, 19] under the general idea that some representations are more suitable than others when solving specific reasoning problems. One observation that has been made is that the more reasoning tasks can be solved efficiently with particular representations, the larger these representations get in size. In the context of constraint encodings to SAT, the conversion of compiled forms to CNFs does not reduce the size of the SAT instance, therefore it is essential to control the size of the representations obtained by knowledge compilation.

Several representations have been studied with respect to different encoding techniques with the purpose of determining which properties of representations are sufficient to ensure propagation strength [1, 2, 11, 12, 16, 17] . Popular representations in this context are DNNF and BDD and their many variants: deterministic DNNF, smooth DNNF, OBDD. . . As mentioned above, a problem occurring when compiling a constraint into such representations is that exponential space may be required. Most notably, it has been shown in [2, 14] that some PB-constraints can only be represented by OBDDs whose size is exponential in √ n, where n is the number of variables. Our contribution is the proof of the following theorem where we lift the statement from OBDD to DNNF.

There is a class of PB-constraints F such that for any constraint f ∈ F on n 2 variables, any DNNF representation of f has size 2 Ω(n) .

Since DNNFs are exponentially more succinct than OBDDs [10] , our result is a generalisation of the result in [2, 14] . The class F is similar to that used in [2, 14] , actually the only difference is the choice of the threshold for the PB-constraints. Yet, adapting proofs given in [2, 14] for OBDD to DNNF is not straightforward, thus our proof of Theorem 1 bears very little resemblance. It has been shown in [18] that there exist sets of PB-constraints such that the whole set (so a conjunction of PB-constraints) requires exponential size DNNF to represent. Our result is a generalisation to single PB-constraints.

Single Boolean variables are written in plain text (x) while assignments to several variables are written in bold (x). We write x ≤ y when the vector y dominates x element-wise. We write x < y when x ≤ y and x = y. In this framework, a Boolean function f over X is a mapping from {0, 1} n to {0, 1}. f is said to accept an assignment x when f (x) = 1, then x is called a model of f . The function is monotone if for any model x of f , all y ≥ x are models of f as well. The set of models of f is denoted f -1 (1). Given f and g two Boolean functions over X, we write f ≤ g when f -1 (1) ⊆ g -1 (1) . We write f < g when the inclusion is strict.

Pseudo-Boolean Constraints. Pseudo-Boolean (PB) constraints are inequalities the form

where the x i are 0/1 Boolean variables, the w i and θ are integers, and 'op' is one of the comparison operator <, ≤, > or ≥. A PB-constraint is associated with a Boolean function whose models are exactly the assignments to {x 1 , . . . , x n } that satisfy the inequality. For simplicity we directly consider PB-constraints as Boolean functions -although the same function may represent different constraints -while keeping the term "constraints" when referring to them. In this paper, we restrict our attention to PB-constraints where 'op' is ≥ and all weights are positive integers. Note that such PBconstraints are monotone Boolean functions. Given a sequence of positive integer weights W = (w 1 , . . . , w n ) and an integer threshold θ, we define the function w : {0, 1} n → N that maps any assignment to its weight by

With these notations, a PB-constraint over X for a given pair (W, θ) is a Boolean function whose models are exactly the x such that w(x) ≥ θ. Example 1. Let n = 5, W = (1, 2, 3, 4, 5) and θ = 9. The PB-constraint for (W, θ) is the Boolean function whose models are the assignments such that

For notational clarity, given any subset Y ⊆ X and denoting x| Y the restriction of x to variables of Y , we overload w so that w(x| Y ) is the sum of weights activated by variables of Y set to 1 in x.

Decomposable NNF. A circuit in negation normal form (NNF) is a single output Boolean circuit whose inputs are Boolean variables and their complements, and whose gates are fanin-2 AND and OR gates. The size of the circuit is the number of its gates. We say that an NNF is decomposable (DNNF) if for any AND gate, the two sub-circuits rooted at that gate share no input variable, i.e., if x or ¬x is an input of the circuit rooted at the left input of the AND gate, then neither x nor ¬x is an input of the circuit rooted at the right input, and vice versa. A Boolean function f is encoded by a DNNF D if the assignments of variables for which the output of D is 1 (true) are exactly the models of f .

Let X be a finite set of Boolean variables and let Π = (X 1 , X 2 ) be a partition of X (i.e., X 1 ∪ X 2 = X and X 1 ∩ X 2 = ∅). A rectangle r with respect to Π is a Boolean function over X defined as the conjunction of two functions ρ 1 and ρ 2 over X 1 and X 2 respectively. Π is called the partition of r. We say that the partition and the rectangle are balanced when |X|

for any assignment x to X the notations x 1 := x| X1 and x 2 := x| X2 . And for any two assignments x 1 and x 2 to X 1 and X 2 , we note (x 1 , x 2 ) the assignment to X whose restrictions to X 1 and X 2 are x 1 and x 2 . Given f a Boolean function over X, a rectangle cover of f is a disjunction of rectangles over X, possibly with different partitions, equivalent to f . The size of a rectangle cover is the number of its rectangles. A cover is called balanced if all its rectangles are balanced.

Example 2. Going back to Example 1, consider the partition

this partition that accepts only models of the PB-constraint from Example 1. Thus it can be part of a rectangle cover for this constraint.

Any function f has at least one balanced rectangle cover as one can create a balanced rectangle accepting exactly one chosen model of f . We denote by C(f ) the size of the smallest balanced rectangle cover of f . The following result from [8] links C(f ) to the size of any DNNF encoding f . 

The strategy to prove Theorem 1 is to find a PB-constraint f over n variables such that C(f ) is exponential in √ n and then use Theorem 2. We first show that we can restrict our attention to covering particular models of f with rectangles rather than the whole function. In this section X is a set of n Boolean variables and f is a PB-constraint over X. Recall that we only consider constraints of the form n i=1 w i x i ≥ θ where the w i and θ are positive integers. Definition 1. The threshold models of f are the models x such that w(x) = θ.

Threshold models should not be confused with minimal models (or minimals).

For a monotone PB-constraint, a minimal model is such that its sum of weights drops below the threshold if we remove any element from it. Any threshold model is minimal, but not all minimals are threshold models. There even exist constraints with no threshold models (e.g. take even weights and an odd threshold) while there always are minimals for satisfiable constraints. 1, 1, 1, 0), (1, 0, 1, 0, 1) and (0, 1, 1, 0, 1) . The first three are threshold models.

Let f * be the Boolean function whose models are exactly the threshold models of f . In the next lemma, we prove that the smallest rectangle cover of f * has size at most C(f ). Thus, lower bounds on C(f * ) are also lower bounds on C(f ).

Let f * be the Boolean function whose models are exactly the threshold models of f . Then C(f ) ≥ C(f * ).

Proof. Let r := ρ 1 ∧ ρ 2 be a balanced rectangle with r ≤ f and assume r accepts some threshold models. Let Π := (X 1 , X 2 ) be the partition of r. We claim that there exist two integers θ 1 and θ 2 such that θ 1 + θ 2 = θ and, for any threshold model x accepted by r, there is w(x 1 ) = θ 1 and w(x 2 ) = θ 2 . To see this, assume by contradiction that there exists another partition θ = θ 1 + θ 2 of θ such that some other threshold model y with w(y 1 ) = θ 1 and w(y 2 ) = θ 2 is accepted by r. Then either w(x 1 ) + w(y 2 ) < θ or w(y 1 ) + w(x 2 ) < θ, but since (x 1 , y 2 ) and (y 1 , x 2 ) are also models of r, r would accept a non-model of f , which is forbidden. Now let ρ * 1 (resp. ρ * 2 ) be the function whose models are exactly the models of ρ 1 (resp. ρ 2 ) of weight θ 1 (resp. θ 2 ). Then r * := ρ * 1 ∧ ρ * 2 is a balanced rectangle whose models are exactly the threshold models accepted by r.

Now consider a balanced rectangle cover of f of size C(f ). For each rectangle r of the cover, if r accepts no threshold model then discard it, otherwise construct r * . The disjunction of these new rectangles is a balanced rectangle cover of f * of size at most C(f ). Therefore C(f ) ≥ C(f * ).

We define the class of hard PB-constraints for Theorem 1 in this section. Recall that for a hard constraint f , our aim is to find an exponential lower bound on C(f ). We will show, using Lemma 1, that the problem can be reduced to that of covering all maximal matchings of the complete n × n bipartite graph K n,n with rectangles. In this section, X is a set of n 2 Boolean variables. For presentability reasons, assignments to X are written as n × n matrices. Each variable x i,j has the weight w i,j := (2 i + 2 j+n )/2. Define the matrix of weights W := (w i,j : 1 ≤ i, j ≤ n) and the threshold θ := 2 2n − 1. The PB-constraint f for the pair (W, θ) is such that f (x) = 1 if and only if x satisfies 1≤i,j≤n

Constraints of this form constitute the class of hard constraints of Theorem 1. One may find it easier to picture f writing the weights and threshold as binary numbers of 2n bits. Bits of indices 1 to n form the lower part of the number and those of indices n + 1 to 2n form the upper part. The weight w i,j is the binary number where the only bits set to 1 are the ith bit of the lower part and the jth bit of the upper part. Thus when a variable x i,j is set to 1, exactly one bit of value 1 is added to each part of the binary number of the sum.

Assignments to X uniquely encode subgraphs of K n,n . We denote U = {u 1 , . . . , u n } the nodes of the left side and V = {v 1 , . . . , v n } those of the right side of K n,n . The bipartite graph encoded by x is such that there is an edge between the u i and v j if and only if x i,j is set to 1 in x. 

• for any i ∈ [n], there is exactly one k such that x i,k is set to 1 in x, • for any j ∈ [n], there is exactly one k such that x k,j is set to 1 in x.

As the name suggests, the maximal matching assignments are those encoding graphs whose edges form a maximal matching of K n,n (i.e., a maximum cardinality matching). One can also see them as encodings for permutations of [n]. 

For a given x, define var k (x) by var k (x) := {j | x k,j is set to 1 in x} when 1 ≤ k ≤ n and by var k (x) := {i | x i,k−n is set to 1 in x} when n + 1 ≤ k ≤ 2n. var k (x) stores the index of variables in x that directly add 1 to the kth bit of w(x). Note that a maximal matching model is an assignment x such that |var k (x) | = 1 for all k. It is easy to see that maximal matching models are threshold models of f : seeing weights as binary numbers of 2n bits, for every bit of the sum the value 1 is added exactly once, so exactly the first 2n bits of the sum are set to 1, which gives us θ. Note that not all threshold models of f are maximal matching models, for instance the assignment from Example 4 does not encode a maximal matching but one can verify that it is a threshold model. Recall that f * is the function whose models are the threshold models of f . In the next lemmas, we prove that lower bounds on the size of rectangle covers of the maximal matching models are lower bounds on C(f * ), and a fortiori on C(f ).

Let Π := (X 1 , X 2 ) be a partition of X. Let x := (x 1 , x 2 ) and y := (y 1 , y 2 ) be maximal matching assignments. If (x 1 , y 2 ) and (y 1 , x 2 ) both have weight θ := 2 2n − 1 then both are maximal matching assignments.

Proof. It is sufficient to show that |var k (x 1 , y 2 ) | = 1 and |var k (y 1 , x 2 ) | = 1 for all 1 ≤ k ≤ 2n. We prove it for (x 1 , y 2 ) by induction on k. First observe that since |var k (x) | = 1 and |var k (y) | = 1 for all 1 ≤ k ≤ 2n, the only possibilities for |var k (x 1 , y 2 ) | are 0, 1 or 2.

• For the base case k = 1, if |var 1 (x 1 , y 2 ) | is even then the first bit of w(x 1 ) + w(y 2 ) is 0 and the weight of (x 1 , y 2 ) is not θ. So |var 1 (x 1 , y 2 ) | = 1. • For the general case 1 < k ≤ 2n, assume that |var 1 (x 1 , y 2 ) | = · · · = |var k−1 (x 1 , y 2 ) | = 1. So the kth bit of w(x 1 ) + w(y 2 ) depends only on the parity of |var k (x 1 , y 2 ) |: the kth bit is 0 if |var k (x 1 , y 2 ) | is even and 1 otherwise. (x 1 , y 2 ) has weight θ so |var k (x 1 , y 2 ) | = 1.

The argument applies to (y 1 , x 2 ) analogously.

Let f be the PB-constraint (1) and letf be the function whose models are exactly the maximal matching assignments. Then C(f ) ≥ C(f ).

Proof. By Lemma 1, it is sufficient to prove that C(f * ) ≥ C(f ). We already know thatf ≤ f * . Let r := ρ 1 ∧ ρ 2 be a balanced rectangle of partition Π := (X 1 , X 2 ) with r ≤ f * , and assume r accepts some maximal matching assignment. Letρ 1 (resp.ρ 2 ) be the Boolean function over X 1 (resp. X 2 ) whose models are the x 1 (resp. x 2 ) such that there is a maximal matching assignment (x 1 , x 2 ) accepted by r. We claim that the balanced rectangler :=ρ 1 ∧ρ 2 accepts exactly the maximal matching models of r. On the one hand, it is clear that all maximal matching models of r are models ofr. On the other hand, all models ofr are threshold models of the form (x 1 , y 2 ), where (x 1 , x 2 ) and (y 1 , y 2 ) encode maximal matchings, so by Lemma 2,r accepts only maximal matching models of r. Now consider a balanced rectangle cover of f * of size C(f * ). For each rectangle r of the cover, if r accepts no maximal matching assignment then discard it, otherwise constructr. The disjunction of these new rectangles is a balanced rectangle cover off of size at most C(f * ). Therefore C(f * ) ≥ C(f ).

Theorem 1. There is a class of PB-constraints F such that for any constraint f ∈ F on n 2 variables, any DNNF encoding f has size 2 Ω(n) .

F is the class of constraints defined in (1). Thanks to Theorem 2 and Lemma 3, the proof boils down to finding exponential lower bounds on C(f ), wheref is the Boolean function on n 2 variables whose models encode exactly the maximal matchings of K n,n (or equivalently, the permutations of [n]).f has n! models. The idea is now to prove that rectangles coveringf must be relatively small, so that covering the whole function requires many of them. 

where we have used a b ≥ (a/b) b and 3/2 ≥ √ 2. Using Lemma 3 we get that C(f ) ≥ C(f ) ≥ 2 Ω(n) . Theorem 2 allows us to conclude. All that is left is to prove Lemma 4.

Let r := ρ 1 ∧ ρ 2 and Π := (X 1 , X 2 ). Recall that U := {u 1 , . . . , u n } and V := {v 1 , . . . , v n } are the nodes from the left and right part of K n,n respectively. Define U 1 := {u i | there exists x i,l ∈ X 1 such that a model of ρ 1 has x i,l set to 1} and V 1 := {v j | there exists x l,j ∈ X 1 such that a model of ρ 1 has x l,j set to 1}. Define U 2 and V 2 analogously (this time using X 2 and ρ 2 ). Figure 1 illustrates the construction of these sets: Fig. 1a shows a partition Π of the edges of K 4,4 (full edges in X 1 , dotted edges in X 2 ) and Fig. 1b shows the contribution of a model of r to U 1 , V 1 , U 2 , and V 2 after partition according to Π.

Models of ρ 1 are clearly matchings of K n,n . Actually they are matchings between U 1 and V 1 by construction of these sets. We claim that they are maximal. To verify this, observe that U 1 ∩ U 2 = ∅ and V 1 ∩ V 2 = ∅ since otherwise r has a model that is not a matching. Thus if ρ 1 were to accept a non-maximal matching between U 1 and V 1 then r would accept a non-maximal matching between U and V . So ρ 1 accepts only maximal matchings between U 1 and V 1 , consequently |U 1 | = |V 1 |. The argument applies symmetrically for V 2 and U 2 . We note k := |U 1 |. It stands that U 1 ∪ U 2 = U and V 1 ∪ V 2 = V as otherwise r accepts matchings that are not maximal. So |U 2 | = |V 2 | = n − k. We now have |ρ -1 1 (1)| ≤ k! and |ρ -1 2 (1)| ≤ (n − k)!, leading to |r -1 (1)| ≤ k!(n − k)! = n!/ n k . Up to k 2 edges may be used to build matchings between U 1 and V 1 . Since r is balanced we obtain k 2 ≤ 2n 2 /3. Applying the same argument to U 2 and V 2 gives us (n − k) 2 ≤ 2n 2 /3, so n(1 − 2/3) ≤ k ≤ n 2/3. Finally, the function k → n!/ n k , when restricted to some interval [[n(1−α), αn]], reaches its maximum at k = αn, hence the upper bound |r -1 (1)| ≤ n!/ n n √ 2/3 .

On CNF encodings of decision diagrams

A new look at BDDs for pseudo-boolean constraints

Generic ILP versus specialized 0-1 ILP: an update

GAC via unit propagation

New encodings of pseudo-boolean constraints into CNF

Knowledge compilation with empowerment

Optimal cell flipping to minimize channel density in VLSI design and pseudo-boolean optimization

Knowledge compilation meets communication complexity

Deciding CLU logic formulas via boolean and pseudo-boolean encodings

A knowledge compilation map

Translating pseudo-boolean constraints into SAT

Explaining propagators for s-DNNF circuits

An FPTAS for #Knapsack and related counting problems

Size of ordered binary decision diagrams representing threshold functions

Some network flow problems solved with pseudo-boolean programming

Two encodings of DNNF theories

Propagation complete encodings of smooth DNNF theories

Pseudo-boolean constraints from a knowledge representation perspective

Compile! In: AAAI Conference on Artificial Intelligence, AAAI

Revisiting graph width measures for CNF-encodings

Optimal test generation in combinational networks by pseudoboolean programming

Branching programs and binary decision diagrams

Acknowledgments. This work has been partly supported by the PING/ACK project of the French National Agency for Research (ANR-18-CE40-0011).