The extension of conflict-based learning from Propositional Satisfiability (SAT) solvers to Pseudo-Boolean (PB) solvers comprises several different learning schemes. However, it is not commonly agreed among the research community which learning scheme should be used in PB solvers. Hence, this paper presents a contribution by providing an exhaustive comparative study between several different learning schemes in a common platform. Results for a large set of benchmarks are presented for the different learning schemes, which were implemented on bsolo, a state of the art PB solver.
In a propositional formula, a literal l j denotes either a variable x j or its complement x¯ j. If a
literal l j = x j and x j is assigned value 1 or l j = x¯ j and x j is assigned value 0, then the literal is
said to be true. Otherwise, the literal is said to be false. A pseudo-Boolean (PB) constraint is
defined as a linear inequality over a set of literals of the following normal form:
such that for each j 2 f1; ; ng, a j 2 Z+ and l j is a literal and b 2 Z+. It is well-known that
any PB constraint (with negative coefficients, equalities or other inequalities) can be converted
into the normal form in linear time [
In a given constraint, if all a j coefficients have the same value k, then it is called a cardinality constraint, since it requires that dbi=ke literals be true in order for the constraint to be satisfied. A PB constraint where any literal set to true is enough to satisfy the constraint, can be interpreted as a propositional clause. This occurs when the value of all a j coefficients are greater than or equal to b.
An instance of the Pseudo-Boolean Satisfiability (PB-SAT) problem can be defined as finding an assignment to the problem variables such that all PB constraints are satisfied. 2.1
Boolean Constraint Propagation (BCP) [
lj6=0 If aumax > s then w is a unit constraint and literal lmuax must be assigned value 1. Notice that given the same partial assignment, more than one literal can be implied by the same PB constraint.
During the search, let x j = vx@k denote the assignment of vx to variable x j at decision level k. In the following sections we often need to associate dependencies (or an explanation) with each implied variable assignment. Dependencies represent sufficient conditions for variable assignments to be implied. For example, let x j = vx be a truth assignment implied by applying the unit clause rule to w. Then the explanation for this assignment is the set of assignments associated with the false literals of w. 2.2
It is well-known that the fundamental operation used to infer new constraints using
propositional clauses is resolution [
If c or c0 is non-integer, a new constraint with non-integer coefficients may result after applying the cutting plane operation. In order to obtain a new constraint with integer coefficients, the rounding operation can be applied as follows: It should be noted that the rounding operation might weaken the constraint such that the number of models of the resulting constraint is larger. For example, suppose we have the constraint w : 2x1 + x2 + x3 3. Applying a coefficient c = 0:5 to w we get a new constraint w0: c(å j a jx j c0(å j a0jx j b) b0) c å j a jx j + c0 å j a0jx j
cb + c0b0 å j a jx j å jda jex j b dbe w0 : x1 + 0:5x2 + 0:5x3
1:5 Applying the rounding operation to w0 results in a new constraint wr0 : x1 + x2 + x3 2. Clearly, all models of w0 are also models of wr0, but not all models of wr0 are models of w0.
Another operation that can be used on PB constraints is reduction [
Consider the constraint w : x1 + 3x2 + 3x¯3 + 2x¯4 + x5 7. If reduction is applied to w in order to remove x1 and x¯3, we would get w0 : 3x2 + 2x¯4 + x5 3. Note that if w is a problem instance constraint, it is not possible to replace w with w0. Constraint w0 is a logical consequence from w, but the converse is not true.
Algorithms to generate cardinality constraints from general pseudo-Boolean constraints can
be found in [
Generally, pseudo-Boolean satisfiability (PB-SAT) algorithms follow the same structure as propositional satisfiability (SAT) backtrack search algorithms. The search for a satisfying assignment is organized by a decision tree (explored in depth first) where each node specifies an assignment (also known as decision assignment) to a previously unassigned problem variable. A decision level is associated with each decision assignment to denote its depth in the decision tree.
Algorithm 1 shows the basic structure of a PB-SAT algorithm. The decide procedure
corresponds to the selection of the decision assignment thus extending the current partial
assignment. If a complete assignment is reached, then a solution to the problem constraints has been
found. Otherwise, the deduce procedure applies Boolean Constraint Propagation (and
possibly other inference methods). If a conflict arises, i.e. a given constraint cannot be satisfied by
extending the current partial assignment, then a conflict analysis [
The main goal of the conflict analysis procedure is to be able to determine the correct explanation for a conflict situation and backtrack (in many cases non-chronologically) to a decision level such that the conflict does no longer occur. Moreover, a no-good constraint results from this process. However, the strategy for no-good generation that results from the conflict analysis differs between several state of the art PB-SAT solvers. These different strategies are reviewed and analysed in section 4.
Another approach to PB-SAT is to encode the problem constraints into a propositional
satisfiability (SAT) problem [
return UNSATISFIABLE; else
backtrack(blevel); end if end while else
return SATISFIABLE; end if end while 4
Consider that the assignment of a problem variable x j is inferred by Boolean Constraint
Propagation due to a PB constraint wi. In this case, wi is referred to as the antecedent constraint [
The implication relationships of variable assignments during the PB-SAT solving process
can be expressed as an implication graph [
When a logical conflict arises, the implication sequence leading to the conflict is analysed to
determine the variable assignments that are responsible for the conflict. The conjunction of
these assignments represents a sufficient condition for the conflict to arise and, as such, its
negation must be consistent with the PB formula [
When an assignment to a problem variable x j is implied by a PB constraint wi, one can see
it as the conjunction of Awi (x j) implying the assignment to x j. Moreover, when a constraint
implies a given assignment, the coefficient reduction rule can be used to eliminate all positive
and unassigned literals except for the implied literal. Hence, the conflict analysis used in SAT
solvers by applying a sequence of resolution steps in a backward traversal of the implication
graph can be directly applied to PB formulas [
In the last pseudo-Boolean solver evaluation, some PB solvers used this approach, namely
bsolo [
The use of PB constraint learning is motivated by the fact that PB constraints are more expressive. It is known that a single PB constraint can represent a large number of propositional clauses. Therefore, the potential pruning power of PB conflict constraints is much larger than that of propositional clauses.
The operation on PB constraints which corresponds to clause resolution is the cutting plane
operation (section 2.2). As such, to learn a general PB constraint, the conflict analysis algorithm
must perform a sequence of cutting plane steps instead of a sequence of resolution steps. In
each cutting plane step one implied variable is eliminated. As with the clause learning conflict
analysis, a backward traversal of the implication graph is performed and the implied variables
are considered in reverse order. The procedure stops when the conflict constraint is unit at a
previous decision level (1UIP cut) [
After the conflict analysis, the algorithm uses the learned constraint to determine to which level it must backtrack as well as implying a new assignment after backtracking. Therefore, the learned constraint must be unsatisfied under the current assignment. Moreover, it must also be an assertive constraint (must become unit after backtracking).
Consider the application of a cutting plane step to two arbitrary constraints w1 with slack
s1 and w2 with slack s2. Moreover, consider that a and b are used as the multiplying factors.
In this situation, the slack of the resulting constraint, here denoted by sr, is given by linearly
combining the slacks of w1 and w2: sr = (a s1) + (b s2). As such, before the application of each
cutting plane step, the learning algorithm verifies if the resulting constraint is still unsatisfied
under the current assignment. If it is not, the implied constraint must be reduced to lower its
slack [
Algorithm 2 presents the pseudo-code for computing the conflict-induced PB constraint w(k). This algorithm performs a sequence of cutting plane steps, starting from the unsatisfied constraint w(c). Notice that this algorithm can also implement a clause learning scheme. In this case, functions reduce1 and reduce2 remove all non-negative literals in w(k) and wi, respectively, except for the implied literal. Next, these procedures can trivially reduce the obtained constraint to a clause. In order to implement a general PB learning scheme, function reduce2 must eliminate only enough non-negative literals in wi to guarantee that after the cutting plane step, the resulting constraint remains unsatisfied at the current decision level. 4.3
Learning general PB constraints slows down the deduction procedure because the watched
literal strategy is not as efficient with general PB constraints as it is with clauses or cardinality
constraints [
The approach for cardinality constraint learning used in Galena [
V V n fx jg [ fxk j xk corresponds to a false literal in wi0 at current decision levelg else w(k) reduce3(w(k)); Add w(k) to W ; btLevel assertingLevel(w(k)); if btLevel < 0 then
return CONFLICT; else backtrack(btLevel); return NO CONFLICT; end if end if end while post-reduction procedure is carried out so that the learned constraint is reduced into a weaker cardinality constraint. In Algorithm 2 this would be done in function reduce3.
Finally, a hybrid learning scheme was already proposed and used in Pueblo [
In implementing a pseudo-Boolean solver, several technical issues must be addressed. In this section the focus is on generating the implication graph and on the use of cutting planes for PB constraint learning. 5.1
It is widely known that lazy data structures [
When generating the implication graph in a breadth-first way, one can guarantee that there is no other possible implication graph such that the length of the longest path between the decision assignment vertex and the conflict vertex is lower than the one considered. Therefore, the learned constraint is probably determined using a smaller number of constraints. Moreover, considering that in PB formulations the same constraint can imply more than one variable assignment, the motivation for a breadth-first propagation is larger than in SAT formulations. 5.2
When performing general PB Learning or any learning scheme that requires performing a sequence of cutting plane steps each time a conflict occurs, the coefficients of the learned constraints may grow very fast. Note that in each cutting plane step two PB constraints are linearly combined. Given two constraints: å j a j l j b and å j c j l j d, the size of the largest coefficient of the resulting constraint may be maxfb d; max jfa jg max jfc jgg in the worst case. Therefore, it is easy to see that during a sequence of cutting plane steps the size of the coefficients of the accumulator constraint may, in the worst case, grow exponentially in the number of cutting plane steps (which is of the same order of the number of literals assigned at the current level).
One problem that may occur in the cutting plane operation is integer overflow. To avoid this problem, a maximum coefficient size was established (we used 106). Therefore, every time the solver performs a cutting plane step, all coefficients of the resulting constraint are checked if one of them is bigger than the established limit. If it is, the solver repeatedly divides the constraint by 2 (followed by rounding) until its largest coefficient is lower than a second maximum coefficient size (we used 105).
During the conflict analysis the accumulator constraint must always have negative slack. However the division rule does not preserve the slack of the resulting constraint, since it does not guarantee that the slack of the resulting constraint is equal to the slack of the original one, which can be verified in the next example where the constraint is divided by 2, followed by rounding: 5 slack = 3 slack = 0 1 As such, before dividing by 2 a coefficient associated with a slack contributing literal, the solver must check if it is odd. In this case it must perform a coefficient reduction step before the division (note that the coefficient reduction rule when applied to slack contributing literals preserves the slack).
3x1(0@1) + 3x2(0@1) + 3x3(1@1) + x4(1@1) 5 slack = 3x1(0@1) + 3x2(0@1) + 2x3(1@1) 3 slack = 1 2x1(0@1) + 2x2(0@1) + x3(1@1) 2 slack = 1 1 5.3
After implementing different learning schemes, it was observed that each of the versions proved to be more effective than the others for some group of instances. One can easily conclude that different learning schemes behave better (or worse) depending on some characteristics of the instances given as input. For instance, a cardinality constraint learning scheme is more appropriate to deal with an instance with a large number of cardinality constraints than a clause learning scheme.
Our goal was then to try to define an initial classification step that could choose the best
fitting learning scheme to solve a given problem instance. Therefore, in a very preliminary
work, algorithm C4.5 [
This section presents the experimental results of applying different learning schemes to the
small integer non-optimization benchmarks from the PB’07 evaluation [
In Table 1, results for several learning schemes are presented. Each line of the table represents a set of instances depending on their origin or encoded problem. Each column represents a version of bsolo for a different learning scheme. Finally, each cell denotes the number of benchmark instances that were found to be satisfiable/unsatisfiable/unknown.
The basis for our work was the bsolo version submitted to PB’07 solver evaluation. This version implements a clause learning scheme and is identified with CL1. Version CL2 corresponds to the previous version, but with a breadth-first approach for generating the implication graph. Next, results for the general PB learning scheme PB and cardinality learning scheme CARD are presented. One should note that both the PB and CARD learning schemes are hybrid (as in Pueblo) and always learn an assertive clause. Preliminary results on pure PB and cardinality learning schemes were not as effective as an hybrid learning scheme. In version COMB, an initial classification step was used in order to select the best fitting learning scheme for each instance (see section 5.3). The training set for the COMB version was composed of 100 instances (out of the total of 371 instances).
It can be observed from Table 1 that the original solver was greatly improved just by changing the propagation order. Version CL2 was able to solve more 17 instances, most of them in the tsp benchmark set. Both the PB and CARD learning schemes improve on the original version of the solver. However, in the PB version, the overhead associated with maintaining the additional no-good PB constraints is a drawback, in particular on the FPGA and pigeon hole instances. Overall, the CARD learning scheme performs much better, proving to be a nice compromise between pruning power of the generated constraints, and the underlying overhead of constraint manipulation. Finally, the COMB version shows that a combination of all these learning schemes allows an even better performance. Finally, one should note that improvements are essentially on unsatisfiable instances. The gain on satisfiable instances is smaller.
In Table 2, the results of the best known solvers can be checked and compared with bsolo. Pueblo is able to solve 6 more instances than the current version of bsolo. By using a hybrid learning scheme, Pueblo seems to have found a nice balance between the additional overhead of new no-good constraints (mostly clauses) and the pruning power of new no-good PB constraints. Nevertheless, the work presented in this paper shows that bsolo can be competitive in a large set of problem instances.
In the Pseudo-Boolean Optimization (PBO) problem, the objective is to find an assignment
such that all constraints are satisfied and a linear cost function is optimized. PB solvers can
be easily modified [
Considering the disparity of results concerning the application of learning schemes in several state of the art PB solvers, the main goal of this work is to provide a contribution by implementing them in the same platform. Our results confirm that hybrid learning schemes perform better on a large set of instances. Moreover, our results show that cardinality constraint learning is more effective and robust learning scheme than others. It obtained much better results than the original clause learning scheme and also on our implementation of the PB hybrid learning scheme included in Pueblo. In our opinion, cardinality constraints are easier to propagate than PB constraints and are also more expressive than clauses. Therefore, this learning scheme seems a reasonable compromise between PB learning and pure clause learning.