=Paper= {{Paper |id=None |storemode=property |title=Boolean Lexicographic Optimization |pdfUrl=https://ceur-ws.org/Vol-616/paper14.pdf |volume=Vol-616 |dblpUrl=https://dblp.org/rec/conf/cpaior/Marques-SilvaAG10 }} ==Boolean Lexicographic Optimization== https://ceur-ws.org/Vol-616/paper14.pdf

Boolean Lexicographic Optimization

Joao Marques-Silva1 , Josep Argelich2 , Ana Graça3 , and Inê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. Ansó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. Manyà. 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. Franzé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. Eén and N. Sö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. Sö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. Graç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. Manyà. MaxSAT, hard and soft constraints. In SAT Hand-
book, pages 613–632. IOS Press, 2009.

14
[22] C. M. Li, F. Manyà, 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.