Unifying Core-Guided and Implicit Hitting Set Based Optimization

1 Introduction

The declarative paradigm of maximum satisfiability (MaxSAT) [Bacchus et al., 2021] is a viable approach to solving NP-hard optimization problems arising from AI and other real-world settings. Much of the success of MaxSAT is due to advances in Boolean satisfiability (SAT) based MaxSAT algorithms capable of computing provably optimal solutions. Two of the most popular and effective algorithmic approaches implemented in MaxSAT solvers are variants of the so-called core-guided (CG) [Fu and Malik, 2006; Marques-Silva and Planes, 2007; Heras et al., 2011; Ans´otegui et al., 2013; Morgado et al., 2013; Morgado et al., 2014; Narodytska and Bacchus, 2014; Alviano et al., 2015; Ans´otegui et al., 2016; Ans´otegui and Gab`as, 2017] and implicit hitting set (IHS) [Davies and Bacchus, 2011; Davies and Bacchus, 2013; Saikko et al., 2016] approaches.

Both CG and IHS are unsatisfiability-based approaches, relying on iteratively extracting unsatisfiable cores using a SAT solver as a core-extracting decision oracle [E´en and S¨orensson, 2003]. However, CG and IHS solvers deal with cores extracted during search differently. CG algorithms reformulate the current working instance-starting with the input MaxSAT instance-to take into account the so-far extracted cores in subsequent search iterations towards an optimal solution. The various different core-guided algorithms differ in the way in which the reformulation steps change the working instance. In contrast, in each iteration of IHS search, the SAT solver is invoked on a subset of clauses of the input instance, without reformulation-style modifications. The choice of the subset of constraints to consider at each iteration is dictated by a (minimum-cost) hitting set computer over the so-far accumulated set of cores. In practice, state-of-the-art core-guided and IHS MaxSAT solvers are both competitive in terms of runtime performance. However, their relative performance on distinct problem domains can vary noticeably, coreguided solvers outperforming IHS on specific domains, IHS outperforming core-guided on distinct other domains [Bacchus et al., 2019]. The fundamental reasons behind this are not well understood, despite recent advances showing that for a specific classic variant of core-guided search, the cores extracted from the reformulated working formulas during CG search are tightly related to cores extracted in IHS search on the original instance [Bacchus and Narodytska, 2014; Narodytska and Bjørner, 2022].

Taking a different view, we develop a general algorithmic framework that captures CG and IHS computations in a unifying way. The framework is based on the recentlyproposed notion of abstract cores originally presented as a performance-improving technique for IHS [Berg et al., 2020] that brings a flavor of CG reformulation into the representation of the hitting set problems solved during IHS search. Our framework provides a unified way of establishing the correctness of variants of core-guided and IHS approaches. Further, the framework can be instantiated in novel ways giving rise to new variants of unsatisfiability-based MaxSAT algorithms. As an illustration of its potential for obtaining novel types of unsatisfiability-based algorithms, we outline and implement a prototype of a core-guided variant for MaxSAT obtained through the framework which turns out to be promising also from a practical perspective.

While our discussion is grounded in MaxSAT, the framework is applicable also for capturing core-guided and IHS search approaches beyond MaxSAT, including ones developed e.g. for pseudo-Boolean optimization [Devriendt et al., 2021; Smirnov et al., 2021; Smirnov et al., 2022], finitedomain constraint optimization problems [Delisle and Bacchus, 2013; Gange et al., 2020] and answer set programming [Andres et al., 2012; Saikko et al., 2018; Alviano and Dodaro, 2020]: core-guided and IHS approaches rely on a core-extracting decision oracle, but the exact constraint language on which the core extraction is performed does not fundamentally influence the overall algorithmic approaches. Our unifying framework can also be viewed as a further development in a longer line of research developing theoretical frameworks that capture the underpinning of automated reasoning engines, such ones proposed for SAT and SMT [Nieuwenhuis et al., 2006; Larrosa et al., 2011; J¨arvisalo et al., 2012; Fazekas et al., 2018]

2 Maximum Satisfiability

For a Boolean variable x there are two literals, x and ¯x. A clause C = l1 ∨ . . . ∨ ln is a disjunction of literals, a conjunctive normal form (CNF) formula F = {C1, . . . ,Cm} is a set of clauses. The set var(C) consists of the variables x for which either x ∈ C or ¯x ∈ C. An assignment τ maps variables to 1 (true) or 0 (false). Assignments extend to a literal l, clause C and formula F in the standard way: τ(¯l) = 1 - τ(l), τ(C) = max{τ(l) | l ∈ C} and τ(F) = min{τ(C) | C ∈ F}. τ satisfies F if τ(F) = 1. We may treat τ as the set of literals τ assigns to 1, so that l ∈ τ denotes τ(l) = 1 and ¯l ∈ τ denotes τ(l) = 0. τ is complete for F if it assigns each variable in F, and otherwise partial.

Cardinality constraints are linear inequalities of the form ∑i xi ≥ k, where each xi is a Boolean variable and k a positive constant. The constraint ∑i xi ≥ k is satisfied by an assignment τ if ∑i τ(xi) ≥ k. We do not make assumptions on the CNF encoding used for cardinality constraints, and abstractly use ASCNF(∑i xi ≥ k) to denote a CNF formula that is satisfiable by an assignment τ iff ∑i τ(xi) ≥ k. Taking a name o to indicate whether a cardinality constraint is satisfied, we also use ASCNF(∑i xi ≤ k ↔ o) to denote a CNF formula that is satisfied by any assignment τ that sets τ(o) = 1 iff ∑i τ(xi) ≥ k. Various CNF encodings of cardinality constraints have been proposed [Bailleux and Boufkhad, 2003; Sinz, 2005; E´en and S¨orensson, 2006; Codish and Zazon-Ivry, 2010; As´ın et al., 2011; Ab´ıo et al., 2013; Karpinski and Piotr´ow, 2019].

An instance F = (F,O) of maximum satisfiability (MaxSAT) consists of a CNF formula F and an objective function O ≡ ∑i wibi, where wi are positive constants and bi is a variable of F. (This view on MaxSAT is equivalent to the classical view on MaxSAT with hard and weighted soft clauses [Berg and J¨arvisalo, 2019].) The set var(O) consists of the variables that appear in O. A complete satisfying assignment τ to F is a solution to F with cost O(τ) = ∑i wiτ(bi). A solution is optimal if there are no solutions with lower cost. The cost of optimal solutions is denoted by OPT(F).

Example 1. Consider the MaxSAT instance F = (F, O) with F = {(b1 ∨ b2 ∨ b3), (b3 ∨ b4 ∨ b5)}, O = b1 + b2 + 3b3 + b4 + 2b5. An optimal solution to F is τ = {¯b1, b2, ¯b3, b4, ¯b5}, assigning all variables except b2, b4 to 0. The cost of τ is O(τ ) = τ (b1) + τ (b2) + 3τ (b3) + τ (b4) + 2τ (b5) = 2.

A clause C is a(n unsatisfiable) core of a MaxSAT instance F = (F,O) if all literals in C are objective variables (i.e.,

Algorithm 1 Core-guided approach to MaxSAT

Input: MaxSAT instance F = (F, O).

Output: Optimal solution τ to F.

• 1: CONSTRS = ∅
• 2: O′ = O
• 3: while true do
• 4: γA = {¯x | x ∈ var(O′ )}
• 5: (res,C, τ) = EXTRACT-CORE(F ∪ CONSTRS, γA)
• 6: if res ='true' then return τ
• 7: (D, out) = CREATE-CARD-CONSTR(C)
• 8: CONSTRS = CONSTRS ∪D
• 9: O′ = REFINE-OBJECTIVE(C, out,O′ )

var(C) ⊆ var(O)) and every solution to F satisfies C (i.e., F logically entails C).

3 Core-Guided and IHS Search for MaxSAT

We develop a unifying algorithmic framework for coreguided [Fu and Malik, 2006; Marques-Silva and Planes, 2007; Morgado et al., 2013; Morgado et al., 2014; Narodytska and Bacchus, 2014; Alviano et al., 2015; Ans´otegui and Gab`as, 2017] and implicit hitting set algorithms [Davies and Bacchus, 2011; Davies and Bacchus, 2013; Saikko et al., 2016]. As background, we describe these approaches in general terms; practical solver implementations employ various heuristics and optimizations which do not affect our main contributions.

Both core-guided and IHS algorithms use an incremental SAT solver that determines the satisfiability of CNF formulas under different sets of assumptions [E´en and S¨orensson, 2003]. Given a CNF formula F and partial assignment γA (constituting a set of assumptions, as a set of literals), we abstract the SAT solver into the subroutine EXTRACT-CORE that returns a triplet (res,C, τ). Here res=true if there is a satisfying assignment τ ⊇ γA of F. If there is no such assignment, res=false and C is a clause over a subset of the variables in γA entailed by F for which γA(C) = 0. Invoked on F under a set of assumptions γA such that F ∧ γA is unsatisfiable, modern SAT solvers provide such C at termination without computational overhead. In core-guided and IHS MaxSAT solving, EXTRACT-CORE is used for extracting cores of a MaxSAT instance F = (F,O) by invoking it on F under a subset of var(O) as the assumptions.

Core-Guided Search. Algorithm 1 details a general abstraction of the core-guided approach to computing an optimal solution to a MaxSAT instance F = (F,O). First the algorithm initializes a set CONSTRS of cardinality constraints as empty and a working objective function O′ as the objective function O (Lines 1-2). In each iteration of the main loop (Lines 3-9) a SAT solver is queried for a solution τ that (i) satisfies all clauses in F and all of the cardinality constraints in CONSTRS and (ii) falsifies all objective variables of the current working objective O′ , i.e., O′ (τ) = 0 (Lines 4-5). If there is such a τ, it is returned as an optimal solution to the original instance (Line 6). Otherwise a core C of (F ∪ CONSTRS,O′ ) is obtained. The core is then relaxed (Lines 7-9), transforming the current instance in a way that

Algorithm 2 IHS for MaxSAT

Input: MaxSAT instance F = (F, O).

Output: Optimal solution τ to F.

• 1: K = ∅
• 2: while true do
• 3: γA = {¯x | x ∈ var(O) \ MINCOST-HS(K)}
• 4: (res,C, τ) = EXTRACT-CORE(F, γA)
• 5: if res = 'true' then return τ
• 6: else K = K∪C

enables (at most) one variable in the core C to incur cost in subsequent iterations. This is done by adding a new cardinality constraint over the core to CONSTRS (Lines 7-8) and updating the current working objective (Line 9).

Conceptually, modern core-guided algorithms differ mainly in the specifics of the core relaxation step. We detail the relaxation of the core-guided OLL algorithm [Morgado et al., 2014; Andres et al., 2012] as arguably one of the most successful core-guided approaches. In OLL CREATE-CARD-CONSTR(C) returns a set of cardinality constraints D = {ASCNF(∑x∈C x ≥ j ↔ oCj ) | 2 ≤ j ≤ |C|} and a set out = {oC2 . . . oC|C| } of output variables. Intuitively, the new cardinality constraints define output variables that count the number of literals in C assigned to 1 in subsequent iterations, since enforcing oCk to 0 limits the number of literals in C assigned to 1 to at most k - 1. The output variable with index 1 is not introduced; since C is a core, every satisfying assignment assigns at least one literal to 1. In the objective reformulation step (REFINE-OBJECTIVE procedure of Algorithm 1), OLL adds the new outputs to the objective in a way that preserves the set of optimal solutions. The coefficient of each x ∈ C is decreased by wC = minx∈Ci {O′ (x)} (removing from O′ every literal whose coefficient decreases to 0). Informally, the termination of OLL follows from observing that at least one literal bis removed from O′ on each iteration, which allows the SAT solver to assign at least one more objective variable to true in subsequent iterations.

Example 2. Invoke OLL on F = (F,O) from Example 1. The first call to EXTRACT-CORE is under the assumptions γA = { ¯ b1, ¯ b2, ¯ b3, ¯ b4, ¯ b5}. Let the first core obtained be C1 = (b1∨b2∨b3∨b4∨b5). Relaxing C1 introduces the cardinality constraint ASCNF(∑x∈C1 x ≥ i ↔ o1i ) for i = 2, 3, 4, 5 and the new objective is O′ = 2b3+b5+o12 +o13 +o14 +o15 . The next call to EXTRACT-CORE is under the assumptions γA = { ¯ b3, ¯ b5, ¯ o12 , ¯ o13 , ¯ o14 , ¯ o15 }. Let the next core obtained be C2 = (o12 ∨ b3). Relaxing C2 introduces the cardinality constraint ASCNF(∑x∈C2 x ≥ 2 ↔ o22 ) and the new objective O′ = b3 + b5 + o13 + o14 + o15 + o22 . The assumptions in the 3rd call to EXTRACT-CORE are γA = { ¯ b3, ¯ b5, ¯ o13 , ¯ o14 , ¯ o15 , ¯ o22 }. Now e.g. the assignment τ = {b1, ¯ b2, ¯ b3, b4, ¯ b5} (that also assigns {o12 , ¯ o13 , ¯ o14 , ¯ o15 , ¯ o22 }) is returned as an optimal solution to F.

IHS Search. Algorithm 2 is a generic abstraction of the IHS approach to MaxSAT. IHS iteratively extracts cores of an input MaxSAT instance and stores them in the set K. Instead of reformulating the objective, IHS invokes the MINCOST-HS(K) procedure that computes a minimum-cost hitting set (MCHS) over K under O. Here an MCHS is a minimum-cost (in terms of O) subset hs of the objective variables such that the variables in hs, assigned to 1, satisfy all cores in K. In each iteration of the main loop (Lines 2-6), EXTRACT-CORE is queried for a solution that falsifies all objective variables that are not contained in the hs computed over the current set of cores (Lines 3-4). If there is such a τ , it is an optimal solution on Line 5. Otherwise a new core is obtained and added to K (Line 6). The MCHS computed in each iteration represents a way of satisfying all cores found so far in an optimal way under O. IHS iterates until the MCHS can be extended into a solution of F , at which point it satisfies (or hits) all cores (not only the cores in K) of the instance implicitly. Note that the assumptions γA set up on Line 3 constitute a partial assignment over the objective variables that can be extended into a solution of K in a unique way.

Example 3. Invoke Algorithm 2 on the MaxSAT instance F = (F,O) from Example 1. In the first iteration there are no cores, so MINCOST-HS(K) = ∅. The first call to EXTRACT-CORE is under the assumptions γA = { ¯ b1, . . . , ¯ b5}. There are a number of cores that could be returned; let the first core obtained be C1 = (b1 ∨ b2 ∨ b3 ∨ b4 ∨ b5). In iteration 2 there are three different MCHSs over K = {C1}. Assume that MINCOST-HS returns {b1}. Then the assumptions for the next call to EXTRACT-CORE are γA = { ¯ b2, ¯ b3, ¯ b4, ¯ b5}. Assume that the next core is C2 = (b3 ∨ b4 ∨ b5). In iteration 3 the only MCHS over K = {C1,C2} is {b4}, the assumptions for the next call to EXTRACT-CORE are γA = { ¯ b1, ¯ b2, ¯ b3, ¯ b5}. Assume that the next core is C3 = (b1, b2, b3). In iteration 4 there are two possible MCHSs over K = {C1,C2,C3}. Assume that MINCOST-HS returns {b2, b4}, leading to the assumptions γA = { ¯ b1, ¯ b3, ¯ b5}. Now EXTRACT-CORE returns the solution τ = { ¯ b1, b2, ¯ b3, b4, ¯ b5} as an optimal solution to F.

4 Unifying CG and IHS

As our main contribution we present UNIMAXSAT, a general algorithmic framework unifying core-guided and IHS-based MaxSAT algorithms. The framework builds on the notion of abstract cores originally proposed as basis for a refinement of IHS [Berg et al., 2020]. We start with defining abstraction sets and abstract cores. On a high level, abstraction sets and abstract cores of a MaxSAT instance capture generic properties of the instance compactly in the sense that a large number of (standard) cores would be needed to express the same properties [Berg et al., 2020].

Definition 1. An abstraction set AB = (in,D, out) consists of a set in of input literals, a set out of output literals, and a satisfiable CNF formula over the literals in ∪ out, i.e., var(in ∪ out) ⊆ var(D). Solutions to D are uniquely defined by assignments to the inputs: for any assignment τ over in there is exactly one extension τ E ⊇ τ that satisfies D.

Given an abstraction set AB = (in,D, out) we call D the definitions of the outputs out. For a collection AB = {(ini,Di, outi) | i = 1, . . . , n} of abstraction sets, DEF(AB) = ⋃ni=1 Di is the CNF formula consisting of the definitions in AB and OUTS(AB) = ⋃ni=1 outi is the set of outputs occurring in AB. We say that AB is feasible for a MaxSAT instance F = (F, O) if DEF(AB) does not change the set of solutions to F, i.e., if every solution τ to F can be uniquely extended into a solution τ E ⊇ τ to F ∪ DEF(AB). We will consider collections of abstractions sets that are feasible for specific MaxSAT instances.

An abstract core is a clause entailed by a formula together with the definitions of a feasible collection of abstraction set. Importantly, an abstract core can contain both objective variables and outputs of abstraction sets.

Definition 2. Given MaxSAT instance F = (F,O) and collection AB of feasible abstraction sets, a clause C is an abstract core of F wrt AB if (i) var(C) ⊆ (var(O) ∪ var(OUTS(AB)) and (ii) τ(C) = 1 for each solution τ of F ∪ DEF(AB).

Every (standard) core of a MaxSAT instance F is also an abstract core wrt any collection of feasible abstraction sets.

Example 4. Consider the (F,O) from Example 1 and the abstraction set AB = ({b1, . . . , b5}, {ASCNF(∑5i=1 bi ≥ j ↔ oj) | j = 2, 3, 4, 5}, {o2, . . . , o5}). Then C = (o2 ∨ b3) is an abstract core as any satisfying assignment of F ∪ DEF(AB) must assign either b3 = 1 or least two variables of {b1, b2, b3, b4, b5} to 1, forcing o2 = 1. Note how C corresponds to the core C2 from Example 2.

Our general framework for core-guided and IHS search is based on computing minimum-cost solutions to abstract cores and extending them to a solution to the MaxSAT instance at hand. To differentiate solutions to the input MaxSAT instance from solutions to cores, we call solutions to a set of abstract cores candidate solutions (candidates for short): for a MaxSAT instance (F,O), a collection AB of abstraction sets and a set K of abstract cores, a complete satisfying assignment δ of K ∪ DEF(AB) that assigns each variable in var(O) is a candidate (solution) to K with cost O(δ). δ is minimum-cost if O(δ) ≤ O(δ′ ) for all candidates δ′ of K.

The following observation details how abstraction sets and abstract cores are used in our framework to compute lower bounds (which are used to prove optimality of solutions).

Proposition 1. Let F = (F,O) be a MaxSAT instance, K a set of abstract cores, and δ a minimum-cost candidate of K. Then O(δ) ≤ OPT(F).

We will show that the correctness of IHS and core-guided algorithms follows from the fact that, instead of ruling out complete candidates on each iteration, it suffices to rule out partial assignments that extend solely to minimum-cost candidates. The notion of a (minimum-cost) abstract candidate is central in this respect.

Definition 3. Let F = (F,O) be a MaxSAT instance, AB a collection of feasible abstraction sets and K a set of abstract cores. A partial assignment γA over a subset of the variables in var(K)∪var(O) is an abstract candidate of K if (i) there is at least one extension τ ⊇ γA which is a solution of DEF(AB) ∪K, i.e., a candidate of K and (ii) all such extensions are minimum-cost candidates of K.

While each minimum-cost candidate of K is also an abstract candidate, the converse need not hold.

Example 5. Consider the MaxSAT instance F = (F,O) from Example 1 and the set K = {(b1 ∨ b2 ∨ b3), (b3 ∨ b4 ∨ b5)} of abstract cores. A minimum-cost candidate of K is δ = { ¯ b1, b2, ¯ b3, b4, ¯ b5}. An abstract candidate is γA = { ¯ b1, ¯ b3, ¯ b5} since the only extension of γA into a solution to K is δ. The set { ¯ b1, ¯ b3} is not an abstract candidate since it extends to the solution { ¯ b1, b2, ¯ b3, ¯ b4, b5} of K which is not minimum-cost.

The assumptions employed during iterations of coreguided algorithms can be seen as abstract candidates; for an example, consider the following, specific to OLL.

Example 6. Recall the MaxSAT instance F = (F,O) from Example 1. Consider the set of cores K = {b1 ∨ b2 ∨ b3 ∨ b4 ∨ b5}, and the abstraction set AB detailed in Example 4. The set γA = { ¯ b3, ¯ b5, ¯ o2, ¯ o3, ¯ o4, ¯ o5} is an abstract candidate as it can be extended into a solution to K ∪ DEF({AB}) by assigning exactly one literal in {b1, b2, b4} to 1 and the rest to 0. Note that γA is exactly the set of assumptions that EXTRACT-CORE is queried under in iteration 2 of OLL in Example 2.

UNIMAXSAT

We now describe UNIMAXSAT, a general algorithmic framework for core-guided and IHS MaxSAT algorithms. Detailed as Algorithm 3 and Figure 1, given a MaxSAT instance F = (F,O) as input, UNIMAXSAT outputs an optimal solution to F. The generic algorithm maintains an increasing set AB and K of abstraction sets and abstract cores, respectively. In each iteration, an abstract candidate γA of K is computed by the ABS-CANDIDATE subroutine. The EX-ABSCORE subroutine is invoked to check for an extension of γA into a solution to F. If one exists, the algorithm terminates and returns the extension as an optimal solution. Otherwise a new abstract core falsified by γA is obtained. The core is added to K, thus blocking γA and all of its extensions from further consideration, and the ADD-ABSSETS subroutine adds new abstraction sets to AB.

We formalize the correctness of Algorithm 3: it terminates on any MaxSAT instance and outputs an optimal solution of the input instance, subject to generic properties of its three subroutines. Importantly, correctness of the general framework allows for establishing the correctness of any Algorithm 3 UNIMAXSAT, a unified framework for coreguided and IHS-based MaxSAT algorithms.

Input: MaxSAT instance F = (F, O). Output: Optimal solution τ to F.

• 1: AB1 = ∅, K1 = ∅
• 2: for i = 1 . . . do
• 3: γA = ABS-CANDIDATE(ABi ,Ki )
• 4: (res,C, τ) = EX-ABSCORE(F, DEF(ABi ), γA)
• 5: if res = 'true' then return τ
• 6: Ki+1 = {C} ∪Ki
• 7: ABi+1 = ABi ∪ ADD-ABSSETS(F,Ki+1 )

of its instantiations-which include known core-guided and IHS algorithms for MaxSAT-by showing how each algorithm can be viewed as an instantiation of the UNIMAXSAT.

Theorem 1. Let F = (F,O) be an input instance to UNIMAXSAT that has solutions. Assume that the following three properties hold on every iteration i of UNIMAXSAT.

1. ABS-CANDIDATE(ABi ,Ki ) computes an abstract candidate of Ki .
2. EX-ABSCORE(F, DEF(ABi ), γA) computes a solution τ ⊇ γA of F ∪ DEF(ABi ), or a core C satisfied by all solutions to F ∪ DEF(ABi ) and falsified by γA.
3. ABi is feasible for F.

Then UNIMAXSAT terminates and returns an optimal solution of F.

The proof of Theorem 1 relies the abstraction sets added and abstract cores obtained decreasing the set of candidates that ABS-CANDIDATE may provide on each iteration.

Lemma 1. Consider an iteration i in which UNIMAXSAT invoked on an instance (F, O) does not terminate. Let Ki and ABi be the set of abstract cores and abstraction sets obtained so-far. Denote by OBJ-SOLSi the restrictions of all solutions to Ki ∪ DEF(ABi ) onto var(O). Then OBJ-SOLSi+1 ⊊ OBJ-SOLSi .

Proof of Theorem 1. By assumptions 1-2, the clause C obtained from EX-ABSCORE is an abstract core of F and ABi . Since ABi ⊆ ABi+1 holds for all i, C is also an abstract core in all subsequent iterations. Thus all clauses in Ki are abstract cores of F and ABi .

For optimality of returned solutions, assume that the algorithm terminates on iteration i and returns a solution τ . Then τ ⊇ γA for an abstract candidate γA of Ki . Since τ is also a solution to DEF(ABi ), τ is a minimum-cost candidate of Ki . Thus O(τ) ≤ OPT(F) ≤ O(τ): the first inequality is by Proposition 1 and the second by τ being a solution to F. We conclude that O(τ) = OPT(F).

Now consider termination. As F has solutions and ABi is feasible, F ∪ DEF(ABi ) has solutions for all i. By definition of abstract cores, all solutions to F ∪ DEF(ABi ) are solutions to DEF(ABi ) ∪ Ki . In each iteration, the abstract candidate γA obtained from ABS-CANDIDATE can be extended into at least one solution to DEF(ABi ) ∪ Ki . We argue that eventually γA can also be extended into a solution to F ∪ DEF(ABi ). This follows from the finite number of possible assignments to the variables in O and Lemma 1 by which, given that the algorithm does not terminate during specific iteration, the number of assignments to variables of O that can be extended into candidates of the found cores will decrease. As the solutions to F ∪ DEF(ABi ) are candidates for any sets of cores, at some iteration ABS-CANDIDATE will return an abstract candidate that can be extended into a solution to F ∪ DEF(ABi ), resulting in termination.

5 Capturing Existing Algorithms

We detail existing unsatisfiability-based MaxSAT algorithms as instantiations of UNIMAXSAT. Specifically, we explain how to instantiate the three subroutines of UNIMAXSAT so that the assumptions of Theorem 1 hold to obtain IHS and core-guided algorithms. By Theorem 1, this yields uniform proofs of correctness for IHS (including its abstract-cores extension [Berg et al., 2020]) and modern core-guided algorithms. For core-guided instantiations, we detail OLL and more shortly explain how the further core-guided variants MSU3 [Marques-Silva and Planes, 2007], WPM3 [Ans´otegui and Gab`as, 2017], PMRES [Narodytska and Bacchus, 2014] and K [Alviano et al., 2015] are obtained.

The EX-ABSCORE subroutine of UNIMAXSAT is in general a core-extracting SAT solver: given a MaxSAT instance F = (F,O), a feasible collection AB of abstraction sets and an abstract candidate γA, EX-ABSCORE invokes a SAT solver on F ∪ DEF(ABi ) under assumptions γA, fulfilling assumption 2 of Theorem 1. Feasibility of abstraction sets computed by each considered algorithm follows from that the definitions of new abstraction sets can only intersect with the input instance and previous abstraction sets on their inputs. We will thus assume abstraction sets to be feasible. With these considerations, we next argue that each of the recent unsatisfiability-based MaxSAT algorithms can be viewed as an instantiation of UNIMAXSAT by (i) specifying the instantiations of ABS-CANDIDATE and ADD-ABSSETS, and (ii) arguing that the instantiation of ABS-CANDIDATE correctly computes an abstract candidate.

5.1 Capturing IHS

IHS. UNIMAXSAT gives the (basic) IHS (Algorithm 2) by instantiating ADD-ABSSETS to never add any abstraction sets and EX-ABSCORE as a procedure that-given a set K of cores-returns the abstract candidate γA = {¯x | x ∈ O \ MINCOST-HS(K)} that assigns all literals in the objective to 0 except the ones in a most recent minimum-cost hitting set MINCOST-HS(K) over K. The correctness of Algorithm 2 now follows by Theorem 1 by observing that the only extension of γA into a candidate of K is {¯x | x ∈ O \ MINCOST-HS(K)} ∪ {x | x ∈ MINCOST-HS(K)} and is minimum-cost. Hence γA is an abstract candidate of K.

IHS with abstract cores. UNIMAXSAT gives IHS enhanced with abstract cores by instantiating EX-ABSCORE as in basic IHS, and ADD-ABSSETS to (heuristically) compute abstraction sets (in,D, out) the inputs in = {x1, . . . , xn} of which are a subset of n objective variables that all have the same coefficient in O, out = {o1, . . . , on} is a set of n new variables, and D = {ASCNF(∑x∈in x ≥ i ↔ oi) | k = 1 . . . n}, resulting in the outputs counting the number of inputs assigned to 1 in all satisfying assignments. The ABS-CANDIDATE subroutine first computes a minimum-cost solution γ to K ∪ DEF(AB) that assigns all variables in var(O) ∪ OUTS(AB), and then returns either γA 1 as the restriction of γ onto the objective variables, or γA 2 as the restriction of γ onto the outputs of the current abstraction sets and objective variables that are not inputs to any abstraction sets. The correctness of IHS with abstract cores is now established by Theorem 1 as follows. Since the only extension of it into a solution of K∪DEF(AB) is γ, γA 1 is an abstract candidate. Finally, γA 2 is an abstract candidate since (i) γ is an extension of γA 2 into a solution of K∪DEF(AB) and (ii) every such extension has the same cost as the inputs to all abstraction sets have the same coefficients in O.

5.2 Capturing Core-Guided Algorithms

Moving to core-guided algorithms, we first give a more detailed description on OLL, and briefly cover other algorithms.

OLL Key to viewing OLL through UNIMAXSAT is that the cardinality constraints introduced by OLL are seen as abstraction sets, i.e., ADD-ABSSETS relaxing a core C introduces abstraction set ABC = (C,D, out) where D = {ASCNF(∑x∈C x ≥ i ↔ oi ) | 2 ≤ i ≤ |C|} and out = {o2 , . . . , o|C| }. The set of assumptions used in SAT solver calls are seen as abstract candidates. We thus assume that ABS-CANDIDATE maintains and updates reformulated objective O′ .

In OLL, the dependencies between the output variables introduced during core relaxation require extra care when instantiating OLL in UNIMAXSAT. More specifically, to ensure that γA = {¯x | x ∈ var(O′ )} is an abstract candidate in each iteration, we include an assumption refinement step as part of ABS-CANDIDATE. After receiving an abstraction set for a core C, ABS-CANDIDATE with assumption refinement checks if γA can be extended into a solution to DEF(AB)∪K, i.e., the definitions of the current collection AB of abstraction sets and set K of abstract cores. If it can, it is returned as an abstract candidate, otherwise a new core is obtained, added to K, and relaxed as other cores.

Important for understanding assumption refinement is that the core extraction steps performed during it do not consider the input clauses. Even so, all cores extracted during assumption refinement remain abstract cores of the input instance, since the cores are satisfied by all solutions to the definitions of the current abstraction sets and cores, which in turn are satisfied by all solutions to the input instance. Each new core discovered during assumption refinement decreases the number of literals in O′ by at least one. Thus the procedure is guaranteed to terminate eventually.

Correctness of OLL now follows by Theorem 1 by arguing that ADD-ABSSETS with assumption refinement results in a partial assignment γA that is an abstract candidate of DEF(AB) ∪ K. We sketch a proof of this for an arbitrary unweighted MaxSAT instance F = (F, O) (all objective coefficients 1; the proof for weighted objectives is similar).

In the following, let INACTIVEi be the set of objective variables and abstraction set outputs that have not been encountered in any cores during the first i - 1 iterations. Then INACTIVEi = var(O′ ) where O′ is the reformulated objective (maintained by ABS-CANDIDATE) during iteration i. We say that the literals in INACTIVEi are inactive. Now consider an iteration i of the UNIMAXSAT instantiated as OLL and let Ki be the set of abstract cores obtained so-far (either from EX-ABSCORE or from assumption refinement) and ABi the set of all abstraction sets corresponding to cardinality constraints introduced so-far. We show that the partial assignment γA = {¯x | x ∈ INACTIVEi } that assigns all inactive literals in INACTIVEi to 0 is an abstract candidate of Ki . The assumption refinement step guarantees that there is at least one extension of γA into a solution to DEF(ABi )∪Ki . Thus what remains to show is that all such extensions will be minimumcost. For this, let τ be a solution of DEF(ABi ) ∪ Ki . We argue that: (i) O(τ) ≥ |Ki | and, (ii) O(τ) ≤ |Ki | if τ ⊇ γA.

Since the output literals of the abstraction sets are defined by cardinality constraints, each new output literal assigned to 1 will result in one more objective variable being assigned to 1, thus incurring cost. Now (i) follows by observing that τ assigns at least one literal in each C ∈ Ki to 1. (ii) follows from the fact that each new abstract core obtained during search is always falsified when assigning the current set of inactive literals to 0. The abstraction set corresponding to a cardinality constraint that is introduced after each core allows exactly one more of the previously inactive literals to be assigned to 1 in subsequent iterations.

Finally, we outline instantiation of UNIMAXSAT which exactly correspond to other modern core-guided algorithms.

MSU3 is obtained by instantiating UNIMAXSAT as follows. ADD-ABSSETS maintains a set INACTIVE of objective literals that have not appeared in any cores. Given a new core C on iteration i all objective literals in C are removed from INACTIVE. A new abstraction set AB = (ACTIVE, ASCNF(∑x∈ACTIVE x ≥ i+1 ↔ oi), {oi}) where ACTIVE = var(O) \ INACTIVE and oi is a fresh variable, is then introduced. The instantiation of ABS-CANDIDATE returns the abstract candidate γA = {¯x | x ∈ INACTIVE} ∪ {¯ oi}.

WPM3 is obtained very similarly as MSU3. However, instead of ADD-ABSSETS maintaining a single abstraction set with all objective variables not in INACTIVE as inputs, it maintains several abstraction sets with different disjoint subsets of the variables x ∈ var(O) \ INACTIVE. Whenever a core containing the outputs of two different abstraction sets AB1 = (in1, ASCNF(∑x∈in1 x ≥ k ↔ o1k ), {o1k }) and AB2 = (in2, ASCNF(∑x∈in2 x ≥ t ↔ o2t ), {o2t }) is extracted by EX-ABSCORE, a new abstraction set (in1 ∪ in2, ASCNF(∑x∈in1∪in2 x ≥ (k + t + 1) ↔ o3k+t+1 ), {o3k+t+1 }) is introduced; and AB1, AB2 removed (i.e., ignored by ABS-CANDIDATE).

PMRES is obtained by ADD-ABSSETS introducing for every core C = (x1, . . . , xn) an abstraction set AB = (C, {xi ∧ (xi+1 ∨ · · · ∨ xn) ↔ oi | 1 ≤ i ≤ n- 1}, {o1, . . . , on-1}). The ABS-CANDIDATE simulates the objective reformulation steps of PMRES, which are very similar to how OLL reformulates the objective. In contrast to OLL, an assumption refinement step is not needed for simulating PMRES; this is essentially due to fact that the abstraction sets introduced do not introduce dependencies that could lead to cores independent of the input clauses.

K combines the cardinality constraints used by OLL and PMRES, and can hence be obtained from UNIMAXSAT by the preceding discussion on OLL and PMRES.

6 Formulating NewAlgorithms

To highlight further the potential of the UNIMAXSAT framework, we describe a novel variant ABSTCG of core-guided search as an instantiation of UNIMAXSAT. While ABSTCG could be designed on its own, viewing it as an instantiation of UNIMAXSAT immediately implies that this new algorithmic variant is correct, highlighting the usefulness of UNIMAXSAT in developing correct new MaxSAT algorithms.

ABSTCG differs from OLL in how a core C containing variables with different coefficients in the reformulated objective O′ are handled. When the literals in C contain m distinct coefficients in O′ , C is partitioned into disjoint sets C = G1 ∪. . .∪Gm so that all variables in a same set Gi have the same coefficients and the sets are ordered by decreasing coefficients. Starting from G1 (corresponding to the largest coefficient in O′ ), ABSTCG introduces in order for each Gi an abstraction set ABi = (ini, {ASCNF(∑x∈ini x ≥ j ↔ oij ) | 1 ≤ j ≤ |ini|}, outi). The inputs ini = Gi ∪ outi-1 consist of the variables in Gi and the outputs of ABi-1. Since C is an abstract core, at least one of its variables has to be assigned to 1 by any solution; the first output of the last abstraction set om1 is not be introduced.

To compute the next abstract candidate, ABSTCG updates the reformulated objective O′ by processing each abstraction set ABi = (in,D, out) very similarly to OLL. Starting from i = 1 the coefficient of each x ∈ in is lowered by wi = min({O′ (x) | x ∈ in}) and each output x ∈ out is included in O′ with coefficient wi . The inputs of each abstract set consist solely of objective variables and outputs of the previous level; hence this procedure is well-defined. Finally, the set γA = {¯x | x ∈ var(O′ )} consisting of the negations of literals in O′ with non-zero coefficients is returned. The correctness of the procedure follows by showing that γA is an abstract candidate, by similar arguments as for OLL.

Example 7. Invoke ABSTCG on F = (F,O) from Example 1 and assume the first core obtained is C1 = (b1 ∨ b2 ∨ b3 ∨ b4 ∨ b5). Core relaxation divides the variables in this core into G1 = {b3}, G2 = {b5} and G3 = {b1, b2, b4} and G2 = {b1}. The abstraction set over G1 has one output variable o11 defined by ASCNF(∑x∈G1 x ≥ 1 ↔ o11 ). (Practical implementations would use the variable b3 directly as o11 .) The abstraction set over G2 has b5 and o11 as inputs and two output variables o2i defined by ASCNF(∑x∈{b5,o1i } x ≥ i ↔ o2i ) for i = 1, 2. The abstraction set over G3 has G3 ∪ {o21 , o22 } as inputs, 4 output variables o3i defined by ASCNF(∑x∈G3∪{o21 ,o22 } x ≥ i ↔ o3i ) for i = 2 . . . 5. After reformulation, the objective O′ is O′ ≡ o11 + o21 + o22 +

o32 + o33 + o34 + o35 and the abstract candidate returned in the next iteration contains the negation of all these variables.

We developed an open-source implementation (available at https://bitbucket.org/coreo-group/cgss2/src/abstcg/) of ABSTCG on top of CGSS2, a state-of-the-art C++ implementation of OLL when compared to solvers in the 2022 MaxSAT Evaluations [Ihalainen, 2022]. To take advantage of the special feature of ABSTCG, the implementation invokes ABSTCG when an instance includes at least three different weights on the soft clauses and the median number of soft clauses for each weight is more than 25 (as a heuristic for instances that likely to contain cores which ABSTCG can divide into weight-sets in a meaningful way), and otherwise OLL.

We empirically compare the runtimes of this prototype to those of CGSS2 (employing OLL) on all 607 weighted instances from MaxSAT Evaluation 2022 using 2.6-GHz Intel Xeon E5-2670 processors under per-instance 3600-s time and 32-GB memory limit. For the 237 instances on which the prototype heuristically invoked ABSTCG (see Figure 2), ABSTCG solved 125 instances, OLL 124. ABSTCG reduced runtime by at least 2x for 13 instances, against OLL being 2x as fast on only 4 instances. The competitiveness of the prototype suggests as a proof of concept that UNIMAXSAT allows for novel algorithmic instantiations that can also be interesting from the perspective of practical solvers.

7 Conclusions

We developed a general algorithmic framework that captures in a unifying way the computations of variants of core-guided and implicit hitting sets algorithms for MaxSAT. The correctness of the framework provides a uniform way of proving the correctness of various unsatisfiability-based MaxSAT algorithms. The framework also suggests novel algorithmic variants through different instantiations; we detailed one such instantiation and showed as a proof of concept that it resulted also from a practical perspective interesting solver variant for MaxSAT. Beyond MaxSAT, the framework can also be similarly instantiated for related constraint optimization paradigms for which core-guided and IHS style solvers can and have been developed based on the constraint-agnostic notion of unsatisfiable cores.

Acknowledgements

This work has been financially supported by University of Helsinki Doctoral Programme in Computer Science DoCS and Academy of Finland under grants 322869 and 342145. The authors wish to thank the Finnish Computing Competence Infrastructure (FCCI) for supporting this project with computational and data storage resources.