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