# divide_and_conquer_towards_faster_pseudoboolean_solving__dac46b75.pdf

Divide and Conquer: Towards Faster Pseudo-Boolean Solving

Jan Elffers and Jakob Nordstr om KTH Royal Institute of Technology {elffers,jakobn}@kth.se

The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean satisﬁability so-called SAT solvers and today conﬂict-driven clause learning (CDCL) solvers are routinely used in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak. A tantalizing solution is to instead use stronger pseudo-Boolean (PB) reasoning, but so far the promise of exponential gains in performance has failed to materialize the increased theoretical strength seems hard to harness algorithmically, and in many applications CDCL-based methods are still superior. We propose a modiﬁed approach to pseudo-Boolean solving based on division instead of the saturation rule used in [Chai and Kuehlmann 05] and other PB solvers. In addition to resulting in a stronger conﬂict analysis, this also improves performance by keeping integer coefﬁcient sizes down, and yields a very competitive solver as shown by the results in the Pseudo Boolean Competitions 2015 and 2016.

1 Introduction

The Boolean satisﬁability problem (SAT) is one of the most fascinating problems in computer science. Though deceptively easy to state given a formula in propositional logic, is it possible to assign variables true and false so that it evaluates to true? it has been the focus of extensive research ever since the dawn of computer science (and even before cf. G odel s famous letter to von Neumann in 1956). SAT was proven NP-complete in [Cook, 1971; Levin, 1973], laying the foundation for computational complexity theory, and a widely accepted hypothesis is that the problem requires exponential time in the worst case [Impagliazzo and Paturi, 2001]. Yet the last couple of decades have seen the development of SAT solvers based on the conﬂict-driven clause learning (CDCL) paradigm introduced in [Marques-Silva and Sakallah, 1999],1 with further improvements in [Moskewicz

1A similar idea in the context of constraint satisfaction problems was independently developed in [Bayardo Jr. and Schrag, 1997].

et al., 2001] and later papers, that are very efﬁcient in practice. Today CDCL solvers are routinely used to solve largescale real-world problems in, e.g., hardware and software veriﬁcation, AI planning, automated theorem proving, and many other areas (see [Biere et al., 2009] for more details). A drawback with CDCL is that from a mathematical point of view the method of reasoning is quite weak it is based on the resolution proof system, for which exponential lower bounds are known even for simple combinatorial principles [Haken, 1985; Urquhart, 1987]. Another issue is that problems have to be encoded in conjunctive normal form (CNF) as a collection of disjunctive clauses, which loses the semantics of higher-level constraints and further hurts the reasoning power. This can be addressed by using preprocessing techniques for, e.g., Gaussian elimination and cardinality reasoning, but these techniques work only in limited cases and are again quite sensitive to the exact encoding of the problem. An attractive option is to instead use (linear) pseudo Boolean (PB) constraints i.e., integral linear inequalities over Boolean variables, which gives a succinct way of encoding problems in many different ﬁelds. PB constraints are more expressive than CNF, but are close enough that CNF-based techniques can be harnessed to attack pseudo-Boolean problems. The connection to integer linear programming (ILP) and, in particular 0-1 programming, makes it natural to also borrow insights from these areas. Some pseudo-Boolean solvers are still based on resolution, in that they translate the input to CNF. This can be done eagerly, so that all linear inequalities are converted to CNF after which a CDCL solver is called (as in Mini Sat+ [E en and S orensson, 2006], Open-WBO [Martins et al., 2014; Joshi et al., 2015], and Na PS [Sakai and Nabeshima, 2015]), or lazily in a modiﬁed CDCL solver that keeps the PB format of the input but derives new information only in the form of clauses (as in one of the methods in the Sat4j library [Le Berre and Parrain, 2010]). Another approach is to go beyond resolution and build solvers using the cutting planes method [Cook et al., 1987]. It should be noted that extending the conﬂict-driven framework to pseudo-Boolean constraints is non-trivial, but methods to do so were designed in the solvers PRS [Dixon and Ginsberg, 2002] and Galena [Chai and Kuehlmann, 2005], and were further developed in Pueblo [Sheini and Sakallah, 2006] and Sat4j [Le Berre and Parrain, 2010] (related, but slightly different, ideas

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

were also explored in bsolo [Manquinho and Marques-Silva, 2006]). Needless to say, this is far from a complete overview of pseudo-Boolean solving see, e.g., the excellent survey in [Biere et al., 2009, Chapter 22] for more information. From a theoretical standpoint, using cutting planes seems clearly preferable, since this method is never worse than resolution but can be exponentially stronger. In practice this is not so, however often CDCL-based solvers outperform PB solvers based on cutting planes! One possible explanation for this state of affairs lies in the tension between the two desiderata that the method of reasoning utilized should (1) be as powerful as possible but also (2) allow for efﬁcient search. Regarding the second consideration, storing and manipulating linear constraints is much more costly than dealing with simple disjunctive clauses, and can slow down the solver prohibitively [Sheini and Sakallah, 2006]. Integer coefﬁcients can also grow very large during search, requiring the usage of multi-precision arithmetic which decreases performance still further. In addition to these implementation concerns, a richer set of derivation rules makes the search space much larger and more challenging to explore. Perhaps partly to address this issue, solvers based on [Chai and Kuehlmann, 2005] do not use the full power of cutting planes. In particular, instead of the division rule they employ the simpler to implement saturation rule. This again makes solvers quite sensitive to details in the input format, however, and causes them to degenerate to resolution in certain cases where cutting planes is very efﬁcient [Hooker, 1992; Vinyals et al., 2018].

Our Contribution In this work, we further develop the theoretical foundations of conﬂict-driven pseudo-Boolean solving in [Chai and Kuehlmann, 2005] to incorporate the division rule2 in [Cook et al., 1987] as well as some other useful extensions, and report results from implementing these ideas in the solver Rounding Sat. The new method has several advantages. For problems where PB reasoning does not seem to afford much of an advantage compared to CDCL, the search speed measured in terms of number of conﬂicts per second is orders of magnitude faster than in other cutting-planes-based PB solvers, approaching the vicinity of standard CDCL. Thanks to the aggressive use of division, integer coefﬁcients normally remain within the range of 32 bits (for inputs with coefﬁcients of bounded size), which makes it possible to employ ﬁxedprecision arithmetic. From a theoretical point of view, using division means that the solver has the potential to be exponentially stronger for problems where 0-1-integer reasoning rather than just CDCL or linear programming is crucial [Vinyals et al., 2018]. It seems fair to say that this is also borne out in practice, as shown by the Pseudo-Boolean Competitions in 2015 and 2016,3 as well as by further improvements obtained since then as reported in this paper.

2As we discuss later in this paper, we have learned that related ideas can also be found in the general integer linear programming solver Cut Sat [Jovanovic and de Moura, 2013]. 3An earlier version of Rounding Sat participated under the name cdcl-cuttingplanes in these events.

Algorithm 1: CDCL main loop.

1 ρ empty trail ; D F

2 until solved do

3 (ρ, Cconﬂ) propagate(ρ, D)

4 if Cconﬂ = NONE then

5 if decision level of ρ = 0 then

6 output UNSAT and terminate

7 Clearnt analyze Conﬂict(Cconﬂ, ρ)

8 Revert ρ to backtrack level of Clearnt

9 D D {Clearnt}

11 if ρ is a total assignment then

12 output SAT and terminate

13 if time to restart then

14 Backtrack ρ to level 0

15 if time for clause database reduction then

16 Erase (roughly) half of learned clauses in D

17 ℓ a literal unassigned by ρ

18 ρ append(ρ, ℓ/d)

Organization of This Paper In Section 2, we review the basics of conﬂict-driven pseudo-Boolean solving, after which our contributions are presented in Section 3. Section 4 contains the results from our empirical evaluations. We conclude in Section 5 with some directions for further research. Some supplemental material (including experimental data) can be found at www.csc.kth.se/ jakobn/Rounding Sat.

2 Conﬂict-Driven Pseudo-Boolean Search In this section we review how conﬂict-driven solving can be extended from CNF to pseudo-Boolean constraints, in order to present the framework on which our contribution is based. Throughout this paper we identify 1 with true and 0 with false. A literal ℓis either a Boolean variable x or its negation x. We say that the sign of x is positive and that of x is negative. By a pseudo-Boolean (PB) constraint we mean a linear inequality over the domain {0, 1} with integer coefﬁcients and integral constant term. In the context of pseudo Boolean solving it is natural to represent the constraints in normalized form P i ciℓi w, where ℓi are literals over pairwise distinct variables, ci are positive integers, and w is a positive integer called the degree of falsity (or just degree). In what follows, by constraint we mean a pseudo-Boolean constraint in normalized form unless otherwise stated. We think of a partial truth value assignment ρ as the set of literals set to true by ρ. Thus, ρ(ℓ) = 1 if ℓ ρ, ρ(ℓ) = 0 if ℓ ρ, and if the variable is unassigned we write ρ(ℓ) = . We ﬁrst recap how conﬂict-driven clause learning (CDCL) works for CNF inputs. Note that the clauses C in a CNF formula F are just PB constraints with all coefﬁcients and degree of falsity equal to 1. The main loop of the CDCL algorithm is presented in Algorithm 1. The solver maintains a partial assignment ρ to the variables, which it is trying to extend to a total assignment satisfying the formula. We identify this ρ with an ordered set, referred to as the trail, containing the literals

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

Algorithm 2: propagate(ρ, D)

1 while there exists a clause C D and an unassigned literal ℓ C implied by C under ρ do

2 ρ append(ρ, ℓ/C)

3 if there exists a clause C D falsiﬁed by ρ then

4 return (ρ, C)

5 return (ρ, NONE)

Algorithm 3: analyze Conﬂict(Cconﬂ, ρ)

1 while Cconﬂis not asserting do

2 ℓ literal assigned last on the trail ρ

3 if ℓoccurs in Cconﬂthen

4 Creason reason(ℓ, ρ)

5 Cconﬂ Res(Cconﬂ, Creason)

6 ρ remove Last(ρ)

7 return Cconﬂ

annotated with additional information why the assignments were made as follows. We write ℓ/C to denote that the literal ℓon the trail was propagated by the constraint C to avoid immediately falsifying the formula (as explained below), and also use the notation C = reason(ℓ, ρ) to show that C was the reason for this propagation of ℓwhen the trail was ρ. We write ℓ/d when the assignment to ℓwas a freely made decision by the solver, in which case reason(ℓ, ρ) = NONE. The decision level of ℓin ρ, denoted level(ℓ, ρ), is the number of decisions up to (and possibly including) ℓ. There are two subroutines, unit propagation (Algorithm 2) and conﬂict analysis (Algorithm 3), which we review next. In unit propagation, the solver repeatedly ﬁnds an unassigned literal which is implied by some clause and adds this literal to the trail. A literal ℓin a clause C is implied, or propagated, by C under ρ if all other literals in C are falsiﬁed by ρ, meaning that ℓhas to be satisﬁed to avoid immediate contradiction. Unit propagation can terminate in two ways: either there are no further implications, or a clause is falsiﬁed. The unit propagation method returns the extended trail, plus potentially the falsiﬁed clause, which is called the conﬂict clause. The solver then calls conﬂict analysis if there was a falsiﬁed clause and makes a new decision otherwise. The purpose of conﬂict analysis is to learn a new clause that explains why the current partial assignment failed, and then add this clause so that the solver can avoid exploring infeasible parts of the search space multiple times. Conﬂict analysis is typically done using the ﬁrst unique implication point (1UIP) learning scheme. The solver starts with the conﬂict clause and the last reason clause in chronological order propagating a literal in the conﬂict clause to false, and resolves these two clauses using the resolution rule: given two clauses C x and D x containing a unique variable x with opposite signs, derive the resolvent Res(C x, D x) = C D. Then this resolvent is in turn resolved with the reason clause propagating the last literal in the resolvent to false, et cetera. The key invariant in this algorithm is that at the end

of each iteration of the loop, the new intermediate conﬂict clause Cconﬂis falsiﬁed by what remains of the trail ρ when the last literal is removed. 1UIP conﬂict analysis terminates the ﬁrst time Cconﬂcontains a single literal ℓ at the last decision level. This clause is then declared to be the learnt clause and is added to the clause database containing the formula F as well as previously learnt clauses. Next the assertion level is calculated, which is the second highest decision level represented in the learnt clause. The trail will then be backtracked to this level, meaning that all assignments at higher levels are removed. It is not hard to see that at this point Cconﬂwill propagate ℓ to true, i.e., ﬂipping the assignment at the time of conﬂict. Clauses having the property that they cause propagation after backtracking are called asserting. What we have presented above is a schematic, and somewhat simpliﬁed, description of CDCL search, with an emphasis on the conﬂict analysis that we want to extend to a pseudo-Boolean setting. We do not dwell on other important aspects, such as restart policy or and clause database erasure, since they are not the main focus of this work. Let us now discuss how to generalize conﬂict-driven search from clauses to PB constraints. The main loop in Algorithm 1 remains the same. To generalize unit propagation, we need the notion of slack of a constraint C .= P i ciℓi w, which is a measure of how close a partial assignment ρ is to falsifying C. It is deﬁned as the difference between the maximum value the sum P i ciℓi may attain given the assignments already made in ρ and the degree of falsity w, i.e.,

slack(C, ρ) = P i:ρ(ℓi) =0 ci w . (1)

The constraint C is falsiﬁed by ρ if the slack is negative, and C implies or propagates a literal ℓi under ρ if ρ(ℓi) = and slack(C, ρ) < ci, meaning that unless ℓi is set to true the constraint C will be falsiﬁed. Note that this generalizes the notion of propagating disjunctive clauses, which have slack 0 and coefﬁcient 1 for the propagated literal. Unit propagation as in Algorithm 2 can now be done by calculating the slack of the constraints. One important problem is that when C is a general constraint and not a disjunctive clause it seems harder to detect efﬁciently whether C is propagating, but we will not discuss this further in this paper. To generalize 1UIP conﬂict analysis, we would like to resolve a falsiﬁed constraint with a sequence of reason constraints in such a way that the ﬁnal constraint is asserting. The natural extension of the resolution rule to general PB constraints is called generalized resolution [Hooker, 1992; Dixon et al., 2004] and is deﬁned as follows. Given constraints C .= aℓ+ P i ciℓi w and C .= bℓ+ P i c iℓ i w containing some literal ℓwith opposite signs, let g = gcd(a, b). Then the (generalized) resolvent Res(C, C , ℓ) is

b g P iciℓi + a

g P ic iℓ i bw + aw ab

(where we implicitly assume that this constraint, as well as the result of any other operation performed below, is again reduced to normalized form). Note that in contrast to resolution applied on clauses we have to give a third argument specifying which literal should be cancelled, since there may be several literals with opposite signs. As an example, for the

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

Algorithm 4: Reduction by weakening and saturation.

1 while slack(Res(Cconﬂ, Creason, ℓ), ρ) 0 do

2 ℓ a literal in Creason not falsiﬁed by ρ, ℓ = ℓ

3 Creason saturate(weaken(Creason, ℓ ))

4 return Creason

constraints C .= 2x1 +2x2 +2x3 3 and C .= x1 +x3 1 the resolvent over x1 is Res(C, C , x1) .= 2x2 + 4x3 3. However, when we try to perform conﬂict analysis as in Algorithm 3 we run into trouble. Recall that the key invariant during CDCL conﬂict analysis is that the currently derived constraint is falsiﬁed by what remains of the trail, meaning that at all times the derived constraint explains the conﬂict. This property no longer holds when we use generalized resolution, as shown in the next example.

Example 2.1 (Failed conﬂict analysis using generalized resolution). Consider a PB instance consisting of just C .= 2x1 + 3x2 + x3 3 and C .= 4x2 + 4x3 + 2x4 + x5 4. Suppose the solver makes decisions x4, after which nothing propagates, and then x3. At this point C propagates x2, which in turn falsiﬁes C , triggering conﬂict analysis. Using resolution, the solver would derive Res(C, C , x2) .= 8x1 + 16x3 + 6x4 + 3x5 12. But this constraint is not falsiﬁed by the assignment x4, x3 remaining on the trail.

In view of this example, generalized resolution on its own is not sufﬁcient for conﬂict analysis. [Chai and Kuehlmann, 2005] solve this problem by designing a reduction algorithm that computes a constraint that is implied by the original reason constraint and for which generalized resolution maintains the key invariant when the reason is replaced by this new constraint. This algorithm uses two additional operations called weakening and saturation, which we describe next. The weakening operation removes a literal from a constraint and subtracts its coefﬁcient from the degree. For example, weakening the constraint C .= x1 + 2x2 + 3x3 4 on x1 yields weaken(C, x1) .= 2x2+3x3 3. This is sound, because weakening on a literal ℓis equivalent to adding the constraint ℓ 0 multiplied by the appropriate coefﬁcient. Saturation applied to a constraint C .= P i ciℓi w returns saturate(C ) .= P i min(ci, w) ℓi w, i.e., it brings the magnitude of all coefﬁcients down to the degree of falsity. As a concrete example, saturating the constraint x1 + 2x2 + 3x3 2 gives x1 + 2x2 + 2x3 2. This is sound because all literals take non-negative integral values, and if P i ciℓi w is satisﬁed by setting some literal ℓi = 1 for which ci > w, then clearly the contribution from w ℓi is also sufﬁcient to satisfy the constraint. The reduction method in [Chai and Kuehlmann, 2005] is presented as Algorithm 4 and works by repeating the following steps. First, it tests whether the generalized resolvent of the reason constraint and the conﬂict constraint satisﬁes the key invariant. If this is the case, then the reason can be used as is and the algorithm terminates. Otherwise, it ﬁnds a non-falsiﬁed literal in the reason constraint different from the propagating literal, weakens the constraint on this literal, applies saturation, and continues with the next iteration.

Let us illustrate by a simple example how a single step in the conﬂict analysis of [Chai and Kuehlmann, 2005] works. Example 2.2 (Illustration of Chai Kuehlmann reduction). Suppose we have a pseudo-Boolean instance consisting of the two constraints C .= 2x1 + 2x2 + 2x3 + 2x4 + x5 6 and C .= 2x1 + 2x2 + 2x3 + 2x4 3. Clearly, C and C are just obfuscated encodings of the mutually contradictory cardinality constraints x1+x2+x3+x4 3 and x1+x2+x3+x4 2, respectively. However, as we shall see reduction by saturation does not allow us to derive contradiction immediately. Suppose the trail is ρ =

x1/d, x2/C, x3/C, x4/C . The constraint C is falsiﬁed and C is the reason (Cconﬂand Creason in Algorithm 4, respectively), and the variable to resolve over is the one that is last on the trail, i.e., x4. We have Res(C , C, x4) .= x5 1, which has non-negative slack 0, so the reason constraint must be reduced. The algorithm chooses a non-falsiﬁed literal different from x4, say x2, and weakens C to obtain 2x1 + 2x3 + 2x4 + x5 4. Applying saturation has no effect. The resolvent Res(C , 2x1 +2x3 +2x4 +x5 4, x4) .= 2x2 + x5 1 has slack 0, triggering further reduction. Say the next variable chosen is x3. Weakening gives 2x1 + 2x4 + x5 2. Saturation again changes nothing, and Res(C , 2x1+2x4+x5 2, x4) .= 2x2+2x3+x5 1 again has slack 0. Finally, weakening on x5 yields 2x1 + 2x4 1, after which saturation returns x1 + x4 1. Now the resolvent Res(C , x1+x4 1, x4) .= 2x2+2x3 1 has negative slack 1, so we are done. Because the slack of the resolvent is too expensive to compute manually after each weakening and saturation step of the reason constraint, an upper bound on the slack is used in practice. This upper bound is based on the subadditivity property of slack, which we state without proof. Fact 2.3 (Slack is subadditive). For any pseudo-Boolean constraints C and C and any partial assignment ρ it holds that slack(C + C , ρ) slack(C, ρ) + slack(C , ρ). In particular, this means that if for C .= aℓ+ P i ciℓi w and C .= bℓ+ P i c iℓ i w we let D = Res(C, C , ℓ ) and g = gcd(a, b), then we have

slack(D, ρ) b slack(C, ρ) + a slack(C , ρ) /g . (3)

The advantage of using this estimate is that we do not need to compute the resolvent in each iteration, but instead it is sufﬁcient to know the slacks of the conﬂict constraint (which remains constant) and the reduced reason constraint.

3 PB Conﬂict Analysis Using Division We now proceed to describe our new method for conﬂict analysis, which we call rounding. The idea is to reduce the reason constraint into suitable form using division instead of saturation, where the result of dividing the constraint C .= P i ciℓi w by a positive integer d is

divide(C, d) .= P

i ci/d ℓi w/d (4)

(which is a sound derivation since all numbers involved are non-negative integers). It is worth noting that this division rule (rather than saturation) is what was used to deﬁne the cutting planes method in [Cook et al., 1987].

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

Algorithm 5: round To One(C, ℓ, ρ)

1 c coeﬃcient(C, ℓ)

2 foreach literal ℓj in C with coefﬁcient cj do

3 if ρ(ℓj) = 0 and cj is not divisible by c then

4 C weaken(C, ℓj)

5 return divide(C, c)

As presented in Algorithm 5, our reduction method round To One(C, ℓ, ρ) takes a constraint C, a literal ℓand a partial assignment ρ and outputs a constraint C rounded on ℓ that is a consequence of C, has coefﬁcient 1 for ℓ, and satisﬁes an additional property (to be discussed further) that makes it a suitable reason reduction algorithm. To reduce the reason round To One is called with Creason = reason(ℓ, ρ) together with ρ and ℓ. The algorithm weakens away all literals not falsiﬁed by ρ and with coefﬁcients not divisible by the coefﬁcient c of ℓin Creason, and then divides by c. In this case, the additional property of the output constraint is that it still implies ℓ. Equivalently, the slack is 0, and this implies that the resolvent in conﬂict analysis is guaranteed to be falsiﬁed, so that our desired invariant in conﬂict analysis holds. The reason for this is that slack is subadditive (see Fact 2.3) and we are resolving a reduced reason constraint with slack 0 and the previous intermediate conﬂict constraint, which has negative slack. Hence, the new intermediate conﬂict constraint also has negative slack as required. Let us formalize and prove these claims. Proposition 3.1. For any trail ρ and any PB constraint C .= P i ciℓi w containing the literal ℓi it holds that slack(round To One(C, ℓi, ρ), ρ) = slack(C, ρ)/ci .

Proof. It is straightforward to verify directly from Eq. (1) that weakening on non-falsiﬁed literals does not change the slack. After the weakening loop, the remaining non-falsiﬁed literals are all divisible by the coefﬁcient ci of the literal ℓi. Therefore, if we would not take the ceiling of the degree of Creason but do exact division, then the (possibly rational) slack would be exactly 1/ci times the original slack. Because we round up the degree after division, the slack is slack(C, ρ)/ci .

Corollary 3.2. If C .= P i ciℓi w is a non-falsiﬁed constraint that propagates ℓi under ρ, i.e., 0 slack(C, ρ) < ci, then slack(round To One(C, ℓi, ρ), ρ) = 0. If instead slack(C, ρ) < 0, then slack(round To One(C, ℓi, ρ), ρ) < 0, i.e., if C is falsiﬁed under ρ, then so is round To One(C, ℓi, ρ). Example 3.3 (Illustration of round To One). To see how our new reduction method works, consider the same PB instance and trail as in Example 2.2. Recall that the trail is ρ =

x1/d, x2/C, x3/C, x4/C and that the reason is C .= 2x1 + 2x2 + 2x3 + 2x4 + x5 6 to be resolved over x4 (the conﬂict constraint is irrelevant for this example). Our method ﬁrst sets the divisor to be the coefﬁcient of x4, which equals 2 (line 1 in Algorithm 5). Then it loops over all literals in the constraint, and weakens away those that are not falsiﬁed by ρ and have coefﬁcient not divisible by 2 (lines 2 4). Literals x2, . . . , x5 are not falsiﬁed, and of these x5 has coefﬁcient not divisible by 2, so x5 gets weakened away. When the loop

Algorithm 6: Rounding Sat conﬂict analysis

1 while Cconﬂcontains no or multiple falsiﬁed literals on the last level do

2 if decision level = 0 then

3 output UNSAT and terminate

4 ℓ literal assigned last on the trail ρ

5 if ℓoccurs in Cconﬂthen

6 Cconﬂ round To One(Cconﬂ, ℓ, ρ)

7 Creason round To One(reason(ℓ, ρ), ℓ, ρ)

8 Cconﬂ Res(Cconﬂ, Creason, ℓ)

9 if overﬂow occurs in Cconﬂthen

10 Round Cconﬂto cardinality constraint

11 Undo ℓon ρ

12 ℓ the literal in Cconﬂlast falsiﬁed by ρ

13 return round To One(Cconﬂ, ℓ, ρ)

ends, the constraint C equals 2x1 + 2x2 + 2x3 + 2x4 5. Finally, division by 2 (line 5) yields x1 + x2 + x3 + x4 3. Thus, we see that we get a stronger constraint than in reduction by saturation, which gives x1 + x4 1.

Remark 3.4 (Variations on round To One). Let us discuss some possible variants of the reduction algorithm. Consider the constraint C .= 2x1+3x2+3x3+3x4 8, to be rounded over x1, together with the assignment ρ = x1, x2, x3, x4 , for which round To One returns x1 + 2x4 1. If instead of doing all literal weakenings in one go we would let the algorithm weaken on one literal at a time and terminate as soon as the slack after division is 0, then we could have obtained the stronger constraint x1 + 2x2 + 2x4 3. However, it can be shown that regardless of the order in which weakenings are carried out, this iterative approach will always weaken almost as many literals as round To One. More precisely, the difference is at most c 1 literals, where c is the divisor. Another possibility would be to weaken partially on literals, e.g., deriving 2x1 + 2x2 + 2x3 + 3x4 6 from C, after which division yields x1 + x2 + x3 + 2x4 3. However, our empirical evaluations of this showed much worse results.

Besides rounding the reason, we employ round To One also in other places. First, we round the intermediate conﬂict constraint Cconﬂbefore resolving it. By Corollary 3.2, this leaves Cconﬂfalsiﬁed, so the key invariant in conﬂict analysis still holds. The other point at which we call round To One is as a postprocessing step. Once we are done with conﬂict analysis, we ﬁnd the literal ℓthat was falsiﬁed last by ρ in the derived constraint, round on ℓ, and declare the result to be the learnt constraint. The full conﬂict analysis is given in Algorithm 6. There are some corner cases in PB conﬂict analysis that make it more complicated than CDCL. First, a resolution operation may cancel all falsiﬁed literals on the current decision level, in which case the analysis may continue to an earlier decision level. This is the reason for the condition no or multiple falsiﬁed literals on the last level on line 1 in Algorithm 6. It may even happen that conﬂict analysis is able to proceed to the topmost decision level, which means the instance is unsatisﬁable. In this case, the solver terminates (lines 2 3). An-

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

other difference is that learnt constraints may be falsiﬁed at their assertion level, in which case repeated conﬂict analysis is performed before calling unit propagation.

Remark 3.5 (Skipping resolution steps). Another interesting contrast to CDCL conﬂict analysis is that if slack(Cconﬂ, ρ) is very negative, then it might be possible to ignore the resolution step with Creason and just remove the propagated literal ℓfrom the trail ρ, still maintaining the invariant slack(Cconﬂ, ρ \ {ℓ}) < 0. Intuitively, it might seem that this should lead to a more compact analysis involving only the reasons truly needed for the conﬂict, and hence potentially produce a better learnt constraint. When we evaluated this empirically the results did not improve, however, and so we ended up not using this idea, but it might still be an interesting observation worthy of further exploration.

Comparison to Cut Sat The idea to use division during conﬂict analysis appears also in the general integer linear programming (ILP) solver Cut Sat [Jovanovic and de Moura, 2013], so let us try to compare and contrast this solver to Rounding Sat. ILP constraints are not normalized but instead have the form C .= P i cixi w, where ci can be negative. In Cut Sat, the trail consists of bound reﬁnements x c or x c. (In the PB case, the trail contains at the very start the bounds xi 0 and xi 1 for all variables xi, and further reﬁnements xi 1 or xi 0 correspond to assignments.) Each reﬁnement has a reason constraint or is a decision. Decisions always ﬁx variable values, so if the currently best bound is x L (x U), then the decision is x L (x U). Cut Sat conﬂict analysis also works by resolving a conﬂict constraint with a sequence of reduced reason constraints. The reduction method outputs tightly propagating (or tight) constraints, which are on the form bx + P cixi w, where x is the reﬁnement variable and b { 1, 1}. The reduced reason implies the same bound reﬁnement on x as the original one with respect to the trail. (In the PB setting this means that the slack is 0.) Cut Sat reduction starts with the reason, derives a constraint C with all coefﬁcients divisible by the coefﬁcient c of the propagated literal, and returns divide(C , c). This is similar to how Rounding Sat works: it also starts with the reason, performs weakening, and then divides. To discuss Cut Sat reduction in more detail, assume for simplicity that the reason constraint is a lower bound reﬁnement C .= cx + P cixi w with all coefﬁcients positive (for negative coefﬁcients the role of upper and lower bounds are just reversed). Cut Sat iterates through the variables of C in reverse chronological order with respect to the trail. If a variable xi has a coefﬁcient ci > 0 not divisible by c, then Cut Sat adds a constraint associated with this variable to C in order to make the coefﬁcient divisible. To do so Cut Sat looks up why xi is bounded from above (which must be the case, since otherwise the reason constraint would not be propagating). If the latest upper bound reﬁnement for xi is due to a reason propagating, then this reason is made tight by calling the reason reduction algorithm recursively. Suppose this call returns the new constraint Ci .= xi + P j c jxj w (with coefﬁcient 1 for xi since we have an upper bound constraint). Then generalized resolution is performed on C and Ci with

respect to xi. This eliminates one coefﬁcient not divisible by c, but may introduce new variables with non-divisible coefﬁcients. All such variables are dealt with in the same way in reverse chronological order with respect to the trail. Suppose instead that the latest upper bound reﬁnement for xi is a decision xi Ui. Because decisions always ﬁx variable values, this means that a matching lower bound reﬁnement forcing xi Ui must exist earlier on the trail. Then this matching constraint is made tight and added to C with the smallest multiplier making the coefﬁcient of xi divisible. For PB instances this works as follows. Assume again that the reason is a lower bound reﬁnement cx + P cixi w with all coefﬁcients positive, and let ci > 0 be not divisible by c > 0. We get a case analysis depending on whether xi 0 appears on the trail or not. If not, then we resolve with the inequality xi 1 (corresponding to weakening in Rounding Sat). If xi 0 is on the trail, then we resolve by the tight reduced constraint obtained from the reason that xi 0 if this reason exists. Otherwise, xi 0 is a decision and we add the tight constraint xi 0 with the smallest multiple so that the coefﬁcient becomes divisible by c. This is equivalent to rounding up the coefﬁcient during a division step. When comparing the two methods, we would argue that Rounding Sat seems clearly simpler to understand and implement (though this is also thanks to the fact that we need not worry about general ILP constraints but can focus on PB constraints). Our method is also more efﬁcient in the worst case, since no recursive calls are made and the conﬂict analysis does not have to go as far back on the trail. While we believe that these aspects also make Rounding Sat signiﬁcantly more efﬁcient not only in the worst case but also in practice, we should add the caveat that we have not performed a thorough empirical evaluation of how Cut Sat and Rounding Sat compare on, e.g., PB competition benchmarks.

4 Experimental Analysis

In this section we report results from an experimental comparison of Rounding Sat to Sat4j and Open-WBO. Recall that Open-WBO is a resolution-based solver that does an eager conversion to clauses and then runs a state-of-the-art CDCL solver. From the Sat4j solver library we test two versions: a resolution-based solver Sat4j Res, doing lazy conversion to clauses, and a cutting planes-based solver Sat4j Res+CP, which, however, also runs the resolution-based solver in parallel since the cutting planes-based solver on its own is not considered competitive enough. In our experiments we gave all solvers the same wall-clock time, which means that Sat4j Res+CP got twice as much CPU time as the other solvers. We evaluated the solvers on benchmarks submitted to the Pseudo-Boolean Competitions over the past two decades in the DEC-SMALLINT-LIN category (decision problems, small integers, linear constraints) since Rounding Sat is currently designed to solve decision problems and represents constraints using 32-bit integers. Our choice of Sat4j and Open-WBO was dictated by the results in the DEC-SMALLINT-LIN category from the Pseudo-Boolean Competition 2016, where these two solvers together with our solver were the top-three performers. We used the latest avail-

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

Rounding Sat Sat4j Res+CP Sat4j Res Open-WBO Total PB05 aloul 36 + 21 36 + 21 36 + 3 36 + 6 57 PB06 manquiho 14 + 0 14 + 0 14 + 0 3 + 0 14 PB06 ppp-problems 4 + 0 4 + 0 4 + 0 3 + 0 6 PB06 uclid 1 + 47 1 + 47 1 + 47 1 + 49 50 PB06 liu 16 + 0 16 + 0 16 + 0 17 + 0 20 PB06 namasivayam 72 + 128 72 + 128 72 + 128 72 + 128 200 PB06 prestwich 10 + 0 11 + 0 9 + 0 14 + 0 18 PB06 roussel 0 + 22 0 + 22 0 + 4 0 + 4 40 PB10 oliveras 34 + 32 34 + 32 34 + 33 34 + 33 80 PB11 heinz 2 + 0 2 + 0 2 + 0 2 + 0 4 PB11 lopes 42 + 26 37 + 25 37 + 25 33 + 28 193 PB12 sroussel 31 + 0 21 + 0 23 + 0 29 + 1 122 PB16 elffers 0 + 287 0 + 229 0 + 142 0 + 213 293 PB16 nossum 68 + 0 39 + 0 39 + 0 55 + 0 180 PB16 quimper 43 + 214 43 + 213 43 + 213 46 + 241 304 Sum 373 + 777 330 + 717 330 + 595 345 + 703 1581

Table 1: Results on benchmarks from past PB competitions (number of solved satisﬁable instances + solved unsatisﬁable instances).

Rounding Sat Sat4j Res+CP Sat4j Res Open-WBO Total Vertex cover, rectangular grids 82 68 26 82 82 Subset cardinality, ﬁxed bandwidth 28 28 4 13 28 Subset cardinality, random matrices 28 28 6 6 28 Perfect matching, random graphs 33 9 10 11 33 Even colouring, odd-dimension grids 25 17 20 25 25 Even colouring, random graphs 22 5 6 6 22

Table 2: Detailed results for some families in the benchmark set PB16 elffers (number of solved instances; all are unsatisﬁable).

able versions of all solvers as of December 1, 2017. We ran our experiments on a cluster with a set-up of 6 AMD Opteron 6238 (2.6 GHz) cores and 16 GB of memory. We used 1800 seconds as the wall clock timeout, the same time limit as in the Pseudo-Boolean Competition 2016, and had a memory limit of 14 GB for all runs. The results are presented in Table 1 (summary for all benchmarks) and Table 2 (detailed results per family in the large benchmark set PB16 elffers). On satisﬁable benchmarks we see that Rounding Sat is typically doing equally well as the other solvers, and the differences between solvers are relatively small. The unsatisﬁable benchmarks differentiate between the solvers much more. We can divide the benchmark sets into two categories: those where pseudo-Boolean reasoning is crucial and those where resolution-based solvers are equally good. The benchmarks for which PB reasoning matters are PB05 aloul, PB06 roussel, and PB16 elffers. In the case where PB reasoning does not matter, we see no large differences between the solvers, except that on the PB16 quimper set Open-WBO solves 12% more unsatisﬁable instances than the best of the other solvers. The cases where pseudo Boolean reasoning matters are relatively rare. PB05 aloul and PB06 roussel are mainly pigeonhole principles encoded with cardinality constraints, which are easy to solve for solvers that can just add up linear inequalities but are exponentially hard

for resolution when encoded into CNF, and so it is not surprising that Rounding Sat and Sat4j Res+CP do much better than the two resolution-based solvers here. The benchmark set PB16 elffers consists of various crafted instances. Subset cardinality formulas encode that we cannot have a majority of true and false variables simultaneously if the total number of variables is odd. For resolution these formulas are exponentially hard when generated from random matrices and easy in theory but challenging in practice when based on ﬁxed bandwidth matrices, but are always easy for cardinality reasoning. This explains the difference in performance between Rounding Sat and Open-WBO. Vertex cover formulas claim the existence of a too small vertex cover for a rectangular, toroidal grid graph. These instances have fractional solutions, however, meaning that proper pseudo-Boolean reasoning is needed (as opposed to for pigeonhole principle and subset cardinality formulas, where linear programming is enough). Perhaps somewhat surprisingly, Open-WBO performs very well although pseudo-Boolean reasoning should be crucial. The reason seems to be that since the input is presented in a helpful order, the CNF encoding of the cardinality constraint for the vertex cover size provides extension variables that allow Open-WBO to perform the required counting argument in resolution. Rounding Sat also solves these instances ef-

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

Rounding Sat Sat4j CP Sat4j Res Open-WBO PB05 aloul* 79 2996 4538 PB06 manquiho 294 4 PB06 ppp-problems 3128 24 4409 4770 PB06 uclid 2050 144 1211 948 PB06 liu 747 35 442 1951 PB06 namasivayam 14702 22 16239 13251 PB06 prestwich 1263 56 2830 6228 PB06 roussel 2076 237 1740 4762 PB10 oliveras 3069 34 1144 844 PB11 heinz 2191 85 2698 2882 PB11 lopes 3433 92 2452 1928 PB12 sroussel 1024 6 1581 1546 PB16 nossum 2832 14 3287 2223 PB16 quimper 4380 101 4206 9542 PB16 elffers

Vertex cover, rectangular grids 6607 177 5412 Subset cardinality, ﬁxed bandwidth* 19 3462 9970 Subset cardinality, random matrices* 11 3623 9273 Perfect matching, random graphs* 5806 98 2299 11073 Even colouring, odd-dimension grids 21293 502 12835 24492 Even colouring, random graphs* 10268 152 3391 10111

Table 3: Average number of conﬂicts per second by family. A dash denotes that all instances were solved within 1 second. An asterisk denotes that Rounding Sat needs a much lower number of conﬂicts to refute the formula than resolution-based solvers.

ﬁciently using native PB reasoning in terms of the original variables. Sat4j Res+CP solves most of the instances, though not the full set, whereas the approach in Sat4j Res with lazy clause generation plus resolution works very poorly. The last two benchmark sets, perfect matching and even colouring formulas, are both special cases of problems on the format P i Ij xi = wj, j [m], where every variable xi occurs in an even number of equations but Pm j=1 wj is odd. These formulas again require pseudo-Boolean reasoning, except when the underlying graph is simple enough to admit an efﬁcient resolution-based approach (as for the instances generated from odd-dimension grids). These instances based on even-odd counting can be efﬁciently refuted in the cutting planes proof system provided that division is used, and indeed Rounding Sat performs well. On random graphs these formulas seem likely to be exponentially hard for resolution, and so it is not surprising that Open-WBO is so bad. For Sat4j we believe that the poor performance is due to precisely the fact that this solver uses saturation rather than division. Overall, we see that Rounding Sat is almost always equally good as the best of the other solvers (with the possible exceptions of PB06 prestwich and PB16 quimper), and for several benchmark families it is markedly better. The differences are particularly stark for many of the crafted unsatisﬁable instances in PB16 elffers, which have been designed to be very easy for pseudo-Boolean reasoning but where Rounding Sat often is the only solver able to prove unsatisﬁability quickly. Besides number of solved instances, we have also studied search speed measured as the number of conﬂicts per sec-

ond4 (see Table 3, where we discard instances solved in less than 1 second). A couple of remarks are in order here. First, the number of conﬂicts per second depends on how many constraints the solver keeps in the database: more aggressive deletion gives a higher speed. We do not know how the solvers compare in this aspect. Second, Rounding Sat solves certain formulas in just a few seconds while the resolutionbased solvers time out. The conﬂict speed decreases over time as the constraint database size increases, so the comparison is then not entirely fair. The cases where we know that this happens are marked with an asterisk in the table. For all benchmark families Rounding Sat reaches a conﬂict speed that is one or several orders of magnitude higher than Sat4j Cutting Planes, the other solver doing PB reasoning. Comparing Rounding Sat to the CDCL-based solvers, for benchmarks where pseudo-Boolean reasoning does not help we see that Rounding Sat is usually at most 3 times slower.

5 Concluding Remarks In this paper we present a new approach to pseudo-Boolean solving, building on the conﬂict-driven search in [Chai and Kuehlmann, 2005] but using division instead of saturation. We report results from implementing these ideas in the solver Rounding Sat and evaluating against other state-of-theart pseudo-Boolean solvers. Our conclusions are that the

4One issue here is that Open-WBO does not output this statistic, so for these particular measurements we had to hack the solver slightly. The values obtained are not perfect, but should be within a 1% error for all benchmarks except those in PB06 manquiho.

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)

proof search is indeed stronger when pseudo-Boolean reasoning is essential, and that the aggressive use of division also helps to keep coefﬁcient sizes down, speeding up the arithmetic operations. Although Rounding Sat cannot compete with state-of-the-art solvers in terms of raw search speed, it is approaching CDCL-based methods measured in terms of number of conﬂicts per second. Our solver performs very well over all on the benchmarks tested. It remains competitive with resolution-based solvers when pseudo-Boolean reasoning does not really seem to pay off, and it can outperform CDCL on instances where more sophisticated reasoning is crucial. It also seems superior to the pseudo-Boolean solving approach with saturation instead of division. An obvious direction for future research is to improve our solver further. As other pseudo-Boolean solvers, Rounding Sat is sensitive to the input format in that it performs quite poorly on CNF formulas. A way to address this would be to implement rules that can rewrite CNF to more efﬁcient linear constraints when possible. In particular, an important challenge is to do cardinality detection for sets of clauses encoding cardinality constraints. Cardinality detection was considered already in [Dixon and Ginsberg, 2002] (in the form of constraint strengthening) and was proposed again as a preprocessing step in [Biere et al., 2014]. It works well for certain crafted instances, but is too costly to implement in general when there is no guarantee that cardinality constraints will be found. Instead, we would like to implement lazy cardinality detection during proof search, where the price is paid only when there are strong indications that this will pay off.

Acknowledgements

We would like to thank Daniel Le Berre for many pleasant and enlightening discussions about pseudo-Boolean solving, and Jo ao Marques-Silva for helping us get an overview of relevant references. We are also grateful for the many detailed comments from the anonymous reviewers, which helped us to improve the manuscript substantially. Our experiments were run on computational resources provided by the Swedish National Infrastructure for Computing (SNIC). The authors received support from the European Research Council under the European Union s Seventh Framework Programme (FP7/2007 2013) / ERC grant agreement no. 279611. The second author was also funded by Swedish Research Council grants 621-2012-5645 and 2016-00782.

References [Bayardo Jr. and Schrag, 1997] R. J. Bayardo Jr. and R. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proc. 14th National Conf. Artif. Intell. (AAAI 97), pp. 203 208, 1997. [Biere et al., 2009] A. Biere, M. J. H. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisﬁability. 2009. [Biere et al., 2014] A. Biere, D. Le Berre, E. Lonca, and N. Manthey. Detecting cardinality constraints in CNF. In Proc. 17th Conf. Theory Appl. Sat. Testing (SAT 14), pp. 285 301, 2014. [Chai and Kuehlmann, 2005] D. Chai and A. Kuehlmann. A fast pseudo-Boolean constraint solver. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 24(3):305 317, 2005.

[Cook et al., 1987] W. Cook, C. R. Coullard, and G. Tur an. On the complexity of cutting-plane proofs. Disc. Appl. Math., 18(1):25 38, 1987. [Cook, 1971] S. A. Cook. The complexity of theorem-proving procedures. In Proc. 3rd Symp. Theory of Computing (STOC 71), pp. 151 158, 1971. [Dixon and Ginsberg, 2002] H. E. Dixon and M. L. Ginsberg. Inference methods for a pseudo-Boolean satisﬁability solver. In Proc. 18th National Conf. Artif. Intell. (AAAI 02), pp. 635 640, 2002. [Dixon et al., 2004] H. E. Dixon, M. L. Ginsberg, and A. J. Parkes. Generalizing Boolean satisﬁability I: Background and survey of existing work. JAIR, 21:193 243, 2004. [E en and S orensson, 2006] N. E en and N. S orensson. Translating pseudo-Boolean constraints into SAT. JSAT, 2(1-4):1 26, 2006. [Haken, 1985] A. Haken. The intractability of resolution. Theor. Comput. Sci., 39(2-3):297 308, 1985. [Hooker, 1992] J. N. Hooker. Generalized resolution for 0-1 linear inequalities. Annals Math. Artif. Intell., 6(1):271 286, 1992. [Impagliazzo and Paturi, 2001] R. Impagliazzo and R. Paturi. On the complexity of k-SAT. JCSS, 62(2):367 375, 2001. [Joshi et al., 2015] S. Joshi, R. Martins, and V. M. Manquinho. Generalized totalizer encoding for pseudo-Boolean constraints. In Proc. 21st Conf. Principles and Practice Constr. Prog. (CP 15), pp. 200 209, 2015. [Jovanovic and de Moura, 2013] D. Jovanovic and L. de Moura. Cutting to the chase solving linear integer arithmetic. J. Automated Reasoning, 51(1):79 108, 2013. [Le Berre and Parrain, 2010] D. Le Berre and A. Parrain. The Sat4j library, release 2.2. JSAT, 7:59 64, 2010. [Levin, 1973] L. A. Levin. Universal sequential search problems. Problemy peredachi informatsii, 9(3):115 116, 1973. [Manquinho and Marques-Silva, 2006] V. M. Manquinho and J. Marques-Silva. On using cutting planes in pseudo-Boolean optimization. JSAT, 2:209 219, 2006. [Marques-Silva and Sakallah, 1999] J. P. Marques-Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satisﬁability. IEEE Trans. Comput., 48(5):506 521, 1999. [Martins et al., 2014] R. Martins, V. M. Manquinho, and I. Lynce. Open-WBO: A modular Max SAT solver. In Proc. 17th Conf. Theory Appl. Sat. Testing (SAT 14), pp. 438 445, 2014. [Moskewicz et al., 2001] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efﬁcient SAT solver. In Proc. 38th Design Automation Conf. (DAC 01), pp. 530 535, 2001. [Sakai and Nabeshima, 2015] M. Sakai and H. Nabeshima. Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers. IEICE Trans. Info. Syst., 98-D(6):1121 1127, 2015. [Sheini and Sakallah, 2006] H. M. Sheini and K. A. Sakallah. Pueblo: A hybrid pseudo-Boolean SAT solver. JSAT, 2(1-4):165 189, 2006. [Urquhart, 1987] A. Urquhart. Hard examples for resolution. J. ACM, 34(1):209 219, 1987. [Vinyals et al., 2018] M. Vinyals, J. Elffers, J. Gir aldez-Cru, S. Gocht, and J. Nordstr om. In between resolution and cutting planes: A study of proof systems for pseudo-Boolean SAT solving. In Proc. 21st Conf. Theory Appl. Sat. Testing (SAT 18), 2018. To appear.

Proceedings of the Twenty-Seventh International Joint Conference on Artiﬁcial Intelligence (IJCAI-18)