Boolean Lexicographic Optimization Joao Marques-Silva1 , Josep Argelich2 , Ana Graça3 , and Inês Lynce3 1 CSI/CASL, University College Dublin, Ireland jpms@ucd.ie 2 DIEI, Universitat de Lleida, Spain jargelich@diei.udl.cat 3 INESC-ID/IST, Technical University of Lisbon, Portugal {assg,ines}@sat.inesc-id.pt Abstract Multi-Objective Combinatorial Optimization (MOCO) problems find a wide range of practical application problems, some of which involving Bool- ean variables and constraints. This paper develops and evaluates algorithms for solving MOCO problems, defined on Boolean domains, and where the optimality criterion is lexicographic. The proposed algorithms build on exist- ing algorithms for either Maximum Satisfiability (MaxSAT), Pseudo-Boolean Optimization (PBO), or Integer Linear Programming (ILP). Experimental re- sults, obtained on problem instances from haplotyping with pedigrees, show that the proposed algorithms can provide significant performance gains over state of the art MaxSAT, PBO and ILP algorithms. 1 Introduction Real-world optimization problems often involve multiple objectives, that can rep- resent conflicting purposes. There has been a large body of work on solving multi- objective combinatorial optimization (MOCO) problems, for example [14, 32, 15]. Nevertheless, some of these MOCO problems have natural Boolean formulations, and so Boolean-based optimization solutions could be expected to provide effective alternative solutions. This paper addresses MOCO problems where the variables are Boolean, the constraints are represented by linear inequalities (or clauses), and the optimization criterion is lexicographic. Given a sequence of cost functions, an optimization criterion is said to be lexicographic whenever there is a preference in the order in which cost functions are optimized. There are many examples where optimization is expected to be lexicograhic. For example, suppose that instead of requiring a balance between price, horsepower and fuel consumption for choosing a new car, you have made a clear hierarchy in your mind: you have a strict limit on how much you can afford, then you will not consider a car with less than 150 horsepower and after that the less the fuel consumption the better. Not only you es- tablish a priority in your preferences, but also each optimization criterion is defined in such a way that the set of potential solutions gets subsequently reduced. Such kind of problems are present not only in your daily life but also in many real appli- cations, and representative examples can be found in recent surveys [15, 32, 14]. This paper develops and evaluates algorithms for Boolean lexicographic opti- mization problems, and has three main contributions. First, it formalizes Boolean Proceedings of the 17th International RCRA workshop (RCRA 2010): Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion Bologna, Italy, June 10–11, 2010 CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings Lexicographic Optimization. Second, it describes practical algorithms for solv- ing Boolean Lexicographic Optimization, either based on pseudo-Boolean opti- mization (PBO), 0-1 Integer Linear Programming (ILP), or Maximum Satisfiabil- ity (MaxSAT) algorithms. Third, the paper illustrates the practical usefulness of the proposed algorithms. The experimental evaluation is focused on a concrete ap- plication, namely haplotyping with pedigree information [18]. Nevertheless, the techniques proposed in this paper are general, and have been successfully used in other contexts 1 . The paper is organized as follows. Section 2 overviews MaxSAT, PBO, and Lexicographic Optimization. Afterwards, Section 3 describes four alternative ap- proaches for solving lexicographic optimization problems. Section 4 conducts a detailed experimental evaluation on hard problem instances from haplotyping with pedigree information. State of the art MaxSAT, PBO and ILP solvers are then com- pared against the algorithms described in this paper. Section 5 summarizes related work and Section 6 concludes the paper. 2 Preliminaries This section overviews the Maximum Satisfiability (MaxSAT) problem and its vari- ants, as well as the Pseudo-Boolean Optimization (PBO) problem. The main ap- proaches used by state-of-the-art solvers are summarized, including recent unsat- isfiability-based MaxSAT algorithms. To conclude, this section provides a brief overview of Multi-Objective Combinatorial Optimization (MOCO) [14, 15], fo- cusing on lexicographic optimization. 2.1 Maximum Satisfiability Given a CNF formula C, the Maximum Satisfiability (MaxSAT) problem con- sists in finding an assignment that maximizes the number of satisfied clauses. Well-known variants of the MaxSAT problem include weighted MaxSAT, partial MaxSAT and weighted partial MaxSAT. All these formulations find a wide range of practical applications [21]. The general weighted partial MaxSAT problem for- mulation assumes a CNF formula C, where each clause c ∈ C is associated with a weight w, and where clauses that must be satisfied have weight w = >. The optimization problem is to find a truth assignment such that the cost of the satisfied clauses is maximized. The last decade has seen a large number of alternative algorithms for MaxSAT. These can be broadly categorized as branch-and-bound with lower bounding, de- composition-based, translation to pseudo-Boolean constraints and unsatisfiability based. Branch-and-bound algorithms integrate lower bounding and inference tech- niques, and represent the more mature solutions, i.e. which have been studied more extensively in the past. A recent alternative are unsatisfiability-based algo- rithms, that are built on the success of modern SAT solvers, and which have been 1 For example, in a recent competition of solvers for solving package upgradeability problems [3]. 2 shown to perform well on problem instances from practical applications. Exam- ples of branch-and-bound algorithms include: MaxSatz [22], IncMaxSatz [23], WMaxSatz [4], and MiniMaxSAT [20]. A well-known example of translation to PB constraints is SAT4J-MaxSAT [8]. Examples of decomposition-based solvers include Clone [30] and sr(w) [31]. In recent years, several unsatisfiability-based MaxSAT algorithms have been proposed. The original approach was proposed in [17], and recent solvers include MSUnCore [28, 27, 26], WBO [26], WPM1 and PM2 [2]. 2.2 Pseudo-Boolean Optimization Pseudo-Boolean Optimization (PBO) is an extension of SAT where constraints are linear inequalities, with integer coefficients and Boolean variables. The objective in PBO is to find an assignment to problem variables such that all problem constraints are satisfied and the value of a linear objective function is optimized. The PBO normal form [7] is defined as follows: P minimize vj · lj j∈N P subject to aij lj ≥ bi , (1) j∈N lj ∈ {xj , x̄j }, xj ∈ {0, 1}, aij , bi , vj ∈ N+ 0 Observe that any pseudo-Boolean formulation can be translated into a normal form. Modern PBO algorithms generalize the most effective techniques used in mod- ern SAT solvers. These include unit propagation, conflict-driven learning and conflict-directed backtracking [25, 9]. Despite a number of common techniques, there are several alternative approaches for solving PBO. The most often used ap- proach is to conduct a linear search on the value of the objective function. In addition, the use of binary search has been suggested and evaluated in the recent past [12, 10]. SAT algorithms can be generalized to deal with pseudo-Boolean con- straints natively [7] and, whenever a solution to the problem constraints is identi- fied, a new constraint is created such that only solutions corresponding to a lower value of the objective function are allowed. The algorithm terminates when the solver cannot improve the value of the cost function. Another often used solution is based on branch and bound search, where lower bounding procedures to esti- mate the value of the objective function are used, and the upper bound is iteratively refined. Several lower bounding procedures have been proposed over the years, e.g. [11, 25]. There are also algorithms that encode pseudo-Boolean constraints into propositional clauses [34, 6, 13] and solve the problem by subsequently us- ing a SAT solver. This approach has been proved to be very effective for several problem sets, in particular when the clause encoding is not much larger than the original pseudo-Boolean formulation. 2.3 MaxSAT, PBO & BMO Although MaxSAT and PBO are different formalisms, there are well-known map- pings from MaxSAT to PBO and vice-versa [19, 1, 20]. The remainder of the paper 3 uses both formalisms interchangeably. A set of clauses or constraints is denoted by C. Without loss of generality, linear constraints are assumed to represent clauses, thus representing instances of the Binate Covering Problem [11]. For the general case where linear constraints represent PB constraints, there are well-known map- pings from PB constraints to CNF formulas [34, 13, 33], which could be used if necessary. Mappings from soft clauses to cost functions and vice-versa P are also well- known [20]. For example, suppose the cost function min j vj · xj . A set of soft clauses can replace this cost function: for each xj create a soft clause (x̄j ) with cost vj . Similarly, a set of soft clauses can be represented with a cost func- tion. Suppose a set of soft clauses Ca , where each clause cj ∈ Ca is associated a weight wj . Replace each clause cj with c0j = cj ∨ s̄j , where sj is a relaxation P variable, and create the cost function min j wj · sj . Boolean Multilevel Optimization [5] is a restriction of weighted (partial) Max- SAT, with an additional condition on the clause weights. BMO is defined on a set of sets of clauses C = C0 ∪C1 ∪. . .∪ Cm , where {C0 , C1 , . . . , Cm } forms a partition of C, and a weight is associated with each set of clauses: hw0 = >, w1 , . . . , wm i, such that wi is associated with each clause c in each set Ci . C0 represents the hard clauses, each with weight w0 = >. Although C0 may be empty, it is assumed that Ci 6= ∅, i = 1, . . . , m. Definition 1 (BMO). An instance of Weighted (Partial) Maximum Satisfiability is an instance of BMO iff the following condition holds: X wi > wj · |Cj | i = 1, . . . , m − 1 (2) i+1≤j≤m BMO can be viewed as a technique for identifying lexicographic optimization conditions in MaxSAT and PBO problem instances. This is further highlighted in the following sections. 2.4 Lexicographic Optimization Multi-Objective Combinatorial Optimization (MOCO) [14, 32, 15] is a well-known area of research, with many practical applications, including Operations Research and Artificial Intelligence. Lexicographic optimization represents a specialization of MOCO, where the optimization criterion is lexicographic. Motivated by the wide range of practical applications, Lexicographic Optimization is also often re- ferred to Preemptive Goal Programming or Lexicographic Goal Programming [32]. This section introduces Boolean Lexicographic Optimization (BLO), a restriction of lexicographic optimization, where variables are Boolean, all cost functions and constraints are linear, and the optimization criterion is lexicographic. The notation and definitions in this section follow [14], subject to these additional constraints. A set X of variables is assumed, with X = {x1 , . . . , xn }. The domain of the variables is X = {0, 1}n . A point in X is represented as x ∈ X or (x1 , . . . , xn ) ∈ X . A set of p linear functions is assumed, all of which are defined on Boolean 4 variables, fk : {0, 1}n → Z, 1 ≤ k ≤ p: X fk (x1 , . . . , xn ) = vk,j · lj (3) 1≤j≤n where lj ∈ {xj , x̄j }, and vk,j ∈ N+ 0 . The p cost functions capturing the opti- mization problem represent a multi-dimensional function: f : {0, 1}n → Zp , with f (x) = (f1 (x), . . . , fp (x)). The optimization problem is defined on these p functions, subject to satisfying a set of constraints: lexmin (f1 (x1 , . . . , xn ), . . . , fp (x1 , . . . , xn )) P subject to aij lj ≥ bi , (4) j∈N lj ∈ {xj , x̄j }, xj ∈ {0, 1}, aij , bi ∈ N+ 0 Any point x ∈ {0, 1}n which satisfy the constraints is called a feasible point. For any two vectors y1 , y2 ∈ Zp , with y1 = (y11 , . . . , yp1 ) and y2 = (y12 , . . . , yp2 ), the lexicographic comparison (, w1 , . . . , wp i Output: Lexicographic Optimum Solution 1 for k ← 1 to p do 2 C ← C0 ∪ · · · ∪ Ck // Current set of clauses 3 Crsc ← RescaleWeights(C, hµ1 , . . . , µk − 1i) // Update clause weights 4 o ← MaxSAT(Crsc ) 5 µk ← GetMinCost(Crsc , o, hµ1 , . . . , µk − 1i) // Record min cost for k 6 return (µ1 , . . . , µp ) Algorithm 2: MaxSAT-based BLO algorithm with weight rescaling Input : Sets of clauses hC0 , C1 , . . . , Cp i with corresponding weights h>, w1 , . . . , wp i Output: Lexicographic Optimum Solution 1 CH ← C0 // Initial hard clauses 2 for k ← 1 to p do 3 CS ← Ck // Current soft clauses 4 r , C r }) ← UnsatMaxSAT({C , C }) (µ, {CH S H S 5 µk ← µ // Record min cost for k 6 CH ← CH r ∪ Cr // Harden soft clauses S 7 return (µ1 , . . . , µp ) Algorithm 3: Unsatisfiability-based MaxSAT BLO algorithm wi · (µi + 1), which can be lower than wi · (|Ci | + 1). The function GetMinCost translates the optimum solution given by the MaxSAT solver, that involves all the sets of clauses up to Ck , to the number of unsatisfied clauses of current set Ck associated to µk . The weights returned by the algorithm may affect the original weights, such that µi ≤ wi . The same holds for the weight associated with hard clauses as it depends on the weights given to soft clauses. Although the rescaling method is effective at reducing the weights that need to be considered, for very large problem instances the challenge of large clause weights can still be an issue. 3.4 Iterative Unsatisfiability-Based MaxSAT Solving Our final approach for solving BLO problems is based on unsatisfiability-based MaxSAT algorithms. A possible organization is shown in Algorithm 3. Similarly to the organization of the other algorithms, Algorithm 3 executes p iterations, and each cost function is analyzed separately, in order. At each step a (unsatisfiability-based) partial MaxSAT solver is called on a set of hard and soft 7 clauses. The result corresponds to the minimum unsatisfiability cost for the set of clauses Ck . In contrast to previous algorithms, the CNF formula is modified in each iteration. Clauses relaxed by the unsatisfiability-based MaxSAT algorithm are kept and become hard clauses for the next iterations. The hardening of soft clauses after each iteration can be justified by associating sufficiently large weights with each cost function. When analyzing cost function k, relaxing clauses associated with cost functions 1 to k − 1 is irrelevant for computing the optimum value at iteration k. The unsatisfiability-based lexicographic optimization approach inherits some of the drawbacks of unsatisfiability-based MaxSAT algorithms. One example is that, if the minimum cost unsatisfiability cost is large, then the number of iterations may render the approach ineffective. Another drawback is that, when compared to the previous algorithms, a tighter integration with the underlying MaxSAT solver is necessary. Interestingly, a well-known drawback of unsatisfiability-based MaxSAT algorithms is addressed by the lexicographic optimization approach. Unsatisfia- bility-based MaxSAT algorithms iteratively refine lower bounds on the minimum unsatisfiability cost. Hence, in case the available computational resources are ex- ceeded, the algorithm terminates without providing an approximate solution to the original problem. In contrast, the lexicographic optimization approach allows ob- taining intermediate solutions, each representing an upper bound on the minimum unsatisfiability cost. 3.5 Discussion The previous sections describe four different approaches for solving Boolean lex- icographic optimization problems. Some of the main drawbacks were identified, and will be evaluated in the results section. Although the proposed algorithms re- turn a vector of optimum cost function values, it is straightforward to obtain an aggregated result cost function, e.g. using (5). Moreover, and besides serving to solve complex lexicographic optimization problems, the proposed algorithms can provide useful information in practical settings. For example, the iterative algo- rithms provide partial solutions (satisfying some of the target criteria) during their execution. These partial solutions can be used to provide approximate solutions in case computing the optimum value exceeds available computation resources. Given that all algorithms analyze the cost functions in order, the approximate solu- tions will in general be much tighter than those provided by algorithms that refine an upper bound (e.g. Minisat+). The proposed techniques can also be used for solving already existing problem instances. Indeed, existing problem instances may encode lexicographic optimiza- tion in the cost function or in the weighted soft clauses. This information can be exploited for developing effective solutions [5]. For example, the BMO condition essentially identifies PBO or MaxSAT problem instances where lexicographic op- timization is modelled with an aggregated cost function (represented explicitly or with weighted soft clauses) [5]. In some settings, this is an often used modelling solution. Hence, the BMO condition can be interpreted as an approach to convert from an aggregated cost function to a lexicographic optimization problem. 8 Finally, the algorithms proposed proposed in the previous sections accept cost functions implicitly specified by soft constraints. This provides an added degree of modelling flexibility when compared with the abstract definition of (Boolean) lexicographic optimization. 4 Results This section evaluates existing state of the art PBO and MaxSAT solvers, as well as the algorithms described in the previous section, on lexicographic optimiza- tion problem instances resulting from haplotyping with pedigree information [18]. The problem of haplotyping with pedigrees is an example of lexicographic opti- mization, because there are two cost functions, and preference is given to one of the cost functions. Albeit this section focuses on a concrete application, similar conclusions have been independently obtained in a recent competition for solving software package upgradeability problems [3]. For the haplotyping with pedigree information problem instances, there are two cost functions. For the software up- gradeability problem instances there are either two or three cost functions. All experimental results were obtained on 3 GHz Xeon 5160 servers, with 4 GB of RAM, and running RedHat Enterprise Linux. The CPU time limit was set to 1000 seconds, and the memory limit was set to 3.5 GB. For the experimenta- tion, a well-known commercial ILP solver as well as the best performing PBO and MaxSAT solvers of the most recent evaluations2 were considered. As a result, the following solvers were used in the experiments: CPLEX, SCIP, Minisat+, BSOLO, MiniMaxSat, MSUnCore, WPM1, SAT4J-PB, SAT4J-MaxSAT. Other well-known MaxSAT solvers (among the best performing in the MaxSAT evaluations) were also considered. However, the large size and intrinsic hardness of the problem in- stances resulted in these solvers being unable to provide results for any instance. Consequently, these solvers were discarded. The haplotyping with pedigrees problem instances can be generated with dif- ferent optimizations to the core model [18]. For the results presented in this section, 500 of the most difficult problem instances were selected. These instances are the most difficult for the best performing solver; hence any other instances would be easier to solve by the best performing solver. The results are organized in two parts. The first part evaluates the number of instances aborted within the CPU time and physical memory limits. The second part compares the CPU times. In all cases, the focus is on evaluating the effectiveness of the proposed algorithms for solving lexi- cographic optimization problems. The approach considered as default corresponds to the aggregated cost function algorithm. Table 1 shows the number of aborted instances, i.e. instances that a given solver cannot prove the optimum within the allowed CPU time limit or memory limit. The results allow drawing several conclusions. First, for some solvers, the use of dedicated lexicographic optimization algorithms can provide remark- able performance improvements. A concrete example is Minisat+. The default solver aborts most problem instances, whereas Minisat+ integrated in an iterative 2 http://www.maxsat.udl.cat/ and http://www.cril.univ-artois.fr/PB09/. 9 # Aborted BLO Solution Solver Plain BLO Default Solvers CPLEX 465 464 Minisat+ 496 56 Iterated PBO BSOLO 456 500 SCIP 495 474 SAT4J-PB 463 435 SAT4J-MaxSAT 464 404 Iterated MaxSAT WPM1 69 72 with Rescaling MSUnCore 84 85 MiniMaxSat 500 500 Iterated Unsat-based MSUnCore 84 51 MaxSAT Table 1: Aborted problems instances (out of 500) pseudo-Boolean BLO solver ranks among the best performing solvers, aborting only 56 problem instances (i.e. the number of aborted instances is reduced in more than 85%). Second, for some other solvers, the performance gains are significant. This is the case with MSUnCore. For MSUnCore, the use of unsatisfiability-based lexicographic optimization reduces the number of aborted faults in close to 40%. SAT4J-PB integrated in an iterative pseudo-Boolean solver, reduces the number of aborted instances in close to 6%. Similarly, SCIP integrated in an iterative pseudo- Boolean solver, reduces the number of aborted instances in more than 4%. Despite the promising results of using iterative pseudo-Boolean solving, there are exam- ples for which this approach is not effective, e.g. BSOLO. This suggests that the effectiveness of this solution depends strongly on the type of solver used and on the target problem instances. The results for the MaxSAT-based weight rescaling algorithm are less conclusive. There are several justifications for this. Given that existing branch and bound algorithms are unable to run large problem instances, the MaxSAT solvers considered are known to be less dependent on clause weights. Figures 1, 2, 3, 4 and 5 show scatter plots comparing the run times for dif- ferent solvers on the same problem instances. Each plot compares two different approaches, where each point represents one problem instance, being the x-axis value given by one approach and the y-axis value given by the other. Again, sev- eral conclusions can be drawn. Figures 1, 2 and 3 confirm the effectiveness of the algorithms proposed in this paper, namely iterative PB solving and iterative unsatisfiability-based MaxSAT. Despite the remarkable improvements in the per- formance of Minisat+ when integrated in a lexicographic optimization algorithm, MSUnCore integrated in lexicographic optimization algorithm provides the best performance in terms of aborted problem instances. Nevertheless, the use of BLO adds overhead to the solvers, and so for most instances the best performance is obtained with the default solver WPM1. These conclusions are further highlighted in Figures 4 and 5. Although WPM1 is the best performing algorithm without lexicographic optimization support, MSUnCore with lexicographic optimization provides more robust performance, namely for the hardest problem instances. 10 103 103 Minisat+-BLO SCIP-BLO 102 102 101 101 100 100 100 101 102 103 100 101 102 103 Minisat+ SCIP Figure 1: Original Minisat+ and SCIP vs. iterated pseudo-Boolean solving 103 103 MSUnCore-BLO MSUnCore-BLO 102 102 101 101 100 100 100 101 102 103 100 101 102 103 Minisat+-BLO SCIP-BLO Figure 2: Iterated unsat-based MaxSAT vs. iterated pseudo-Boolean solving 4.1 Discussion The experimental results provide useful insights about the behavior of the solvers considered. For example, Minisat+ performs poorly when an aggregated cost func- tion is used. However, it is among the best performing solvers when integrated in the iterative pseudo-Boolean solving framework. In contrast, the improvements to SCIP are far less notable. These performance differences are explained by the structure of the problem instances. For Minisat+ the main challenge is the relatively complex aggregated cost function. Hence, the use of iterated pseudo-Boolean solv- ing eliminates this difficulty, and so Minisat+ is able to perform very effectively on the resulting problem instances, which exhibit hard to satisfy Boolean constraints. In contrast, SCIP is less sensitive to the cost function, and the iterative approach does not help with solving the (hard to solve) Boolean constraints. Hence, the use of iterative pseudo-Boolean solving is less effective for SCIP for the problem in- stances considered. The results for MSUnCore and iterative unsatisfiability-based MaxSAT indicate that the use of BLO solvers provides added robustness, at the cost of additional overhead for problem instances that are easy to solve. 5 Related Work Recent surveys on MaxSAT and PBO solvers are available in [21, 33]. Lexico- graphic optimization has a long history of research, with many different algorithms and applications. Examples of recent surveys are provided in [14, 15, 32]. The it- erative pseudo-Boolean solving approach (see Section 3.2) is tightly related with the standard organization of Lexicographic Optimization algorithms [14]. 11 103 103 MSUnCore-BLO Minisat+-BLO 102 102 101 101 100 100 100 101 102 103 100 101 102 103 MSUnCore SCIP-BLO Figure 3: Comparison of BLO solutions 103 103 MSUnCore-BLO MSUnCore 102 102 101 101 100 100 100 101 102 103 100 101 102 103 WPM1 WPM1 Figure 4: BLO improvement on MSUnCore vs. WPM1 In the area of Boolean-based optimization procedures, there has been prelim- inary work on solving pseudo-Boolean MOCO problems [24]. Nevertheless, this work addresses exclusively Pareto optimality, and does not cover lexicographic op- timization. In the area of constraints and preferences, lexicographic optimization has been the subject of recent work (for example, [16]), but the focus has been on the use of standard CSP algorithms. 6 Conclusions and Future Work This paper formalizes the problem of Boolean lexicographic optimization (BLO), and develops algorithms for this problem. General lexicographic optimization is a well-known variant of multi-objective combinatorial optimization [14], with a large number of practical applications. The restriction considered in this paper assumes Boolean variables, linear constraints and linear cost functions. The paper outlines four different algorithmic solutions for BLO, either based on aggregating cost functions in a single cost function, iterative pseudo-Boolean solving, iterative MaxSAT with weight rescaling and iterative unsatisfiability-based MaxSAT. The four algorithmic solutions were evaluated on complex lexicographic optimization problem instances from haplotyping with pedigree information [18]. The experimental evaluation allows drawing several conclusions. First, the use of a single aggregated cost function can impact performance negatively. Second, the use of iterative solutions (either based on PBO solvers or on unsatisfiability-based MaxSAT solvers) can yield significant performance gains when compared with the original solvers, resulting in remarkable reductions in the number of problem 12 103 103 Minisat+-BLO 102 102 Minisat+ 101 101 100 100 100 101 102 103 100 101 102 103 WPM1 WPM1 Figure 5: BLO improvements on Minisat+ vs. WPM1 instances unsolved. Despite the experimental evaluation focusing on the concrete case of haplotyping with pedigree information, recent experimental evaluations in the area of software upgradeability [3] yielded similar conclusions. Future work will address tighter integration between default solvers and the algorithms for lexicographic optimization. Concrete examples include clause reuse and incremental interface with the default solvers. Acknowledgments Claude Michel provided insights on Lexicographic Opti- mization. This work was partially funded by the SFI PI Grant 09/IN.1/I2618, FP7 EU grants ICT/217069 and ICT/214898, FCT Project PTDC/EIA/64164/2006 and PhD Grant SFRH/BD/28599/2006, and Spanish CICYT Projects TIN2007-68005- C04-01/02 and TIN2009-14704-C03-01/02. References [1] F. A. Aloul, A. Ramani, I. L. Markov, and K. A. Sakallah. Generic ILP versus specialized 0-1 ILP: an update. In International Conference on Computer- Aided Design, pages 450–457, November 2002. [2] C. Ansótegui, M. L. Bonet, and J. Levy. Solving (weighted) partial MaxSAT through satisfiability testing. In International Conference on Theory and Ap- plications of Satisfiability Testing, pages 427–440, July 2009. [3] J. Argelich, D. L. Berre, I. Lynce, J. Marques-Silva, and P. Rapicault. Solving linux upgradeability problems using Boolean optimization. In FLoC Work- shop on Logics for Component Configuration, July 2010. [4] J. Argelich, C. M. Li, and F. Manyà. An improved exact solver for partial Max-SAT. In International Conference on Nonconvex Programming: Local and Global Approaches, pages 230–231, December 2007. [5] J. Argelich, I. Lynce, and J. Marques-Silva. On solving Boolean multilevel optimization problems. In International Joint Conference on Artificial Intel- ligence, pages 393–398, July 2009. [6] O. Bailleux, Y. Boufkhad, and O. Roussel. A translation of pseudo Boolean constraints to SAT. Journal on Satisfiability, Boolean Modeling and Compu- tation, 2:191–200, March 2006. 13 [7] P. Barth. A Davis-Putnam enumeration algorithm for linear pseudo-Boolean optimization. Technical Report MPI-I-95-2-003, Max Plank Institute for Computer Science, 1995. [8] D. L. Berre. SAT4J library. www.sat4j.org. [9] D. Chai and A. Kuehlmann. A fast pseudo-Boolean constraint solver. In Design Automation Conference, pages 830–835, June 2003. [10] A. Cimatti, A. Franzén, A. Griggio, R. Sebastiani, and C. Stenico. Satisfi- ability modulo the theory of costs: Foundations and applications. In Tools and Algorithms for the Construction and Analysis of Systems, pages 99–113, March 2010. [11] O. Coudert. On solving covering problems. In Design Automation Confer- ence, pages 197–202, June 1996. [12] N. Eén and N. Sörensson. Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2(3-4):1–25, 2006. [13] N. Een and N. Sörensson. Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2:1–26, March 2006. [14] M. Ehrgott. Multicriteria Optimization. Springer, 2005. [15] M. Ehrgott and X. Gandibleux. A survey and annotated bibliography of multi- objective combinatorial optimization. OR Spektrum, 22(4):425–460, Novem- ber 2000. [16] E. Freuder, R. Heffernan, R. Wallace, and N. Wilson. Lexicographically- ordered constraint satisfaction problems. Constraints, 15(1):1–28, 2010. [17] Z. Fu and S. Malik. On solving the partial MAX-SAT problem. In Interna- tional Conference on Theory and Applications of Satisfiability Testing, pages 252–265, August 2006. [18] A. Graça, I. Lynce, J. Marques-Silva, and A. L. Oliveira. Haplotype inference combining pedigrees and unrelated individuals. In Workshop on Constraint Based Methods for Bioinformatics, September 2009. [19] P. Hansen and B. Jaumard. Algorithms for the maximum satisfiability prob- lem. Computing, 44(4):279–303, December 1990. [20] F. Heras, J. Larrosa, and A. Oliveras. MiniMaxSat: An efficient weighted Max-SAT solver. Journal of Artificial Intelligence Research, 31:1–32, Jan- uary 2008. [21] C. M. Li and F. Manyà. MaxSAT, hard and soft constraints. In SAT Hand- book, pages 613–632. IOS Press, 2009. 14 [22] C. M. Li, F. Manyà, and J. Planes. New inference rules for Max-SAT. Journal of Artificial Intelligence Research, 30:321–359, October 2007. [23] H. Lin and K. Su. Exploiting inference rules to compute lower bounds for MAX-SAT solving. In International Joint Conference on Artificial Intelli- gence, pages 2334–2339, January 2007. [24] M. Lukasiewycz, M. Glaß, C. Haubelt, and J. Teich. Solving multi-objective pseudo-Boolean problems. In International Conference on Theory and Ap- plications of Satisfiability Testing, pages 56–69, May 2007. [25] V. Manquinho and J. Marques-Silva. Satisfiability-based algorithms for Boolean optimization. Annals of Mathematics and Artificial Intelligence, 40(3-4):353–372, 2004. [26] V. Manquinho, J. Marques-Silva, and J. Planes. Algorithms for weighted Boolean optimization. In International Conference on Theory and Applica- tions of Satisfiability Testing, pages 495–508, July 2009. [27] J. Marques-Silva and V. Manquinho. Towards more effective unsatisfiability- based maximum satisfiability algorithms. In International Conference on Theory and Applications of Satisfiability Testing, pages 225–230, March 2008. [28] J. Marques-Silva and J. Planes. Algorithms for maximum satisfiability using unsatisfiable cores. In Design, Automation and Testing in Europe Conference, pages 408–413, March 2008. [29] N. V. Phillips. A weighting function for pre-emptive multicriteria assignment problems. The Journal of the Operational Research Society, 38(9):797–802, September 1987. [30] K. Pipatsrisawat, A. Palyan, M. Chavira, A. Choi, and A. Darwiche. Solving weighted Max-SAT problems in a reduced search space: A performance anal- ysis. Journal on Satisfiability Boolean Modeling and Computation, 4:191– 217, 2008. [31] M. Ramı́rez and H. Geffner. Structural relaxations by variable renaming and their compilation for solving MinCostSAT. In International Confer- ence on Principles and Practice of Constraint Programming, pages 605–619, September 2007. [32] C. Romero. Extended lexicographic goal programming: a unifying approach. Omega, 29(1):63–71, February 2001. [33] O. Roussel and V. Manquinho. Pseudo-Boolean and cardinality constraints. In SAT Handbook, pages 695–734. IOS Press, 2009. [34] J. P. Warners. A linear-time transformation of linear inequalities into con- junctive normal form. Information Processing Letters, 68(2):63–69, 1998. 15