SAT solvers have proved to be very efficient in verifying the correctness of automotive product documentations. However, in many applications a car configuration has to be optimized with respect to a given objective function prioritizing the selectable product components. Typical applications include the generation of predictive configurations for production planning and the reconfiguration of non-constructible customer orders. So far, the successful application of core guided MaxSAT solvers and ILP-based solvers like CPLEX have been described in literature. In this paper, we consider the linear search performed by DPLL-based PBO solvers as a third solution approach. The aim is to understand the capabilities of each of the three approaches and to identify the most suitable approach for different application cases. Therefore we investigate real-world benchmarks which we derived from the product description of a major German premium car manufacturer. Results show that under certain circumstances DPLL-based PBO solvers are clearly the better alternative to the two other approaches.
An already well-established approach in the automotive industry is
to describe the set M of technically feasible vehicle configurations
by a propositional formula ' such that M = f j (') = 1g holds,
where is a satisfying assignment of formula ' [
In the literature of the last few years different applications of this
optimization problem are described as well as several approaches to
solve it. Similar optimization problems arise for example from the
task to minimize or maximize product properties such as price or
weight [
This work is organized as follows: Section 2 introduces the basics of Propositional Logic, Maximum Satisfiability (MaxSAT), PseudoBoolean Optimization (PBO) and Integer Linear Programming (ILP) and their respective algorithmic solving techniques. Section 3 points out related work. Section 4 describes different optimization problems in automotive configuration. Section 5 presents a detailed evaluation of the different introduced optimization approaches for these problems including a discussion of the results. Finally, Section 6 concludes this work. 2
In this work, we focus on propositional logic with the standard
logical operators :; ^; _; !; $ over the set of Boolean variables X and
with the constants ? and >, representing false and true, respectively.
The set of variables of a formula ' is denoted by var('). A formula
' is called satisfiable, if and only if there is an assignment , a
mapping from the set of Boolean variables var(') to f0; 1g, under which
the formula ' evaluates to 1. The evaluation of a formula under an
assignment is the standard evaluation procedure for propositional
logic, denoted by ('). The values 0 and 1 are also referred to as
false and true. The well-known NP-complete SAT problem asks the
question whether a formula is satisfiable or not [
The established input format of a SAT solver nowadays is a
conjunctive normal form (CNF) of a formula ', where ' is transformed
into a conjunction of clauses and each clause is a disjunction of
literals (variables or negated variables). The variable of a literal l is
denoted by var(l). For a formula ' = Vik=1 Wjm=i1 li;j in CNF we also
make use of the notation of ' as a set of clauses where each clause
is a set of literals: ' = ffl1;1; : : : ; l1;m1 g; : : : ; flk;1; : : : ; lk;mk gg.
The transformation of an arbitrary formula ' into a CNF is done by a
Tseitin- or Plaisted-Greenbaum-Transformation [
For a given clause set ' = fc1; : : : ; cmg, m 2 N, the MaxSAT
problem [
X i=1 MaxSAT(') = max (ci) 2 f0; 1gjvar(')j ) (1)
The corresponding problem of finding the minimum number of clauses which can be simultaneously unsatisfied is called MinUNSAT.
The partial weighted MaxSAT problem is an extended version where: (i) An additional clause set 'hard of hard clauses is taken into account, which has to be satisfied, and (ii) weights wi 2 N are assigned to the soft clauses of ' = fc1; : : : ; cmg. The resulting problem, PWMaxSAT('hard; '), consists of finding the maximal sum of weights of satisfied clauses of ' while satisfying 'hard. To simplify reading we refer to partial weighted MaxSAT just as MaxSAT in the rest of this work.
MaxSAT can be solved by using a SAT solver as a black box,
e.g. by linear search or binary search. Firstly, a fresh variable bi,
called blocking variable, is added to each soft clause, which serves
to enable or disable the clause. Linear search iteratively checks the
SAT instance 'hard and ' with an additional constraint
CNF
m !
X wi :bi > k ;
where initially k = 0. With this check we search for a model with a
sum of weights of at least 1. The constraint Pim=1 wi :bi > k is
a Pseudo-Boolean constraint (see Subsection 2.2 for details), which
can be transformed to a CNF, see for example [
Another approach is the usage of unsatisfiable cores delivered by a
SAT solver for the unsatisfiable case, which was introduced in [
The OPEN-WBO framework [
In addition to clauses we consider linear pseudo-Boolean (LPB) constraints, which are linear inequalities of the form k X aili . b; i=1
Pseudo-Boolean solving (PBS) is the decision problem whether a set of LPB constraints can be satisfied by an assignment . Hence, PBS is a generalization of SAT. Like SAT solvers, most PBS solvers which prove satisfiability are able to provide a satisfying assignment to the user.
Given a satisfiable set of LPB constraints another problem is to identify a best possible assignment with respect to a linear objective function: s.t.
min
V j
Pi aj;ilj;i . bj
This problem is called pseudo-Boolean optimization (PBO) [
In order to solve the satisifiability problem PBS, DPLL-style algorithms can be used to benefit from recent progress of modern SAT solvers. One approach is to transform the LPB-constraints into CNF and to apply SAT solvers to the resulting formula. Another approach is based on generalized constraint propagation and conflict-based learning, i. e. DPLL-based SAT solvers are enabled to handle LPB constraints directly. Generally learning methods analyze the conflict and learn a new constraint which is falsified on the conflict level and which propagates a new assignment on a higher decision level.
Given a PBS solver, the PBO problem of Formula (4) itself can be solved by iteratively applying the solver to perform a linear search or a binary search. Both approaches proceed analogously to the linear and binary search approaches for MaxSAT using a SAT solver.
In the linear search approach, models of the formula ' are calculated in order to gradually approach the optimal objective value. Through an extra LPB constraint, a model providing a better objective value is enforced. If the extra LPB constraint leads to an unsatisfiable PBS instance, the model last calculated is the optimal one.
In the binary search approach the search space is bisected by every single PBS-instance. If the optimal objective value lies inside the interval [L; U ], a model with the objective value M = (L + U )=2 is searched for. If such a model exists, the minimal objective value lies inside [L; M ]. If no such model exists, the minimal objective value lies inside [M; U ].
For the calculations in Section 5 we used the Sat4j library. The library is based on a Java version of MiniSat, which was expanded by generalized constraint propagation and conflict-based learning. The PBO solver contained therein realizes a simple linear search. The PBS solver called for this linear search is able to perform the following two learning methods.
The clause-based learning method calculates so-called UIPs (unique implications points) by means of propositional resolution just like in modern SAT solvers. SAT solvers such as MiniSat derive a UIP on the basis of the conflict clause and the reason clauses which were propagating the assignments of the conflict clause. If a conflict constraint occurs in the form of a LPB constraint, Sat4j first reduces this constraint to a conflict clause
K =
_ l2!C ; (l)=0 l; where is the partial assignment, that leads to the conflict in the LPB constraint !C . Analogously, reasons given by LPB constraints are reduced to reason clauses: If ! is a LPB constraint, that propagates ~l under the partial assignment , the clause
R(~l) =
_ (4) (5) (6) is an implication of ! and also propagates the literal ~lunder .
In a second learning method that is implemented in Sat4j more
expressive LPB constraints instead of clauses are learned. For this
purpose the principle of propositional resolutions in forms of
Hookers cutting planes [
Like linear programming, integer linear programming deals with the optimization of linear objective functions over a set which is limited by linear equations and inequations. The difference is that while in linear optimizations any real values can be taken on, in integer optimization some or all variables are restricted to whole-number values. (7) s.t.
min
Pseudo-Boolean Optimization, see Formula (4), can be easily
transformed into 0-1 integer linear programming (ILP): Negative
literals :x are replaced by (1 x) and Boolean variables become
decision variables x 2 f0; 1g. Consequently, commercially available
state-of-the-art ILP solvers such as CPLEX [
Sinz et al. suggest a SAT-based procedure to check consistency of the
product documentation of a German car manufacturer [
Tilak Singh et al. make use of such a product overview formula
in [
Walter et al. [
The product overview defines the set of valid product configurations 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 configuration is determined by the bill of materials (BOM). The combination of the product overview and the bill of material is referred to as the product documentation.
Reconfiguration of invalid configurations, as described in [
Another major task is the prognosis of future part demands in production planning. However, historical demands cannot easily be extrapolated because planning situations in the automotive industry are constantly changing. A typical planning state used for making a forecast comprises the product documentation (option A is only available, if option B is selected; part x is needed exactly iff the order satisfies the part rule 'x; etc.), estimated customer buying behavior (option C is selected by 30% of the customers; etc.), capacity restrictions (only 5000 units of part X are available; etc.), production plans that fix the total number of planned vehicles. From a mathematical point of view a planning state consists of two parts: 1. The Boolean formula POF, whose models describe the technically feasible configurations, 2. the statistical frequency of certain atoms of the product formula. A common approach to evaluate the planning state is to calculate an amount of N technically feasible variations that approximates the statistical guidelines as good as possible. Eventually, for indicating the future unit demand, the calculated variations are analyzed by means of the BOM.
Singh et al. [
In column generation, calculated configurations of previous iterations are partially replaced by new configurations. Thus, solved PBO instances do not necessarily result in a configuration also contained in the final solution. Therefore, it is particularly important to ensure an efficient calculation of the individual PBO instances. 4 tiu 3 m m eop th 2 ceano t ts 1 i d 0 150 liseab rav100 l aud reo -zn 50 o n #
0 0 100
200 #iterations 300 0 100
300 200 #iterations
The typical approximation to the planning state when using column generation is shown in Figure 1. As one can see on the left side, the majority of iterations is used to overcome the last small step towards the optimum. Yet, illustrated by the graph on the right side, approximation is accompanied by increasingly complex target functions of the PBO instances: the number of non-zero dual variables is increasing. It must be noted that the maximum number of non-zero dual variables is usually proportional to the number of statistical requirements of the planning state.
Concerning implementations of column generation described in
the literature, integer linear programming is the method of choice
for producing columns. This approach is also taken in [
In this section we present our main contribution by evaluating the different previously described methods on optimization problems from automotive configuration.
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. 5.1
We evaluate several test series, each of which is composed of a real-world product overview and of randomly generated linear objective functions. We looked at product overviews of two different Type A B
Fixed Attributes market, model, body type, engine, steering type market, model, body type #Clauses 1200-5900 types, see A and B in Table 1. Both types of product overviews differ in the extent to which attributes are fixed. Additionally, Table 1 shows the minimum and maximum number of clauses for the product overviews of one type. For generating objective functions, n variables were randomly selected (by using Java’s Random class with the default constructor) and each was assigned to a random integer coefficient 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 total of 200 PBO instances. Corresponding test series were generated for 13 different product overviews of type A and for 6 different product overviews of type B. 5.2
The test series from the previous section were solved by 3 solvers:
1. OPENWBO as a core guided MaxSat solver [
For solving the PBO instances a timeout of 60 seconds was set. In order to set up the linear search correctly, two different learning methods 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 Cutting Planes
Clauses 50 100 150 #variables in the objective function 200 depending on the complexity of the objective function. Based on these results, Sat4j was limited to learning clauses when comparing the 3 solvers.
product overview with 133700 clauses
In Figure 3 the running times of OPENWBO, Sat4j and CPLEX are compared. The upper graph shows the average running times of the test series of type A concerning objective functions of different complexity. Accordingly the bottom graph displays the results 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, the DPLL-based solvers OPENWBO and Sat4j perform significantly better than CPLEX with regard to objective functions of low complexity. In test series of type A the solver Sat4j performs better than CPLEX concerning objective functions of up to N = 170 variables. s n o i t a tr e i # e g a r e v a 15 10 5 0
Sat4j
OPENWBO 0 50 100 150
200 The MaxSAT solver OPENWBO, however, produces reliable running times for up to N = 70 variables.
In contrast to the DPLL-based solvers, there was only a slight increase 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 however, OPENWBO leads to slower running times for objective functions of only N = 30 variables. This observation is especially illustrated by the most extensive product overview of type B (137700 clauses) as demonstrated in Figure 4, where the time-domain is restricted to 3400 ms.
Timeouts were observed exclusively for the MaxSAT solver OPENWBO. Complementary to the results of running times, Figure 5 shows the average number of timeouts when solving 10 instances.
For a better understanding of the observed difference in running times of both DPLL-based approaches, Figure 6 shows the average number of DPLL-calls. The graphs refer exclusively to the test series of type A and represent the numbers of SAT/UNSAT-calls for OPENWBO or, in case of Sat4j, the numbers of PBS-calls. 5.3
The test instances described in Section 5.1 differ with respect to the following aspects: the complexity of the objective function (number of variables N = 10; 20; : : : ; 200) the size of the product overview (number of models and number of clauses; type A and B) The findings of the previous section lead us to the following conclusions:
Using DPLL allows the quick calculation of a model of a formula - in that way DPLL-based solvers are superior to ILP solvers. Yet, when objective functions become more and more complex, the particular suitability of CPLEX in solving 0-1-optimization problems dominates. The latter point is evident in the strong increase of running times for the DPLL-based methods once a certain length of objective functions has been reached.
In comparison with OPENWBO, Sat4j leads to significantly better running times. This is also due to the special suitability of the examined instances for a linear search (see Figure 6). The number of iterations for a linear search increases only linearly with the numbers of variables in the objective function - this is a surprising result. Hence, the nonlinear increase of running times can only be explained by the growing complexity of PBS instances in linear search.
Concerning product overviews of type A, the critical length of the objective function for Sat4j is between N = 160 and N = 200. With increasing scale of the product overview, this critical value shifts upwards. In some cases of the product overviews of type B, the critical value is greater than N = 200, such as seen in Figure 4.
In order to optimally configure customer orders, an optimal subset of about 20 options has to be determined. For this purpose the linear search implemented in Sat4j and the core guided MaxSAT solver OPENWBO are more than sufficient.
For calculating predictive configurations for the product planning
(see Figure 1) Sat4j can be far more effective than the other tested
methods, at least for the first iterations of a column generation based
process. Yet it is possible that the critical area of linear search is
reached depending on the given number of statistical requirements in
the planning state. In such a case configurations should be calculated
by CPLEX just like in [
We compared current state-of-the-art solvers to calculate optimal product configurations of a major German car manufacturer. So far, the use of core guided MaxSAT solvers and ILP solvers like CPLEX for PBO-instances of automotive industry was described in the literature. For the purpose of comparison we additionally applied a DPLLbased linear search.
Results were analyzed with respect to the granularity of the product overview and with respect to complexity of the objective functions. The results show that the investigated approaches have different suitability for different application cases. For reconfiguration the linear search performed by a PBS-Solver is a stronger alternative compared to core guided MaxSAT. For calculating predictive configurations – up to a certain amount of given frequency restrictions – the DPLL-based linear search is even more suitable than CPLEX.
An important result is the small number of iterations observed in linear search. The approach of linear search thus appears to be especially suitable for PBO-instances whose constraints are given by a product overview. For reliable usage of the DPLL-based linear search, also for instances of long objective functions, a customized PBS solver needs to be developed. Such a solver must be able to more efficiently solve PBS instances that are characterized by a set of product overview clauses and one extensive LPB constraint. 72