Optimal Base Encodings for Pseudo-Boolean Constraints

Optimal Base Encodings for Pseudo-Boolean Constraints? Michael Codish1 , Yoav Fekete1 , Carsten Fuhs2 , and Peter Schneider-Kamp3

arXiv:1007.4935v1 [cs.DM] 28 Jul 2010

1

Department of Computer Science, Ben Gurion University of the Negev, Israel [email protected] 2 LuFG Informatik 2, RWTH Aachen University, Germany [email protected] 3 IMADA, University of Southern Denmark, Denmark [email protected]

Abstract. This paper formalizes the optimal base problem, presents an algorithm to solve it, and describes its application to the encoding of Pseudo-Boolean constraints to SAT. We demonstrate the impact of integrating our algorithm within the Pseudo-Boolean constraint solver MiniSat+ . Experimentation indicates that our algorithm scales to consider bases involving numbers up to 1,000,000, improving on the restriction in MiniSat+ to prime numbers up to 17. We show that, while for many examples primes up to 17 do suffice, encoding with respect to arbitrary bases improves the subsequent SAT solving time considerably.

1

Introduction

The optimal base problem is all about finding an efficient representation for a given collection of positive integers. One measure for the efficiency of a representation is the sum of the digits of the numbers. Consider for example the decimal numbers S = {16, 30, 54, 60}. The sum of their digits is 25. Taking binary representation we have S(2) = {10000, 11110, 110110, 111100} and the sum of digits is 13, which is smaller. Taking ternary representation gives S(3) = {121, 1010, 2000, 2020} with an even smaller sum of digits, 12. Considering the mixed radix base B = h3, 5, 2, 2i, the numbers are represented as S(B) = {101, 1000, 1130, 10000} and the sum of the digits is 9. The optimal base problem is to find a (possibly mixed radix) base for a given sequence of numbers to minimize the size of the representation of the numbers. When measuring size as “sum of digits”, the base B is indeed optimal for the numbers of S. In this paper we present the optimal base problem and illustrate why it is relevant to the encoding of Pseudo-Boolean constraints to SAT. We present also an algorithm and show that our implementation is superior to current implementations. Pseudo-Boolean constraints take the form a1 x1 +a2 x2 +· · ·+an xn ≥ k, where a1 , . . . , an are integer coefficients, x1 , . . . , xn are Boolean literals (i.e., Boolean variables or their negation), and k is an integer. We assume that constraints are ?

Supported by GIF grant 966-116.6 and the Danish Natural Science Research Council.

in Pseudo-Boolean normal form [3] so that the coefficients ai and k are always positive and Boolean variables occur at most once in a1 x1 + a2 x2 + · · · + an xn . Pseudo-Boolean constraints are well studied and arise in many different contexts, for example in verification [6] and in operations research [5]. Typically we are interested in the satisfiability of a conjunction of Pseudo-Boolean constraints. Since 2005 there is a series of Pseudo-Boolean Evaluations [9] affiliated to the SAT conference which aim to assess the state of the art in the field of PseudoBoolean solvers. We adopt these competition problems as a benchmark for the techniques proposed in this paper. Pseudo-Boolean constraint satisfaction problems are often reduced to SAT. There are many works that describe techniques to encode these constraints to propositional formulas [1, 2, 8]. The Pseudo-Boolean solver MiniSat+ ([8], cf. http://minisat.se) chooses between three techniques to generate SAT encodings for Pseudo-Boolean constraints. These convert the constraint to: (a) a BDD structure, (b) a network of sorters, and (c) a network of (binary) adders. The network of adders is the most concise encoding, but it has the weakest propagation properties and often leads to higher SAT solving times than the BDD based encoding which, on the other hand, generates the largest encoding. The encoding based on sorting networks is often the one applied and is the one we consider in this paper. To demonstrate how sorters can be used to translate Pseudo-Boolean constraints, consider the constraint x1 + x2 + x3 + 2x4 + 3x5 ≥ 4 where x5 y1 = 1 the sum of the coefficients is 8. The figure on the x5 y2 = 1 right illustrates an 8 × 8 sorter where x1 , x2 , x3 are x5 y3 = 1 x4 y4 = 1 each fed into a single input, x4 into two of the inx4 y5 puts, and x5 into three of the inputs. To assert x3 y6 x2 y7 the constraint, one first represents the sorting netx1 y8 work as a Boolean formula and then asserts that the top four outputs (i.e., y1 , . . . , y4 ) are true (take value 1). This suffices because the outputs contain the same values as the inputs, but in sorted order. But what happens if the coefficients in a constraint are larger than in this example? How should we encode a constraint of the form 16x1 + 30x2 + 54x3 + 30x4 + 60x5 ≥ 87? How should we handle very large coefficients (larger than 1,000,000)? To this end, the authors in [8] generalize the above idea and propose a method to decompose the constraint into a number of interconnected sorting networks. Each sorter represents a digit in a mixed radix base. This construction is governed by the choice of a suitable mixed radix base and the objective is to find a base which minimizes the size of the sorting networks. This is where we find a variation on the optimal base problem, as the size of the networks is closely related to the sum of the digits for representing the coefficients of the constraint in the selected base. In MiniSat+ the search for an optimal base is performed using a brute force algorithm and the resulting base is constructed from prime numbers up to 17. 2

The starting point for this paper is the following remark from [8] (Footnote 8) which states: This is an ad-hoc solution that should be improved in the future. Finding the optimal base is a challenging optimization problem in its own right. In this paper we take the challenge and present an algorithm which scales to find an optimal base consisting of elements (primes or non-primes) with values up to 1,000,000. We illustrate that in many cases finding a better base leads also to better SAT solving time. Section 2 formalizes the optimal base problem. Section 3 illustrates how MiniSat+ , starting from a mixed radix base, encodes a Pseudo-Boolean constraint to SAT. Section 4 shows how to find a base for which the encoding is optimal. Sections 5– 7 introduce our algorithm in three steps: Heuristic pruning, best-first branch and bound, and base abstraction. Sections 8 and 9 present an experimental evaluation and some related work, and Section 10 concludes.

2

Optimal Base Problems

In the classic base r radix system, positive integers are represented as sequences of digits d = hd0 , . . . , dk i (we denote the least significant digit as d0 ) where for each digit 0 ≤ di < r and the most significant digit, dk > 0. The integer value associated with d is v = d0 + d1 r + d2 r2 + · · · + dk rk . A mixed radix system is a generalization where a base is a radix sequence hr0 , r1 , r2 , . . .i of integers, ri > 1 and the sequence of digits d corresponds to the integer value v = d0 + d1 r0 + d2 r0 r1 + · · · + dk

k−1 Y

ri

(1)

i=0

where 0 ≤ di < ri for each digit and also dk > 0. If a base consists of prime numbers only, we say that it is a prime base. We also consider finite mixed radix bases of the form B = hr0 , r1 , r2 , . . . , rk−1 i. So numbers always have k + 1 digits (possibly padded with zeroes) and are of the form d = hd0 , . . . , dk i where 0 ≤ di < ri for each digit i < k and dk ≥ 0. For a (finite or infinite) base B = hr0 , r1 , r2 , . . .i we denote the sequence ˜ where w0 = 1 and for i ≥ 0, wi+1 = wi ri . These are the hw0 , w1 , w2 , . . .i by B “weights” contributed by the corresponding digits in a sequence d representing a number in the base. We denote by v(B) = hd0 , d1 , d2 , . . . , dk i the representation of a number v in base B. For any (finite or infinite) sequence S, we denote the ith element by Si , the length by |S|, Q the maximal element by max(S), and the multiplication of the elements by S. For a sequence S of positive integers with |S| = n and a finite base B with |B| = k, we denote the n × (k + 1) matrix of digits of elements from S in base B as S(B) . Namely, the element aij of this matrix is the j th digit of the ith number. Definition 1 (sum digits). Let S be a sequence of positive integers and B a base. The sum of the digits of the numbers from S in base B is denoted sum digits(S(B) ). 3

Example 2. The usual binary “base 2” and ternary “base 3” are represented as the infinite sequences B1 = h2, 2, 2, . . .i and B2 = h3, 3, 3, . . .i. The finite sequence B3 = h3, 5, 2, 2i and the empty sequence B4 = h i are also bases. The empty base is often called the “unary base” (every number in this base has a single digit). Let S = {16, 30, 54, 60}. Then, sum digits(S(B1 ) ) = 13, sum digits(S(B2 ) ) = 12, sum digits(S(B3 ) ) = 9, and sum digits(S(B4 ) ) = 160. Let S be a sequence of positive integers. A cost function for S is a function cost S which associates bases with natural numbers. For now we will assume a cost function cost S (B) = sum digits(S(B) ). In this paper we are concerned with the following optimal base problem. Definition 3 (optimal base problem). Let S be a finite non-empty sequence of positive integers and cost S a cost function. We say that a base B is an optimal base for S with respect to cost S , if for all bases B 0 , cost S (B) ≤ cost S (B 0 ). The corresponding optimal base problem is to find an optimal base B for S. The following lemma implies that for all practical purposes we can restrict attention to finite bases. We need first a definition. Definition 4 (redundant base). Let S be a sequence of positive integers and B a base. We say that B is redundant for S if there exists an index i such that for all v ∈ S, and all i ≤ j, the j th digit in v(B) is zero. Lemma 5. To solve the optimal base problem we can restrict attention to nonredundant (and hence finite) bases. Moreover, when the cost function is sum digits, we can restrict attention to bases involving prime numbers only. Lemma 6. To solve the optimal base problem with respect to the sum digits cost function we can restrict attention to prime bases. How hard is it to solve an instance of the optimal base problem? The following lemma provides an upper bound on the size of the search space. This provides a bound for a brute force pseudo-polynomial time algorithm as the number of bases for a finite sequence S of positive integers is polynomial in max(S). Lemma 7. Let S be a set of positive integers with m = max(S). Then the number of non-redundant bases for S is less than m1+ρ where ρ = ζ −1 (2) ≈ 1.73 and where ζ is the Riemann zeta function.

3

Encoding Pseudo-Boolean Constraints

This section illustrates the relation between optimal base problems and the encoding of Pseudo-Boolean constraints. We demonstrate the construction underlying the sorter based encoding of Pseudo-Boolean constraints applied in MiniSat+ [8]. The construction is governed by the choice of a mixed radix base, 4

the optimal selection of which is the topic of this paper. For the experimentation presented later in this paper and to demonstrate our contribution, we apply the MiniSat+ tool “as is”, but with the exception that we introduce the implementation of our algorithm to determine the underlying optimal base with respect to which the construction is then performed (by MiniSat+ ). The construction sets up a series of sorting networks which encode the digits (in base B) of the sum of the terms on the left side of a constraint ψ = a1 x1 + a2 x2 + · · · + an xn ≥ k. These digits are then compared with k(B) from the right side in the encoding to SAT. We demonstrate the construction, step by step, through an example. Encoding the constraint as a CNF formula is then straightforward. For further details the reader should consult [8]. Consider for this section the base B = h2, 3, 3i and the Pseudo-Boolean constraint ψ = 2x1 + 2x2 + 2x3 + 2x4 + 5x5 + 18x6 ≥ 23. Step one - representation in base: The coefficients of ψ form a sequence A(ψ) and their representation in base B forms an 6 × 4 matrix, A(ψ)(B) .     2 0100 2 0 1 0 0 2(B) = h0, 1, 0, 0i 0 1 0 0  2   5(B) = h1, 2, 0, 0i A(ψ) =  A(ψ)(B) =   2 0 1 0 0 5 1 2 0 0 18(B) = h0, 0, 0, 1i 18

0001

Step two - counting: Numbers in base B = h2, 3, 3i have 4 digits and corre˜ = h1, 2, 6, 18i. To add the terms on the left side of ψ, we spond to the weights B set up a series of four sorting networks to sum up individually the digits from the sum corresponding to each weight. To this end observe that   0 1 0 0 ! 0 1 0 0 1
0 1 0 0 2  2x1 + 2x2 + 2x3 + 2x4 + 5x5 + 18x6 = x1 x2 x3 x4 x5 x6 ×  0 1 0 0× 6 1 2 0 0 0 0 0 1

18

Hence, the series of sorting networks and their inputs are constructed like this:

x5

count 10 s

x1 x2 x3 x4 x5 x5

x6

count 20 s

count 60 s

count 180 s

Step three - converting to base: To view the outputs of these 4 sorting networks as the digits of a number in base B = h2, 3, 3i, we need to encode also the “carry” operation from each digit position to the next. The first 3 sorting networks must represent unary numbers less than h2, 3, 3i respectively. In our example the single violation to this restriction is on the second network, which has 6 outputs. To this end we add two components to the encoding: (1) each third output of the second network is fed into the third network as an additional 5

input (a carry); and (2) additional clauses are added to encode that the output of the second network is to be considered modulo 3. We call these additional clauses a normalizer. Denoting the outputs from the second sorting network by Y = hy1 , . . . , y6 i, we convey y3 and y6 as inputs to the third sorting network. The normalizer defines two outputs R = hr1 , r2 i and introduces clauses specifying that the (unary) value of R equals the (unary) value of Y mod 3. x1 x2 x3 x4 x5 x5

x5

0

count 1 s

y6 y5 y4 y3 y2 y1

y6 y3 r1 r2

0

count 2 s

x6

0

count 6 s

count 180 s

Step four - comparison: The outputs from these four units now specify a number in base B, each digit represented in unary notation. This number is now compared (via an encoding of the lexicographic order) to 23(B) (the value from the right-hand side of ψ).

4

Optimal Pseudo-Boolean Constraint Networks

We now return to the objective of this paper: For a given Pseudo-Boolean constraint, how can we choose a mixed radix base with respect to which the encoding of the constraint via sorting networks will be of minimal size? To this end, Section 2 introduces the optimal base problem. If we take sum digits as a cost function, then solving the optimal base problem for the coefficients of a constraint provides a base which minimizes the number of inputs (originating from the coefficients) to the sorting networks. In [8], the authors propose to approximate the size of the encoding in terms of the total number of inputs to the sorting networks of the construction, including the carry bits introduced along the way. To capture this formally, we define a cost function sum carry which specifies the total number of inputs to the sorting networks of the encoding. We then solve the optimal base problem with respect to this cost function. Definition 8 (cost function: sum carry). Let S be a non-empty sequence of n positive integers, B be a base of length k, and S(B) = (aij ) the corresponding n × (k + 1) matrix of digits. The “sum of digits with carry” cost function is Pk+1 defined by sum carry(S(B) ) = j=1 inputsB S (j) where

inputsB S (j)

(P n aij = Pi=1 n B i=1 aij + div(inputsS (j − 1), B(j − 2)) 6

if j = 1 if j > 1

(2)

Example 9. Consider again the Pseudo-Boolean constraint ψ = 2x1 + 2x2 + 2x3 + 2x4 + 5x5 + 18x  6 ≥ 23 with coefficients S = 2, 2, 2, 2, 5, 18 and base B = h2, 3, 3i from Section 3 and consider also the base B 0 = h2, 9i.

x1 x2 x3 x4 x5 x5

x5

count 10 s

x6

count 20 s

count 180 s

First observe that sum digits(S(B) ) = sum digits(S(B 0 ) ) = 8. So, the sum digits cost function ranks the two bases B and B 0 as equal. On the other hand, the sum carry cost function ranks B 0 as superior to B because sum carry(S(B) ) = 10 and sum carry(S(B 0 ) ) = 8. Indeed the network of sorters obtained with respect to B 0 is smaller (and no normalizers are required). We consider an additional cost function. The odd-even sorting network [4] applied in MiniSat+ leads to an encoding with O(n log2 n) clauses. A better approximation on the size of the construction is obtained with the cost function which estimates the number of clauses that encode the comparators of the sorting networks. Definition 10 (cost function: num comparators). Let S and B be as in Definition 8 and inputsj as in Equation (2). Then, num comparators(S(B) )=

k+1 X

f (inputsB S (j))

j=1

where f (x)=x · max((dlog2 xe)2 , 1). Example 11. Consider a constraint with coefficients S = bases B = h3, 2, 2i and B 0 = h3, 2i. We have



3, 6, 9, 17



and two

sum carry(S(B) ) = sum carry(S(B 0 ) ) = 10. So, sum carry ranks the two bases B and B 0 as equal. However, num comparators ranks B as preferable, and indeed the total size of the sorting networks when using B is smaller.

5

Optimal Base Search I: Heuristic Pruning

This section introduces a simple, heuristic-based, depth-first, tree search algorithm to solve the optimal base problem. The algorithm itself is very similar to the brute force algorithm applied in MiniSat+ . Our contribution is to introduce a heuristic function and to identify early on branches in the search tree which can be pruned. The resulting algorithm provides the basis for the further improvements introduced in Sections 6 and 7. We first formalize the search space. The set of bases that must be considered when seeking an optimal base for a sequence S is described as a tree. Algorithms will then generate/traverse this tree. 7

Definition 12 (base domain). Let S be a non-empty sequence of positive integers. Q base domain for S, denoted by Base(S), is the tree with nodes  The V = B B ≤ max(S) , with root h i (the empty base), and with an edge from node B ∈ V to node B 0 ∈ V if and only if B 0 is obtained from B by concatenating to it an integer value greater than 1. The prime base domain for S is the restriction of Base(S) to prime bases and denoted Base p (S). The `-bounded (prime) base domain for S is the restriction of Base(S) (Base p (S)) to bases containing elements no larger than ` and denoted Base` (S) (Base `p (S)). The algorithm applied in MiniSat+ to find an optimal base for a sequence of integers S is a straightforward depth-first traversal of Base 17 p (S) identifying the node with the optimal value for the cost function cost S (B) = sum carry(S(B) ). To improve this algorithm we apply a pruning technique which during tree traversal identifies a node B for which all descendants are guaranteed to be less optimal than the best base already identified. The subtree rooted at B may be pruned. We need first a definition. Definition 13 (base extension, partial cost, and admissible heuristic). Let S be a sequence of positive integers and let B and B 0 be finite (prime) bases. We say that: (1) B 0 extends B, denoted B 0  B, if B is a prefix of B 0 , (2) ∂cost S is a partial cost function if ∀B 0  B. cost S (B 0 ) ≥ ∂cost S (B), and (3) hS is an admissible heuristic function for cost S and ∂cost S if ∀B 0  B. cost S (B 0 ) ≥ ∂cost S (B 0 ) + hS (B 0 ) ≥ ∂cost S (B) + hS (B). The intuition is that ∂cost S (B) signifies a part of the cost of B which will be a part of the cost of any extension of B, and that hS (B) is an under-approximation on the additional cost of extending B (in any way) given the partial cost of B. The next lemma provides the basis for heuristic pruning using the two cost functions introduced above. Lemma 14. The following definitions (employed in our search algorithm) provide two alternative admissible heuristics for the cases when: Pn 1. cost S (B) = sum carry(S(B) ), ∂cost S (B) = sum carry(S(B) ) − i=1 ai(k+1) where |S| = n, |B| = k, and S(B) = (aij ) is an n × (k + 1) matrix obtained when representing the elements of S in B. P  k B 2. cost S (B) = num comparators(S(B) ), ∂cost S (B) = j=1 f (inputsS (j)) + 2 B f (div(inputsB S (k), b)) where f (x) = x · max((dlog2 xe) , 1) and inputsS (j) is defined in Equation (2).  Q In both settings we take hS (B) = x ∈ S x ≥ B .

The algorithm is now stated as Figure 1. Let S be a non-empty sequence of positive integers, max(S) = m, and s be the number of distinct numbers in S. Then our implementation of this algorithm has space complexity O(log(m)) which is the maximum depth of the recursion. Reasoning with Lemma 7, the search space is bounded by O(m2.73 ) bases. Each base evaluation requires O(s) (as it uses the cost of the base it extended) and therefore, total runtime is in O(s ∗ m2.73 ). By s ≤ m we can conclude that runtime is bounded by O(m3.73 ). 8

Input: non-empty number sequence S 1. Initialize a variable bestB to the finite binary base h2, . . . , 2i of size blog2 (max(S))c. This variable will always denote the best base from those encountered so far (and the initial finite binary base). 2. Apply a depth-first tree construction/traversal. When visiting at a node B, for the next, yetQ unconsidered, child B 0 extending B with a (prime) integer value p such that p × B ≤ max(S), perform two actions: (a) if cost S (B 0 ) < cost S (bestB) then update bestB = B 0 ; and (b) if ∂cost S (B 0 ) + hS (B 0 ) ≥ cost S (bestB) then prune the subtree rooted at B 0 from the search Output: bestB is the optimal base for S. Fig. 1. Algorithm #1: searching for an optimal base

6

Optimal Base Search II: Branch and Bound

In this section we further improve the search algorithm for an optimal base. The data structure for representing the search space is the same as before: a tree structure of potential bases for a non-empty sequence of positive integers S. The search algorithm is, as before, a traversal of the search space using the same partial cost and heuristic functions as before to prune the tree. The difference is that instead of a depth first search, we maintain a priority queue of nodes that still need to be expanded in the traversal and apply a best-first, branch and bound search strategy. Figure 2 illustrates our enhanced search algorithm. We call it BF-B&B (bestfirst, branch and bound). We assume the same cost S , ∂cost S , and hS functions as in the previous section. The input to the algorithm is a multiset of integers S. The output is an optimal base. The abstract data type base has two operations extenders() and extend(int). For a base B and an integer p, B.extend(p) is the base obtained by extending B by p, and B.extenders() is the set of integer values by which B can be extended. The definition of this operation depends on the context: limited to primes, limited by an upper bound, or limited only by the fact that the base product is no greater than max(S). The abstract data type priority queue has operations popMin(), peek() (peeks at the minimal entry) and push(base). Its elements are bases prioritized by the sum of ∂cost S and hS . On line /*1*/ in the figure, we initialize the variable bestB to a finite binary base of size blog2 (max(S))c (same as in Figure 1). On line /*2*/ we initialize the queue to contain the root of the search space (the empty base). As long as there are still nodes to be expanded in the queue that are potentially interesting (line /*3*/), we select (at line /*4*/) the best candidate base B from the frontier of the tree in construction for further expansion. Now the search tree is expanded for each of the relevant integers (calculated at line /*5*/). For each child newB of B (line /*6*/), we check if pruning at newB should occur (line /*7*/) and if not 9

base findBase(multiset S) /*1*/ base bestB = h2, 2, ..., 2i; /*2*/ priority queue Q = h i ; /*3*/ while (Q 6= {} && ∂cost S (Q.peek())+hS (Q.peek()) < cost S (bestB)) /*4*/ base B = Q.popMin(); /*5*/ foreach (p ∈ B.extenders()) /*6*/ base newB = B.extend(p); /*7*/ if (∂cost S (newB) + hS (newB) ≤ cost S (bestB)) { Q.push(newB); /*9*/ if (cost S (newB) < cost S (bestB)) bestB = newB; } /*10*/ return bestB; Fig. 2. Algorithm BF-B&B: best-first, branch and bound base findBase(multiset S) /*1*/ base bestB = h2, 2...2i;  /*2*/ priority queue Q = 1 ; /*3*/ hash H; H[1] = h i; /*4*/ while (Q 6= {} && ∂cost S (H[Q.peek()])+hS (H[Q.peek()]) < cost S (bestB)) /*5*/ base B = H[Q.popMin()]; /*6*/ foreach (p ∈ B.extenders()) /*7*/ base newB = B.extend(p); /*8*/ if (∂cost S (newB) + hS (newB) ≤ cost S (bestB)) /*9*/ if (cost bestB = newB; Q QS (newB) < cost S (bestB)) Q /*10*/ if (H[ newB] = ⊥) {H[ newB] = newB; Q.push( newB);} Q Q /*11*/ elseif (∂cost S (H[ newB]) > ∂cost S (newB)) H[ newB] = newB; /*12*/ return bestB; Fig. 3. Algorithm BNB: best-first, branch and bound, with hash table

we check if a better bound has been found (line /*9*/) Finally, when the loop terminates, we have found the optimal base and return it (line /*10*/).

7

Optimal Base Search III: Search Modulo Product

In this section we observe a Property 1 of bases in the search space which enables usQto improve Q the search algorithm: Consider two bases B1 and B2 such that B1 = B2 and such that ∂cost S (B1 ) ≤ ∂cost S (B2 ). Then for any extension of B1 and of B2 by the same sequence C, cost S (B1 C) ≤ cost S (B2 C) and ∂cost S (B1 ) + hS (B1 ) ≤ ∂cost S (B2 ) + hS (B2 ). In particular, if one of those two bases might be extended to an optimal base, then we can always use B1 . A direct implication is that when maintaining the frontier of the search space as a priority queue, we only need one representative of the class of bases which have the same product (the one with the minimal cost). A second Property 2 is more subtle and true for any cost function that has the first property: Assume that in the algorithm described as Figure 2 we at some stage remove a base B1 from the priority Q queue.QThis implies that if in the future we encounter any base B2 such that B1 = B2 , then we can be sure 10

that cost S (B1 ) ≤ cost S (B2 ) and immediately prune the search tree from B2 . A direct implication is that we can now provide a tighter bound on the complexity of the search algorithm. Theorem 15. The modulo product algorithm provides an optimal base for any cost function which satisfies Property 1. We now present our final algorithm in Figure 3. To control the search strategy we use, as before, a priority queue. But now, instead of maintaining a queue of nodes (bases), we maintain a queue of node products, never introducing the same product twice. Each queue element (an integer value) is associated via a hash table to the best base which has that product that was encountered so far in the search. Initially, the queue contains the value 1, and the hash table associates it with the empty base and is undefined for all other values. The while loop (line /*4*/) in Figure 3 is similar to the loop in Figure 2, except that now we view bases on the queue via the hash table (also on line /*5*/). When processing each new candidate base (in the main loop), as before we consider: if to prune (line /*8*/), and if to update the variable bestB (line /*9*/). Now we also consider if to update the corresponding values on the hash table. One subtlety is that we expect the priority queue to “reorder” each time we update the hash table. The analysis of this algorithm involves 2 parts. First count the total number of queue operations. In the worst case the queue contains m = max(S) entities. The cost per (Fibonacci) queue operation is log m and hence for the queue operations we have O(m log m). The second part is to count the number of bases evaluated during the entire search. Note that we extend only bases which we extract from the queue and in the worst case we can extract one representative for each class of bases with the same product. Let k be the product of a class representative. Then any base B with product k has at most m/k integers which extend it to a non-redundant base. So in total we have O(

m X

k=1

m/k) = O(m

m X

1/k) = O(m ∗ log(m))

k=1

Let s be the number of different integers in S. Then each base evaluation costs O(s) and in total we get O(m ∗ log(m)) + O(m ∗ log(m) ∗ s) ≤ O(m2 ∗ log(m)). Restricting the extenders to be prime numbers yields O(m2 ∗ log(log(m))) (proof in the appendix).

8

Experiments

We implemented our algorithm as an extension to MiniSat+ [8]. All experiments are performed on a Quad-Opteron 848 at 2.2 GHz, 16 GB RAM, running Linux. The reader is invited to experiment with our implementation on our web 11

interface.4 Here one can enter either an optimal base problem (i.e., a sequence of positive integers) or a set of Pseudo-Boolean constraints to obtain optimal bases for the different settings described in the paper (algorithm, cost function, maximal prime, use non-primes). Our benchmark suite originates from 1945 Pseudo-Boolean Evaluation [9] instances from the years 2006–2009 containing a total of 74,442,661 individual Pseudo-Boolean constraints. After normalizing and removing trivial constraints we are left with 115,891 different optimal base problems.

Experiment 1: Search Time Our first experiment focuses on the search for an optimal base. We compare the search times in four configurations: M17 is the MiniSat+ tool searching for bases consisting of primes up to 17, and three configurations, BNB’1,000,000, BNB’10,000, and BNB’17 of the algorithm from Figure 3 where base elements are restricted to be prime numbers less than 1,000,000, less than 10,000 and less than or equal to 17. In all four configurations we take the sum carry cost function. The results for Experiment 1 are summarized in Figure 4, which is obtained as follows. Each run results in a pair specifying the search time in milliseconds (time-out is 10 minutes) and the maximal number M in the given optimal base problem (maximal value is 231 −1). These points are clustered, and for each value dlogk M e we depict the average runtime in the graph. The value k = 1.975 is chosen to minimize the standard deviation from these averages. The configuration M17 times out on 28 problems. The other configurations have maximal runtimes of 350 seconds, 15 seconds and 2 seconds, respectively. Figure 4 shows clearly

Fig. 4. Search times for optimal base in four configurations 4

http://aprove.informatik.rwth-aachen.de/forms/unified_form_PBB.asp

12

that even with primes up to 10,000, the runtime of our algorithm is essentially negligible. Experiment 2: Base Quality From the 115,891 optimal base problems, we find a base with a prime larger than 17 for 6314, and with a non-prime element for 91,258. The maximal prime/non-prime we find in a base is 8191/895. At the level of Pseudo-Boolean instances, from the 1945 instances, 184 involve a prime larger than 17 and 790 involve a non-prime number. From here on we limit base search to elements up to 10,000. Experiment 3: Influence on SAT solving Figure 5 illustrates the influence of improved base search on SAT solving for Pseudo-Boolean Constraints. Both graphs depict the number of instances checked for satisfiability (the x-axis) within a given time limit (the y-axis). The left graph focuses on SAT solving time, while the right graph indicates total solving time (including base search). Both graphs consider all Pseudo-Boolean instances where a base element is non-prime or greater than 17 (781 instances) and compare solving times with bases found using three setups. The left curve corresponds to MiniSat+ with prime base elements ≤ 17 , the middle and right curves correspond to BNB with non-prime bases of elements ≤ 10, 000 using carry cost and comparator cost, respectively. As in the Pseudo-Boolean competitions, 30 minute timeouts are imposed. The average total runtimes (in sec) are 175, 146, 126 (left, middle, right) and the total number of instances solved are 431, 440, 445 (same order). The graphs of Figure 5 clearly show two things. First, SAT solving time clearly dominates over base finding time. Second, on average, our BNB configuration outperforms MiniSat+ . For some examples, the SAT solving time is reduced quite significantly.

9

Related Work

Recent work [2] encodes Pseudo-Boolean constraints via “totalizers” similar to sorting networks, determined by the representation of the coefficients in an underlying base. Here the authors choose the standard base 2 representation of numbers. It is straightforward to generalize their approach for an arbitrary mixed base, and our algorithm is directly applicable. In [10] the author analyzes the cost of representing the natural numbers up to some n with non-stationary bases. Our Lemma 6 is a contribution in that context.

10

Conclusion

We formalize the optimal base problem and significantly improve the search algorithm currently used in MiniSat+ . Our algorithm scales to consider base elements up to 1,000,000, in contrast to 17 for MiniSat+ . We show that for 13

Fig. 5. SAT (left) and total (right) solving times for MiniSat+ vs. BNB.

14

a range of Pseudo-Boolean instances, finding a better base does influence the subsequent SAT solving times. We anticipate that the idea that, when solving a constraint involving (possibly large) coefficients, it is possible to decompose the constraint by representing the coefficients in an optimal base may lead to many future developments. In the SAT solving arena, bit-blasting is a common approach. However it is typically applied using binary (sometimes unary) representation. We propose to consider bit-blasting using arbitrary (optimal) bases. Acknowledgement We thank Daniel Berend and Carmel Domshlak for useful discussions.

References 1. O. Bailleux, Y. Boufkhad, and O. Roussel. A translation of pseudo boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 2(1-4):191–200, 2006. 2. O. Bailleux, Y. Boufkhad, and O. Roussel. New encodings of pseudo-boolean constraints into CNF. In Proc. Theory and Applications of Satisfiability Testing (SAT ’09), pages 181–194, 2009. 3. P. Barth. Logic-based 0-1 constraint programming. Kluwer Academic Publishers, Norwell, MA, USA, 1996. 4. K. E. Batcher. Sorting networks and their applications. In AFIPS Spring Joint Computing Conference, volume 32 of AFIPS Conference Proceedings, pages 307– 314. Thomson Book Company, Washington D.C., 1968. 5. R. E. Bixby, E. A. Boyd, and R. R. Indovina. MIPLIB: A test set of mixed integer programming problems. SIAM News, 25:16, 1992. 6. R. E. Bryant, S. K. Lahiri, and S. A. Seshia. Deciding CLU logic formulas via boolean and pseudo-boolean encodings. In Proc. Intl. Workshop on Constraints in Formal Verification (CFV ’02), 2002. 7. B. Chor, P. Lemke, and Z. Mador. On the number of ordered factorizations of natural numbers. Discrete Mathematics, 214(1-3):123–133, 2000. 8. N. E´en and N. S¨ orensson. Translating pseudo-boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 2(1-4):1– 26, 2006. 9. V. M. Manquinho and O. Roussel. The first evaluation of Pseudo-Boolean solvers (PB’05). Journal on Satisfiability, Boolean Modeling and Computation (JSAT), 2(1-4):103–143, 2006. 10. N. Sidorov. Sum-of-digits function for certain nonstationary bases. Journal of Mathematical Sciences, 96(5):3609–3615, 1999.

A

Appendix: Proofs

Available by request from the authors.

15