=Paper= {{Paper |id=Vol-1128/intro3 |storemode=property |title=Applications of MaxSAT in Automotive Configuration |pdfUrl=https://ceur-ws.org/Vol-1128/paper3.pdf |volume=Vol-1128 |dblpUrl=https://dblp.org/rec/conf/confws/WalterZK13 }} ==Applications of MaxSAT in Automotive Configuration== https://ceur-ws.org/Vol-1128/paper3.pdf

Rouven Walter, Christoph Zengler, Wolfgang Küchlin 21

Applications of MaxSAT in Automotive Configuration

Rouven Walter and Christoph Zengler and Wolfgang Küchlin∗

Abstract The first question can be answered with proof tracing tech-
niques [Zhang and Malik, 2003; Ası́n et al., 2010]. Here a
We give an introduction to possible applications
CDCL SAT solver records a trace while solving the formula.
of MaxSAT solvers in the area of automotive
From this trace, a resolution based proof can be deduced,
(re-)configuration. Where a SAT solver merely
which shows the clauses involved in the unsatisfiable core.
produces the answer “unsatisfiable” when given an
An unsatisfiable core is also called conflict.
inconsistent set of constraints, a MaxSAT solver
computes the maximum subset which can be sat- The answer to the second question can be of important
isfied. Hence, a MaxSAT solver can compute re- practical use, too. For example, a customer may want to know
pair suggestions, e.g. for non-constructible vehi- a maximal valid subset of an invalid O. Similarly, the car
cle orders or for inconsistent configuration con- manufacturer may want to know which maximal subset of C
straints. We implemented different state-of-the-art is still satisfied by a currently invalid, but frequently desired
MaxSAT algorithms in a uniform setting within a option set. This optimization problem can be answered with
logic framework. We evaluate the different algo- MaxSAT, a generalization of the SAT problem (see Chapter
rithms on (re-)configuration benchmarks generated 19 in [Biere et al., 2009]). Instead of deciding the satisfiabil-
from problem instances of the automotive industry ity of a propositional formula, MaxSAT computes the maxi-
from our collaboration with German car manufac- mum number of satisfiable clauses in an unsatisfiable formula
turer BMW. in CNF. The Partial MaxSAT variant splits the clause set into
hard and soft clauses in a way that the number of satisfied
soft clauses is maximized while all the hard clauses have to
1 Introduction be satisfied. In the weighted variant of MaxSAT, clauses may
The well-known NP-complete SAT problem of proposi- carry an additional weight, such as the price of an option o.
tional logic—is a given propositional formula satisfiable— Some modern MaxSAT algorithms use SAT solvers as
has many practical applications; see [Marques-Silva, 2008] sub-routines by reducing the problem to several SAT solver
for an overview. Küchlin and Sinz [Küchlin and Sinz, 2000] calls [Fu and Malik, 2006; Marques-Silva and Planes, 2008;
pioneered the application of SAT solving for the verification Ansótegui et al., 2009]. With this approach, we can make
of the configuration constraints and the bill-of-materials in use of all modern techniques (such as clause learning, non-
the product documentation of the automotive industry on the chronological backtracking, or watched literals) of state-of-
example of Mercedes-Benz. A standard problem to be solved the-art SAT solvers, which are not generally applicable to
there is the following: Given a (sub-)set O = {o1 , . . . , on } of MaxSAT solvers.
equipment options and a set C = {c1 , . . . , cm } of configura- MaxSAT can be used to answer further questions of prac-
tion constraints whose variables are all options, is it possible tical use. For example: (1) After choosing components with
to configure a car with the options in O such that C is sat- priorities, what is the maximum sum of priorities that can be
isfied? This gives us the SAT problem SAT(C ∪ O), where achieved for a valid configuration? (2) When considering the
the options form unit clauses. If the answer is true, then the price of each component, how much is the minimal cost of a
partial configuration O is valid and can be extended to a full valid configuration?
valid configuration F which satisfies C, and F can be readily Reconfiguration is of high practical relevance in the au-
obtained from the SAT solver. tomotive industry [Manhart, 2005]. The after-sales business
For the unsatisfiable case, two main questions arise: (1) asks for extensions, replacements, or removal of components
Which constraints (or clauses for a CNF formula C) of the of a valid configuration with minimal effort. For example,
input formula caused the unsatisfiability? (2) How many (and when replacing the alarm system with a newer one, or when
which) clauses can be maximally satisfied? moving a vehicle from the U.S. to Europe, we would like to
∗
Symbolic Computation Group, WSI Informatics, Uni- keep the maximal number of already installed components.
versität Tübingen, Germany, www-sr.informatik. One approach for reconfiguration uses answer set program-
uni-tuebingen.de ming (ASP), which is a decidable fragment of first-order logic

Michel Aldanondo and Andreas Falkner, Editors
Proceedings of the 15th International Configuration Workshop
August 29-30, 2013, Vienna, Austria
22 Rouven Walter, Christoph Zengler, Wolfgang Küchlin

[Friedrich et al., 2011]. In this paper, we will describe a a CNF formula in propositional logic, where each satisfying
MaxSAT based approach for reconfiguration. assignment is called a valid configuration of a car. The latter
This paper is organized as follows. Section 2 defines the approach was investigated in [Küchlin and Sinz, 2000].
MaxSAT variants and notations. In Section 3 we give a short We will give a simplified and short introduction into this
introduction to automotive configuration based on SAT, fol- representation: (1) Each component (option) c is represented
lowed by a complete example. In Section 4 we describe by a separate variable xc ; the component will be used in the
our approach to use MaxSAT for automotive configuration final configuration assignment v if and only if v(xc ) = 1; (2)
to solve the above questions followed by detailed complete components of a family (e.g. different steering wheels) will
examples. Section 6 shows experimental proof-of-concept re- be restricted by cardinality constraints [Sinz, 2005; Bailleux
sults based on different modern MaxSAT solvers. Section 8 et al., 2009] to choose exactly one (or at most one, if the
concludes the paper. component is an optional feature); (3) dependencies between
components are expressed as clauses (e.g. the implication
2 Preliminaries: SAT and MaxSAT variants (xa ∧ xb ) → (xc ∨ xd ) means “If components a and b are
A Boolean assignment v is a mapping from a set of Boolean chosen, then component c or d has to be chosen (or both)”; in
variables X to {0, 1}. If a propositional formula ϕ evaluates clause form (¬xa ∨ ¬xb ∨ xc ∨ xd )).
to true under an assignment v (denoted as v |= ϕ), we call v The resulting formula in CNF is:
a satisfying assignment or model for ϕ, otherwise an unsat- ϕcar := ϕcc ∧ ϕdep (3)
isfying assignment. The SAT problem of propositional logic
is the question whether such a satisfying assignment v exists Where ϕcc are the clauses of the families’ cardinality con-
for a given formula ϕ or not. straints and ϕdep are the clauses of the dependencies between
A literal is a variable or its negation. A clause isVa disjunc- the components. With this representation, we can answer the
m
tion of literals. Given a propositional formula ϕ = i=1 ψi in following questions using a SAT solver:
conjunctive normal form (CNF) over n variables, where ψi is 1. Validation of a partial configuration.
a clause for all 1 ≤ i ≤ m and m ∈ N≥0 , the solution to the
Maximum Satisfiability problem (MaxSAT) is the maximal 2. Forced component: A component, which is used in ev-
number of clauses which can be satisfied by an assignment v. ery valid configuration.
Equation (1) shows a formal definition. 3. Redundant component: A component, which can
  never be used in any valid configuration.
X m 
MaxSAT(ϕ) := max kψi kv v ∈ {0, 1}n (1) 3.1 Example: SAT based Configuration
 
j=1
We consider the families of components with their limitations
Where kψi kv = 1, if v |= ψi , otherwise kψi k = 0. listed in Table 1.
We notice that for the corresponding MinUNSAT problem
whose solution is the minimum number of unsatisfied clauses,
Table 1: Component families with limitations
equation (2) holds.
family alternatives limit
MaxSAT(ϕ) + MinUNSAT(ϕ) = m (2)
engine E1 , E2 , E3 =1
Equation (2) also holds for the same resulting model. As a gearbox G1 , G2 , G3 =1
consequence, we only have to compute one problem to di- control unit C1 , C2 , C3 , C4 , C5 =1
rectly get the optimum and the corresponding model for both dashboard D1 , D2 , D3 , D4 =1
problems. navigation system N1 , N2 , N3 ≤1
There are two extensions of the MaxSAT problem, air conditioner AC1 , AC2 , AC3 ≤1
called Weighted MaxSAT (WMaxSAT) and Partial MaxSAT alarm system AS1 , AS2 ≤1
(PMaxSAT). As the name suggests, in a weighted MaxSAT radio R1 , R2 , R3 , R4 , R5 ≤1
instance each clause ψi has a weight wi ∈ N≥0 (denoted
by the tuple (ψi , wi )). The Weighted MaxSAT problem then
asks for the maximal sum of weights of satisfied clauses. Fur- Furthermore, we consider the dependencies between the
thermore, in a partial MaxSAT instance, the clauses are di- components listed in Table 2.
vided into disjoint hard and soft clauses sets: Hard ∪˙ Soft.
An optimal solution satisfies all hard clauses and a maximal
Table 2: Component dependencies
number of soft clauses. Both extensions can be combined to
Partial Weighted MaxSAT (PWMaxSAT). premise conclusion
The relationship of equation (2) also holds for each G1 E1 ∨ E2
MaxSAT variant. N1 ∨ N2 D1
N3 D2 ∨ D3
3 Automotive Configuration with SAT AC1 ∨ AC3 D1 ∨ D2
Automotive configuration can be represented as a constraint AS1 D2 ∨ D3
satisfaction problem (c. f. [Astesana et al., 2010]) and also as R1 ∨ R2 ∨ R5 D1 ∨ D4

Michel Aldanondo and Andreas Falkner, Editors
Proceedings of the 15th International Configuration Workshop
August 29-30, 2013, Vienna, Austria
Rouven Walter, Christoph Zengler, Wolfgang Küchlin 23

For example, the implication “G1 → E1 ∨ E2 ” means “If 2. (Maximization of priorities) We can generalize the use
gearbox G1 is chosen, then engine E1 or E2 has to be cho- case 1 by attaching priorities to the components: A cus-
sen”. tomer chooses components c1 , . . . , cn which lead to an
With the resulting formula ϕcar from the above specifica- invalid configuration. Additionally, the customer has
tions, we consider two customer cases: priorities p1 , . . . , pn , pi ∈ N>0 , for each component.
1. A customer chooses engine E1 and control unit C1 for We can answer the question, which sum of priorities can
the car. But she does not want the air conditioner AC2 . be maximally reached for a valid configuration by solv-
We test Formula (4) for satisfiability. ing Formula (6) with a Partial Weighted MaxSAT solver.
ϕcar ∧ xG1 ∧ xC1 ∧ ¬xAC2 (4) ϕcar ∧ (xc1 , p1 ) ∧ . . . ∧ (xcn , pn ) (6)
|{z} | {z }
The result is true. Derived from the resulting model, hard clauses soft clauses
we can choose the components D1 , C1 , G1 , E1 to get a
complete valid configuration assignment. 3. (Reconfiguration) We can use the introduced tech-
niques in the use cases 1 and 2 for reconfiguration. Let
2. A customer chooses the components E1 , G2 , C2 , D3 and us assume a customer wants to add, replace, or remove
N2 , AC1 , AS1 , R2 . The result is false. components of her existing car. She chooses the com-
The question now is, which maximal subset of the orig- ponents c1 , . . . , ck with priorities p1 , . . . , pk ∈ N>0 . If
inal choice will lead to a valid configuration? the priority or partial state (hard or soft) of a clause of
3.2 Advantage of the MaxSAT based approach an originally chosen component has changed, the origi-
nal clause will be replaced by the new partial weighted
With the SAT based configuration, two main problems arise. clause. Otherwise, the clause will be kept. We solve
First, if the configuration is not valid, it is not possible to Formula (7) with a Partial Weighted MaxSAT solver to
know which components cause the conflict. Second, even reach the maximal sum of priorities.
if we know the components causing the conflict, we do not
know, which components to omit to get a valid configuration ϕcar ∧ (xc1 , p1 ) ∧ . . . ∧ (xcn , pn ) (7)
|{z} | {z }
with a maximal number of components we wanted originally. hard clauses soft clauses
The example 2 of Subsection 3.1 shows such a case.
As mentioned in the introduction, the first problem can be To force certain new components to be installed or old
handled with proof tracing to explain a conflict for an in- components to be kept, we can designate the correspond-
valid configuration. The second problem can be handled with ing clauses as hard clauses.
MaxSAT and its extensions. We explain this approach in the To reach a valid reconfiguration for the customer, a re-
next section in detail. configuration scenario can be considered as a process in
different steps:
4 Automotive Configuration with MaxSAT • Check for validation after the customer chooses
For the representation of automotive configuration as a new components with priorities as previously de-
MaxSAT instance we consider the Partial MaxSAT problem. scribed.
We use the SAT based specification ϕcar of Section 3 and • If the hard clauses are unsatisfiable, check for vali-
divide the clauses into hard and soft ones. First, all cardinal- dation after the sales division sets additional depen-
ity constraints are marked as hard clauses, because they have dencies as soft clauses (with priorities).
to be satisfied (e.g. it is not possible to configure a car with • If the hard clauses are unsatisfiable, check for vali-
more than one steering wheel). Second, it is possible that the dation after the engineering divison sets additional
dependencies between components do not necessarily have dependencies as soft clauses (with priorites).
to be satisfied (e.g. a dependency could have been created
If the hard clauses are unsatisfiable after all steps, there
due to marketing reasons; “No black seats for all Japanese
is no valid configuration, because technical limitations
cars”). On the other hand, technical dependencies have to
are reached which can not be set as soft clauses. Other-
be satisfied (e.g. a conflict between an engine and a gearbox).
wise, if the hard clauses are satisfiable in one step, we
For simplicity reasons, we also mark all dependencies as hard
can compute the maximal sum of priorities of the soft
clauses.
clauses while satisfying the hard clauses.
With the representation above, we can consider the follow-
ing advanced use cases and answer the new arising questions 4. (Minimization of costs) The components c1 , . . . , cn
with the help of a Partial (Weighted) MaxSAT solver: have prices p1 , . . . , pn , pi ∈ N>0 . We want to know
1. (Maximization of chosen components) A customer which components have to be chosen, to get a valid con-
chooses components c1 , . . . , cn which lead to an invalid figuration with minimal cost. We can answer the ques-
configuration. We can answer the question, what the tion by solving Formula (8) with a Partial Weighted Min-
maximal number of the chosen components for a valid UNSAT solver.
configuration is, by solving Formula (5) with a Partial ϕcar ∧ (¬xc1 , p1 ) ∧ . . . ∧ (¬xcn , pn ) (8)
MaxSAT solver. |{z} | {z }
hard clauses soft clauses
ϕcar ∧ xc1 ∧ . . . ∧ xcn (5)
|{z} | {z } Instead of finding the minimal costs of a valid configu-
hard clauses soft clauses ration, we could also compute a valid configuration of

Michel Aldanondo and Andreas Falkner, Editors
Proceedings of the 15th International Configuration Workshop
August 29-30, 2013, Vienna, Austria
24 Rouven Walter, Christoph Zengler, Wolfgang Küchlin

minimal weights, CO2 emissions, or other interesting
targets. Table 4: Customer prioritized choices and PWMaxSAT re-
sults
In all situations above, the resulting model of the solver tells family choice priority result
us which components to choose to get the optimum. engine E1 8 E1
Additionally, we can add arbitrary hard clauses to enforce gearbox G2 5 G2
certain constraints: (1) Unit clauses to enforce the in- or control unit C2 7 C2
exclusion of a component; (2) Additional dependencies be- D2 8
tween components (e.g. “When engine E1 is chosen, then dashboard D3 15 D4
choose gearbox G2 ”; (xE1 → xG2 )); (3) Additional cardi- D4 15
nality constraints (e.g. xD1 ∨ xD2 to ensure that one of the navigation system N2 20 –
dashboards D1 or D2 will be chosen). air conditioner AC1 7 –
For example, in Situation 4 (minimization of costs), we alarm system AS1 2 –
could add unit clauses to enforce the inclusion of certain com- radio R2 15 R2
ponents and then compute the minimal costs of the configu-
ration. The result is a valid configuration with minimal costs
which includes our chosen components.

4.1 Example: MaxSAT based Configuration Table 4 shows the result, scoring 50 priority points, after
solving Formula (6).
We reconsider the example in Subsection 3.1.

1. In the second case, the choice of the customer was unsat-
isfiable. With the MaxSAT based approach of configura- 3. After the previous configuration, the customer wants to
tion we can find an assignment of a valid configuration reconfigure her existing car. Table 5 shows her choice.
where a maximum number of components is included. We can imagine that for technical or financial reasons,
After solving Formula (5) with a Partial MaxSAT solver, the engine E1 and gearbox G2 can not be replaced. We
we obtain the results shown in Table 3. set them as hard clauses. However, control unit C2 and
dashboard D4 can possibly be replaced and therefore are
set as soft clauses.
Table 3: Customer choices and Partial MaxSAT results
family choice result
engine E1 E1
gearbox G2 G2
control unit C2 C2 Table 5: Reconfiguration choice and PWMaxSAT results
dashboard D3 D1 family state new priorities choice results
navigation system N2 N2 engine E1 hard E1 E1
air conditioner AC1 AC1 gearbox G2 hard G2 G2
alarm system AS1 – control unit C2 (5, soft) C2 C2
radio R2 R2 dashboard D4 (2, soft) D4 D2
navigation system – (10, soft) N3 N3
air conditioner – hard AC1 ∨ AC2 AC2
alarm system – (5, soft) AS1 AS1
We can reach a valid configuration by changing two of radio R2 (13, soft) R2 –
the choices (bold rows in the table) and therefore, we
can keep 6 of our 8 original components at most. For the
alarm system, the resulting model did not set another
alarm system variable to true, because this is an optional
feature.
In general, the result obtained from the solver may not The results show that dashboard D4 was replaced by
be the only optimum. There can be other different as- dashboard D2 and radio R2 has to be removed in favor
signments with the same number of satisfied clauses. of other components.
2. We consider another case, where the customer chooses
the components with priorities as shown in Table 4. Ad-
ditionally, she wants dashboard D2 , D3 , or D4 . To en- 4. Now we associate the components with prices (as shown
force this constraint, we add the hard clause (xD2 ∨xD3 ∨ in Table 6) and we want to know a valid configuration
xD4 ). with a minimal total price.

Michel Aldanondo and Andreas Falkner, Editors
Proceedings of the 15th International Configuration Workshop
August 29-30, 2013, Vienna, Austria
Rouven Walter, Christoph Zengler, Wolfgang Küchlin 25

Basic SAT-based Given an unsatisfiable SAT problem ϕ =
Table 6: Components with prices {C1 , . . . , Cm }, we may iteratively try to remove individual
family alternatives clauses Ci until the subproblem ϕ0 becomes satisfiable. ϕ0
engine E1 E2 E3 will then be maximal in the sense that adding another clause
price (e) 4,000 2,500 4,500 will make it unsatisfiable, but another, larger, subproblem
gearbox G1 G2 G3 may exist which could be found by removing clauses from
price (e) 500 800 300 ϕ in a different order.
control unit C1 C2 C3 C4 C5 In SAT solving, clause removal can be simulated by aug-
price (e) 800 2,000 1,500 1,600 1,200 menting each clause Ci with a fresh blocking variable bi . As
dashboard D1 D2 D3 D4 long as bi is set to false, the solver needs to satisfy Ci , but the
price (e) 300 500 600 450
constraint Ci can effectively be blocked by setting bi to true
navigation system N1 N2 N3
price (e) 100 150 130 instead. Now, in order to remove as few clauses as possible,
air conditioner AC1 AC2 AC3 we add m blocking variables to ϕ as above and restrict the
price (e) 180 100 90 use of the bi by an additional cardinality constraint CC(k),
alarm system AS1 AS2 which is a formula that prevents more than k of the bi to be set
price (e) 300 250 to true. Iterating over k from below until ϕ(k) becomes satis-
radio R1 R2 R3 R4 R5 fiable, or from above until ϕ(k) becomes unsatisfiable, gives
price (e) 100 80 200 180 150 us the MaxSAT result m − k, and the subset of clauses whose
bi are set to false forms one satisfiable subset of maximum
For the minimal costs we solve Formula (8) with a Par- cardinality.
tial Weighted MinUNSAT solver. For the maximal costs Algorithm 1 reflects basic approach. One improvement of
we solve Formula (6) with a Partial Weighted MaxSAT this approach is the use of binary search.
solver by considering the prices as priorities. The results
are: Algorithm 1: Basic SAT-based approach
• Minimal cost: e 3,900 Input: ϕ = {C1 , . . . , Cm }
• Maximal cost: e 8,625 Output: Minimal number of unsatisfied clauses
Table 7 lists the components to choose to reach the min- ϕ ← {C1 ∨ b1 , . . . , Cm ∨ bm }
imal and maximal costs. cost ← m Pm
while SAT(ϕ ∪ CNF( i=1 bi < cost)) do
cost ← cost − 1
Table 7: Choices for minimal and maximal costs return cost
choice
family minimal cost maximal cost
engine E2 E3 Core-guided SAT-based Modern proof-tracing SAT
gearbox G3 G2 solvers return an unsatisfiable subset (unsat core) µ ⊆ ϕ
control unit C1 C2 when given an unsatisfiable ϕ. It is then clear that at least one
dashboard D1 D3 clause of µ has to be blocked before ϕ can become satisfiable,
navigation system – N3 and thus the search can be narrowed compared to the basic
air conditioner – AC2 approach. An algorithm based on this idea was proposed by
alarm system – AS1 Fu and Malik for partial MaxSAT [Fu and Malik, 2006]. In
radio – R3 every iteration where the instance is unsatisfiable, we add a
new blocking variable to all soft clauses of the unsatisfiable
5 Algorithmic techniques core and a new cardinality constraint to achieve that exactly
one of the currently added blocking variables has to be
In order to give the reader an impression of how MaxSAT satisfied. We can not just iterate over the unsat cores and
can be computed, we present a short incomplete overview of count them, because they may not be disjoint.
some algorithmic techniques. This idea can also be extended for partial weighted
MaxSAT [Ansótegui et al., 2009].
Branch-and-Bound The general branch and bound ap-
proach to explore the search tree of optimization problems 6 Experimental Results
can also be used for solving MaxSAT and its extensions.
Each node of the tree represents a variable of the instance For our benchmarks we used product configuration formulas
and has two children for the two values the variable can be of a current (2013) product line of the German car manufac-
assigned to. Tree pruning is used as soon as a partial solu- turer BMW. We added unit clauses to create unsatisfiable cus-
tion becomes worse than the best solution found elsewhere in tomer orders. We defined the following three categories for
the tree. Heuristics have been developed e.g. by Wallace and hard and soft clauses:
Freuder to narrow the search space predicting the final value • Order: Soft clauses are unit clauses of the customer’s
of partial solutions [Wallace and Freuder, 1993]. order. All other clauses are hard. This asks, wich of the

Michel Aldanondo and Andreas Falkner, Editors
Proceedings of the 15th International Configuration Workshop
August 29-30, 2013, Vienna, Austria
26 Rouven Walter, Christoph Zengler, Wolfgang Küchlin

customer’s wishes can be maximally satisfied. variables x1 , . . . , xn . We encode this constraint through the
Wn Vn Vn
• Packages: Soft clauses are clauses which represent constraints ( i=1 xi ) and i=1 j=i+1 (¬x i ∨ ¬x j ) . The
packages, e.g. a sports package, which triggers all rel- cardinality constraints in the PM2 approach uses general lim-
evant sports components. The unit clauses of the cus- itations, which we implemented with the encoding proposed
tomer’s order and all other clauses are hard. This asks, in [Bailleux et al., 2009].
which of the package restrictions can be maximally sat-
isfied w.r.t. the customer’s wishes. All our benchmarks were run on the same environment:
Operating System: Ubuntu 12.04 64 Bit; Processor: Intel
• Packages & more: Soft clauses are package clauses
Core i7-3520M, 2,90 GHz; Main memory: 8 GB; JVM 1.7.0
and additional other sales relevant conditions. The unit
(for Fu & Malik and PM2).
clauses of the customer’s order and all other clauses are
hard. This asks, which of the package restrictions and Table 9 shows the results of our time measurements of
additional restrictions can be maximally satisfied w.r.t. each solver in each category. The listed times are the aver-
the customer’s wishes. age times a solver needed to solve an instance of a category.
The upper half of Table 8 shows detailed statistics about each We listed the average time in each category Solver akmaxsat
category. The second half of the table shows how many in- has an average time of remarkable less than 0.6 seconds in
stances have an optimum. No optimum means that there is each category. Our implementation of Fu & Malik has a rea-
at least one conflict involving only hard clauses. The average sonable average time of less than 6 seconds in each category.
optimum is the average of the result of the minimal number Our implementation of PM2 has a reasonable average time
of unsatisfiable clauses. For example, the average optimum for the first category ‘Order’, but exceeded our time limit of
of 2.127 within the ‘Order’ category means that on average 3, 600 seconds per instance on too many instances of cate-
2.127 of the customer’s choices can not be satisfied. gories ‘Packages’ and ‘Packages & more’ to get a reasonable
average time.

Table 8: Benchmark details
Benchmark categories
Order Packages Packages & more Table 9: Benchmark results with a time limit of 3,600 sec.
#instances 777 777 777 per instance
Avg. #variables 896 896 896 Avg. time (sec) akmaxsat Fu & Malik PM2
Avg. #hard clauses 4474 3928 3592
Avg. #soft clauses 15 561 897 Order 0.165 4.367 4.180
Packages 0.025 1.664 exceeded limit
#no optimum 0 688 0
Packages & more 0.535 5.387 exceeded limit
#with optimum 777 89 777
Avg. optimum 2.127 1.348 4.067

We applied our benchmarks to three different state-of-the- Figures 1, 2 and 3 show the performance of each solver
art MaxSAT solvers, namely: in the first category ‘Order’. These figures show the relation
• akmaxsat [Kügel, 2012]: A partial weighted MaxSAT between the optimum and the response time of the instances.
solver based on a branch-and-bound approach. One of Especially for Fu & Malik and PM2 the response time seems
the best performing solvers in last year’s MaxSAT com- to grow linearly with increasing optimum.
petition1 .
• Fu & Malik [Fu and Malik, 2006]: A partial MaxSAT
solver based on exploiting unsatisfiable cores and adding 0.5
blocking variables to each soft clause of each found un- 0.45
satisfiable core. 0.4

• PM2 [Ansótegui et al., 2009]: A partial MaxSAT solver 0.35
based on exploiting unsatisfiable cores. But unlike the 0.3
Time (sec)

Fu & Malik solver this approach only uses exactly one 0.25
blocking variable to each clause.
0.2
For akmaxsat we used the implementation of Adrian Kügel2 . 0.15
We implemented the Fu & Malik and PM2 algorithms on top 0.1
of our own Java SAT solver, which is optimized for our in-
0.05
dustrial collaborations. The cardinalityPconstraints in the Fu
n 0
& Malik approach are only of the form i=1 xi = 1 for given 1 2 3 4 5 6 7
Optimum (quantity)
1
http://maxsat.ia.udl.cat:81/12
2
http://www.uni-ulm.de/in/theo/m/alumni/ Figure 1: Benchmark ‘Order’ with akmaxsat
kuegel.html

Michel Aldanondo and Andreas Falkner, Editors
Proceedings of the 15th International Configuration Workshop
August 29-30, 2013, Vienna, Austria
Rouven Walter, Christoph Zengler, Wolfgang Küchlin 27

9 7 Related Work
8 In [Junker, 2004] general satisfaction problems are consid-
7 ered, where we have a knowlegde base of constraints which
6 have to be satisfied and customer requirements, which we
would like to satisfy. In the context of MaxSAT, the knowl-
Time (sec)

5
edge base can be considered as hard clauses, whereas the cus-
4 tomer requirements can be considered as soft clauses. In the
3 case of inconsistency, the proposed algorithm QuickXplain
2 delivers preferred explanations, which are based on a given
total ordering of the constraints.
1
The work of [Reiter, 1987] proposes an algorithm for com-
0
1 2 3 4 5 6 7
puting minimal diagnoses using a conflict detection algo-
Optimum (quantity) rithm. A diagnosis is a minimal subset ∆ of the customer
requirements, such that the constraints without ∆ is consis-
Figure 2: Benchmark ‘Order’ with Fu & Malik tent. In [Felfernig et al., 2012] another algorithm is proposed,
called FastDiag, which computes a preferred minimal diagno-
sis without calculating the corresponding conflicts.

8 Conclusion
9
In this paper we showed detailed examples of how MaxSAT
8
and its extensions can be applied in automotive configuration.
7 With this approach we are able to repair an unsatisfiable cus-
6 tomer order by computing the optimal solution which satisfies
as many of the customer’s choices as possible. Furthermore,
Time (sec)

5
we showed how MaxSAT also can be used in reconfiguration
4
scenarios. From an already configured car we can compute
3 the minimal number of components to change when adding,
2 changing, or removing components.
1
We created realistic benchmarks for our MaxSAT applica-
tions out of the product formulas of our commercial collab-
0
1 2 3 4 5 6 7 oration with BMW. Our time measurements of these bench-
Optimum (quantity) marks against the state-of-the-art MaxSAT solvers akmaxsat,
Fu & Malik, and PM2, showed that we have a reasonable re-
Figure 3: Benchmark ‘Order’ with PM2 sponse time, except for PM2 in two categories. These results
suggest that MaxSAT can be applied for industrial automotive
(re-)configuration problems.
In Figure 4 we can also recognize the linear growing re-
sponse time with increasing optimum. Also note the lower
References
line of quickly solvable instances. [Ansótegui et al., 2009] Carlos Ansótegui, Maria Luisa
Bonet, and Jordi Levy. On solving MaxSAT through SAT.
In Proceedings of the 2009 conference on Artificial Intel-
18 ligence Research and Development, pages 284–292. IOS
16 Press Amsterdam, Amsterdam, Netherlands, 2009.
14 [Ası́n et al., 2010] Robert Ası́n, Robert Nieuwenhuis, Al-
12 bert Oliveras, and Enric Rodrı́guez-Carbonell. Practical
algorithms for unsatisfiability proof and core generation
Time (sec)

10
in SAT solvers. AI Communications, 23(2–3):145–157,
8
2010.
6
[Astesana et al., 2010] Jean Marc Astesana, Yves Bossu,
4 Laurent Cosserat, and Helene Fargier. Constraint-based
2 modeling and exploitation of a vehicle range at Renault’s:
0
Requirement analysis and complexity study. In Proceed-
0 2 4 6 8 10 12 14 16 18 20 ings of the 13th Workshop on Configuration, pages 33–39,
Optimum (quantity)
2010.
[Bailleux et al., 2009] Olivier Bailleux, Yacine Boufkhad,
Figure 4: Benchmark ‘Packages & more’ with Fu & Malik
and Olivier Roussel. New encodings of pseudo-boolean

Michel Aldanondo and Andreas Falkner, Editors
Proceedings of the 15th International Configuration Workshop
August 29-30, 2013, Vienna, Austria
28 Rouven Walter, Christoph Zengler, Wolfgang Küchlin

constraints into CNF. In Oliver Kullmann, editor, Theory [Reiter, 1987] Raymond Reiter. A theory of diagnosis from
and Applications of Satisfiability Testing—SAT 2009, vol- first principles. Artificial Intelligence, 32(1):57 – 95, April
ume 5584 of Lecture Notes in Computer Science, pages 1987.
181–194. Springer Berlin Heidelberg, 2009. [Sinz, 2005] Carsten Sinz. Towards an optimal CNF en-
[Biere et al., 2009] Armin Biere, Marijn Heule, Hans van coding of boolean cardinality constraints. In Peter
Maaren, and Toby Walsh, editors. Handbook of Satisfi- van Beek, editor, Principles and Practice of Constraint
ability: Volume 185 Frontiers in Artificial Intelligence and Programming—CP 2005, Lecture Notes in Computer Sci-
Applications, volume 185. IOS Press, Amsterdam, Nether- ence, pages 827–831. Springer Berlin Heidelberg, 2005.
lands, 2009. [Wallace and Freuder, 1993] Richard Wallace and Eugene C.
[Felfernig et al., 2012] A. Felfernig, M. Schubert, and C. Ze- Freuder. Comparative studies of constraint satisfaction and
hentner. An efficient diagnosis algorithm for inconsistent Davis-Putnam algorithms for maximum satisfiability prob-
constraint sets. Artificial Intelligence for Engineering De- lems. In David S. Johnson and Michael A. Trick, editors,
sign, Analysis and Manufacturing, 26(1):53 – 62, 2012. Cliques, Coloring, and Satisfiability: Second DIMACS Im-
plementation Challenge, volume 26 of Discrete Mathe-
[Friedrich et al., 2011] Gerhard Friedrich, Anna Ryabokon, matics and Theoretical Computer Science, pages 587–615.
Andreas A. Falkner, Alois Haselböck, Gottfried Schen- American Mathematical Society, USA, 1993.
ner, and Herwig Schreiner. (re)configuration using answer [Zhang and Malik, 2003] Lintao Zhang and Sharad Malik.
set programming. In Kostyantyn Shchekotykhin, Dietmar
Validating SAT solvers using an independent resolution-
Jannach, and Markus Zanker, editors, IJCAI-11 Config-
based checker: Practical implementations and other ap-
uration Workshop Proceedings, pages 17–24, Barcelona,
plications. In Proceedings of the conference on Design,
Spain, July 2011.
Automation and Test in Europe, volume 1, pages 10880–
[Fu and Malik, 2006] Zhaohui Fu and Sharad Malik. On 10885. IEEE Computer Society, 2003.
solving the partial MAX-SAT problem. In Armin Biere
and Carla P. Gomes, editors, Theory and Applications
of Satisfiability Testing—SAT 2006, volume 4121 of Lec-
ture Notes in Computer Science, pages 252–265. Springer
Berlin Heidelberg, 2006.
[Junker, 2004] Ulrich Junker. QUICKXPLAIN: Preferred
explanations and relaxations for over-constrained prob-
lems. In Deborah L. McGuinness and George Ferguson,
editors, Proceedings of the Nineteenth National Confer-
ence on Artificial Intelligence, Sixteenth Conference on In-
novative Applications of Artificial Intelligence, pages 167
– 172. AAAI Press / The MIT Press, 2004.
[Küchlin and Sinz, 2000] Wolfgang Küchlin and Carsten
Sinz. Proving consistency assertions for automotive prod-
uct data management. Journal of Automated Reasoning,
24(1–2):145–163, 2000.
[Kügel, 2012] Adrian Kügel. Improved exact solver for the
weighted max-sat problem. In Daniel Le Berre, editor,
POS-10. Pragmatics of SAT, volume 8 of EPiC Series,
pages 15–27. EasyChair, 2012.
[Manhart, 2005] Peter Manhart. Reconfiguration – a prob-
lem in search of solutions. In Dietmar Jannach and
Alexander Felfernig, editors, IJCAI-05 Configuration
Workshop Proceedings, pages 64–67, Edinburgh, Scot-
land, July 2005.
[Marques-Silva and Planes, 2008] João Marques-Silva and
Jordi Planes. Algorithms for maximum satisfiability us-
ing unsatisfiable cores. In Design, Automation and Test in
Europe, pages 408–413. IEEE, 2008.
[Marques-Silva, 2008] João Marques-Silva. Practical appli-
cations of boolean satisfiability. In Discrete Event Sys-
tems, 2008. WODES 2008. 9th International Workshop on,
pages 74–80. IEEE, 2008.

Michel Aldanondo and Andreas Falkner, Editors
Proceedings of the 15th International Configuration Workshop
August 29-30, 2013, Vienna, Austria