Read-Once Resolution for Unsatisfiability-Based Max-SAT Algorithms

1 Introduction

The Satisfiability problem in propositional logic (SAT) is the task of deciding whether a given propositional formula has a model. Max-SAT is an optimization variant of SAT and it can be seen as a generalisation of the SAT problem. Given a propositional formula in conjunctive normal form (CNF), the objective of the Max-SAT problem is to find a variable assignment that maximizes the number of satisfied clauses.

In weighted Max-SAT, each clause has an associated weight and the goal becomes maximizing the sum of the weights of the satisfied clauses. In many problems coming from real world domains, a subset of the (hard) clauses must be satisfied, and the remaining (soft) clauses may be satisfied or not.

Algorithms for Max-SAT have been the subject of significant improvements over the last years and several families of algorithms have been developed including branch and bound algorithms [Li et al., 2007; Larrosa et al., 2008], approaches based on reformulating Max-SAT as a Weighted CSP [de Givry et al., 2003], algorithms based on iteratively calling a SAT solver [Berre and Parrain, 2010], compilation-based algorithms [Pipatsrisawat et al., 2008], and algorithms based on computing unsatisfiable cores with a SAT solver [Fu and Malik, 2006]. In particular, two families of algorithms have been intensively investigated.

∗This work is partially supported by SFI grant BEACON (09/PI/I2618).

The first family of algorithms is based on a branch and bound algorithm and they perform quite well on random and crafted instances [Li et al., 2007; Larrosa et al., 2008; Heras et al., 2008]. To reduce the search space, they compute a lower bound formed by an underestimation component and an inference component which applies inference rules based on the resolution rule for Max-SAT [Bonet et al., 2007; Larrosa et al., 2008] to transform the formula into an equivalent but simpler one.

The second family identifies unsatisfiable sub-formulas by performing successive calls to a SAT solver. Each call returns a trace from which a resolution proof of its unsatisfiability can be built [Zhang and Malik, 2003]. Each soft clause in the trace is extended with relaxation variables and cardinality constraints are added for the subsequent SAT call. These algorithms are highly competitive for industrial problems [Fu and Malik, 2006; Marques-Silva and Planes, 2008; Manquinho et al., 2009; Ans´otegui et al., 2009; 2010] and we will refer to them as unsatisfiability-based algorithms.

Unsatisfiability-based Max-SAT algorithms perform well on industrial problem instances. However, the number of relaxation variables, and the number and size of cardinality constraints can represent a drawback for these algorithms. One approach to reduce the number of relaxation variables and (indirectly) the number and size of cardinality constraints would be to actually apply Max-SAT resolution [Bonet et al., 2007; Larrosa et al., 2008] on the resolution proofs generated by unsatisfiability-based algorithms.

Building on this idea, this paper proposes the integration of the techniques used in both families of algorithms. In particular, we study how the resolution rule for Max-SAT can be applied in unsatisfiability-based solvers. First, we show that the resolution rule for Max-SAT can be safely applied as dictated by the resolution proof associated with an unsatisfiable core when such proof is read-once [Iwama and Miyano, 1995], that is, each clause is used at most once in the whole resolution process. Second, we study how this property can be integrated in an unsatisfiability-based solver. Essentially, the resolution rule for Max-SAT is applied to read-once proofs or to read-once subparts of a general resolution proof. Note that we focus our study in the algorithm of [Fu and Malik, 2006] and extended to handle weighted partial Max-SAT in [Ans´otegui et al., 2009; Manquinho et al., 2009], but read-once resolution could be also applied to other unsatisfiability-based Max-SAT solvers. Finally, we perform an empirical investigation on crafted and industrial instances of recent Max-SAT evaluations. The results show that the performance of an unsatisfiability-based Max-SAT solver is clearly improved in many benchmarks.

The paper is organized as follows. Section 2 introduces preliminary definitions and notation. Section 3 presents an unsatisfiability-based algorithm for Max-SAT. Section 4 studies read-once resolution in the Max-SAT context and Section 5 proposes its integration on unsatisfiability-based Max-SAT solvers. The experimental investigation is presented in Section 6. Finally, Section 7 points out some concluding remarks and future work.

2 Definitions

In this Section we introduce the necessary definitions and notation related to the SAT and Max-SAT problems.

2.1 SAT

We define X = {x1, x2, . . . , xn} as the set of Boolean variables. A literal is either a variable xi or its negation ¯xi. The variable to which a literal l refers is denoted by var(l). Given a literal l, its negation ¯l is ¯ xi if l is xi and it is xi if l is ¯ xi .

A clause C is a disjunction of literals. Hereafter, capital letters will represent clauses. The size of a clause, noted |C|, is the number of literals that it has. A formula in conjunctive normal form (CNF) ϕ is a set of clauses.

An assignment is a set of literals A = {l1, l2, . . . , lk} such that for all li ∈ A, its variable var(li) = xi is assigned value true or false. If variable xi is assigned to true , literal xi is satisfied and literal ¯xi is falsified. Similarly, if variable xi is assigned false , literal ¯ xi is satisfied and literal xi is falsified. If all variables in X are assigned, the assignment is called complete, otherwise it is called partial. An assignment satisfies a literal iff it belongs to the assignment, it satisfies a clause iff it satisfies one or more of its literals and it falsifies a clause iff it contains the negation of all its literals. The empty clause noted ✷ has no literals (size 0) and cannot be satisfied. If a clause is falsified by an assignment, the clause is conflicting and it can be represented using the empty clause. A model is a complete assignment that satisfies all the clauses in a CNF formula ϕ. The SAT problem is the task of finding a model for a given formula.

The Classical resolution is a well-known sound and complete inference mechanism for SAT. Given two clashing clauses (x ∨ A) and (¯x ∨ B) then the clause (A ∨ B) can be added to the formula. The new clause is usually referred to as resolvent. Clauses of size one are called unit clauses. When a formula contains a unit clause l , it can be simplied by removing all clauses containing l and removing ¯l from all the clauses where it appears. The application of this rule until fixed-point is called unit propagation and it can be understood as a resolution-based simplification.

Given a CNF formula, a subset of clauses is inconsistent if all them cannot be simultaneously satisfied by any variable assignment. The clauses involved in an inconsistent subset of clauses can be determined with several steps of resolution. This process is called resolution proof. Let each clause C be identified by a label i and denote it as Ci. A resolution proof is an ordered set:

Each clause Cj with i ≤ j ≤ k is the resolvent of applying resolution (represented by symbol ▷◁) between clashing clauses Cj′ and Cj′′ . The last resolvent in the resolution proof is always the empty clause (i.e. Ci+k = ✷). Clashing clauses generated in a previous resolution step of a resolution proof are called derived clauses, otherwise they are original. If all the clauses involved in a resolution proof are used at most once, it is called a read-once resolution proof [Iwama and Miyano, 1995], otherwise it is a general resolution proof.

Given an unsatisfiable SAT formula ϕ, a subset of clauses ϕC whose conjunction is still unsatisfiable is called an unsatisfiable core (or trace) [Zhang and Malik, 2003] of the original formula (ϕC ⊆ ϕ). Modern SAT solvers can be instructed to generate an unsatisfiable core or a general resolution proof for unsatisfiable formulas [Zhang and Malik, 2003]. Observe that an unsatisfiable core only contains the original clauses used in the related resolution proof.

2.2 Max-SAT

A weighted clause is a pair (C,w), where C is a clause and w is the cost of its falsification, also called its weight. Many real problems contain clauses that must be satisfied. We call these clauses mandatory or hard and we associate to them a special weight ⊤. Note that any weight w ≥ ⊤ indicates that the associated clause must be necessarily satisfied. Thus, we can replace w by ⊤ without changing the problem. Consequently, we can assume all weights in the interval [0..⊤]. Non-mandatory clauses are also called soft clauses. A weighted formula in conjunctive normal form (WCNF) ϕ is a set of weighted clauses.

A model is a complete assignment that satisfies all mandatory clauses. The cost of an assignment is the sum of weights of the clauses that it falsifies. Given a WCNF formula, Weighted Max-SAT is the problem of finding a model of minimum cost. Note that if a formula contains only mandatory clauses, weighted Max-SAT is equivalent to classical SAT. If all the clauses have weight 1, we have the (unweighted) MaxSAT problem. Hereafter, we will assume weighted Max-SAT.

A weighted formula ϕ′ is a relaxation of ϕ (noted ϕ′ ⊑ ϕ ) if the optimal cost of ϕ′ is less than or equal to the optimal cost in ϕ (non-models are considered to have cost infinity). Two weighted formulas ϕ′ and ϕ are equivalent (denoted as ϕ′ ≡ ϕ) if ϕ′ ⊑ ϕ and ϕ ⊑ ϕ′ .

Let u and w be two weights. Their sum is defined as, u ⊕ w = min(u + w, ⊤) in order to keep the result within the interval [0..⊤]. If u ≥ w, their subtraction is defined as,

The De Morgan laws cannot be used in Max-SAT [Bonet et al., 2007; Larrosa et al., 2008]. Instead, the following rule should be repeatedly used until the conjunctive normal form is achieved: (A ∨ l ∨C,w) ≡

{(A ∨ ¯ C,w), (A ∨ ¯l ∨ C,w)}. If a formula contains clauses (C, u) and (C, v), they can be replaced by (C, u⊕v). If a formula contains the clause (C, 0), such clause can be removed. The empty clause may appear in a formula. If its weight is ⊤, i.e. (✷,⊤), it is clear that the formula does not have any model. If its weight is w, i.e. (✷,w), the cost of any assignment will include that weight, therefore w is a lower bound of the formula optimal cost.

The resolution rule can be extended from SAT to Max-SAT [Bonet et al., 2007; Larrosa et al., 2008] as {(x ∨ A, u), (¯x ∨ B, w)} ≡ {(A∨B, m), (x∨A, u⊖m), (¯x∨B, w⊖m), (x∨ A∨ ¯B, m), (¯x ∨ ¯ A ∨ B, m)} where m = min(u, w). Briefly, (x∨A, u) and (¯x∨B, w) are the clashing clauses, (A∨B, m) is the resolvent, (x ∨ A, u ⊖ m) and (¯x ∨ B, w ⊖ m) are the posterior clashing clauses, and (x∨A∨ ¯B, m) and (¯x ∨ ¯ A ∨ B,m) are the compensation clauses.

The resolution step i of a resolution proof R including weighted clauses is noted (Ci,wi) = (Ci′ ,wi′ ) ▷◁ (Ci′′ , wi′′ ), where (Ci, wi) is the resolvent and (Ci′ , wi′ ) and (Ci′′ ,wi′′ ) are the clashing clauses. The set of compensation clauses produced by such resolution step will be noted as [(Ci′ , wi′ ) ▷◁ (Ci′′ , wi′′ )].

3 An Unsatisfiability-BasedMax-SAT Solver

Algorithm 1 summarizes a unsatisfiability-based MaxSAT algorithm to handle weighted partial Max-SAT formulas [Manquinho et al., 2009; Ans´otegui et al., 2009]. The algorithm iteratively finds unsatisfiable cores by calling a SAT solver (line 4). Lines 11-21 should be omitted as they introduce read-once resolution that will be explained later.

The input of Algorithm 1 is a Max-SAT formula ϕ. Besides, it maintains a working formula ϕW and a lower bound λ of the optimal solution which are initialized to ϕ and 0, respectively. For each unsatisfiable sub-formula ϕC, the minimum weight m of the soft clauses (i.e. (C, w) with w < ⊤) in the sub-formula (line 9) is computed. Then, the minimum weight is used to update the lower bound (line 10). Soft clauses in the unsatisfiable sub-formula are relaxed (lines 22 to 30) by adding new relaxation variables and requiring that exactly one of the relaxation variables must be assigned to true. This is usually expressed by adding cardinality constraints (line 31). Observe that if the weight of a clause is larger than m, then a copy clause of the original clause with weight m is created (and relaxed), and the weight of the original clause is decreased by m.

The first unsatisfiability-based algorithm for Max-SAT [Fu and Malik, 2006] was designed to handle unweighted partial Max-SAT, it added several relaxation variables to the same clause and it used the pairwise encoding for the cardinality constraints. More sophisticated algorithms have been developed in recent years, which add only one relaxation variable per clause, use alternative encodings for the cardinality constraints, and are able to handle weighted soft clauses and hard clauses [Marques-Silva and Planes, 2008; Manquinho et al., 2009; Ans´otegui et al., 2009; 2010].

Theorem 1 The value returned by Algorithm 1 (excluding lines 11-21) is the minimum cost of unsatisfied clauses in ϕ. Proof 1 Proof included in [Ans´otegui et al., 2009].

Algorithm 1 Weighted partial Max-SAT algorithm enhanced with read-once resolution

SOLVE(ϕ) 1 ϕW ←ϕ 2 λ← 0 3 while true 4 do (status, ϕC) ← SAT(ϕW ) 5 if status = true 6 then ✄ Solution to Weighted Max-SAT problem 7 return λ 8 ϕW ← ϕW - ϕC 9 m ← min{w|(C, w) ∈ ϕC ∧ w < ⊤} 10 λ ← λ + m 11 RC ← getProof(ϕC ) 12 for each (Ci, wi) = (Ci′ , wi′ ) ▷◁ (Ci′′ , wi′′ ) ∈ RC 13 do 14 if ROR((Ci, wi), RC ) 15 then (Ci′ , wi′ ) ← (Ci′ , wi′ ⊖ m) 16 (Ci′′ , wi′′ ) ← (Ci′′ , wi′′ ⊖ m) 17 ϕC ← ϕC - {(Ci′ , wi′ ), (Ci′′ , wi′′ )} 18 ϕW ← ϕW ∪ {(Ci′ , wi′ ), (Ci′′ , wi′′ )} 19 ϕW ← ϕW ∪ {[(Ci′ , wi′ ) ▷◁ (Ci′′ , wi′′ )]} 20 if Ci ̸= ✷ 21 then ϕC ← ϕC ∪ {(Ci , m)} 22 VR ← ∅ 23 for each (C, w) ∈ ϕC with w < ⊤ 24 do 25 r is a new relaxation variable 26 VR ← VR ∪ {r} 27 ϕC ← ϕC ∪ {(C ∪ {r}, m)} 28 if w > m 29 then (C, w) ← (C, w ⊖ m) 30 else ϕC ←ϕC - {(C,w)} 31 ϕC ← CNF(∑r∈VR r = 1) 32 ϕW ← ϕW ∪ ϕC

4 Read-Once Resolution inMax-SAT

For each unsatisfiable core, unsatisfiability-based Max-SAT algorithms add a set of relaxation variables and cardinality constraints to the formula. Recall that we can always retrieve a resolution proof from any unsatisfiable core. A different approach would be to apply Max-SAT resolution as dictated by such a resolution proof in order to increase the weight of the empty clause. As a result, the relaxation variables and cardinality constraints would not be necessary. However, this approach cannot be applied in general:

Example 1 Let ϕ = {(x1 ∨ x2, 1)i1, (¯x1 ∨ x2, 1)i2, (¯x2 ∨ x3, 1)i3, (¯x2 ∨ ¯x4, 1)i4, (¯x3 ∨ x4, 1)i5} and a SAT solver returned the following resolution proof R = {(i6 = i1 ▷◁ i2), (i7 = i6 ▷◁ i3), (i8 = i7 ▷◁ i5), (i9 = i6 ▷◁ i4), (i10 = i8 ▷◁ i9)}. The soft clause with identifier i6 is used twice in the proof. In the Max-SAT context, the application of MaxSAT resolution between two clashing soft clauses produces a new resolvent but also the clashing clauses may disappear (ie. their weight equals 0). Hence, if we apply MaxSAT resolution as dictated by R, we cannot continue at step (i9 = i6 ▷◁ i4) because clause i6 has been consumed at step (i7 = i6 ▷◁ i3). Then, the empty clause cannot be increased.

In other words, when soft clauses with weights greater than 0 are resolved more than once, Max-SAT resolution does not ensure to produce resolvents with weight greater than 0. Hence, it would be interesting to study what happens if we restrict the application of resolution to the case in which each clause is used at most once in a proof. This process is referred to as Read-once resolution (ROR) [Iwama and Miyano, 1995]. ROR is an incomplete calculus in which pairs of clashing clauses (x ∨ A) and (¯x ∨ B) are resolved into (A ∨ B) and then both clashing clauses disappear from the formula.

Remark 1 ROR is an incomplete calculus, that is, it cannot generate resolution proofs for some unsatisfiable formulas. This is a known result [Iwama and Miyano, 1995].

When we look at the recent Max-SAT resolution, we observe that it has precisely a similar behavior to read-once resolution. In particular, when both clashing clauses are soft, they may disappear after the resolution step. The main difference is that Max-SAT resolution adds new compensation clauses to recover an equivalent Max-SAT formula.

Observe that current branch and bound Max-SAT solvers apply the Max-SAT resolution rule when different unsatisfiable formulas describing a specific pattern are detected [Li et al., 2007; Larrosa et al., 2008; Heras and Larrosa, 2008; Li et al., 2010]. Such patterns include a small set of binary and unary clauses and each clause is resolved once. In [Heras et al., 2008], it is shown that for each unsatisfiable sub-formula detected by unit propagation, a resolution proof using each clause once can be always built. However, there are unsatisfiable sub-formulas with ROR proofs that cannot be detected by solely applying unit propagation:

Example 2 Let be ϕ = {(x1 ∨ x2)i1, (¯x1 ∨ x2)i2, (x1 ∨ ¯x2)i3, (¯x1 ∨ ¯x2)i4} and its associated ROR proof R = {(i5 = i1 ▷◁ i2), (i6 = i3 ▷◁ i4), (i7 = i5 ▷◁ i6)}. Clearly, unit propagation cannot prove the unsatisfiability of ϕ.

In [Cooper et al., 2010], the same observation reported in Example 1 is studied in the context of the Weighted Constraint Satisfaction Problem (WCSP). Recall that the MaxSAT problem can be seen as a WCSP in which variables are boolean and clauses are forbidden tuples of weighted constraints. The authors propose using rational weights in order to produce equivalent WCSP problems which remain in the arc level, that is, all transformations produce constraints of at most size two. Differently, our approach considers natural weights but it allows resulting clauses of size greater than 2.

5 Unsatisfiability-BasedMax-SAT with ROR

Algorithm 1 contains the necessary code to apply MaxSAT resolution when the read-once resolution (ROR) criterion is executed between lines 11-21. The resolution proof RC associated to each unsatisfiable core is built in line 11 [Zhang and Malik, 2003]. Then, the algorithm iterates over the resolution steps as dictated by RC. For each read-once step, Max-SAT resolution is actually applied (line 14 to 21). In particular, the weights of the clashing clauses (Ci′ ,wi′ ) and (Ci′′ ,wi′′ ) are decreased by m (lines 15 and 16). If the clashing clauses are soft (this detail is omitted from the pseudocode), they are removed from the unsatisfiable core ϕC

Algorithm 2 Determines if a clause is hard or not.

HARD((Ci, wi), R) 1 if Input((Ci,wi),R) ∧wi = ⊤ 2 then 3 return true 4 if Input((Ci,wi),R) ∧wi ̸= ⊤ 5 then 6 return false 7 {(Ci′ ,wi′ ), (Ci′′ ,wi′′ )} ← ancestors((Ci,wi),R) 8 return Hard((Ci′,wi′ ),R) ∧Hard((Ci′′ ,wi′′ ),R)

Algorithm 3 Determines if a clause is hard or it and its ancestors are used at most once.

ROR((Ci, wi), R) 1 if Hard((Ci,wi),R) 2 then 3 return true 4 if Input((Ci,w)i,R) ∧Used(Ci,w),R) = 1 5 then 6 return true 7 if Used(Ci,wi),R) > 1 8 then 9 return false 10 {(Ci′ ,wi′ ), (Ci′′ , wi′′ )} ← ancestors((Ci, wi),R) 11 return ROR((Ci′ ,wi′ ),R) ∧ROR((Ci′′ ,wi′′ ),R)

(line 17) but the resolvent is added to ϕC (line 21). If the clashing clauses are hard they are just maintained in the core as they may be used again in a different resolution step. Finally, the clashing and compensation clauses are added to the working formula ϕW (lines 18 and 19).

In what follows we introduce the read-once criterion. Let be (Ci,wi) = (Ci′ ,wi′) ▷◁ (Ci′′ ,wi′′) a resolution step in a proof R. The function ancestors((Ci,wi),R) returns the pair of clauses (Ci′ , wi′ ) and (Ci′′ , wi′′ ) from which (Ci , wi) was derived as dictated by R. Predicate Input((Ci, wi),R) returns true if clause (Ci,wi) is an original clause in proof R (i.e. it is not a resolvent of any step in R), otherwise it returns false. Function Used((Ci,wi),R) returns how many times clause (Ci,wi) is resolved in proof R. Predicate Hard((Ci,wi),R) (see Algorihm 2) returns true if clause (Ci,wi) is an input hard clause or if all its ancestors are hard, otherwise it returns false. Finally, predicate ROR((Ci,w),R) (see Algorihm 3) returns true if clause (Ci,wi) is hard or if it and all of its soft ancestors have been used at most once in the resolution proof R.

Consider (Ck,wk) = (Ck′ ,wk′ ) ▷◁ (Ck′′ ,wk′′ ), where (Ck, wk) is the last resolvent in a resolution proof R. Clearly, if ROR((Ck,wk)) is true it means that the entire resolution proof R is read-once. When this happens the algorithm does not need to add relaxation variables neither cardinality constraints. This could be a key advantage to improve the efficiency of the original algorithm. More concretely, when the last step of resolution is ROR the related resolvent is equal to the empty clause (✷,m). As we have increased the lower bound in line 10 we don't add the empty clause to the formula as it would mean adding twice the same contribution to the lower bound (line 20).

Observe that Algorithms 2 and 3 are in practice implemented with a standard depth first search, that visits each resolution proof node at most once.

Theorem 2 Algorithm 1 with ROR (including lines 11-21) returns the minimum cost of unsatisfied clauses in ϕ.

Proof 2 (Sketch) The proof shows that any transformation to the working formula ϕW results in a Max-SAT equivalent formula [Ans´otegui et al., 2009]. This invariant needs to be maintained in the whole algorithm. The general algorithm (i.e. by excluding lines 11-21) is known to be correct, again because at each iteration ϕW is transformed into an equivalent formula [Ans´otegui et al., 2009]. What remains to be shown is that the lines 11-21 respect the invariant. Suppose any subtree of a general resolution proof where each clause is used at most once (ie. ROR subtree). Max-SAT resolution can be applied to such subtree and then the resulting formula is guaranteed to be equivalent and the last resolvent has weight greater than 0 [Bonet et al., 2007; Larrosa et al., 2008] (otherwise the subtree is not ROR). Let be R the resulting resolvent of the last resolution step after applying resolution to such ROR subtree. Now, the general resolution proof can be transformed by replacing the whole ROR subtree with the resulting clause R (and compensation clauses are properly added to the working formula). Finally, the modifications made in 11-21 provide an equivalent formula and unsatisfiable core for the line 22, hence the termination is guaranteed from [Ans´otegui et al., 2009].

6 Experimental Results

In order to evaluate the use of read-once resolution inside an unsatisfiability-based Max-SAT solver, we extended the C++ MSUNCORE [Manquinho et al., 2009] Max-SAT solver (shortly WMSU1) which interfaces PICOSAT [Biere, 2008] as SAT solver. WMSU1 is similar to the original [Fu and Malik, 2006] solver but it is extended to handle weighted partial Max-SAT [Ans´otegui et al., 2009; Manquinho et al., 2009] and it uses the bitwise encoding for the cardinality constraints [Prestwich, 2007].

Due to clause minimization techniques in PICOSAT, it returns traces which contain only the original clauses involved in the core, but the order of clauses does not represent the actual resolutions steps. To integrate ROR into the Max-SAT solver, these unordered traces need to be reordered into actual resolution proofs [Beame et al., 2004]. The reordeing is performed with the TRACECHECK tool 1 .

In our experiments, we considered all industrial and partial crafted instances coming from recent Max-SAT Evaluations 2 . We considered all the unweighted Max-SAT industrial and unweighted partial Max-SAT industrial instances from the 2009 Max-SAT Evaluation since in the 2010 edition only a subset was considered. For the remaining categories, we considered the instances in the 2010 Max-SAT Evaluation. All experiments were conducted on a HPC cluster with 50 nodes, each node is a CPU Xeon E5450 3GHz, 32GB RAM and Linux. A time limit of 1200 seconds and 2GB of memory were given for each execution.

1 http://fmv.jku.at/booleforce/

2 http://www.maxsat.udl.cat/

Preliminary experiments with ROR transformations showed that traces (input files for TRACECHECK) and actual proofs (output files of TRACECHECK) can be very large for some industrial benchmarks (up to hundreds of megabytes). Besides, for too large proofs, the unrestricted application of resolution could increase substantially the size of the formula. For these reasons, we restricted the application of ROR to traces and proofs up to a maximum file size (2 MB for traces and 20 MB for proofs). We manually set such limits with respect to a small set of industrial instances and such limit was fairly good in general.

Table 1 shows the number of instances solved by each solver within the time limit. The first column shows the name of the benchmark set. The second column presents the total number of instances for each set. The third and fourth columns show the number of solved instances by WMSU1 and the average time for the solved instances of each set, respectively. Similarly, the fifth and sixth columns show the number of solved instances by WMSU1-ROR (ie. WMSU1 with ROR) and the average time for each set, respectively.

We observe that ROR improve the performance of WMSU1 in many of the 31 benchmark sets. In particular, there is an improvement in 14 sets and a slight worsening in 2 sets. Significant improvements are reported in some industrial benchmarks such as Bcp-fir, Bcp-hipp-su, and Bcp-msp but also in crafted benchmarks such as Scheduling, Warehouses and RandomNet. Observe that 211 unsolved instances by WMSU1 become solved by WMSU1-ROR, that is, 19% of the instances are solved by adding ROR.

Figure 1 presents a scatter plot comparing the cpu time in seconds required by WMSU1 and WMSU1-ROR in all the instances that can be solved by at least one of them. The scatter plot shows that WMSU1 requires less time for instances that can be solved by both solvers. But, WMSU1ROR aborts much fewer instances than WMSU1.

Finally, Table 2 shows the number of solved instances by state-of-the-art Max-SAT solvers including WPM1 [Ans´otegui et al., 2009] , MINIM [Heras et al., 2008], SAT4J [Berre and Parrain, 2010], PM2 [Ans´otegui et al., 2009] and WPM2 [Ans´otegui et al., 2010]. For unweighted MaxSAT, WMSU1-ROR notably improves the performance of WMSU1 but there are more efficient solvers. For weighted Max-SAT, WMSU1 is the most robust solver.

7 Conclusions and Future Work

This paper proposes to apply Max-SAT resolution in an unsatisfiability-based Max-SAT solver when the unsatisfiable core has an associated ROR proof or to subparts of a general proof which are also read-once. Future work includes integrating read-once resolution in other unsatisfiabilitybased Max-SAT solvers, including WMSU4 [Marques-Silva and Planes, 2008], PM2 [Ans´otegui et al., 2009] and WPM2[Ans´otegui et al., 2010]. Moreover, we will study under which conditions general proofs can be converted into ROR proofs for Max-SAT.