We introduce a product configurator with the ability of optimal re-configuration built on MaxSAT as the background engine. A product configurator supported by a SAT solver can provide an answer at any time about which components are selectable and which are not. But if a user wants to select a component which has already been disabled, a purely SAT based configurator does not support a guided re-configuration process. With MaxSAT we can compute the minimal number of changes of component selections to enable the desired component again. We implemented a product configurator - called ReMax - using state-of-the-art MaxSAT algorithms. Besides the demonstration of handmade examples, we also evaluate the performance of our configurator on problem instances based on real configuration data of the automotive industry.
Using Propositional Logic encodings and SAT solving techniques to
answer the question whether a formula is satisfiable or not has a wide
range of applications [
In [
In this paper, we extend this idea by considering product configuration in general. We focus on product configuration based on families of options, because this is the normal case when a user configures a product. Within a family of options, the user must select exactly one option out of a regular family or else may select at most one option out of an optional family. With the focus on families, we can distinguish two solving approaches: 1. SAT Solving: With a SAT aided product configurator, we can validate a configuration after each step of the configuration process. 2. MaxSAT Solving: With a MaxSAT aided product configurator, we can compute an optimal solution for an invalid configuration, such that a user has to make a minimal number of changes in the current configuration to regain validity.
We identify different use cases. We describe them in detail and make remarks about extensions or variants of them. We also show how a user process can look like using a MaxSAT aided product configurator.
This paper is organized as follows. Section 2 introduces all relevant mathematical definitions and notations needed for the later sections. In Section 3 we describe the basic concepts of SAT-based product configuration. Section 4 shows use cases of SAT aided product configuration. After that we describe use cases for MaxSAT aided product configuration in detail in Section 5 and illustrate a possible configuration process. Sections 6 and 7 describe the techniques we used for our implementation and experimental results with benchmarks based on industrial configuration instances. Section 8 describes related work and finally, Section 9 concludes this paper. 2
We consider propositional formulas with the standard logical operators :; ^; _; !; $ over the set of Boolean variables X and with the constants ? and >, representing false and true, respectively. Let vars(') be the set of variables of a formula '. We call a formula ' satisfiable, if there exists an assignment, a mapping from the set of Boolean variables X to f0; 1g, under which the formula ' evaluates to 1. The evaluation procedure is assumed to be the standard evaluation for propositional formulas. The Boolean values 0 and 1 are also referred to as false and true. If no such assignment exists, we say the formula is unsatisfiable. The question whether a propositional formula is satisfiable or not is well-known as the satisfiability (SAT) problem, which is NP-complete.
In most cases a SAT solver accepts only formulas in conjunctive normal form (CNF). A formula in CNF is a conjunction of clauses, where a clause is a disjunction of literals (variables or negated variables). Let var(l) be the variable of a literal l.
If a formula ' = Vik=1 Wjm=i1 li;j in CNF is unsatisfiable, we can ask the question about the maximal number of clauses that can be satisfied at the same time. This optimization variant of the SAT problem is called maximum satisfiability (MaxSAT) problem. The corresponding question about the minimal number of unsatisfied clauses is analogously called minimum unsatisfiabitlity (MinUNSAT) problem. A solution to one of the two problems can be used to easily compute the solution of the other one, because the following relationship holds: k = MaxSAT(') + MinUNSAT('). It is worth noting that a model of the optimum of the MaxSAT problem is also a model of the optimum of the MinUNSAT problem and vice versa. In general, there are several models for the optimum.
The MaxSAT problem can be extended in different ways: (i) we can assign a non-negative integer weight to each clause (denoted with (C; w) for a clause C and a weight w) and ask for the maximum sum of weights of satisfied clauses, which is known as the Weighted MaxSAT problem, (ii) we can split the clauses in hard and soft clauses and ask for the maximum number of satisfied soft clauses while satisfying all hard clauses, which is known as the Partial MaxSAT problem, and finally (iii) we can combine both specifications, which is known as the Weighted Partial MaxSAT problem. The mentioned relationship above between the MaxSAT and MinUNSAT problem also holds for all MaxSAT variants.
Given a set of Boolean variables F = fM1; :::; Mng and the restriction that exactly one variable has to be satisfied, Pn i=1 Mi = 1, we call the set F a regular family and the elements members of the family. For example, given a set of Boolean variables E = fE1; E2; E3g representing the selectable engines of a car. An engine 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.
Given a family F = fM1; :::; Mng with the restriction that at most one variable has to be true, we call the set F an optional family. For example, given a set of Boolean variables AC = fAC1; AC2; AC3; AC4g representing the selectable air conditioners of a car. An air conditioner is an optional feature in a car, but there can be at most one air conditioner. This makes the set AC an optional family.
The restrictions of a regular family or an optional family are special cases of cardinality constraints, which restrict the number of satisified variables of a set of Boolean variables to be f ; <; =; > ; g a non-negative integer k. The restriction for a regular family can be encoded in CNF with the following two formulas, while an optional family can be encoded by using only the second formula:
i=1 Mi
2. At most one satisfied variable: Vin=1 Vjn=i+1(:Mi _ :Mj )
The given encodings for the two special cases = 1 and 1 are very
simple and require only O n2 clauses without adding new
auxiliary variables. There are also encodings using auxiliary variables in
exchange for a fewer number of clauses [
Since we consider only regular and optional family types, more general cardinality constraints than the above-mentioned special cases are not necessary and thus not considered in this paper. In the context of automotive configuration, we usually deal with rules and families of certain model series. For example, the number of seats 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 of seats between two and four. 3
In this section, we describe the basic concept of SAT-based product configuration. We concentrate on rules in Propositional Logic, because 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 product configuration: Definition 1. (Product Configuration Instance2) A product configuration instance is a triple (R; F ; S):
Set R = f'1; : : : ; 'kg, where 'i is a propositional formula. Set F = fF1; : : : ; Fmg, where Fi is a family.
Mapping S : Sim=1 vars(Fi) ! fno; yesg (N 0 [ f1g). 2 In the configuration literature a product configuration instance is a solution for a configuration problem, whereas we refer to the term as a description of a product configuration problem.
The following relation holds between rules and families:
R2R F2F
The rules R describe the relationship among the family members of the different families. They determine the possible valid combinations. The set F contains all optional and regular families. The mapping S represents the selections and deselections of the family members in respect of a priority. For simplicity reasons we will only use the term selections to refer to both selections and deselections. There are three main cases for a member s: 1. S(s) = (c; 0) with c 2 fno; yesg:
The user made no decision about the member (priority 0). 2. S(s) = (c; p) with c 2 fno; yesg and p 2 N 1:
The user made a selection (priority greater zero). 3. S(s) = (c; 1) with c 2 fno; yesg:
The user made an indispensable (hard) selection (infinity priority). We abbreviate the mapping S for a member s as follows: For a positive selection we write a positive literal s and for a negative selection we write the negative literal :s. We can then write a single tuple (s; p) with p 2 N 0 [ f1g and describe the mapping S as a set of tuples. For simplicity reasons we leave each member s with priority 0 out of S in the given examples of this paper.
The set S of selections can be seen as a partial assignment given by the user of the product configurator and can be divided in two disjoint sets of positive and negative selections: Pos(S) := f(s; p) j (s; p) 2 S and s is a positive literalg and Neg(S) := f(s; p) j (s; p) 2 S and s is a negative literalg.
The priority of a selected member is only relevant when it comes to the question of re-configuration. Then the priorities represent the users preferences.
Example 1. We consider a product configuration instance (R; F ; S), where R and F describe components of a computer system and dependencies among them. Table 1 shows the families and Table 2 shows the rules. Let S = ;, which means a user has not made selections so far.
Family
Type
Members M (Mainboard) regular V (Videocard) regular C (CPU) regular P (Power Supply) regular CD (CD-Device) optional CR (Card-Reader) optional
M1; M2; M3; M4 V1; V2; V3; V4; V5 C1; C2; C3; C4 P1; P2 CD1; CD2; CD3
CR1; CR2 We will now define the criteria of a valid configuration: Definition 2. (Valid Configuration) A product configuration instance is called a valid configuration if the following formula is satisfiable: ^ R ^ ^ CC(F) ^ Where CC(F) are the appropriate cardinality constraints of a family (described in the preliminaries).
If a configuration instance is valid, the corresponding (partial) variable assignment (also called model or configuration solution) is of interest, because the variable assignment describes which members are chosen and which are not.
A configuration solution is in general not complete, e.g. when the selections S made by a user contain selections with priority 0.
After defining the basic product configuration concepts, we will go into more detail in the next section by describing which use cases of a SAT aided product configurator exist and finally by showing an iterative process of SAT aided product configuration. 4
With SAT solving a product configurator can validate a user’s selection and also compute the selectable members for the remaining families. The overall plan is quite simple: Each selection of an option results in a true valuation of that option. Regular families result in propagations of the value false to the remaining options, after one family member has been selected. Given a partial valuation, it is easy to compute by SAT solving which of the remaining options can still be selected, and which must be set to true or false, respectively, as a consequence of previous selections.
We describe these use cases in detail in the following subsections and afterwards consolidate them in an iterative user process. 4.1
Given a product configuration instance (R; F ; S), we can validate the selections with a SAT solver by checking the formula of Definition 2 for satisfiability. Algorithm 1 shows the procedure. Only selections with a priority 6= 0 are taken into account for the validation.
Algorithm 1: Validation & completion of a (partial) selection Input: (R; F ; S) Output: (result; model), where result is true if the (partial) selection is valid, otherwise false and model is a complete variable assignment return SAT
V CNF(R) ^ R2R
V CC(F) ^ F2F
V (s;p)2S;p6=0 s !
Because most SAT solvers take CNF as input, we write CNF(R)
to indicate the transformation of an arbitrary rule to its CNF
representation. In practice we use a polynomial formula
transformation [
If the configuration instance is valid, the algorithm also returns a complete variable assignment. This complete variable assignment gives an example which selections have to be made to complete the given configuration instance. In general, the given model is not uniqe and there exist several models.
Example 2. We reconsider the computer system configuration Example 1. In the following two selection examples, we do not use priorities because we just want to check the validity of the selections. 1. S = fM1; V4g leads to a valid configuration, which can be completed to fM1; V4; C3; P1; CD3; CR2g. 2. S = fM1; C1g leads to an invalid configuration, because M1 requires P1 and C1 requires P2, but due to the family constraints, both cannot be selected at the same time. 4.2
During the configuration process a user would like to know which of the remaining family members are still selectable, i.e. which selections lead to a valid configuration. We can compute the selectable members by validating the (partial) selections with a SAT solver. Algorithm 2 shows the procedure. We iteratively make one SAT call for each member and check if selecting this member is valid. Algorithm 2: Computation of selectable members Input: (R; F ; S) Output: Mapping V from SF2F F to fno; yesg indicating whether a member is selectable or not V Initialize mapping foreiafch m 2 SF2F F do
V CNF(R) ^ R2R
V CC(F) ^ F2F
V (s;p)2S;p6=0 s ^ m ! SAT then
V else
V return V Remarks: (m; yes) (m; no)
After the computation of selectable members, the SAT aided product configurator can display the result to the user (i.e. by disabling all non-selectable members). Then the user knows about the selectable members. 1. In the special case S = ;, in which no selection has been made by the user so far, the computation of the selectable members implicitly brings up members which can never be part of a valid configuration (redundant members) and members which have to be part of each valid configuration (forced members). 2. The performance of Algorithm 2 can be improved. If a family already contains a positively selected member, then we know that all remaining members are not selectable anymore due to the family constraints. We just have to check families with no positively selected member.
The performance can be improved further. We use an incremental and decremental SAT solver, which allows us to load all rules, family constraints and selections first and check each member m by adding and removing the unit clause m from the SAT solver. We do not have to load the invariant constraints repeatedly for each check.
Example 3. We compute the selectable members for our computer system configuration (see Example 1): 1. S = ;: Table 3 shows the remaining selectable members. 2. S = fM1; V4g: Table 4 shows the remaining selectable members.
Selectable Memb.
Non-Selectable Memb. 1. Valid configuration: In the case of a valid configuration, the user can continue selecting members. Additionally, to guide the user we can compute the selectable members for the current configuration. After new selections, the process iterates. 2. Invalid configuration: In the case of an invalid configuration, the user has to take back one or more of the previously made selections. The user can validate each backtracking step again until a valid configuration state is reached.
Remark: If a given complete example model l1 ^ : : : ^ ln in the SAT case does not satisfy the demands of the user, she can exclude this model by adding the hard clause :l1 _ : : : _ :ln. Then another complete model will be produced if one exists, otherwise we encounter the UNSAT case.
In a SAT aided product configuration process described above, the user is left to herself when it comes to the question which selections should be undone to regain a valid configuration. Perhaps the user made a selection of a highly desired member, which she does not want to take back. Now the user has to try different configuration changes by herself and a guidance is missing which one to choose. This is the point where MaxSAT aided product configuration can help. We will describe re-configuration use cases in detail in the following section. 5
In this section we describe how re-configuration can be done with partial (weighted) MaxSAT as a background engine. We show two basic use cases, describe possible variations of them and finally integrate the re-configuration step into our iteractive user process. 5.1
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 of the following:
We have to re-configure either the rules or the selections to regain validity. For now we consider all rules as hard limitations that we can not soften, which is the common case. We will discuss reconfiguration of rules later in Section 5.4.
Considering the rules as a hard restrictions, the question arises, how many of the selections can be kept maximally to reach a valid configuration. Remember, a user may have done multiple selections at once without validating the current configuration and without considering 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 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:
Hard
:= Soft := [ CNF(R) [ [ CC(F) [ R2R
[ (s;p)2S;p6=0;p6=1
F2F fsg
[ (s;p)2S;p=1 fsg Selections with priority 1 are also considered as indispensable and will be encoded as hard unit clauses. Only dispensable selections will be re-configured. Algorithm 3 shows the re-configuration procedure.
With the resulting model, we can give the user an example of a complete selection which requires a minimal number of changes in order to regain a valid configuration compared to the original selections. Or, the other way round, the model gives an example about how to keep the maximal number of selections.
Algorithm 3: Re-Configuration of a (partial) selection Remark: As desribed before we use a transformation like Tseitin or Plaisted-Greenbaum instead of CNF(R) in practice. Even though the Tseitin and Plaisted-Greenbaum transformations are only equisatisfiable, this is not an issue for MaxSAT when converting formulas into hard clauses. Since the Tseitin and Plaisted-Greenbaum transformations share the same models on the original variables, one can easily verify that the search space between the converted and the original instance remains the same.
Extensions:
The described use case can be extended as follows: 1. User constraints: A user can add additional constraints considered as hard clauses.
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 rules (M1 ! V2) ^ (M2 ! V5) as constraints to the rules R. 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 selected members within a family will be considered during the re-configuration computation.
E.g. if a user focuses on mainboards M1; M3; M4, a hard clause (M1 _ M3 _ M4) will be added to the rules R.
Example 4. We continue our canonical Example 1: Table 5 shows multiple selections of members within families and a result model re-configuration. For all selections shown we choose priority 1, that means no selection in this example is an indispensable one.
In the previous use case we treated all soft clauses as equivalent. A user may prefer one member over the other, which results in priorization of the selected members. We can handle priorities with Partial Weighted MaxSAT solving. The encoding for this use case is basically the same as before, but now we bring priorities into play. Algorithm 4 shows the complete computation procedure. Algorithm 4: Re-Configuration of a (partial) selection with priorities Input: (R; F ; S) Output: (optimum; model), where optimum is the minimal number of priority points to change to regain a valid configuration and model is a model for the optimum
foreach R 2 R do
foreach F 2 F do
else Result: We have to make 5 changes minimally to regain a valid configuration. Without the focus set for the video cards family V , we We reconsider the process of Figure 1 in Step 3a. UNSAT where the 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 which selections have to be undone to regain a valid configuration. But now, we can help the user at this point by using re-configuration with MaxSAT. Figure 2 illustrates both Use Cases 5.1 and 5.2 embedded in a product configuration process using MaxSAT.
User
3a. No solutio n 1. Re-configurate 1. No solution: If the indispensable selections (with priority 1) collide with the rules or the family constraints, then there is no solution. In this case, the user has to weaken some of the indispensable selections in order to make a re-configuration possible. The user can use high priorities to weaken the desired members to ensure they will be preferred over other selections. 2. Solution: If the indispensable selections can be satisfied, then there exists a solution with an optimum for the prioritized selections. In this case, the user will be told about the optimum, i.e. about the number of minimal changes to regain a valid configuration. Also, an example model with the optimum will be given to the user.
Remark: Similiar to the SAT aided configuration process the following holds: If the given complete example model l1 ^ : : : ^ ln in the solution case does not satisfy the demands of the user, she can exclude this model by adding the hard clause :l1 _ : : : _ :ln. Then another model with the same optimum will be produced, if one exists. If there is no other model with the same optimum, the next best optimum under the new conditions will be computed with an example model.
In case there is no solution and a user just do not want to weaken her selections with priority 1, we can consider weakening the rules. In the next section, we will describe this possibility in detail. 5.4
It is possible that the selections a user made have no solution when trying to re-configure them. Assuming the rules themselves are not contradictory, then the cause for no solution are too many selections with priority 1. There are two cases which can occur or both at the same time: 1. Violation of the family constraints: If a user selects more than one member of a family with infinity priority, the family constraints are violated. 2. Violation of rules: If a user does not violate the family constraints, then the selected members with priority infinity are in collision with the rules.
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, we can not re-configure the selections w.r.t. the rules. But when we 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 restriction, but only exists for marketing or similiar purposes. A company may be willing to violate or change some of these rules to build the product. Knowing the miminum number of rule changes in order to permit a desired vehicle configuration can help in managing the set of marketing rules.
For this use case, we extend Definition 1 by an additional mapping SR : R ! (N 0 [ f1g), which represents the priorities of the rules a user made. After softening some of the rules this way we can 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.
Algorithm 5: Re-Configuration of rules else else
foreach F 2 F do
foreach R 2 R ^ SR(R) 6= 0 do if p = 1 then
Since a rule R is an arbitrary formula, we can not just convert
R to its CNF and add the resulting clauses as soft clauses. In
general, 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
a group MaxSAT problem [
The group MaxSAT problem can be reduced to a partial MaxSAT
problem as follows: For each non-indispensable rule R we introduce
a new variable bR and add the hard clauses CNF(bR ! R).
Additionally we add a unit soft clause fbRg for each new variable. Each
satisfied variable bR implies the whole group of clauses in CNF(R)
to be satisfied. Therefore, satisfying a maximal number of the newly
introduced variables satisfies a maximal number of the corresponding
formulas. On the other hand, with the help of the newly introduced
variables, we can identify, from the resulting model, which
formulas are satisfied and show this result to the user. For a more detailed
explanation, see [
Extension: Of course, rules can also have different priorities and we can extend this use case by assigning priorities to rules and selections to compute the maximal sum of priority points. This extension can be realized analogously as described for Use Case 5.2, thus we will not describe it explicitly. 6
We implemented the above SAT-based and MaxSAT-based use cases
in one product configurator — called ReMax — on top of our
uniform logic framework, which we use for commercial applications
within the context of automotive configuration. Our SAT solver
provides an incremental and decremental interface. We maintain two
versions (Java and .NET) and decided to implement ReMax using
.NET 4.0 with C# along with the WPF Framework for the GUI.
We implemented state-of-the-art partial (weighted) MaxSAT solvers
Fu&Malik, PM2 and WPM1 on top of our SAT solver [
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 [
We implemented WPM1 on top of our own SAT solver while msu4 is an external solver3.
Our environment for the benchmarks has the following hardware and software settings. Processor: Intel Core i7-3520M, 2,90 GHz; Main memory: 8 GB. WPM1, based on .NET 4.0, runs under Windows 7 while msu4 runs under Ubuntu 12.04.
For Use Case 5.2 we created three categories as follows: Out of 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 seconds. The abbreviation “exc.” means that the time limit of 30 minutes was exceeded. As we can see, msu4 performs very well in all categories 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.
Problem M01_01 M01_02 M01_03 M02_01 M02_02 30%
50% WPM1 msu4
WPM1 msu4
70%
WPM1
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 with infinity priority, which leads to an invalid configuration in general 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 seconds. As we can see, both solvers can handle all instances in each category in reasonable time. While WPM1 takes from about 3 seconds up to about 72 seconds, the external solver msu4 takes from less than one second up to about 9 seconds in the worst case. 3 http://logos.ucd.ie/web/doku.php?id=msuncore WPM1 msu4 8
Another approach for re-configuration uses answer set programming
(ASP) on a decidable fragment of first-order logic [
An algorithm for computing minimal diagnoses using a conflict
detection algorithm is introduced in [
The indicated idea above is further improved in [
We did not consider works dealing with explanations like MUS (Minimal Unsatisifable Subset) iteration. When using MUS iteration for re-configuration, a user not only has to manually solve each conflict, but also will not necessarily solve the conflicts in an optimal manner, i.e. only changing a minimal number of selections. 9
We described product configuration for propositional logic based rule sets which are widely used in the automotive industry. We showed applications of SAT solving by two use cases. Furthermore, we showed use cases of how MaxSAT can be used for product configuration when it comes to an invalid configuration. With MaxSAT we are able to re-configure an invalid configuration in an optimal way, i.e. we can compute the minimal number of necessary changes. We embedded both scenarios in configuration processes showing how a user can be guided during the configuration process.
We presented an implementation of a product configurator — ReMax — supporting all of the described use cases using state-of-theart SAT and MaxSAT solving techniques. From real automotive configuration data from two different German premium car manufacturers we created synthetic product configuration benchmarks for the presented use cases. Besides our own MaxSAT solver we used the external solver msu4 to measure and compare the performance. As our experimental results show, we can re-configure those problem instances in reasonable time. Since some problem instances could be solved within a few seconds, our product configurator could be used as an interactive tool in these cases. Other problem instances took over a minute in the worst case, but is still more than adequate for a responsive batch service. While this may seem long, we were told that the manual configuration of an order without tool support by a trial and error process may well take on the order of half an hour.
We do not claim that our approach is currently fit for use as a consumer configurator. However, many business units of a car manufacturer, such as engineering or after sales are in need of a (re-)configurator that feeds directly off the engineering product documentation. E.g., many test prototypes must be built before start of production with a varying set of options.
Expert users sometimes need some complete car configurations which cover all valid combinations of a subset of options, e.g. for testing purposes. With a SAT based (re-)configurator, an expert user can start the configuration from the desired options instead of tediously following the given configuration process in a usual sales 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.