Core-Guided Linear Programming-Based Maximum Satisfiability

OLL is an algorithm for solving MaxSAT that belongs to a class of iterative SAT-based algorithms known as core-guided. It was introduced by Andres et al. [1] in the context of ASP and adapted to MaxSAT by Morgado et al. [19]. Its pseudocode is shown in Algorithm 1.

OLL optimistically tries to find a solution with 0 cost at each iteration, by asking a SAT solver to solve the CNF instance that results from setting all literals in the objective function to false (line 5). If that succeeds, this is optimal and it returns in line 7. If it fails, it extracts a core from that formula and uses it to increase the lower bound by $c^i$, the minimum cost of any variable in the core (line 8). It then reformulates the instance in line 9 so that each feasible assignment of $F$ has its cost reduced by exactly $c^i$ in $F^{i+1}$. The reformulation involves introducing new variables in the objective function, modifying the costs of existing variables, as well as building a subformula $f_{\mathrm{OLL}}^i$ which logically defines the new variables. As long as the reformulation step is correct, OLL increases the lower bound at each iteration, hence it is guaranteed to eventually reach the true optimum and terminate.

In order to avoid confusion between cores of the original formula and cores of the reformulated formulas - which can be different - we follow [22] and refer to cores of $H\cup f_{\mathrm{OLL}}^i$ as metas.

We complete the description of OLL with a description of the reformulation step. Let the meta at iteration $i$ be $m^i=\{x_1^i,x_2^i,\mathrm{\dots },x_{k^i}^i\}$. By the definition of ${F^i\mid }_{w=0}$, all literals that appear in $m^i$ have positive cost. We abuse notation and write $w^{i-1}(m^i)={\min }_{x\in m^i}{w}^{i-1}(x)$ for the minimum cost among the literals that appear in $m^i$. OLL increases the lower bound by $w^{i-1}(m^i)$ and introduces sum variables, defined as $o_j^i\iff {\sum }_{x\in m^i}\ge j$ for $2\le j\le k^i$. Finally, it reduces by $w^{i-1}(m^i)$ the cost of all literals in $m^i$ and sets to $w^{i-1}(m^i)$ the cost of the positive literals of all $o_j^i$. Formally,

To see why this is a reformulation, observe that we can combine the fact that ${\sum }_{x\in m^i}x\ge 1$ with the definition of the sum variables to get

because when $d$ of the $k^i$ variables in $m^i$ are true, exactly the $d-1$ sum variables $o_2^i,\mathrm{\dots },o_d^i$ will be true, by their definition. To complete the reformulation, we multiply equation (1) by $w^{i-1}(m^i)$ and replace its left-hand side in $w^{i-1}$ by its right hand side, which gives $w^i$. Note that this differs from the usual proof of correctness of OLL, but is useful to better understand the new algorithm OL³P.

Linear programs are problems of the form $\min c^{T}x:Ax=b\wedge x\in {ℝ}_{\ge 0}^n$, where $x$ is a vector of $n$ real (rational) valued variables, $c\in {ℝ}^n$, $b\in {ℝ}^m$ and $A\in {ℝ}^{m\times n}$. The problem can be solved in polynomial time. We restrict our attention here to the case where $x\in {[0,1]}^n$.

This form of linear programs, where all constraints are equalities, is called the augmented form. It is possible to convert any linear program which includes inequalities by introducing slack variables. For example the constraint $a^{T}x\ge b$ becomes ${\left[a-1\right]}^T[xs]=b$, where $s$ is a fresh variable and is the slack variable of this constraint.

For each linear program $P$ (called the primal), we can define a dual problem $D(P)$, which is $\max b^{T}y:A^{T}y\le c\wedge y\in {ℝ}^m$, where $y$ is a vector of $m$ real variables, called the dual variables or dual multipliers. An important theorem in linear programming is strong duality: the optima of $P$ and $D(P)$ are exactly the same. In fact, for every feasible solution $y$ of $D(P)$, its cost is a lower bound on the optimum of $P$.

There exists a correspondence between variables of the primal and constraints of the dual. Indeed, the $i^{\text{th}}$ column of $P$ contains the coefficients of the $i^{\text{th}}$ primal variable and also describes the $i^{\text{th}}$ dual constraint. From each dual solution $y$, we can define the reduced cost of each primal variable, $r{c}^y(x)$. This is the slack of the corresponding dual constraint, i.e., $c_i-A_i^{T}y$. The theorem of complementary slackness states that for every pair of optimal solutions $x,y$, it holds $x_i(c_i-A_i^{T}y)=0$, i.e., if the reduced cost of x is non-zero, then $x$ must be 0 in the primal and vice versa.

Reduced costs are used typically for reduced cost fixing when the linear program is a relaxation of a discrete optimization problem. For a given dual solution $y$, $c^{T}y+c_i-A_i^{T}y$ is a lower bound on the cost of any solution that assigns $x_i$ a non-zero value. If that matches or exceeds the cost of an incumbent solution of the discrete problem, we can fix $x_i$ to 0. By convention, if a variable is fixed to its 1 in the primal, its reduced cost is non-positive and $c^{T}y-c_i+A_i^{T}y$ is a lower bound on the cost of any solution that assigns $x_i$ less than 1 ²²2Negative reduced costs are not true reduced costs. The would imply negative slack of the corresponding dual constraint, which means a non-feasible dual solution. Instead, they are the negated reduced cost of a slack variable and LP solvers use this convention to avoid exposing this slack variable..

In the case of augmented form linear programs, we can make a stronger statement on reduced costs: for any feasible $y$, the function $b^{T}y+{(r{c}^y)}^{T}x$ is equal to $c^{T}x$ in every feasible point of the primal. We can therefore reformulate $P$ using the reduced costs. We give an elementary proof of this fact below.

MaxHS [9], an implicit hitting set solver, which encodes the optimization part of MaxSAT as an integer linear program (ILP), makes extensive use of seeding. Given a MaxSAT formula $F=⟨H,w⟩$, before it enters the main loop, MaxHS looks for clauses $c\in H$ which contain only literals of variables that appear in the objective. Then, it adds $c$ to the ILP representation of the problem it solves. In addition, when there is a small number of additional variables that must be added to the ILP in order to give it some clauses, MaxHS adds those variables and corresponding clauses. While this may make the ILP larger and hence more difficult to solve, it can also provide useful information which improves both the bounds and the efficiency of the ILP solver.

We can do the same with OL³P. However, where MaxHS can simply add clauses to the ILP problem it maintains, we are restricted to having LPs in augmented form. Hence, when we find a clause $c$ that is suitable for seeding, we add $L{P}_{\mathrm{OLL}}(c)$ to $L{P}^0$. The problem with this is that, while in MaxHS adding a clause to the ILP is just a single constraint, in OL³P we need to add 4 times as many non-zeros and introduce $2|c|-1$ new variables. This encoding has to be mirrored on the SAT side. However, only a relatively small number of constraints get a non-zero dual multiplier. Even if the LP and SAT solvers can determine that all the extra variables that appear in constraints with 0 dual multiplier are redundant, it still increases preprocessing time.

We can do better than that by reconsidering the proof of theorem 1. We can see that it is not necessary for the LP to have all constraints in the form $Ax=b$. Indeed, suppose that an LP has both equality constraints $Ax=b$ and inequality constraints $A^{\prime }x\ge b^{\prime }$ and suppose that the dual multiplier of every constraint in $A^{\prime }$ is 0. Then we can rewrite equation (2) as follows:

But since $y$ assigns 0 to the multiplier of every constraint in A’, we have $A_{}^{\prime }{}_{}{}^{T}y=0$ and the proof proceeds as before.

This allows us to make a simple but important optimization in seeding: when we initially seed the LP, we can leave all clauses as inequality constraints. This reduces the total number of variables in the LP and removes the need to add the corresponding sum constraints on the SAT side. When we actually solve an LP and find an inequality with non-zero dual multiplier, we can convert it to an equality, add all the necessary slack variables and corresponding sum constraint on the SAT side, then reuse the same dual solution to continue execution. But the number of constraints with non-zero dual multiplier is typically much smaller than the entire set of constraints. For instances where we can seed many or even all the initial clauses of the problem, this technique can represent significant savings.

Algorithm 2 is presented as extracting reduced cost-based metas at each iteration. As our argument in section 3.1 showed, however, the correctness of the algorithm does not depend in any way on the specific type of constraints. To this end, recall that when viewed as an ILP, $L{P}_{\mathrm{OLL}}$ encodes a hitting set problem over a set of cores derived from the metas discovered so far [17]. Hence, if we solve this minimum hitting set problem, we get a new source of cores. These cores are easier to discover than the metas discovered by the main OL³P loop.

Unfortunately, in early experiments, CPLEX proved to be very poor at solving $IL{P}_{\mathrm{OLL}}$, the integer version of $L{P}_{\mathrm{OLL}}$. Even in cases where the optimum of the LP matches the optimum of the ILP, CPLEX struggles to find the optimum solution. Exploring this direction further remains future work.

As mentioned earlier, reduced cost fixing is a technique that is widely used in ILP solving, as well as in constraint programming [13] and in MaxHS [4]. In the literature of core-guided solvers, the closest analogue is hardening [15]. In particular, if we use exactly the potentially suboptimal dual solutions described previously [17] that simulate OLL, reduced cost fixing is exactly equivalent to hardening. Here, we use an optimal solution, which means we can potentially fix more variables. Note, however, that finding optimal reduced costs is itself a non-trivial problem [8].

There are two considerations for using reduced cost fixing with OL³P. First, note that a practical implementation of OL³P must implement techniques like stratification and weight-aware core extraction (covered in later sections). These split the execution of the solver into distinct phases of core (meta) extraction, each of which finishes with a satisfiable instance, generating a solution, hence an upper bound. This enables reduced cost fixing in the first place. However, it is now no longer necessary that the execution of the solver finishes with a SAT instance.

A second consideration is that, knowing the specific relationship among the variables $o_2^i,\mathrm{\dots },o_{k^i}^i$, we can compute better reduced costs. Consider $o_3^i$ for some $i$. When that is true, it implies also $o_2^i$, therefore we incur the cost of the reduced cost of both $o_2^i$ and $o_3^i$. In other words, the true marginal cost of $o_3^i$ is $mc(o_3^i)\ge r{c}^y(o_2^i)+r{c}^y(o_3^i)$. This generalizes to all indices of a sum. In preliminary experiments, we found that this technique can be very effective in fixing a large number of sum variables, but ends up hindering the performance of the SAT solver. We therefore do not use this technique in section 4.

Stratification [15, 2] is a technique for improving solving of instances with diverse sets of costs. It splits variables of the objective into buckets, such that the higher the bucket index, the smaller the cost of the variable. It then solves the instance ignoring all but the first bucket of variables, i.e., treating all the other variables as if they have reduced cost 0. When that finishes, it adds variables from the next bucket and so on.

Stratification is that much more important for OL³P. The dual solution is not guaranteed to yield integer reduced costs and in fact there typically exist many variables with very small reduced cost. Without stratification, OL³P will be left to find metas with very small cost and make slow progress towards the optimum.

In addition, we implement rank-based stratification. We define the rank of an original variable of the instance to be $rank(x)=0$. For all sum or equality variables corresponding to meta $m^i$, let $r$ be the maximum rank among all $x\in m_i$. Then we set $rank(o_j^i)=rank(e_j^i)=r+1$ for $j\in [2,k^i]$. For each cost-based bucket, we first extract all metas involving variables of rank 0, then 1, and so on. Note that metas of rank 0 are cores of the original formula.

The reasoning for this heuristic is that the higher the rank of the variables in a core, the harder it is for the SAT solver to discover, hence we want to extract the easier cores first.

We implemented OL³P as an alternative algorithm on top of MaxHS ³³3https://github.com/gkatsi/OLLLP. We evaluate two variants. The first, OL³P, implements the base algorithm OL³P shown in Algorithm 2, with rank-based stratification, reduced cost fixing, weight aware cost extraction, and seeding as described in section 3.1. The second, OL³P-S is the same but performs no seeding. This variant is the closest to base OLL, as the only major difference is that it uses LP for reformulation. Both variants use IBM CPLEX version 22.1.1.0 to solve the LP and CaDiCaL version “sc-2021” as a SAT solver. The ILP solver of CPLEX is not used. Additionally, both variants use the MaxPRE preprocessor [18].

We compare against CashWMaxSAT version “DisjCom-S6” [23], the winner of the 2024 MaxSAT evaluation in the weighted track. By default, CashWMaxSAT uses a portfolio strategy whereby, before launching OLL, it gives an instance to the SCIP ILP solver [7] and lets it run for some time. Only if SCIP does not solve the instance, does it execute the OLL algorithm. On the other hand, it does not use MaxPRE by default. We tested four configurations of CashWMaxSAT, varying the use of this feature and the use of MaxPRE:

1. 1.

   As run in the 2024 evaluation, where the SCIP timeout is 600 seconds

2. 2.

   As above, but with the SCIP timeout set to 300 seconds to match the lower timeout we used (see below)

3. 3.

   With SCIP disabled, but using MaxPRE

4. 4.

   Without either SCIP or MaxPRE

The latter two are more directly comparable to OL³P-S, as they are not portfolios. They all use CaDiCaL version 2.0.0 as a SAT solver.

Finally, we compared against MaxHS, in its configuration from the 2022 MaxSAT evaluation, which is the last time it participated, using IBM CPLEX version 22.1.1.0 to solve the ILP and CaDiCaL version “sc-2021” as a SAT solver. MaxHS is also a portfolio solver. When the number of soft clauses is relatively small, it launches LSU instead. When the problem is small or the number of variables that do not appear in soft clauses is small, it delegates to CPLEX.

We compare the solvers on the instances from the weighted track of the 2024 MaxSAT evaluation. We ran all solvers for 1800 seconds of CPU time on a cluster of 14-core Intel Xeon E5-2695 v3 CPUs running at 2.30GHz.

Surprisingly, the four different configurations of CashWMaxSAT varied little in their performance, solving 405, 409, 410, and 406 instances, respectively. It is possible that the shorter timeout compared to the evaluation made the portfolio ineffective. We retained configurations 2 and 3, as those exhibiting the best performance.

We show in Figure 1 a plot of the relative performance of the four solvers. Comparing only the core-guided solvers, we see that even though the solvers end at similar numbers of solved instances, both variants of OL³P-S are better than CashWMaxSAT. We give a more detailed breakdown of the number of instances solved by family in Table 1. We see that most of the gains of OL³P come from the judgement-aggregation family. There, the seeded LP computes a near optimum bound, then it takes just a few iterations to find the optimum solution and prove optimality. In OL³P-S and CashWMaxSAT, this information is not available and they make slow progress, ending with a significant optimality gap. In the rest of the families, OL³P sometimes exhibits a small advantage, but not consistently.

We also give in Table 2 the average time needed to solve instances (ignoring instances that timed out), as well as the PAR2 score of each solver (the sum of the runtimes over all instances, with instances that timed out or ran out of memory counting as twice the timeout, hence 3600 here). We see that both OL³P-S and OL³P have significantly reduced average solving time and lower PAR2 compared to CashWMaxSAT. This means that, not only does OL³P solve more instances, it does so more quickly on average. The CashWMaxSAT +SCIP configuration does particularly poorly in these metrics because of the sequential portfolio it uses: for every instance that SCIP is unable to solve, it pays a penalty of 300 seconds. These observations are confirmed in the scatter plots in Figure 2. However, these plots additionally show that no solver dominates another, as there exist several instances that are solved by only one solver in each pair.

In comparison to MaxHS, all core-guided solvers perform worse overall. However, in some families, like judgement-aggregation and warehouses, OL³P reduces the performance gap. Additionally, the average solving time of both OL³P-S and OL³P is signficantly lower in solved instances where it does prove optimality, although this is not sufficient to cover the gap in PAR2 score caused by the difference in number of instances solved.

A natural question for both OL³P-S and OL³P is on the overhead of LP solving, since we replace the very cheap reformulation procedure of OLL by solving an LP. For OL³P-S, this overhead is negligible. The solver spent just 16s solving the LP over the entire set of solved instances. The maximum amount of time spent in the LP solver in any one instances was just 1.15 s. In only 3 instances was the LP solver time more than 1 second, and they all were instances where the total time to solve them was more than 300 seconds. For OL³P, the overhead is much greater. Cumulatively, OL³P spent 8163.91 seconds in the LP solver (25 seconds per solved instance on average). The maximum amount of time in the LP solver in any one instance was 1343 seconds. The judgement-aggregation instances consume most of that time, with 4 of them spending more than 1000 seconds in the LP solver, each. Part of the reason for this overhead is that the current implementation is not particularly careful to be efficient with its use of the LP solver. These results suggest that more attention should be given to this, especially if other sources of constraints are used to populate the LP. Techniques like column and row generation can also speed up LP solving.