Reduced Cost Fixing for Maximum Satisfiability

1 Introduction

Beyond its importance as a classical NP-hard optimization problem, maximum satisfiability (MaxSAT) is today a thriving constraint optimization paradigm, with successful applications in a range of real-world domains. The underlying declarative language of MaxSAT consists of conjunctive normal form (CNF) propositional formulas extended with weights assigned to individual clauses. The aim is to find an optimal truth assignment, i.e., one that maximizes the weight of satisfied clauses. Algorithmically, however, MaxSAT is typically treated as the equivalent problem of minimizing the weight (or cost) of falsified clauses.

The currently most successful exact MaxSAT solvers make iteratively use of Boolean satisfiability (SAT) solvers, either to extract unsatisfiable cores (unsatisfiable sets of soft clauses) or to extract truth assignments with ever-improving cost (e.g., [Koshimura et al., 2012]). Pure SAT-based solvers that extract cores (e.g., [Martins et al., 2014; Ans´otegui et al., 2015; Alviano et al., 2015; Morgado et al., 2014]) use these cores to modify the formula until eventually a formula is obtained that is satisfiable and whose satisfying truth assignments are optimal truth assignments for the original input formula. Implicit hitting set (IHS) solvers [Davies and Bacchus, 2011; Davies, 2013; Saikko et al., 2016a] also extract cores, but then use an integer programming (IP) solver to compute a minimum-cost hitting sets (MCHS) of the accumulated set of cores. If removing such a hitting set (which is a set of soft clauses) from the input formula makes the formula satisfiable, then the satisfying truth assignment must be an optimal truth assignment for the original input formula.

∗This is an abridged version of "Reduced Cost Fixing in MaxSAT" that won the CP 2017 Distinguished Paper Award. This work was financially supported by Academy of Finland (grants 251170, 276412, 295673, 312662) and DoCS Doctoral Programme in Computer Science, University of Helsinki.

The hybrid approach implemented in IHS solvers for MaxSAT opens up opportunities for making use of various proven IP solving techniques to further speed up MaxSAT solving. In this work we investigate utilizing the known IP technique of reduced cost fixing for this purpose.

In the context of MaxSAT, truth assignments found during solving provide an upper bound on the cost of an optimal truth assignment. Every MCHS of the cores on the other hand provides a lower bound. The linear programming (LP) relaxation of the MCHS problem thus also provides a lower bound. This LP can also be used to obtain a reduced cost for every soft clause ci. The reduced cost of ci specifies a minimum increase in the cost of the LP that would arise from falsifying (satisfying) ci which was satisfied (falsified) in the LP solution. If this cost increase makes the LP MCHS lower bound greater than the best known upper bound, we can conclude that ci must be fixed to its status in the LP solution; that is, ci must be falsified (satisfied) by any optimal truth assignment. This reasoning can be extended to cover the case where the increase in cost makes the lower bound equal to the upper bound. In this case, we know that fixing the status of ci preserves at least one optimal solution. Fixing the status of various soft clauses makes solving MaxSAT instances easier, as our empirical results demonstrate.

To facilitate the integration of reduced cost fixing, we present IHS search in terms of improving upper and lower bounds. To study the impact of reduced cost fixing for MaxSAT, we present results from an extensive empirical evaluation on the effect of integrating reduced cost fixing into the MaxHS IHS solver, showing that reduced cost fixing considerable speeds up this state-of-the-art MaxSAT solver.

In terms of related work, different techniques of using lower and upper bounds for speeding up MaxSAT solvers have been studied in varying contexts, including branch and bound for MaxSAT [Li et al., 2006; Lin and Su, 2007; Lin et al., 2008; Li et al., 2008], use of bounds for MaxSAT solvers in general [Heras et al., 2012], and hardening based on the costs of residual formulas in pure SAT-based coreguided MaxSAT solving [Ans´otegui et al., 2013; Morgado et al., 2012]. To the best of our knowledge, linear programming relaxation based reduced cost fixing has not been previously proposed in the context of MaxSAT. However, besides being a standard technique in IP solving [Wolsey, 1998; Danzig et al., 1954; Crowder et al., 1983; Nemhauser and Wolsey, 1999], there have been a number of recent works on exploiting reduced cost fixing in constraint programming, IP/constraint logic programming, and IP/constraint programming, e.g., [Thorsteinsson and Ottosson, 2002; Focacci et al., 1999; Yunes et al., 2010].

2 Maximum Satisfiability and Hitting Sets

An instance of (weighted partial) MaxSAT (Fh, Fs, wt) consists a set of hard clauses Fh, a set of soft clauses Fs, and weight function wt : Fs → R+. A MaxSAT solution τ is a truth assignment for the variables in Fh ∪ Fs that satisfies all clauses in Fh. The cost of a solution, cost(τ), is the sum of the weights of soft clauses not satisfied by τ . A MaxSAT solution τ ′ is optimal if it has minimum cost over all solutions, τ ′ ∈ argminτ(cost(τ)). A subset of soft clauses κ ⊆ Fs is an unsatisfiable core if the clauses in κ cannot be simultaneously satisfied by any solution.

A hitting set HS of a set of cores K is a set which contains at least one element of each κ ∈ K, i.e., HS ∩ κ ̸= ∅ for all κ ∈ K. A minimum-cost hitting set (MCHS) of K is a hitting set which minimizes ∑ci∈HS wt(ci) over all hitting sets HS of K. The optimal cost of a MaxSAT instance is equal to the cost of the minimum-cost hitting sets of the set of all cores of the MaxSAT instance.

Example 2.1. Consider the MaxSAT instance (Fh, Fs, wt) with the hard clauses

and soft clauses

with wt(c1) = wt(c2) = 2, wt(c3) = 4, wt(c4) = 1. The cores of this instance form the set K = {{c1, c2}, {c2, c3}, {c3, c4}}. For example, {c1, c2} is a core since x5 = 1 (c1) implies x4 = 0 and x1 = 1, and x6 = 1 (c2) implies x1 = 0; thus both cannot be satisfied by the same solution. An optimal solution is τ : x1 = x3 = x5 = x7 = 1, x2 = x4 = x6 = x8 = 0 with cost(τ) = 3. One MHCS of K is {c1, c3} with cost 3.

3 The Implicit Hitting Set Approach

We focus on IHS MaxSAT solvers [Davies and Bacchus, 2011; 2013a; 2013b; Davies, 2013; Saikko et al., 2016a] which instantiate the implicit hitting set paradigm [Karp,

2010; Moreno-Centeno and Karp, 2013; Saikko et al., 2016b] as natural candidates for integrating reduced cost fixing. IHS solvers iteratively alternate between computing a set of unsatisfiable cores K of the MaxSAT instance and minimum-cost hitting sets over the mononotonically growing K. To obtain a MCHS HS, an IP solver is employed on the MCHS IP formulation

associating a new binary variable bi with each soft clause ci. At each iteration the satisfiability of Fh∪(Fs\HS) is checked with a SAT solver. If satisfiable, the set HS implicitly hits all cores of the instance and, as first shown in [Davies and Bacchus, 2011], the optimality of HS implies the optimality of the MaxSAT solution, terminating the MaxSAT search.

To make use of reduced cost fixing, upper bounds on the cost of optimal MaxSAT solutions are needed. As originally described in [Davies and Bacchus, 2011], IHS does not directly provide upper bounds during search. However, upper bounds are obtained in the IHS solvers MaxHS and LMHS when non-optimal hitting sets are used as described in [Davies and Bacchus, 2013b]. In particular, for any hitting set HS, if the SAT solver finds a satisfying assignment τ for Fh ∪ (Fs \ HS), then cost(τ) is an upper bound (cost(τ) is equal to the optimal cost if HS is a MCHS).

Here we provide a bounds-based view on the iterations and termination of the IHS algorithm for MaxSAT. Illustrated in Figure 1, the bounds-based IHS algorithm for MaxSAT starts by initializing the SAT solver and IP solver with their respective inputs. The SAT solver is initialized with the CNF formula Fh ∪ Fs, while the IP solver is initialized with the soft clause weights wt . The hitting set HS and set of cores K are both initially empty. The upper bound UB is initialized to ∞ and LB to 0. We assume for simplicity that Fh is satisfiable. The first SAT solver invocation tests the entire set of clauses Fh ∪ Fs. If the formula is satisfiable, we obtain an upper bound of 0 and terminate as LB = UB. Otherwise we obtain an unsatisfiable core κ and add it to K.

In order to obtain the upper bounds required for reduced cost fixing, we deviate from the original IHS algorithm. Instead of immediately computing a new optimal hitting set for K we add the clauses of the new core κ to HS, forming a non-optimal hitting set of K, and check the satisfiability of Fh ∪ (Fs \ HS ) again. (A non-optimal hitting set of K ∪ {κ} could be also obtained in other ways [Davies and Bacchus, 2013b]). This is repeated, adding cores κ to K and the clauses of the new core to HS, until Fh ∪ (Fs \ HS) becomes satisfiable (this is the "disjoint" strategy of [Saikko, 2015]). Fh is satisfiable, so this condition will eventually be met when HS grows sufficiently large. Once Fh ∪ (Fs \ HS) is satisfiable, a MaxSAT solution is obtained. Its cost gives an upper bound value and UB is updated. At this point the IP solver is invoked to compute a minimum-cost hitting set HS for K. The hitting set HS is optimal, so its cost gives a lower bound for the cost of the optimal MaxSAT solution and LB is updated.

The algorithm terminates when LB = UB and returns the MaxSAT solution which yielded UB. By the same argument as presented in [Davies and Bacchus, 2011] the algorithm must eventually terminate. A detailed proof of correctness is provided in [Bacchus et al., 2017].

Example 3.1. Consider again the MaxSAT instance (Fh, Fs,wt) from Example 2.1. Following Figure 1, a SAT solver is called on Fh ∪ Fs. Assume that it returns UNSAT with the core κ = {c2, c3}. The SAT solver is called again on Fh ∪ (Fs \ κ), now returning the solution τ : x1 = x3 = x5 = x7 = 1, x2 = x4 = x6 = x8 = 0. This solution has cost(τ) = 3, which gives an upper bound UB = 3. The IP solver then called to compute a minimum-cost hitting set over K = {{c2, c3}}. Clearly, HS = {c2}. The SAT solver is called on (Fh ∪ Fs) \ {c2}. It returns UNSAT with core κ = {c3, c4}. The next SAT solver call over (Fh ∪ Fs) \ {c2, c3, c4} returns SAT but cannot improve UB. The IP solver is called for a minimum-cost hitting set over K = {{c2, c3}, {c3, c4}}. This gives HS = {c2, c4} and LB = 3. Now UB = LB and the search terminates.

4 Reduced Cost Fixing for IHS

Reduced cost fixing is a standard technique in IP solving [Wolsey, 1998; Danzig et al., 1954; Crowder et al., 1983; Nemhauser and Wolsey, 1999]. It uses an upper bound and reduced costs obtained from an LP relaxation to fix variables in an IP. Given a minimization IP P containing Boolean (0/1) variables, we can solve P as an LP by allowing the Boolean variables to take on intermediate values between 0 and 1. The cost of the LP solution will be a lower bound on the optimal cost of P. The LP solver also provides a reduced cost for the non-basic 1 variables set at 0 or 1 in the LP solution. These reduced costs specify a minimum increase in the cost of the LP that would arise from changing a non-basic variable at 0 (1) to 1 (0). Suppose we know a feasible IP solution to P with cost z. If changing a non-basic variable causes the LP solution to increase in cost beyond z, then we can fix that variable to the value it has in the LP solution. Since the LP solution is a lower bound, putting such variables at their opposite values would cause the cost of the IP to increase beyond the cost of an already known feasible solution. Here we explain how this technique can be used within IHS MaxSAT solvers.

1 The variables in the LP solution are either basic or non-basic. All of the non-basic variables will be at their upper or lower bounds in the LP solution [Chv´atal, 1983].

Theorem 4.1. For a MaxSAT problem F = (Fh, Fs, wt), suppose we have (a) B = {b1, . . . , bn} a set of Boolean variables where each bi = 0 (bi = 1) represents the satisfaction (falsification) of a soft clause ci ∈ Fs, (b) IPHS an IP over the bi representing the minimum-cost hitting set problem over the current set of cores, (c) LPHS the LP relaxation of IPHS , (d) best τ a feasible solution to F, (e) an optimal solution to LPHS with cost zLPHS opt , and (f) LP reduced costs rc(bi) at the optimal basis.

Then the following simplifications can be performed without changing opt cost(F ). (1) For every non-basic variable bi set to 0 in the optimal LPHS solution we can make the soft clause ci hard in F if zLPHS opt + rc(bi) > cost(best τ) or if zLPHS opt + rc(bi) = cost(best τ) and ci is satisfied in best τ. (2) For every non-basic variable bi set to 1 in the optimal LPHS we can make soft clause ci false in F if zLPHS opt - rc(bi) > cost(best τ) or if zLPHS opt - rc(bi) = cost(best τ) and ci is falsified in best τ.

For more intuition on how reduced cost fixing allows for hardening and falsifying soft clauses during IHS search for an optimal MaxSAT solution, we consider the following example.

Example 4.2. Consider again the MaxSAT instance (Fh, Fs,wt) from Example 2.1 and the first iteration of the execution of IHS as described in Example 3.1. After obtaining from the SAT solver the first solution best τ with cost(best τ) = 3, the IP solver is called for a hitting set over K = {{c2, c3}}. The LP-relaxation of the hitting set problem LPHS can be formulated as

where s is a surplus variable. This LP can be solved using different algorithms, clearly the optimal LP solution is b2 = 1, b1 = b3 = b4 = s = 0, which has cost zLPHS opt = 2. This induces a lower bound LB = 2. In this case, the optimal LP solution happens to be the optimal solution to the IP HS problem, i.e. HS = {c2}.

A feasible solution to an LP can be represented using a basis, where non-basic variables are at their upper or lower bounds. Consider the basis consisting of b3. The basic variables can be written as a function of the non-basic ones, in this case as b3 = 1 - b2 + s. This allows the objective to be rewritten solely as a function of the non-basic variables as

The coefficients in front of the non-basic variables are the reduced costs and (obviously) specify the change of the objective to modifications of the non-basic variables. Now, since

• [Ans´otegui et al., 2015] Carlos Ans´otegui, Fr´ed´eric Didier, and Joel Gab`as. Exploiting the structure of unsatisfiable cores in MaxSAT. In Proc. IJCAI, pages 283-289, 2015.
• [Bacchus et al., 2017] Fahiem Bacchus, Antti Hyttinen, Matti J¨arvisalo, and Paul Saikko. Reduced cost fixing in MaxSAT. In Proc. CP, volume 10416 of LNCS, pages 641-651. Springer, 2017.
• [Chv´atal, 1983] Vaˇsek Chv´atal. Linear Programming. Freeman, 1983.
• [Crowder et al., 1983] Harlan Crowder, Ellis L. Johnson, and Manfred Padberg. Solving large-scale zero-one linear programming problems. Operations Research, 31(5):803834, 1983.
• [Danzig et al., 1954] George B. Danzig, Delbert R. Fulkerson, and Selmer M. Johnson. Solution of a large-scale traveling-salesman problem. Operations Research, 2:393410, 1954.
• [Davies and Bacchus, 2011] JessicaDavies and FahiemBacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Proc. CP, volume 6876 of LNCS, pages 225-239. Springer, 2011.
• [Davies and Bacchus, 2013a] Jessica Davies and Fahiem Bacchus. Exploiting the power of MIP solvers in MaxSAT. In Proc. SAT, volume 7962 of LNCS, pages 166-181. Springer, 2013.
• [Davies and Bacchus, 2013b] Jessica Davies and Fahiem Bacchus. Postponing optimization to speed up MAXSAT solving. In Proc. CP, volume 8124 of LNCS, pages 247262. Springer, 2013.
• [Davies, 2013] Jessica Davies. Solving MAXSAT by Decoupling Optimization and Satisfaction. PhD thesis, University of Toronto, 2013. http: //www.cs.toronto.edu/˜jdavies/Davies_ Jessica_E_201311_PhD_thesis.pdf.
• [Focacci et al., 1999] Filippo Focacci, Andrea Lodi, and Michela Milano. Cost-based domain filtering. In Proc. CP, volume 1713 of LNCS, pages 189-203. Springer, 1999.
• [Heras et al., 2012] Federico Heras, Ant´onio Morgado, and Jo˜ao Marques-Silva. Lower bounds and upper bounds for MaxSAT. In Proc. LION 6, volume 7219 of LNCS, pages 402-407. Springer, 2012.
• [Karp, 2010] RichardM. Karp. Implicit hitting set problems and multi-genome alignment. In Proc. CPM, volume 6129 of LNCS, page 151. Springer, 2010.
• [Koshimura et al., 2012] Miyuki Koshimura, Tong Zhang, Hiroshi Fujita, and Ryuzo Hasegawa. QMaxSAT: A partial Max-SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 8(1/2):95-100, 2012.
• [Li et al., 2006] Chu Min Li, Felip Many`a, and Jordi Planes. Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In Proc. AAAI, pages 86-91. AAAI Press, 2006.
• [Li et al., 2008] Chu Min Li, Felip Many`a, Nouredine Ould Mohamedou, and Jordi Planes. Transforming inconsistent subformulas in MaxSAT lower bound computation.
• In Proc. CP, volume 5202 of LNCS, pages 582-587. Springer, 2008.
• [Lin and Su, 2007] Han Lin and Kaile Su. Exploiting inference rules to compute lower bounds for MAX-SAT solving. In Proc. IJCAI, pages 2334-2339, 2007.
• [Lin et al., 2008] Han Lin, Kaile Su, and Chu Min Li. Within-problem learning for efficient lower bound computation in Max-SAT solving. In Proc. AAAI, pages 351-356. AAAI Press, 2008.
• [Martins et al., 2014] Ruben Martins, Vasco M. Manquinho, and Inˆes Lynce. Open-WBO: A modular MaxSAT solver. In Proc. SAT, volume 8561 of LNCS, pages 438-445. Springer, 2014.
• [Moreno-Centeno and Karp, 2013] Erick Moreno-Centeno and Richard M. Karp. The implicit hitting set approach to solve combinatorial optimization problems with an application to multigenome alignment. Operations Research, 61(2):453-468, 2013.
• [Morgado et al., 2012] Ant´onio Morgado, Federico Heras, and Jo˜ao Marques-Silva. Improvements to core-guided binary search for MaxSAT. In Proc. SAT, volume 7317 of LNCS, pages 284-297. Springer, 2012.
• [Morgado et al., 2014] Ant´onio Morgado, Carmine Dodaro, and Joao Marques-Silva. Core-guided MaxSAT with soft cardinality constraints. In Proc. CP, volume 8656 of LNCS, pages 564-573. Springer, 2014.
• [Nemhauser andWolsey, 1999] George L. Nemhauser and Laurence A. Wolsey. Integer and Combinatorial Optimization. Wiley-Interscience, 1999.
• [Saikko et al., 2016a] Paul Saikko, Jeremias Berg, andMatti J¨arvisalo. LMHS: A SAT-IP hybrid MaxSAT solver. In Proc. SAT, volume 9710 of LNCS, pages 539-546. Springer, 2016.
• [Saikko et al., 2016b] Paul Saikko, Johannes Peter Wallner, andMatti J¨arvisalo. Implicit hitting set algorithms for reasoning beyond NP. In Proc. KR, pages 104-113. AAAI Press, 2016.
• [Saikko, 2015] Paul Saikko. Re-implementing and extending a hybrid SAT-IP approach to maximum satisfiability. Master's thesis, University of Helsinki, 2015. http: //hdl.handle.net/10138/159186.
• [Thorsteinsson and Ottosson, 2002] Erlendur S. Thorsteinsson and Greger Ottosson. Linear relaxations and reducedcost based propagation of continuous variable subscripts. Annals of Operations Research, 115(1-4):15-29, 2002.
• [Wolsey, 1998] Laurence A. Wolsey. Integer Programming. John Wiley, 1998.
• [Yunes et al., 2010] Tallys H. Yunes, Ionut D. Aron, and John N. Hooker. An integrated solver for optimization problems. Operations Research, 58(2):342-356, 2010.