=Paper=
{{Paper
|id=Vol-1220/paper9
|storemode=property
|title=ReMax - A MaxSAT aided Product (Re-)Configurator
|pdfUrl=https://ceur-ws.org/Vol-1220/09_confws2014_submission_6.pdf
|volume=Vol-1220
|dblpUrl=https://dblp.org/rec/conf/confws/WalterK14
}}
==ReMax - A MaxSAT aided Product (Re-)Configurator==
https://ceur-ws.org/Vol-1220/09_confws2014_submission_6.pdf
ReMax – A MaxSAT aided Product (Re-)Configurator
Rouven Walter and Wolfgang Küchlin1
Abstract. We introduce a product configurator with the ability of user process can look like using a MaxSAT aided product configura-
optimal re-configuration built on MaxSAT as the background engine. tor.
A product configurator supported by a SAT solver can provide an an- This paper is organized as follows. Section 2 introduces all rele-
swer at any time about which components are selectable and which vant mathematical definitions and notations needed for the later sec-
are not. But if a user wants to select a component which has already tions. In Section 3 we describe the basic concepts of SAT-based prod-
been disabled, a purely SAT based configurator does not support a uct configuration. Section 4 shows use cases of SAT aided product
guided re-configuration process. With MaxSAT we can compute the configuration. After that we describe use cases for MaxSAT aided
minimal number of changes of component selections to enable the product configuration in detail in Section 5 and illustrate a possible
desired component again. We implemented a product configurator configuration process. Sections 6 and 7 describe the techniques we
— called ReMax — using state-of-the-art MaxSAT algorithms. Be- used for our implementation and experimental results with bench-
sides the demonstration of handmade examples, we also evaluate the marks based on industrial configuration instances. Section 8 de-
performance of our configurator on problem instances based on real scribes related work and finally, Section 9 concludes this paper.
configuration data of the automotive industry.
2 Preliminaries
1 Introduction
We consider propositional formulas with the standard logical oper-
Using Propositional Logic encodings and SAT solving techniques to ators ¬, ∧, ∨, →, ↔ over the set of Boolean variables X and with
answer the question whether a formula is satisfiable or not has a wide the constants ⊥ and >, representing false and true, respectively. Let
range of applications [10]. The application of SAT solving for ver- vars(ϕ) be the set of variables of a formula ϕ. We call a formula
ification of automotive product documentation for inconsistencies, ϕ satisfiable, if there exists an assignment, a mapping from the set
e.g. within the bill-of-materials, has been pioneered by Küchlin and of Boolean variables X to {0, 1}, under which the formula ϕ eval-
Sinz [7]. uates to 1. The evaluation procedure is assumed to be the standard
In [16] we considered applications of MaxSAT in automotive con- evaluation for propositional formulas. The Boolean values 0 and 1
figuration. We mentioned the possible usage of re-configuration with are also referred to as false and true. If no such assignment exists,
MaxSAT to make an invalid configuration valid again by keeping the we say the formula is unsatisfiable. The question whether a proposi-
maximal number of the customer selections. Re-configuration is of tional formula is satisfiable or not is well-known as the satisfiability
highly practical relevance [9]. For example, the after-sales business (SAT) problem, which is NP-complete.
in the automotive industry wants to extend, replace or remove com- In most cases a SAT solver accepts only formulas in conjunctive
ponents with minimal effort while keeping the configuration valid. normal form (CNF). A formula in CNF is a conjunction of clauses,
In this paper, we extend this idea by considering product configu- where a clause is a disjunction of literals (variables or negated vari-
ration in general. We focus on product configuration based on fami- ables). Let var(l) be V W i of a literal l.
the variable
lies of options, because this is the normal case when a user configures If a formula ϕ = ki=1 m j=1 li,j in CNF is unsatisfiable, we can
a product. Within a family of options, the user must select exactly one ask the question about the maximal number of clauses that can be
option out of a regular family or else may select at most one option satisfied at the same time. This optimization variant of the SAT prob-
out of an optional family. With the focus on families, we can distin- lem is called maximum satisfiability (MaxSAT) problem. The corre-
guish two solving approaches: sponding question about the minimal number of unsatisfied clauses is
analogously called minimum unsatisfiabitlity (MinUNSAT) problem.
1. SAT Solving: With a SAT aided product configurator, we can val- A solution to one of the two problems can be used to easily com-
idate a configuration after each step of the configuration process. pute the solution of the other one, because the following relationship
2. MaxSAT Solving: With a MaxSAT aided product configurator, holds: k = MaxSAT(ϕ) + MinUNSAT(ϕ). It is worth noting that
we can compute an optimal solution for an invalid configuration, a model of the optimum of the MaxSAT problem is also a model of
such that a user has to make a minimal number of changes in the the optimum of the MinUNSAT problem and vice versa. In general,
current configuration to regain validity. there are several models for the optimum.
The MaxSAT problem can be extended in different ways: (i) we
We identify different use cases. We describe them in detail and make
can assign a non-negative integer weight to each clause (denoted with
remarks about extensions or variants of them. We also show how a
(C, w) for a clause C and a weight w) and ask for the maximum
1 Symbolic Computation Group, WSI Informatics, Universität Tübingen, sum of weights of satisfied clauses, which is known as the Weighted
Germany, www-sr.informatik.uni-tuebingen.de, email: MaxSAT problem, (ii) we can split the clauses in hard and soft clauses
{walterr,kuechlin}@informatik.uni-tuebingen.de and ask for the maximum number of satisfied soft clauses while sat-
isfying all hard clauses, which is known as the Partial MaxSAT prob- The
S following relation
S holds between rules and families:
lem, and finally (iii) we can combine both specifications, which is vars(R) ⊆ F.
R∈R F∈F
known as the Weighted Partial MaxSAT problem. The mentioned re-
lationship above between the MaxSAT and MinUNSAT problem also The rules R describe the relationship among the family members
holds for all MaxSAT variants. of the different families. They determine the possible valid combi-
Given a set of Boolean variables F = {M1 , ..., MP n } and the re- nations. The set F contains all optional and regular families. The
striction that exactly one variable has to be satisfied, n i=1 Mi = 1, mapping S represents the selections and deselections of the family
we call the set F a regular family and the elements members of members in respect of a priority. For simplicity reasons we will only
the family. For example, given a set of Boolean variables E = use the term selections to refer to both selections and deselections.
{E1 , E2 , E3 } representing the selectable engines of a car. An engine There are three main cases for a member s:
is chosen if and only if the corresponding variable is set to true. A
car has exactly one engine, which makes the set E a family. 1. S(s) = (c, 0) with c ∈ {no, yes}:
Given a family F = {M1 , ..., Mn } with the restriction that The user made no decision about the member (priority 0).
at most one variable has to be true, we call the set F an op- 2. S(s) = (c, p) with c ∈ {no, yes} and p ∈ N≥1 :
tional family. For example, given a set of Boolean variables AC = The user made a selection (priority greater zero).
{AC1 , AC2 , AC3 , AC4 } representing the selectable air conditioners 3. S(s) = (c, ∞) with c ∈ {no, yes}:
of a car. An air conditioner is an optional feature in a car, but there The user made an indispensable (hard) selection (infinity priority).
can be at most one air conditioner. This makes the set AC an optional
family. We abbreviate the mapping S for a member s as follows: For a posi-
The restrictions of a regular family or an optional family are spe- tive selection we write a positive literal s and for a negative selection
cial cases of cardinality constraints, which restrict the number of we write the negative literal ¬s. We can then write a single tuple
satisified variables of a set of Boolean variables to be {≤, <, =, > (s, p) with p ∈ N≥0 ∪ {∞} and describe the mapping S as a set of
, ≥} a non-negative integer k. The restriction for a regular family tuples. For simplicity reasons we leave each member s with priority
can be encoded in CNF with the following two formulas, while an 0 out of S in the given examples of this paper.
optional family can be encoded by using only the second formula: The set S of selections can be seen as a partial assignment
given by the user of the product configurator and can be divided
1. At least one satisfied variable: Vn
W
i=1 M
Vni in two disjoint sets of positive and negative selections: Pos(S) :=
2. At most one satisfied variable: n i=1 j=i+1 (¬Mi ∨ ¬Mj ) {(s, p) | (s, p) ∈ S and s is a positive literal} and Neg(S) :=
{(s, p) | (s, p) ∈ S and s is a negative literal}.
The given encodings for the two special cases = 1 and ≤ 1 are very The priority of a selected member is only relevant when it comes
simple and require only O n2 clauses without adding new auxil- to the question of re-configuration. Then the priorities represent the
iary variables. There are also encodings using auxiliary variables in users preferences.
exchange for a fewer number of clauses [14].
Since we consider only regular and optional family types, more Example 1. We consider a product configuration instance
general cardinality constraints than the above-mentioned special (R, F, S), where R and F describe components of a computer sys-
cases are not necessary and thus not considered in this paper. In the tem and dependencies among them. Table 1 shows the families and
context of automotive configuration, we usually deal with rules and Table 2 shows the rules. Let S = ∅, which means a user has not
families of certain model series. For example, the number of seats made selections so far.
is fixed and therefore we do not need to handle a family of seats
where we would need a cardinality constraint to restrict the selection Family Type Members
of seats between two and four. M (Mainboard) regular M1 , M2 , M3 , M4
V (Videocard) regular V1 , V2 , V3 , V4 , V5
C (CPU) regular C1 , C2 , C3 , C4
3 Product Configuration Concepts for P (Power Supply) regular P1 , P2
SAT-Configuration CD (CD-Device) optional CD1 , CD2 , CD3
In this section, we describe the basic concept of SAT-based product CR (Card-Reader) optional CR1 , CR2
configuration. We concentrate on rules in Propositional Logic, be- Table 1: Families F of the computer system
cause in our main application context of automotive configuration
we always deal with this type of rules. Along with the set of rules
we consider families, which results in the following definition for Rules
product configuration:
M1 → ((V1 ∨ V2 ∨ V4 ) ∧ (C1 ∨ C3 ) ∧ P1 ∧ ¬CD1 )
2
Definition 1. (Product Configuration Instance ) A product configu- M2 → ((V2 ∨ V5 ) ∧ (C2 ∨ C3 ) ∧ (P1 ∨ P2 ) ∧ ¬CD1 )
ration instance is a triple (R, F, S): M3 → ((V3 ∨ V4 ) ∧ (C2 ∨ C3 ∨ C4 ) ∧ P1 )
M4 → ((V1 ∨ V2 ) ∧ (C1 ∨ C4 ) ∧ P1 ∧ ¬CD2 )
• Set R = {ϕ1 , . . . , ϕk }, where ϕi is a propositional formula. C1 → ((V2 ∨ V3 ) ∧ P2 )
• Set F = {F1 ,S. . . , Fm }, where Fi is a family. C2 → (V4 ∨ V5 )
• Mapping S : m C3 → (V3 ∨ V4 )
i=1 vars(Fi ) → {no, yes} × (N≥0 ∪ {∞}).
2 In the configuration literature a product configuration instance is a solution
Table 2: Configuration rules R of the computer system
for a configuration problem, whereas we refer to the term as a description
of a product configuration problem. We will now define the criteria of a valid configuration:
Definition 2. (Valid Configuration) A product configuration instance Example 2. We reconsider the computer system configuration Ex-
is called a valid configuration if the following formula is satisfiable: ample 1. In the following two selection examples, we do not use pri-
^ ^ ^ orities because we just want to check the validity of the selections.
R∧ CC(F) ∧ s
R∈R F∈F (s,p)∈S,p6=0 1. S = {M1 , V4 } leads to a valid configuration, which can be com-
pleted to {M1 , V4 , C3 , P1 , CD3 , CR2 }.
Where CC(F) are the appropriate cardinality constraints of a family 2. S = {M1 , C1 } leads to an invalid configuration, because M1
(described in the preliminaries). requires P1 and C1 requires P2 , but due to the family constraints,
If a configuration instance is valid, the corresponding (partial) both cannot be selected at the same time.
variable assignment (also called model or configuration solution) is
of interest, because the variable assignment describes which mem-
bers are chosen and which are not. 4.2 Use Case: Computation of selectable members
A configuration solution is in general not complete, e.g. when the During the configuration process a user would like to know which
selections S made by a user contain selections with priority 0. of the remaining family members are still selectable, i.e. which se-
After defining the basic product configuration concepts, we will lections lead to a valid configuration. We can compute the selectable
go into more detail in the next section by describing which use cases members by validating the (partial) selections with a SAT solver. Al-
of a SAT aided product configurator exist and finally by showing an gorithm 2 shows the procedure. We iteratively make one SAT call for
iterative process of SAT aided product configuration. each member and check if selecting this member is valid.
4 SAT aided Product Configuration Algorithm 2: Computation of selectable members
Input: (R, F, S)
With SAT solving a product configurator can validate a user’s se- S
lection and also compute the selectable members for the remaining
Output: Mapping V from F∈F F to {no, yes} indicating
whether a member is selectable or not
families. The overall plan is quite simple: Each selection of an op-
V ← InitializeSmapping
tion results in a true valuation of that option. Regular families result
foreach m ∈ F∈F F do
in propagations of the value false to the remaining options, after one if
family member has been selected. Given a partial valuation, it is easy
!
V V V
to compute by SAT solving which of the remaining options can still SAT CNF(R) ∧ CC(F) ∧ s∧m
R∈R F∈F (s,p)∈S,p6=0
be selected, and which must be set to true or false, respectively, as a
consequence of previous selections. then
We describe these use cases in detail in the following subsections V ← (m, yes)
and afterwards consolidate them in an iterative user process. else
V ← (m, no)
return V
4.1 Use Case: Validation & completion of a
(partial) selection
After the computation of selectable members, the SAT aided prod-
Given a product configuration instance (R, F, S), we can validate
uct configurator can display the result to the user (i.e. by disabling all
the selections with a SAT solver by checking the formula of Def-
non-selectable members). Then the user knows about the selectable
inition 2 for satisfiability. Algorithm 1 shows the procedure. Only
members.
selections with a priority 6= 0 are taken into account for the valida-
tion.
Remarks:
Algorithm 1: Validation & completion of a (partial) selection
1. In the special case S = ∅, in which no selection has been made by
Input: (R, F, S) the user so far, the computation of the selectable members implic-
Output: (result, model), where result is true if the (partial) itly brings up members which can never be part of a valid config-
selection is valid, otherwise false and model is a uration (redundant members) and members which have to be part
complete variable assignment ! of each valid configuration (forced members).
V V V 2. The performance of Algorithm 2 can be improved. If a family al-
return SAT CNF(R) ∧ CC(F) ∧ s
R∈R F∈F (s,p)∈S,p6=0 ready contains a positively selected member, then we know that
all remaining members are not selectable anymore due to the fam-
ily constraints. We just have to check families with no positively
Because most SAT solvers take CNF as input, we write CNF(R) selected member.
to indicate the transformation of an arbitrary rule to its CNF rep- The performance can be improved further. We use an incremental
resentation. In practice we use a polynomial formula transforma- and decremental SAT solver, which allows us to load all rules,
tion [15, 12] to get an equisatisfiable formula to avoid the potentially family constraints and selections first and check each member m
exponential blow-up that occurs when using the distributive law. by adding and removing the unit clause m from the SAT solver.
If the configuration instance is valid, the algorithm also returns We do not have to load the invariant constraints repeatedly for
a complete variable assignment. This complete variable assignment each check.
gives an example which selections have to be made to complete the
given configuration instance. In general, the given model is not uniqe Example 3. We compute the selectable members for our computer
and there exist several models. system configuration (see Example 1):
1. S = ∅: Table 3 shows the remaining selectable members. Remark: If a given complete example model l1 ∧ . . . ∧ ln in the
SAT case does not satisfy the demands of the user, she can exclude
Family Selectable Memb. Non-Selectable Memb. this model by adding the hard clause ¬l1 ∨ . . . ∨ ¬ln . Then an-
other complete model will be produced if one exists, otherwise we
M (Mainboard) M1 , M2 , M3 , M4
encounter the UNSAT case.
V (Videocard) V1 , V2 , V3 , V4 , V5
In a SAT aided product configuration process described above, the
C (CPU) C2 , C3 , C4 C1
user is left to herself when it comes to the question which selec-
P (Power Supply) P1 , P2
tions should be undone to regain a valid configuration. Perhaps the
CD (CD-Device) CD1 , CD2 , CD3
user made a selection of a highly desired member, which she does
CR (Card-Reader) CR1 , CR2
not want to take back. Now the user has to try different configu-
Table 3: Selectable members for an empty selection ration changes by herself and a guidance is missing which one to
choose. This is the point where MaxSAT aided product configura-
tion can help. We will describe re-configuration use cases in detail in
2. S = {M1 , V4 }: Table 4 shows the remaining selectable members.
the following section.
Family Selectable Memb. Non-Selectable Memb.
C (CPU) C3 C1 , C2 , C4 5 MaxSAT aided Product (Re-)Configuration
P (Power Supply) P1 P2 In this section we describe how re-configuration can be done with
CD (CD-Device) CD2 , CD3 CD1 partial (weighted) MaxSAT as a background engine. We show two
CR (Card-Reader) CR1 , CR2 basic use cases, describe possible variations of them and finally inte-
Table 4: Result of the selectable members computation grate the re-configuration step into our iteractive user process.
5.1 Use Case: Re-configuration of the selections
4.3 SAT aided configuration process
During the configuration process we may reach a state where we have
an invalid configuration. The cause of the conflict can be one or both
Figure 1 illustrates a possible SAT aided configuration process in-
of the following:
volving both Use Cases 4.1 and 4.2. After the user has made one or
multiple selections, the SAT solver validates the current configura- 1. The selections S conflict with the rules R.
tion. This results in two cases: 2. The selections S conflict with the family constraints.
1. Valid configuration: In the case of a valid configuration, the user We have to re-configure either the rules or the selections to re-
can continue selecting members. Additionally, to guide the user gain validity. For now we consider all rules as hard limitations that
we can compute the selectable members for the current configura- we can not soften, which is the common case. We will discuss re-
tion. After new selections, the process iterates. configuration of rules later in Section 5.4.
2. Invalid configuration: In the case of an invalid configuration, the Considering the rules as a hard restrictions, the question arises,
user has to take back one or more of the previously made selec- how many of the selections can be kept maximally to reach a valid
tions. The user can validate each backtracking step again until a configuration. Remember, a user may have done multiple selections
valid configuration state is reached. at once without validating the current configuration and without con-
sidering the selectable members. Therefore, removing only the last
selection does not lead to a valid configuration again in general. Also
the last selection could be of infinity priority, so it is no option for
3a. UNSAT the user to remove the last selection.
To answer the question we set the selections as soft unit clauses
and re-configure the selections with a partial MaxSAT solver. The
following encoding represents our requirements:
1. Select 2. Encode SAT Solver
[ [ [
Hard := CNF(R) ∪ CC(F) ∪ {s}
R∈R F∈F (s,p)∈S,p=∞
User 3b. SAT
[
Soft := {s}
(s,p)∈S,p6=0,p6=∞
Configuration
Verify &
Selections with priority ∞ are also considered as indispensable and
Complete
4. Feedback will be encoded as hard unit clauses. Only dispensable selections will
Selectable be re-configured. Algorithm 3 shows the re-configuration procedure.
Members
With the resulting model, we can give the user an example of a
complete selection which requires a minimal number of changes in
Figure 1. SAT aided configuration process order to regain a valid configuration compared to the original selec-
tions. Or, the other way round, the model gives an example about
how to keep the maximal number of selections.
would have to make 4 changes minimally, e.g. by choosing M2 , V5 ,
Algorithm 3: Re-Configuration of a (partial) selection
C2 , P1 , CD3 , CR2 .
Input: (R, F, S)
Output: (optimum, model), where optimum is the minimal
number of changes to regain a valid configuration and 5.2 Use Case: Re-Configuration of the selections
model is a model for the optimum with priorities
Hard ← ∅ In the previous use case we treated all soft clauses as equivalent. A
Soft ← ∅ user may prefer one member over the other, which results in prior-
foreach R ∈ R do ization of the selected members. We can handle priorities with Par-
Hard ← Hard ∪ CNF(R) tial Weighted MaxSAT solving. The encoding for this use case is
foreach F ∈ F do basically the same as before, but now we bring priorities into play.
Hard ← Hard ∪ CC(F) Algorithm 4 shows the complete computation procedure.
foreach (s, p) ∈ S ∧ p 6= 0 do
if p = ∞ then Algorithm 4: Re-Configuration of a (partial) selection with pri-
Hard ← Hard ∪ {s} orities
else Input: (R, F, S)
Soft ← Soft ∪ {s} Output: (optimum, model), where optimum is the minimal
(optimum, model) ← PartialMinUNSAT(Hard, Soft) number of priority points to change to regain a valid
return (optimum, model) configuration and model is a model for the optimum
Hard ← ∅
Soft ← ∅
Remark: As desribed before we use a transformation like Tseitin
foreach R ∈ R do
or Plaisted-Greenbaum instead of CNF(R) in practice. Even though Hard ← Hard ∪ CNF(R)
the Tseitin and Plaisted-Greenbaum transformations are only equi-
foreach F ∈ F do
satisfiable, this is not an issue for MaxSAT when converting for-
Hard ← Hard ∪ CC(F)
mulas into hard clauses. Since the Tseitin and Plaisted-Greenbaum
transformations share the same models on the original variables, one foreach (s, p) ∈ S ∧ p 6= 0 do
can easily verify that the search space between the converted and the if p = ∞ then
original instance remains the same. Hard ← Hard ∪ {s}
else
Soft ← Soft ∪ {(s, p)}
Extensions: The described use case can be extended as follows:
(optimum, model) ←
1. User constraints: A user can add additional constraints consid- PartialWeightedMinUNSAT(Hard, Soft)
ered as hard clauses. return (optimum, model)
If, e.g., mainboard M1 is selected, the user definitely wants video
card V2 to be selected. But if mainboard M2 is selected, the user
definitely wants video card V5 to be selected. Then we add the
Extension: All extensions presented in Subsection 5 carry over to
rules (M1 → V2 ) ∧ (M2 → V5 ) as constraints to the rules R.
this use case.
2. Focus on selection: For each family an option “choose one of the
selected” can be offered to add a constraint such that only positive Example 5. We reconsider our re-configuration Example 4 and add
selected members within a family will be considered during the a priority of 2 for member V2 . Table 6 shows our selections with the
re-configuration computation. corresponding weights in parentheses and the results.
E.g. if a user focuses on mainboards M1 , M3 , M4 , a hard clause
(M1 ∨ M3 ∨ M4 ) will be added to the rules R. Family Focus Selections Results
M No (M1 , 1), (M2 , 1), (¬M3 , 1) M4
Example 4. We continue our canonical Example 1: Table 5 shows V Yes (V1 , 1), (V2 , 2) V2
multiple selections of members within families and a result model C No (C2 , 1), (C3 , 1) C4
re-configuration. For all selections shown we choose priority 1, that P No P1
means no selection in this example is an indispensable one. CD No (¬CD1 , ∞) CD3
CR No CR2
Family Focus Selections Results
Table 6: Users selections with priorities and results
M No (M1 , 1), (M2 , 1), (¬M3 , 1) M4
V Yes (V1 , 1), (V2 , 1) V1
C No (C2 , 1), (C3 , 1) C4 Result: We have to change 5 priority points minimally to regain a
P No P1 valid configuration. If we would still be choosing member V1 instead
CD No (¬CD1 , ∞) CD3 of member V2 we would have to change 6 priority points, because of
CR No CR2 the higher priority of V2 .
Table 5: Users selections and results
5.3 A MaxSAT aided re-configuration process
Result: We have to make 5 changes minimally to regain a valid We reconsider the process of Figure 1 in Step 3a. UNSAT where the
configuration. Without the focus set for the video cards family V , we user gets the feedback that her current selections lead to an invalid
configuration. With a SAT solver only, the user has to try by herself 1. Violation of the family constraints: If a user selects more than
which selections have to be undone to regain a valid configuration. one member of a family with infinity priority, the family con-
But now, we can help the user at this point by using re-configuration straints are violated.
with MaxSAT. Figure 2 illustrates both Use Cases 5.1 and 5.2 em- 2. Violation of rules: If a user does not violate the family con-
bedded in a product configuration process using MaxSAT. straints, then the selected members with priority infinity are in
collision with the rules.
3a. No solution The first case can be handled by a product configurator by simply
not allowing to choose more than one member with priority infinity
or giving the user a warning message when doing so.
In the second case, if the user is not willing to soften her selections,
MaxSAT we can not re-configure the selections w.r.t. the rules. But when we
1. Re-configurate 2. Encode
Solver have a closer look at the rules, there may be some rules, which we
can soften, e.g. when a rule is not a physical or technical restric-
User 3b. Solution tion, but only exists for marketing or similiar purposes. A company
Invalid Configuration may be willing to violate or change some of these rules to build the
Optimum product. Knowing the miminum number of rule changes in order to
+ permit a desired vehicle configuration can help in managing the set
4. Feedback
Example of marketing rules.
Model For this use case, we extend Definition 1 by an additional mapping
SR : R → (N≥0 ∪ {∞}), which represents the priorities of the
rules a user made. After softening some of the rules this way we can
Figure 2. MaxSAT aided configuration process re-configure the rules by maximizing the number of satisfied rules,
respectively violating only a minimal number of rules. Algorithm 5
shows this procedure more formally.
After the user gets the feedback UNSAT, she can start a re- Algorithm 5: Re-Configuration of rules
configuration of her current selections. This results in two cases: Input: (R, F, S)
Output: (optimum, model), where optimum is the minimal
1. No solution: If the indispensable selections (with priority ∞) col-
number of changes to regain a valid configuration and
lide with the rules or the family constraints, then there is no solu-
model is a model for the optimum
tion. In this case, the user has to weaken some of the indispensable
Hard ← S
selections in order to make a re-configuration possible. The user
Soft ← S
can use high priorities to weaken the desired members to ensure
foreach F ∈ F do
they will be preferred over other selections.
Hard ← Hard ∪ CC(F)
2. Solution: If the indispensable selections can be satisfied, then
there exists a solution with an optimum for the prioritized selec- foreach R ∈ R ∧ SR (R) 6= 0 do
tions. In this case, the user will be told about the optimum, i.e. if p = ∞ then
about the number of minimal changes to regain a valid configura- Hard ← Hard ∪ CNF(R)
tion. Also, an example model with the optimum will be given to else
Hard ← Hard ∪ CNF(bR → R)
the user.
Soft ← Soft ∪ {bR }
Remark: Similiar to the SAT aided configuration process the fol- foreach (s, p) ∈ S ∧ p 6= 0 do
lowing holds: If the given complete example model l1 ∧ . . . ∧ ln in if p = ∞ then
Hard ← Hard ∪ {s}
the solution case does not satisfy the demands of the user, she can
else
exclude this model by adding the hard clause ¬l1 ∨ . . . ∨ ¬ln . Then
Soft ← Soft ∪ {s}
another model with the same optimum will be produced, if one ex-
ists. If there is no other model with the same optimum, the next best (optimum, model) ← PartialMinUNSAT(Hard, Soft)
optimum under the new conditions will be computed with an exam- return (optimum, model)
ple model.
In case there is no solution and a user just do not want to weaken Since a rule R is an arbitrary formula, we can not just convert
her selections with priority ∞, we can consider weakening the rules. R to its CNF and add the resulting clauses as soft clauses. In gen-
In the next section, we will describe this possibility in detail. eral, some of these clauses will be satisfied and some not. Instead we
want to maximize the number of rules. In other words, we are facing
5.4 Use Case: Re-configuration of rules a group MaxSAT problem [2, 6], where each CNF(R) is a group of
clauses. The goal of group MaxSAT is to satisfy the maximum num-
It is possible that the selections a user made have no solution when ber of groups. A group is satisfied if all clauses within the group are
trying to re-configure them. Assuming the rules themselves are not satisfied.
contradictory, then the cause for no solution are too many selections The group MaxSAT problem can be reduced to a partial MaxSAT
with priority ∞. There are two cases which can occur or both at the problem as follows: For each non-indispensable rule R we introduce
same time: a new variable bR and add the hard clauses CNF(bR → R). Addi-
tionally we add a unit soft clause {bR } for each new variable. Each Rules Families
satisfied variable bR implies the whole group of clauses in CNF(R) Problem Quantity #Variables Quantity Avg. size
to be satisfied. Therefore, satisfying a maximal number of the newly M01_01 2074 1772 34 34,294
introduced variables satisfies a maximal number of the corresponding M01_02 2430 2087 41 39,293
formulas. On the other hand, with the help of the newly introduced M01_03 1137 880 30 18,233
variables, we can identify, from the resulting model, which formu- M02_01 11627 996 188 6,282
las are satisfied and show this result to the user. For a more detailed M02_02 4465 612 174 5,321
explanation, see [2, 6].
Table 7: Statistics about car manufacturer problems
Extension: Of course, rules can also have different priorities and
we can extend this use case by assigning priorities to rules and selec- For the following benchmarks we used two partial weighted
tions to compute the maximal sum of priority points. This extension MaxSAT solvers, which are based on the following principles:
can be realized analogously as described for Use Case 5.2, thus we
will not describe it explicitly. 1. WPM1: An unsat core-guided approach with iterative SAT calls.
In each iteration a new blocking variable will be added to each
soft clause within the unsat core [1].
6 Implementation techniques 2. msu4: An unsat core-guided approach with iterative SAT calls us-
ing a reduced number of blocking variables [11].
We implemented the above SAT-based and MaxSAT-based use cases
in one product configurator — called ReMax — on top of our uni- We implemented WPM1 on top of our own SAT solver while msu4
form logic framework, which we use for commercial applications is an external solver3 .
within the context of automotive configuration. Our SAT solver pro- Our environment for the benchmarks has the following hardware
vides an incremental and decremental interface. We maintain two and software settings. Processor: Intel Core i7-3520M, 2,90 GHz;
versions (Java and .NET) and decided to implement ReMax using Main memory: 8 GB. WPM1, based on .NET 4.0, runs under Win-
.NET 4.0 with C# along with the WPF Framework for the GUI. dows 7 while msu4 runs under Ubuntu 12.04.
We implemented state-of-the-art partial (weighted) MaxSAT solvers For Use Case 5.2 we created three categories as follows: Out of
Fu&Malik, PM2 and WPM1 on top of our SAT solver [5, 1]. 30%, 50% and 70% of the families one member is selected randomly
with a random priority between 1 and 10. The rules have infinity
priority. In general, this leads to an invalid configuration because the
rules are violated. For each category we created 10 instances.
Table 8 shows the results for each category as average time in sec-
onds. The abbreviation “exc.” means that the time limit of 30 minutes
was exceeded. As we can see, msu4 performs very well in all cate-
gories with reasonable times from less than one second up to about
25 seconds. Our solver WPM1 also has reasonable times from about
2 seconds up to about 28 seconds, but exeeds the time limit in two
categories for the instance M02_01.
30% 50% 70%
Problem WPM1 msu4 WPM1 msu4 WPM1 msu4
M01_01 7,34 0,66 12,70 1,08 15,59 1,84
M01_02 8,59 0,74 16,48 1,32 27,44 2,96
M01_03 2,10 0,33 4,10 0,45 5,80 0,85
M02_01 20,99 2,16 exc. 5,91 exc. 24,45
M02_02 3,90 0,48 9,60 1,56 13,01 4,77
Table 8: Results of Use Case 5.2 scenario
Figure 3. Screenshot of ReMax with open “Families” tab
For Use Case 5.4 we created three categories as follows: Out of
30%, 50% and 70% of the families one member is selected randomly
Figure 3 shows an example screenshot from the ReMax GUI with with infinity priority, which leads to an invalid configuration in gen-
the “Families” tab opened. eral because the rules are violated. But this time, we assign all rules
a priority of 1. For each category we created 10 instances.
Table 9 shows the results for each category as average time in sec-
7 Experimental Results onds. As we can see, both solvers can handle all instances in each
category in reasonable time. While WPM1 takes from about 3 sec-
onds up to about 72 seconds, the external solver msu4 takes from less
Table 7 show statistics about the real configuration data from two
than one second up to about 9 seconds in the worst case.
different German car manufacturers, called M01 and M02, which we
used for our benchmarks. Car manufacturer M01 uses arbitrary for-
3 http://logos.ucd.ie/web/doku.php?id=msuncore
mulas as rules, whereas M02 uses clauses as rules.
30% 50% 70% (re-)configurator that feeds directly off the engineering product doc-
Problem WPM1 msu4 WPM1 msu4 WPM1 msu4 umentation. E.g., many test prototypes must be built before start of
M01_01 9,35 2,39 16,19 3,93 20,63 4,35 production with a varying set of options.
M01_02 12,86 2,80 19,32 5,47 27,82 4,82 Expert users sometimes need some complete car configurations
M01_03 2,54 0,78 5,71 1,45 6,76 1,74 which cover all valid combinations of a subset of options, e.g. for
testing purposes. With a SAT based (re-)configurator, an expert user
M02_01 18,40 4,43 41,16 8,33 71,29 8,55
can start the configuration from the desired options instead of te-
M02_02 5,13 0,49 9,88 1,04 16,32 1,48
diously following the given configuration process in a usual sales
Table 9: Results of Use Case 5.4 scenario configurator. At any time, the user can ask the configurator for “any
completion” or, using MaxSAT, for a “minimal completion” of the
partial configuration to a complete configuration.
8 Related Work
Another approach for re-configuration uses answer set programming REFERENCES
(ASP) on a decidable fragment of first-order logic [4]. Hence the
[1] Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy, ‘Solving
used language is more expressive. With the growing performance of
(weighted) partial MaxSAT through satisfiability testing’, in Theory
SAT solvers in the last decade, SAT solving in turn has been used to and Applications of Satisfiability Testing - SAT 2009, ed., Oliver Kull-
solve problem instances of ASP [8]. mann, volume 5584 of Lecture Notes in Computer Science, 427–440,
An algorithm for computing minimal diagnoses using a conflict Springer Berlin Heidelberg, (2009).
detection algorithm is introduced in [13]. A minimal subset ∆ of [2] Josep Argelich and Felip Many, ‘Exact Max-SAT solvers for over-
constrained problems.’, Journal of Heuristics, 12(4–5), 375–392,
constraints is called a diagnosis if the original constraints without ∆ (September 2006).
are consistent. Although this approach is described for constraints [3] A. Felfernig, M. Schubert, and C. Zehentner, ‘An efficient diagnosis al-
of first-order sentences, the technqiues can be generalized to a wide gorithm for inconsistent constraint sets’, Artificial Intelligence for En-
range of other logics. gineering Design, Analysis and Manufacturing, 26(1), 53 – 62, (2012).
[4] Gerhard Friedrich, Anna Ryabokon, Andreas A. Falkner,
The indicated idea above is further improved in [3], where an al-
Alois Haselböck, Gottfried Schenner, and Herwig Schreiner,
gorithm — called FastDiag — is introduced which computes a pre- ‘(re)configuration using answer set programming’, in IJCAI-11
ferred minimal diagnosis while improving performance. Configuration Workshop Proceedings, eds., Kostyantyn Shcheko-
We did not consider works dealing with explanations like MUS tykhin, Dietmar Jannach, and Markus Zanker, pp. 17–24, Barcelona,
(Minimal Unsatisifable Subset) iteration. When using MUS iteration Spain, (July 2011).
[5] Zhaohui Fu and Sharad Malik, ‘On solving the partial MAX-SAT prob-
for re-configuration, a user not only has to manually solve each con- lem’, in Theory and Applications of Satisfiability Testing—SAT 2006,
flict, but also will not necessarily solve the conflicts in an optimal eds., Armin Biere and Carla P. Gomes, volume 4121 of Lecture Notes
manner, i.e. only changing a minimal number of selections. in Computer Science, 252–265, Springer Berlin Heidelberg, (2006).
[6] Federico Heras, Antnio Morgado, and Joo Marques-Silva, ‘An empir-
ical study of encodings for group MaxSAT’, in Canadian Conference
9 Conclusion on AI, eds., Leila Kosseim and Diana Inkpen, volume 7310 of Lecture
Notes in Computer Science, pp. 85–96. Springer, (2012).
We described product configuration for propositional logic based rule [7] Wolfgang Küchlin and Carsten Sinz, ‘Proving consistency assertions
sets which are widely used in the automotive industry. We showed for automotive product data management’, Journal of Automated Rea-
soning, 24(1–2), 145–163, (2000).
applications of SAT solving by two use cases. Furthermore, we [8] Fangzhen Lin and Yuting Zhao, ‘ASSAT: Computing answer sets of a
showed use cases of how MaxSAT can be used for product configu- logic program by SAT solvers.’, Artifical Intelligence, 157(1–2), 115–
ration when it comes to an invalid configuration. With MaxSAT we 137, (August 2004).
are able to re-configure an invalid configuration in an optimal way, [9] Peter Manhart, ‘Reconfiguration – a problem in search of solutions’, in
IJCAI-05 Configuration Workshop Proceedings, eds., Dietmar Jannach
i.e. we can compute the minimal number of necessary changes. We
and Alexander Felfernig, pp. 64–67, Edinburgh, Scotland, (July 2005).
embedded both scenarios in configuration processes showing how a [10] João Marques-Silva, ‘Practical applications of boolean satisfiability’, in
user can be guided during the configuration process. Discrete Event Systems, 2008. WODES 2008. 9th International Work-
We presented an implementation of a product configurator — Re- shop on, 74–80, IEEE, (2008).
Max — supporting all of the described use cases using state-of-the- [11] João Marques-Silva and Jordi Planes, ‘Algorithms for maximum satis-
fiability using unsatisfiable cores’, in Proceedings of the Conference on
art SAT and MaxSAT solving techniques. From real automotive con- Design, Automation and Test in Europe, DATE ’08, pp. 408–413. IEEE,
figuration data from two different German premium car manufactur- (2008).
ers we created synthetic product configuration benchmarks for the [12] David A. Plaisted and Steven Greenbaum, ‘A structure-preserving
presented use cases. Besides our own MaxSAT solver we used the clause form translation’, Journal of Symbolic Computation, 2(3), 293–
304, (September 1986).
external solver msu4 to measure and compare the performance. As
[13] Raymond Reiter, ‘A theory of diagnosis from first principles’, Artificial
our experimental results show, we can re-configure those problem in- Intelligence, 32(1), 57 – 95, (April 1987).
stances in reasonable time. Since some problem instances could be [14] Carsten Sinz, ‘Towards an optimal CNF encoding of boolean
solved within a few seconds, our product configurator could be used cardinality constraints’, in Principles and Practice of Constraint
as an interactive tool in these cases. Other problem instances took Programming—CP 2005, ed., Peter van Beek, Lecture Notes in Com-
puter Science, 827–831, Springer Berlin Heidelberg, (2005).
over a minute in the worst case, but is still more than adequate for [15] G. S. Tseitin, ‘On the complexity of derivations in the propositional cal-
a responsive batch service. While this may seem long, we were told culus’, Studies in Constructive Mathematics and Mathematical Logic,
that the manual configuration of an order without tool support by a Part II, 115–125, (1968).
trial and error process may well take on the order of half an hour. [16] Rouven Walter, Christoph Zengler, and Wolfgang Küchlin, ‘Applica-
tions of MaxSAT in automotive configuration’, in Proceedings of the
We do not claim that our approach is currently fit for use as
15th International Configuration Workshop, eds., Michel Aldanondo
a consumer configurator. However, many business units of a car and Andreas Falkner, pp. 21–28, Vienna, Austria, (August 2013).
manufacturer, such as engineering or after sales are in need of a