=Paper=
{{Paper
|id=Vol-1453/11_KuebartWalterKuechlin_DifferentSolvingStrategiesOn_Confws-15_p67
|storemode=property
|title=Different solving strategies on PBO Problems from automotive industry
|pdfUrl=https://ceur-ws.org/Vol-1453/11_KuebartWalterKuechlin_DifferentSolvingStrategiesOn_Confws-15_p67.pdf
|volume=Vol-1453
|dblpUrl=https://dblp.org/rec/conf/confws/KubartWK15
}}
==Different solving strategies on PBO Problems from automotive industry==
https://ceur-ws.org/Vol-1453/11_KuebartWalterKuechlin_DifferentSolvingStrategiesOn_Confws-15_p67.pdf
Different Solving Strategies on PBO Problems from
Automotive Industry
Thore Kübart 1 and Rouven Walter 2 and Wolfgang Küchlin2
Abstract. SAT solvers have proved to be very efficient in verifying of Propositional Logic, Maximum Satisfiability (MaxSAT), Pseudo-
the correctness of automotive product documentations. However, in Boolean Optimization (PBO) and Integer Linear Programming (ILP)
many applications a car configuration has to be optimized with re- and their respective algorithmic solving techniques. Section 3 points
spect to a given objective function prioritizing the selectable product out related work. Section 4 describes different optimization problems
components. Typical applications include the generation of predic- in automotive configuration. Section 5 presents a detailed evaluation
tive configurations for production planning and the reconfiguration of of the different introduced optimization approaches for these prob-
non-constructible customer orders. So far, the successful application lems including a discussion of the results. Finally, Section 6 con-
of core guided MaxSAT solvers and ILP-based solvers like CPLEX cludes this work.
have been described in literature. In this paper, we consider the linear
search performed by DPLL-based PBO solvers as a third solution ap-
2 Preliminaries
proach. The aim is to understand the capabilities of each of the three
approaches and to identify the most suitable approach for different In this work, we focus on propositional logic with the standard logi-
application cases. Therefore we investigate real-world benchmarks cal operators ¬, ∧, ∨, →, ↔ over the set of Boolean variables X and
which we derived from the product description of a major German with the constants ⊥ and >, representing false and true, respectively.
premium car manufacturer. Results show that under certain circum- The set of variables of a formula ϕ is denoted by var(ϕ). A formula
stances DPLL-based PBO solvers are clearly the better alternative to ϕ is called satisfiable, if and only if there is an assignment τ , a map-
the two other approaches. ping from the set of Boolean variables var(ϕ) to {0, 1}, under which
the formula ϕ evaluates to 1. The evaluation of a formula under an
assignment τ is the standard evaluation procedure for propositional
1 Introduction logic, denoted by τ (ϕ). The values 0 and 1 are also referred to as
An already well-established approach in the automotive industry is false and true. The well-known NP-complete SAT problem asks the
to describe the set M of technically feasible vehicle configurations question whether a formula is satisfiable or not [6].
by a propositional formula ϕ such that M = {τ | τ (ϕ) = 1} holds, The established input format of a SAT solver nowadays is a con-
where τ is a satisfying assignment of formula ϕ [11, 19], i.e. every junctive normal form (CNF) of a formula ϕ, where ϕ is transformed
model of ϕ is a feasible configuration. SAT solvers are the method into a conjunction of clauses and each clause is a disjunction of lit-
of choice for calculating configurations that comprise certain options W i of a literal l is de-
erals (variables or negated variables).VThe variable
o1 , . V
. . , om : A model has to be determined that satisfies the formula noted by var(l). For a formula ϕ = ki=1 m j=1 li,j in CNF we also
ϕ∧ m make use of the notation of ϕ as a set of clauses where each clause
i=1 oi . If there is no such model of the desired configuration,
the user is often interested in an alternative model of optimal config- is a set of literals: ϕ = {{l1,1 , . . . , l1,m1 }, . . . , {lk,1 , . . . , lk,mk }}.
ured options oi with respect to given priorities wi . To reach a best The transformation of an arbitrary formula ϕ into a CNF is done by a
possible configuration, a model ofP the formula ϕ has to be calculated Tseitin- or Plaisted-Greenbaum-Transformation [16, 20] (denoted as
that optimizes the target function m Tseitin(ϕ)). The resulting formula is not semantically equivalent,
i=1 wi oi .
In the literature of the last few years different applications of this but equisatisfiable. Also, the models of ϕ and Tseitin(ϕ) are the
optimization problem are described as well as several approaches to same when restricted to the original variables var(ϕ).
solve it. Similar optimization problems arise for example from the
task to minimize or maximize product properties such as price or 2.1 MaxSAT
weight [21]. Another example is the task of optimal reconfiguration,
For a given clause set ϕ = {c1 , . . . , cm }, m ∈ N, the MaxSAT
e.g., the selected options for a car are not feasible with the constraint
problem [13] asks for the maximum number of clauses which can be
set [21]. Furthermore valid configurations that optimize linear objec-
simultaneously satisfied:
tive functions play an important role in demand forecasts [18]. We
compare the underlying solving approaches by analyzing real-world
instances of a major German premium car manufacturer.
(m )
X |var(ϕ)|
This work is organized as follows: Section 2 introduces the basics MaxSAT(ϕ) = max τ (ci ) τ ∈ {0, 1} (1)
i=1
1 Steinbeis-Transferzentrum Objekt- und Internet-Technologien, Sand 13,
72076 Tübingen, Germany The corresponding problem of finding the minimum num-
2 Symbolic Computation Group, WSI Informatics, Universität Tübingen, ber of clauses which can be simultaneously unsatisfied is called
Germany, www-sr.informatik.uni-tuebingen.de MinUNSAT.
67 Juha Tiihonen, Andreas Falkner, and Tomas Axling, Editors
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
The partial weighted MaxSAT problem is an extended version Pseudo-Boolean solving (PBS) is the decision problem whether a
where: (i) An additional clause set ϕhard of hard clauses is taken set of LPB constraints can be satisfied by an assignment τ . Hence,
into account, which has to be satisfied, and (ii) weights wi ∈ N are PBS is a generalization of SAT. Like SAT solvers, most PBS solvers
assigned to the soft clauses of ϕ = {c1 , . . . , cm }. The resulting prob- which prove satisfiability are able to provide a satisfying assignment
lem, PWMaxSAT(ϕhard , ϕ), consists of finding the maximal sum τ to the user.
of weights of satisfied clauses of ϕ while satisfying ϕhard . To sim- Given a satisfiable set of LPB constraints another problem is to
plify reading we refer to partial weighted MaxSAT just as MaxSAT identify a best possible assignment τ with respect to a linear objec-
in the rest of this work. tive function:
MaxSAT can be solved by using a SAT solver as a black box, P
e.g. by linear search or binary search. Firstly, a fresh variable bi , min i ci li
called blocking variable, is added to each soft clause, which serves s.t. V P (4)
to enable or disable the clause. Linear search iteratively checks the j i aj,i l j,i . b j
SAT instance ϕhard and ϕ with an additional constraint
This problem is called pseudo-Boolean optimization (PBO) [17].
m
!
X In order to solve the satisifiability problem PBS, DPLL-style al-
CNF wi · ¬bi > k , (2) gorithms can be used to benefit from recent progress of modern SAT
i=1 solvers. One approach is to transform the LPB-constraints into CNF
where initially k = 0. With this check we search and to apply SAT solvers to the resulting formula. Another approach
P for a model with a is based on generalized constraint propagation and conflict-based
sum of weights of at least 1. The constraint m i=1 wi · ¬bi > k is
a Pseudo-Boolean constraint (see Subsection 2.2 for details), which learning, i. e. DPLL-based SAT solvers are enabled to handle LPB
can be transformed to a CNF, see for example [4, 8]. The degree k is constraints directly. Generally learning methods analyze the conflict
increased to the sum of weights of the last model plus one in order and learn a new constraint which is falsified on the conflict level and
to check if we can find a better model. Binary search, in contrast, which propagates a new assignment on a higher decision level.
follows the same scheme but restricts the search space with a lower Given a PBS solver, the PBO problem of Formula (4) itself can be
and an upper bound simultaneously. Linear search requires m SAT solved by iteratively applying the solver to perform a linear search or
calls in the worst case, whereas binary search requires only log2 (m) a binary search. Both approaches proceed analogously to the linear
SAT calls in the worst case. and binary search approaches for MaxSAT using a SAT solver.
Another approach is the usage of unsatisfiable cores delivered by a In the linear search approach, models of the formula ϕ are cal-
SAT solver for the unsatisfiable case, which was introduced in [3, 9]. culated in order to gradually approach the optimal objective value.
The idea is to iteratively call the SAT solver and relax the soft clauses Through an extra LPB constraint, a model providing a better objec-
contained in the unsatisfiable core by introducing blocking variables tive value is enforced. If the extra LPB constraint leads to an unsat-
until the formula becomes satisfiable. Solvers using an unsatisfi- isfiable PBS instance, the model last calculated is the optimal one.
able core approach performed well on industrial instances in recent In the binary search approach the search space is bisected by every
MaxSAT competitions3 . single PBS-instance. If the optimal objective value lies inside the
The OPEN - WBO framework [15] is based on using MiniSat-like interval [L, U ], a model with the objective value ≤ M = (L + U )/2
solvers [7] and was one of the best performing MaxSAT algorithms is searched for. If such a model exists, the minimal objective value
on industrial instances in the recent MaxSAT competition. Both lies inside [L, M ]. If no such model exists, the minimal objective
linear search and unsatisfiable-core guided solvers are included in value lies inside [M, U ].
different variations within the OPEN - WBO framework. The default For the calculations in Section 5 we used the Sat4j library. The li-
solver, called WBO, is an unsatisfiable-core guided modification brary is based on a Java version of MiniSat, which was expanded by
of [3] which partitions the soft clauses [2, 14]. Therefore, only a sub- generalized constraint propagation and conflict-based learning. The
set of the soft clauses are given to the SAT solver to make the SAT PBO solver contained therein realizes a simple linear search. The
solver focus on relevant clauses. On the other hand, this can lead to PBS solver called for this linear search is able to perform the follow-
additional SAT calls in the case where a model is found but not all ing two learning methods.
soft clauses were considered. We used this solver for our evaluations, The clause-based learning method calculates so-called UIPs
see Section 5. (unique implications points) by means of propositional resolution
just like in modern SAT solvers. SAT solvers such as MiniSat de-
rive a UIP on the basis of the conflict clause and the reason clauses
2.2 DPLL-based PBO which were propagating the assignments of the conflict clause. If a
In addition to clauses we consider linear pseudo-Boolean (LPB) con- conflict constraint occurs in the form of a LPB constraint, Sat4j first
straints, which are linear inequalities of the form reduces this constraint to a conflict clause
_
k
X K= l, (5)
ai li . b, .∈ <, ≤, >, ≥, = , (3) l∈ωC , β(l)=0
i=1
where ai ∈ Z and li are literals of Boolean variables. Under some where β is the partial assignment, that leads to the conflict in the LPB
assignment τ , the left side is the sum over the coefficients of the constraint ωC . Analogously, reasons given by LPB constraints are
satisfied literals and the LPB constraintWis satisfied iff the respective reduced to reason clauses: If ω is a LPB constraint, that propagates ˜ l
For example, clauses m under the partial assignment β, the clause
inequality holds.P i=1 li can be generalized as
LPB constraints m i=1 li ≥ 1.
_
R(˜
l) = l∨˜
l, ω |= R(˜
l), (6)
3 http://www.maxsat.udl.cat/ l∈ω, β(l)=0
Juha Tiihonen, Andreas Falkner, and Tomas Axling, Editors 68
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
is an implication of ω and also propagates the literal ˜
l under β. Reconfiguration of invalid configurations, as described in [21], is
In a second learning method that is implemented in Sat4j more an important issue in automotive configuration. Several practical rel-
expressive LPB constraints instead of clauses are learned. For this evant use cases exist, such as the reconfiguration of customer orders,
purpose the principle of propositional resolutions in forms of Hook- the reconfiguration of constraints for a given fixed order or the com-
ers cutting planes [10] is directly applied to the LBP constraints [5]. putation of a maximal/minimal car w.r.t. to an assigned value of the
options like weights (kg).
Another major task is the prognosis of future part demands in pro-
2.3 Integer Linear Programming duction planning. However, historical demands cannot easily be ex-
trapolated because planning situations in the automotive industry are
Like linear programming, integer linear programming deals with the constantly changing. A typical planning state used for making a fore-
optimization of linear objective functions over a set which is limited cast comprises
by linear equations and inequations. The difference is that while in
linear optimizations any real values can be taken on, in integer opti- • the product documentation (option A is only available, if option B
mization some or all variables are restricted to whole-number values. is selected; part x is needed exactly iff the order satisfies the part
P rule ϕx ; etc.),
min i ci xi • estimated customer buying behavior (option C is selected by 30%
s.t. of the customers; etc.),
V P (7)
j i aj,i xj,i . bj • capacity restrictions (only 5000 units of part X are available; etc.),
xj,i ∈ Z • production plans that fix the total number of planned vehicles.
Pseudo-Boolean Optimization, see Formula (4), can be easily From a mathematical point of view a planning state consists of two
transformed into 0-1 integer linear programming (ILP): Negative lit- parts:
erals ¬x are replaced by (1 − x) and Boolean variables become de-
cision variables x ∈ {0, 1}. Consequently, commercially available 1. The Boolean formula POF, whose models describe the technically
state-of-the-art ILP solvers such as CPLEX [1] can be used to solve feasible configurations,
PBO. Usually, they are based on the branch and cut strategy. 2. the statistical frequency of certain atoms of the product formula.
A common approach to evaluate the planning state is to calculate
3 Related Work an amount of N technically feasible variations that approximates
the statistical guidelines as good as possible. Eventually, for indi-
Sinz et al. suggest a SAT-based procedure to check consistency of the cating the future unit demand, the calculated variations are analyzed
product documentation of a German car manufacturer [19]. There- by means of the BOM.
fore, they consider vehicle configurations as assignments to propo- Singh et al. [18] propose a linear optimization model for finding
sitional variables and define a propositional formula, called product such a set of N technically feasible variations. A solution of their
overview formula (POF), which evaluates to true iff the vehicle con- model is calculated by column generation: In every iteration a tech-
figuration is technically feasible. Their work also lays the foundation nically feasible variation is determined which further improves the
for formulating the restrictions of the product documentation as a solution set. For this, a PBO problem is solved. Its objective function
constraint in mathematical models. is given by the dual variables of the current approximation and its
Tilak Singh et al. make use of such a product overview formula constraints are given by the restrictions of the product overview.
in [18]. They describe a mathematical model to calculate car config- In column generation, calculated configurations of previous itera-
urations aimed at providing the production planning with test vari- tions are partially replaced by new configurations. Thus, solved PBO
ants before actual sales orders are received. Their configurations are instances do not necessarily result in a configuration also contained
calculated on the basis of PBO problems that are solved by CPLEX. in the final solution. Therefore, it is particularly important to ensure
This approach is described in greater detail in Section 4. an efficient calculation of the individual PBO instances.
Walter et al. [21] describe the possible usage of MaxSAT in au-
4
tomotive configuration by pointing out various use cases. Whenever 150
faced with an over-constrained configuration, MaxSAT can be used
#non-zero dual variables
distance to the optimum
3
to reconfigure the invalid configuration by providing an optimal solu- 100
2
tion, e.g. giving a repair suggestion of the (possibly prioritized) over-
constrained selections of a user by a minimal number of changes. 1
50
0 0
4 Optimization Problems from Automotive 0 100 200
#iterations
300 0 100 200
#iterations
300
Configuration
The product overview defines the set of valid product configurations Figure 1. Typical approximation to the optimum using column generation
and is usually describable as a set of propositional constraints. This
means a configuration is only valid if it satisfies the conjunction of all
constraints, which is also called the product overview formula (POF).
The physical demand of building components for a valid configura- The typical approximation to the planning state when using col-
tion is determined by the bill of materials (BOM). The combination umn generation is shown in Figure 1. As one can see on the left side,
of the product overview and the bill of material is referred to as the the majority of iterations is used to overcome the last small step to-
product documentation. wards the optimum. Yet, illustrated by the graph on the right side,
69 Juha Tiihonen, Andreas Falkner, and Tomas Axling, Editors
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
approximation is accompanied by increasingly complex target func-
tions of the PBO instances: the number of non-zero dual variables is Type A
increasing. It must be noted that the maximum number of non-zero
dual variables is usually proportional to the number of statistical re-
4,000
quirements of the planning state.
Concerning implementations of column generation described in
Cutting Planes
the literature, integer linear programming is the method of choice 3,000
Clauses
for producing columns. This approach is also taken in [18] us-
time in ms
ing CPLEX. An important objective of this paper is to investigate
2,000
whether DPLL-based methods are suitable alternatives to CPLEX
for calculating predictive configurations.
1,000
5 Experimental Evaluation
0
In this section we present our main contribution by evaluating the dif-
ferent previously described methods on optimization problems from 0 50 100 150 200
automotive configuration. #variables in the objective function
As test environment for the experimental evaluations we used
Windows 7 Professional 64 Bit on an Intel(R) Core(TM) i7-4800MQ
CPU with 2.70 GHz and 2 GB main memory. Figure 2. Learning Cutting Planes vs. Clauses in Sat4j
5.1 Benchmark Statistics
We evaluate several test series, each of which is composed of a
Type A
real-world product overview and of randomly generated linear ob-
jective functions. We looked at product overviews of two different
200
Type Fixed Attributes #Clauses
A market, model, body type, en- 1200-5900
gine, steering type 150
CPLEX
B market, model, body type 19100-137700
Sat4j
time in ms
O PEN WBO
100
Table 1. Characteristics of type A and B
50
types, see A and B in Table 1. Both types of product overviews dif- 0
fer in the extent to which attributes are fixed. Additionally, Table 1
0 50 100 150 200
shows the minimum and maximum number of clauses for the prod-
#variables in the objective function
uct overviews of one type. For generating objective functions, n vari-
ables were randomly selected (by using Java’s Random class with the Type B
default constructor) and each was assigned to a random integer coef-
ficient from a range between −10, 000, 000 and 10, 000, 000. That
way, 10 objective functions were generated for different numbers of
variables (n = 10, 20, . . . , 200) so that one test series contains a
1,000
total of 200 PBO instances. Corresponding test series were gener-
time in ms
ated for 13 different product overviews of type A and for 6 different CPLEX
product overviews of type B. Sat4j
O PEN WBO
500
5.2 Results
The test series from the previous section were solved by 3 solvers:
1. O PEN WBO as a core guided MaxSat solver [15]. 0
2. Sat4j as an implementation of the DPLL-based linear search [12]. 0 50 100 150 200
3. CPLEX as an ILP solver [1].
#variables in the objective function
For solving the PBO instances a timeout of 60 seconds was set. In or-
der to set up the linear search correctly, two different learning meth-
Figure 3. Running times for type A and B
ods of the underlying PBS solver of Sat4j were tested. Concerning
the test series of type A, Figure 2 shows the average running time for
learning of
Juha Tiihonen, Andreas Falkner, and Tomas Axling, Editors 70
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
1. clauses Type A
2. cutting planes
depending on the complexity of the objective function. Based on 15
these results, Sat4j was limited to learning clauses when comparing
the 3 solvers. Sat4j
average #iterations
O PEN WBO
10
product overview with 133700 clauses
3,000 5
time in ms
2,000
0
0 50 100 150 200
CPLEX #variables in the objective function
1,000 Sat4j
O PEN WBO
Figure 6. Average number of DPLL-calls for O PEN WBO and Sat4j
0
0 50 100 150 200
#variables in the objective function
The MaxSAT solver O PEN WBO, however, produces reliable run-
ning times for up to N = 70 variables.
In contrast to the DPLL-based solvers, there was only a slight in-
Figure 4. Running times for the largest product overview of type B crease in the running times for CPLEX with a growing number of
variables in the objective function. Hence, once a certain length of
the target function has been reached, CPLEX leads to better results.
Across all test series of type B, Sat4j performed on average better
than CPLEX (Figure 3, bottom graph). Compared to CPLEX how-
Type A ever, O PEN WBO leads to slower running times for objective func-
tions of only N = 30 variables. This observation is especially il-
lustrated by the most extensive product overview of type B (137700
8 Type A
Type B
clauses) as demonstrated in Figure 4, where the time-domain is re-
stricted to 3400 ms.
Timeouts were observed exclusively for the MaxSAT solver
average #timeouts
6
O PEN WBO. Complementary to the results of running times, Fig-
ure 5 shows the average number of timeouts when solving 10 in-
4
stances.
For a better understanding of the observed difference in running
2 times of both DPLL-based approaches, Figure 6 shows the average
number of DPLL-calls. The graphs refer exclusively to the test se-
ries of type A and represent the numbers of SAT/UNSAT-calls for
0
O PEN WBO or, in case of Sat4j, the numbers of PBS-calls.
0 50 100 150 200
#variables in the objective function 5.3 Discussion
The test instances described in Section 5.1 differ with respect to the
Figure 5. Average number of timeouts for O PEN WBO following aspects:
• the complexity of the objective function (number of variables
N = 10, 20, . . . , 200)
In Figure 3 the running times of O PEN WBO, Sat4j and CPLEX • the size of the product overview (number of models and number
are compared. The upper graph shows the average running times of of clauses; type A and B)
the test series of type A concerning objective functions of differ- The findings of the previous section lead us to the following conclu-
ent complexity. Accordingly the bottom graph displays the results sions:
of the test series of type B. Time was limited in both subfigures
(200ms, 1400ms). In average, for all test series of type A and B, • Using DPLL allows the quick calculation of a model of a formula
the DPLL-based solvers O PEN WBO and Sat4j perform significantly - in that way DPLL-based solvers are superior to ILP solvers.
better than CPLEX with regard to objective functions of low com- • Yet, when objective functions become more and more complex,
plexity. In test series of type A the solver Sat4j performs better than the particular suitability of CPLEX in solving 0-1-optimization
CPLEX concerning objective functions of up to N = 170 variables. problems dominates.
71 Juha Tiihonen, Andreas Falkner, and Tomas Axling, Editors
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria
The latter point is evident in the strong increase of running times for [3] Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy, ‘Solving
the DPLL-based methods once a certain length of objective functions (weighted) partial MaxSAT through satisfiability testing’, in Theory
and Applications of Satisfiability Testing - SAT 2009, ed., Oliver Kull-
has been reached. mann, volume 5584 of Lecture Notes in Computer Science, 427–440,
In comparison with O PEN WBO, Sat4j leads to significantly bet- Springer Berlin Heidelberg, (2009).
ter running times. This is also due to the special suitability of the [4] Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel, ‘A transla-
examined instances for a linear search (see Figure 6). The number tion of pseudo boolean constraints to SAT’, Journal on Satisfiability,
of iterations for a linear search increases only linearly with the num- Boolean Modeling and Computation, 2(1–4), 191–200, (2006).
[5] Donald Chai and Andreas Kuehlmann, ‘A fast pseudo-boolean con-
bers of variables in the objective function - this is a surprising result. straint solver’, IEEE Transactions on CAD of Integrated Circuits and
Hence, the nonlinear increase of running times can only be explained Systems, 24(3), 305–317, (2005).
by the growing complexity of PBS instances in linear search. [6] Stephen A. Cook, ‘The complexity of theorem-proving procedures’, in
Concerning product overviews of type A, the critical length of the Proceedings of the Third Annual ACM Symposium on Theory of Com-
puting, STOC ’71, pp. 151–158, New York, NY, USA, (1971). ACM.
objective function for Sat4j is between N = 160 and N = 200. With [7] Niklas Eén and Niklas Sörensson, ‘An extensible SAT-solver’, in The-
increasing scale of the product overview, this critical value shifts up- ory and Applications of Satisfiability Testing—SAT 2003, eds., Enrico
wards. In some cases of the product overviews of type B, the critical Giunchiglia and Armando Tacchella, volume 2919 of Lecture Notes in
value is greater than N = 200, such as seen in Figure 4. Computer Science, 502–518, Springer Berlin Heidelberg, (2004).
In order to optimally configure customer orders, an optimal subset [8] Niklas Eén and Niklas Sörensson, ‘Translating pseudo-boolean con-
straints into SAT’, Journal on Satisfiability, Boolean Modeling and
of about 20 options has to be determined. For this purpose the linear Computation, 2, 1–26, (2006).
search implemented in Sat4j and the core guided MaxSAT solver [9] Zhaohui Fu and Sharad Malik, ‘On solving the partial MAX-SAT prob-
O PEN WBO are more than sufficient. lem’, in Theory and Applications of Satisfiability Testing—SAT 2006,
For calculating predictive configurations for the product planning eds., Armin Biere and Carla P. Gomes, volume 4121 of Lecture Notes
in Computer Science, 252–265, Springer Berlin Heidelberg, (2006).
(see Figure 1) Sat4j can be far more effective than the other tested [10] John N. Hooker, ‘Generalized resolution and cutting planes’, Annals of
methods, at least for the first iterations of a column generation based Operations Research, 12(1), 217–239, (1988).
process. Yet it is possible that the critical area of linear search is [11] Wolfgang Küchlin and Carsten Sinz, ‘Proving consistency assertions
reached depending on the given number of statistical requirements in for automotive product data management’, Journal of Automated Rea-
the planning state. In such a case configurations should be calculated soning, 24(1–2), 145–163, (2000).
[12] Daniel Le Berre and Anne Parrain, ‘The Sat4j library, release 2.2’, Jour-
by CPLEX just like in [18]. nal on Satisfiability, Boolean Modeling and Computation, 7(2–3), 59–6,
(2010).
[13] Chu Min Li and Felip Manyà, ‘MaxSAT, hard and soft constraints’, in
6 Conclusion Handbook of Satisfiability, eds., Armin Biere, Marijn Heule, Hans van
Maaren, and Toby Walsh, volume 185 of Frontiers in Artificial Intelli-
We compared current state-of-the-art solvers to calculate optimal gence and Applications, chapter 19, 613–631, IOS Press, (2009).
product configurations of a major German car manufacturer. So far, [14] Ruben Martins, Vasco M. Manquinho, and Inês Lynce, ‘On partitioning
the use of core guided MaxSAT solvers and ILP solvers like CPLEX for maximum satisfiability’, in ECAI 2012 - 20th European Conference
on Artificial Intelligence, eds., Luc De Raedt, Christian Bessière, Di-
for PBO-instances of automotive industry was described in the litera- dier Dubois, Patrick Doherty, Paolo Frasconi, Fredrik Heintz, and Peter
ture. For the purpose of comparison we additionally applied a DPLL- J. F. Lucas, volume 242 of Frontiers in Artificial Intelligence and Ap-
based linear search. plications, pp. 913–914. IOS Press, (2012).
Results were analyzed with respect to the granularity of the prod- [15] Ruben Martins, Vasco M. Manquinho, and Inês Lynce, ‘Open-WBO:
A modular MaxSAT solver’, in Theory and Applications of Satisfiabil-
uct overview and with respect to complexity of the objective func- ity Testing – SAT 2014, eds., Carsten Sinz and Uwe Egly, volume 8561
tions. The results show that the investigated approaches have dif- of Lecture Notes in Computer Science, pp. 438–445. Springer Interna-
ferent suitability for different application cases. For reconfiguration tional Publishing, (2014).
the linear search performed by a PBS-Solver is a stronger alternative [16] David A. Plaisted and Steven Greenbaum, ‘A structure-preserving
compared to core guided MaxSAT. For calculating predictive config- clause form translation’, Journal of Symbolic Computation, 2(3), 293–
304, (September 1986).
urations – up to a certain amount of given frequency restrictions – [17] Olivier Roussel and Vasco M. Manquinho, ‘Pseudo-boolean and car-
the DPLL-based linear search is even more suitable than CPLEX. dinality constraints’, in Handbook of Satisfiability, eds., Armin Biere,
An important result is the small number of iterations observed in Marijn Heule, Hans van Maaren, and Toby Walsh, volume 185 of Fron-
linear search. The approach of linear search thus appears to be es- tiers in Artificial Intelligence and Applications, chapter 22, 695–733,
IOS Press, (2009).
pecially suitable for PBO-instances whose constraints are given by [18] Tilak Raj Singh and Narayan Rangaraj, ‘Generation of predictive con-
a product overview. For reliable usage of the DPLL-based linear figurations for production planning’, in Proceedings of the 15th In-
search, also for instances of long objective functions, a customized ternational Configuration Workshop, eds., Michel Aldanondo and An-
PBS solver needs to be developed. Such a solver must be able to dreas Falkner, pp. 79–86, Vienna, Austria, (August 2013).
more efficiently solve PBS instances that are characterized by a set [19] Carsten Sinz, Andreas Kaiser, and Wolfgang Küchlin, ‘Formal meth-
ods for the validation of automotive product configuration data’, Artifi-
of product overview clauses and one extensive LPB constraint. cial Intelligence for Engineering Design, Analysis and Manufacturing,
17(1), 75–97, (January 2003). Special issue on configuration.
[20] G. S. Tseitin, ‘On the complexity of derivations in the propositional cal-
REFERENCES culus’, Studies in Constructive Mathematics and Mathematical Logic,
Part II, 115–125, (1968).
[1] IBM ILOG CPLEX Optimizer. http://www- [21] Rouven Walter, Christoph Zengler, and Wolfgang Küchlin, ‘Applica-
01.ibm.com/software/commerce/optimization/cplex- tions of MaxSAT in automotive configuration’, in Proceedings of the
optimizer/index.html, June 2015. 15th International Configuration Workshop, eds., Michel Aldanondo
[2] Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy, ‘Im- and Andreas Falkner, pp. 21–28, Vienna, Austria, (August 2013).
proving SAT-based weighted MaxSAT solvers’, in Principles and Prac-
tice of Constraint Programming - 18th International Conference, CP
2012, ed., Michela Milano, volume 7514 of Lecture Notes in Computer
Science, pp. 86–101. Springer, (2012).
Juha Tiihonen, Andreas Falkner, and Tomas Axling, Editors 72
Proceedings of the 17th International Configuration Workshop
September 10-11, 2015, Vienna, Austria