A key challenge in pseudo-boolean solving is the eficient detection and processing of unit literals. In SAT solving this is done by using the watched literal scheme, but for general pseudo-boolean constraints there is no dominant method. This paper introduces the significant literal framework to generalize existing watched literal schemes for pseudo-boolean solvers, which is implemented in a modification of the RoundingSAT solver. For this modification, small improvements can be observed on the instances from the decision and optimization tracks of the 2024 Pseudo-Boolean Competition, and a substantial improvement in instances with large coeficients like Knapsack.
Contemporary satisfiability (SAT) solvers achieve eficiency by conflict driven clause learning (CDCL) and unit propagation, making them a powerful tool for boolean problems like model checking in chip development, formal software verification and scheduling problems. On the other hand, Integer Linear Programming (ILP) solvers use integer relaxation and the branch-and-cut procedure to dominate in industrial applications including production planning, network optimization and portfolio selection. Pseudo-boolean solving has emerged as a promising middle ground between the two approaches, aiming to combine the advantages of both methods. SAT methods like unit propagation and conflict analysis are now applied to the powerful cutting plane system underlying ILP solvers.
However, neither unit propagation nor conflict analysis can be generalized to arbitrary
pseudoboolean constraints without careful considerations. The latter received significant attention, with
various papers discussing diferent methods of constructing conflict constraints [
This paper aims to demonstrate that the watched literal scheme of RoundingSAT can be further
improved by introducing significant literals, which are especially efective for constraints with large
coeficient sizes. Our approach uses a tighter upper bound by finding the maximum coeficient of
unassigned significant literals, but keeps the fixed upper bound as in Devriendt’s scheme [
We give a detailed description of the algorithm behind the significant literal approach in section 3, and then in section 4 present performance comparisons with the current RoundingSAT implementation across various datasets.
A pseudo-boolean problem consists of variables ∈ {0, 1}, with literals representing either or := 1 − and pseudo-boolean constraints of the form ∑︀=1 ≥ for , ∈ N.
Without loss of generality we will assume that the coeficients are in descending order, so ∀ : ≥ +1. A cardinality constraint is a pseudo-boolean constraint with ∀ : = 1. If additionally = 1, the constraint is a clause.
We denote the current (partial) assignment of the variables with , identified with the set of literals set to 1. The slack of a pseudo-boolean constraint with the current assignment is defined as (, ) = − + ∑︀∈/ .
Informally, the slack represents the amount by which the left-hand side can exceed the right-hand side without unassigning literals. Thus, if (, ) < 0, the constraint can not be satisfied with , and we need to backtrack.
A literal is called a unit literal, if (, ) < . This means that must be set to 1 in order to satisfy the constraint , as otherwise (, ∪ {}) < 0.
For a pseudo-boolean constraint we denote its watched literals with (), a subset of its nonfalsified literals, i.e. () ⊆ { ∈ : ∈/ }. Note that () depends on the current assignment . The maximum coeficient of a constraint is defined as := max{ ∈ : , ∈/ }. If all literals of are assigned, we define it as = 0.
The watch slack is the slack restricted to (): (, ) = − + ∑︀∈ () . By definition (, ) ≤ (, ) holds.
Lemma 1. contains a unit literal if and only if no watched literals set () exists such that (, ) ≥ .
Proof. If contains a unit literal, then by definition we have an unassigned literal with (, ) < and ≥ . So we arrive at ≥ > (, ) ≥ (, ). Thus, no watched literal set () with (, ) ≥ can exist.
If for all sets of literals () we have (, ) < , this also holds true for () = { | ∈/ }, i.e. if we watch all non-falsified literals. In that case we have (, ) = (, ), leading us to (, ) < , and therefore the literal corresponding to must be unit.
If we replace with an upper bound, a weaker version of Lemma 1 still holds: Lemma 2. Let be an upper bound, i.e. ≥ . If contains a unit literal, then no watched literals set () exists such that (, ) ≥ .
Proof. By Lemma 1 we know that if contains a unit literal, then we can not choose watched literals () such that (, ) ≥ . Since ≥ , this immediately implies that we also can not find () with (, ) ≥ .
The problem of using Lemma 1 as a criterion for finding unit literals is that needs to be known
for all constraints. So every time a variable is assigned or unassigned, we have to update in all
constraints that contain or . This procedure can take up to two thirds of the total unit propagation
runtime [
RoundingSAT instead uses a criterion based on Lemma 2 with = 1 [
The idea behind significant literals is finding a middle ground between always updating and replacing it with a constant upper bound. For that we choose an arbitrary criterion determining if is significant for a constraint . We denote the set of all significant literals for with (). Since the criterion does not depend on , () is constant.
Now we define := max{ ∈ : , ∈/ ∨ ∈/ ()}, i.e. is the largest coeficient of a literal which is either unassigned or not significant. As with , if all literals are assigned and significant, we simply define = 0. By definition ≥ , so we can apply Lemma 2 with = .
This framework generalizes the two previously mentioned methods. If we choose a significance
criterion which declares all literals as significant, we have = and recover the method which
calculates for all constraints. If we instead declare no literal to be significant for any constraint,
we have = 1 and recover the current method in RoundingSAT [
To elaborate what significance criteria are useful, we look at the following “worst case” constraint for the current RoundingSAT unit propagation system: 100 + ∑︀1=001 ≥ 10.
Starting with = ∅, we have 1 = = 100 and (, ) = 190. Then the implementation iteratively adds watched literals until (, ) ≥ 100, which results in () = {, 1, . . . 10}. If the next decision of the solver is = {}, all 100 literals will be added to () without achieving (, ) ≥ 100. This means that until the solver reverses the assignment of , the watched set () will be unnecessarily large, and no unit literal can exist until at least 90 of the variables are assigned.
When we instead use significant literals and a criterion which declares to be significant for the constraint, we only need (, ) ≥ 1 after = {}. This allows for the much smaller watched set () = {1, . . . 11}, which reduces the workload for updating the watched literal scheme in further assignments.
Here the diference between the two watched literal schemes is exaggerated, as the example constraint is deliberately chosen to amplify this problem. Simply choosing the equivalent constraint 10 + ∑︀1=001 ≥ 10 allows the current RoundingSAT implementation to watch only roughly twice as many literals as the significant literal approach. However, it still illustrates that the diference between the two watched literal schemes is mainly dependent on the size of the constraint coeficients. This will also be supported by empirical evidence in the following section.
Algorithm setSmax demonstrates how to set . to the value of . Here .[] is a reference to a literal occurring in , .[] denotes its corresponding coeficient, and size() denotes the number of literals in . We also count the number of backjumps which occurred so far with . In the while loop we search for an unassigned or non-significant literal, and finish immediately if we found one. Since the literals in are sorted by descending order of their coeficients, the first found literal is guaranteed to have the largest coeficient, and we have found .
To further optimize this procedure, we remember the index at which we left the loop in the last call
to setSmax. If no backtracking occurred in the meantime, no literals have been unassigned and so all
literals before are still assigned and significant. Thus, the first condition in algorithm setSmax ensures
that we only restart the search from the beginning if a backjump occurred. This idea is directly inspired
by the algorithm propagate first presented by Devriendt [
When we now assign a literal we check in each constraint in which it is significant, if its corresponding coeficient is equal to of that constraint. Only if that it is the case, we need to call algorithm setSmax to update the value. For unassigning we only need to check for each significant constraint if its corresponding coeficient is bigger than and if so set to its coeficient.
Now we need to integrate the new . into the unit propagation of RoundingSAT, which
consists of propagateOpt, processWatches and backjump [
However, one has to be careful which optimizations of propagateOpt are still logically sound for a non-constant . The first optimization can be kept, as the following lemma shows. Lemma 3. If no backtracking occurred, the while loops in line 7 and 19 can be restarted at the index where they left of in the last call, without changing the behaviour of the algorithm.
Proof. Without backtracking any literal assigned in at the last call to function propagate remain assigned. Thus, if is the index, where the while loop of line 7 left of, the literals 1, . . . − 1 either remain false or are already watched, and we can safely skip them.
Similarly, if the while loop of line 19 terminates with index , then all literals 1, . . . − 1 are already assigned. Without backtracking this still holds true now, and we can restart the search with index .
The second optimization, which skips the search for new watched literals if .wslk + .[] ≥ ., does not work for non-constant . The idea behind it is that if at some assignment the while loop of line 7 terminates because of the condition .wslk < ., all non-falsified literals are watched. Until we have backtracked so far that this specific assignment is reversed, all non-falsified literals remain watched, and any further search for new literals to watch will be unnecessary. However, with a non-constant further assignments can make it possible to fulfil (, ) ≥ , even if that was not possible at some past call. Thus, the optimization can only be applied if is constant in the constraint. In our case we simply check this when () = ∅, since we have = 1 if no literals are significant for a constraint.
We experiment with various significance criteria, which aim to identify literals where the increased
cost of updating is outweighed by allowing for a smaller watched literal set (). Let ∈ N be
a fixed cut-of value, and ∈ R a fixed scaling factor . We consider the following criteria, where the
literal with coeficient is significant for a constraint if:
Algorithm 2 propagate (constraint , integer ), modification of propagateOpt [
=2
It should be noted that for the latter two criterion always either all or none of the literals are declared to be significant, since the definition does not depend on . Additionally, each of the three criteria can also be restricted to only input constraints, which we will mark as “ input ∧ criterion” in the legends of runtime plots. If no criterion is specified, we simply define all literals in input constraints to be significant.
To perform the evaluation we use commit d34b6bed of the RoundingSAT solver, which is the latest
version as of December 2024 [
All runtime measurements are done without proof logging, although we verified all certificates of
an independent run using the VeriPB verifier [
Our first dataset will consist of the 398 selected instances of the DEC-LIN track in the
PseudoBoolean Competition 2024 [
Figure 1 demonstrates that the counting method is less eficient than the unit propagation by Devriendt
[
As shown in appendix A, the most successful criteria for DEC-LIN also perform well on the OPTLIN track in the Pseudo Boolean Competition 2024, which comprises a collection of 487 optimization problems. Here again, a small improvement compared to RoundingSAT can be observed.
Across both datasets we notice that unit propagation with significant literals works best when it is only applied to the input constraints and not to the learned constraints. Our explanation for this behaviour is the diference in the distribution of coeficient sizes as shown in Figures 2 and 3.
To produce Figure 2 we have collected all constraints in the selected instances of the DEC-LIN track, which are not clauses or cardinality constraints and group all their coeficients by absolute values in buckets. For Figure 3 we did the same for all learned constraints RoundingSAT on the dataset, but excluded instances which are not solved within the 3600 timeout.
We observe that coeficients in input constraints are far more unevenly distributed. Thus, can often be far smaller than 1, leading to a smaller and therefore less expensive watched literal set. On learned constraints with a more even distribution, remains similar to 1, thus the cost of updating outweighs the benefit of only marginally smaller watched literal sets.
While significant literals already yield a small improvement on general instances, they are substantially better if the instances mainly consist of constraints with large coeficients. One example are the 6 −111−01 − 1001 0.5 0 783 Knapsack instances submitted to the OPT-LIN track of the Pseudo Boolean Competition 2024, as Figure 4 shows.
The plot demonstrates that the two criteria clearly outperform the unmodified RoundingSAT solver, both in the number of instances solved and the general runtime of hard instances.
We further support this observation by looking at another application with large coeficient in the
benchmark dataset of the Pseudo Boolean Competition, the “Virtual Machine Consolidation” problem
[
It has been successfully demonstrated how significant literals can speedup unit propagation for pseudoboolean constraints. Especially for applications with a large average coeficient size we have observed a substantial improvement compared to the current RoundingSAT watched propagation scheme.
In addition, an avenue for future improvements is indicated by the observation that the performance
diferences between the watched literal schemes is mainly determined by the distribution of coeficients.
One possibility could be to select the significance criterion itself during the preprocessing step based on
the coeficients of the individual instance. Another improvement could be the adaptation of the logging
method developed by Robert Nieuwenhuis et al. [
This paper is based on the first author’s Master’s Thesis [
The authors have not employed any Generative AI tools.
The comparison for the OPT-LIN track of the Pseudo-Boolean Competition 2024 is shown in figure 6.
In figures 7 through 12, we compare the runtime of diferent significance criteria on the DEC-LIN instances of the Pseudo-Boolean Competition 2024.
R-SAT (213) input ∧ 1 > 100 (213) input ∧ 1 > 500 (213) input ∧ .1 > 5 · (.2 + .3) (212) .1 > 5 · (.2 + .3) (206)
input (214)
R-SAT input ∧ > 1 input ∧ > 10 input ∧ > 50 input ∧ > 100 input ∧ > 500 0 180 185 190 0 230 235 240 245 250
R-SAT input ∧ 1 > 10 input ∧ 1 > 50 input ∧ 1 > 100 input ∧ 1 > 500 3,500 3,000 2,500 0 230 235 240 245 250 3,500 3,000 2,500 1,000