This paper presents an evaluation of decision heuristics of solvers of the Boolean satisfiability problem (SAT) in the context of constraint-based product configuration. In product configuration, variable assignments are searched in real-time, based on interactively formulated user requirements. Operating on user's successive input poses new requirements, such as low-latency interactivity as well as deterministic and minimal implicit product changes. This work presents a performance evaluation of several heuristics from the SAT literature along with new variants that address the special real-time requirements of incremental product configuration. Our results show that the execution time on an industrial benchmark can be significantly improved with our new heuristic.
customized and personalized products rises in
manufacturing and service industries, which previously only
utilized the advantages of mass production to ofer
standardized products for a good value. Shaped by Stanley
Davis and his 1987 book Future Perfect [
© 2023 Copyright for this paper by its authors. Use permitted under Creative Commons License the time of the SAT solving therefore plays an essential role for interactive, low-latency product configuration. evaluation is done with the product configurator Merlin
Luckily, many SAT formulas that model real world CPQ by the CAS Software AG . Merlin has a specialized
problems can be solved quickly thanks to the classic DPLL solving process of incremental problems from
interacalgorithm [
The area of product configuration tends to place difer- configuration benchmarks and specifically focus our efent demands on a solver than the classical SAT formulas. forts on speeding up the more complex to solve problems The process of incremental product configuration gener- to enable fluid and user-friendly configuration of the deally leads to less complex computations, since we solve sired product, even in these taxing cases. Experimental many simple formulas and not just one complex formula. results show that the performance of the especially ex
New challenges arise when the last user requirement pensive benchmarks is roughly doubled by the best of cannot be met with a previously selected configuration. the presented branching heuristics. The possibility of stating conflicting requirements is in- Interactive product configuration is a unique domain, tentional, as the user may not be aware of all the interac- so general-purpose heuristics do not necessarily achieve tions between diferent requirements, or may be in the the best performance here. In this paper, we introprocess of making fundamental changes. In either case, duce new branching heuristics that achieve better perforthe user relies on feedback from the configurator, and it is mance in the domain of interactive product configuration the solver’s job to calculate a new valid product configu- than the well-known top dogs for more general-purpose ration. This amounts to solving an optimization problem benchmarks. It remains to be seen, how the heuristics where the new configuration contains as few changes evaluated in this paper behave in other benchmark doas possible while omitting as few user requirements as mains. possible. To realize this idea, the configurator weights the user’s requirements so that changes are associated 1.3. Related Work with costs.
Furthermore, not only a single optimal solution is of interest but every solution with the smallest cost or within a certain delta. So the user is able to select one of the best iftting alternatives. The optimization problem can be realized as a minimum-cost satisfiability (MinCostSAT) problem or an equivalent maximum satisfiability (MaxSAT) problem. Nevertheless, the additional challenges posed by product configuration also present new opportunities to derive better heuristics for this specific use case.
Most modern satisfiability solvers are based on the highly
influential foundation of Davis and Putnam [
Reductions to SAT are also well known in the context
of product configuration [
The most dominant decision heuristic in SAT solving of the last century is probably Dynamic Largest Individual Sum (DLIS) [20] found in GRASP, the algorithm that revolutionized DPLL and gave birth to the new solving paradigm Conflict-driven Clause Learning (CDCL).
The predominant decision heuristic in CDCL solvers in
the last two decades has been Variable State
Independent Decaying Sum (VSIDS) which was first presented
in Chaf [
Nevertheless, decision heuristics for CDCL are a vital research area [21]. Application-specific specialized
This paper lays the focal point on the goal of reaching an as optimal as possible performance of decision heuristics for SAT in the context of incremental product configuration with weighted user requirements as described in the previous section. We implemented four decision heuristics under the additional requirement of deterministic user experience, i.e., the configurator keeps producing the same results. So a user receives the same selection of alternative configurations for every repetition of a specific interactive configuration sequence. The performance of various known branching heuristics from SAT solving as well as new heuristic ideas are evaluated in the product configuration context. We examine how the diferent sub-formula types and literal types can be exploited efectively in these heuristics.
The implementation of the heuristics and the following heuristics are evaluated regularly [22, 23, 24]. Recently, one or more literals. A literal is either a Boolean variable approaches based on reinforcement learning have been (positive literal) or the negation of a variable (negative successfully used to select heuristics dynamically [25, 26]. literal). In contrast to CNF formulas, a formula in dis
Eforts to develop specialized heuristics for product junctive normal form (DNF) if it is a disjunction of terms, configuration were made in [ 27] by applying graph analy- where a term is a conjunction of literals. sis to propositional formulas in Merlin CPQ. Nevertheless, The Merlin product configurator supports formulas the resulting heuristic based on coreness is not adaptively constructed as conjunctions of both types of normal reacting to conflicts that will often appear in DPLL and forms, CNF and DNF formulas, as well as at-most-one thus could not dethrone VSIDS, which still is Merlin’s (AMO) constraints over sets of literals. An AMO constandard heuristic. straint evaluates to true if and only if at most one of its literals is true. There are several ways to encode this 1.4. Overview constraint in propositional logic but further details are unimportant for this paper.
tions covering propositional logic as well as SAT and 2.2. Propositional Satisfiability MaxSAT solving in the context of incremental product configuration. In Chapter 3, we explain the ideas and mo- The satisfiability (SAT) problem asks the question tivations behind the branching heuristics under consider- whether it is possible to find a complete variable assignation. The implementation in Merlin CPQ is described in ment that interprets a given formula to true (satisfiable) Chapter 4. Subsequently, Chapter 5 presents the results or declares this impossible (unsatisfiable). A SAT solver of our performance evaluation of the presented heuris- can be used to answer such problem instances. We can adtics. Lastly, we provide a summary and our perspective ditionally call a propositional formula valid if it evaluates on potential future work in Chapter 6. to true for every possible assignment.
The easiest way to determine satisfiability is achieved by creating a truth table for the whole formula and check 2. Theoretical Preliminaries whether any resulting value is true. The issue is the efort of this procedure, which grows exponentially with the number of variables.
to represent values of ”true” and ”false”. Propositional formulas are built from Boolean variables and operators such as negation, conjunction, and disjunction.
These operators are interpreted with respect to the usual semantics, i.e., the negation of an argument is true if and only if the argument is false, the conjunction of a set of arguments is true if and only if all arguments are true, and the disjunction of a set of arguments is false if and only if all arguments are false.
A variable assignment maps all Boolean variables of a formula to Boolean constants. The truth value of a formula under a given assignment is determined by replacing the variables with Boolean constants accordingly and by successively interpreting the truth value of all sub-formulas according to the operator semantics. 2.1.1. Normal Forms and Clause Types
conjunctive normal form (CNF). A CNF formula is a conjunction of clauses. Each clause itself is a disjunction of 2.2.1. DPLL Algorithm
partial assignment is successively collected for a given CNF formula by adding literals during its search procedure. The assigned variables are then used to simplify the original formula.
Central to DPLL is unit propagation. If the CNF contains a unit clause (a clauses that consist of only a single literal), then the clause’s literal is immediately used to extend the current partial assignment. All further clauses where this literal occurs can then be dropped from the formula because they are satisfied by the assignment.
Furthermore, the negation of the literal is removed from all clauses in which it occurs and we call clauses where this happens ”touched” (this will be important later). The propagation stops when no more unit clauses are present.
Afterwards, one of three states is reached. If no clause remains, the instance is satisfiable and the algorithm returns a satisfying assignment. If an empty clause emerges, i.e., all literals in that clause are falsified, the instance is unsatisfied under the current partial assignment.
This means that decisions have to be undone (backtracking) and if no decision can be undone the instance is unsatisfiable. Otherwise, we need to heuristically pick a decision variable which we use to extend the current partial assignment. Two recursive calls have to be made search is interrupted and always greedily continued at now; the variable is assigned true in one branch and false another branch that sits on the path of minimal cost. A in the other. relaxed version with a reduced memory consumption
This algorithm covers all possible branches in the is the beam search. Instead of potentially exploring all worst case, which makes it sound and complete but also promising branches, only a maximum number of the not better than the naive approach regarding this aspect. cost-optimized children (defined by the beam width) are However, the performance on real world problems is com- considered. monly clearly superior to the worst-case performance due to unit propagation and further techniques.
2.2.2. Clause Learning
A major improvement made to DPLL-based solvers is computationally hard. Nonetheless, DPLL in
combinahas been the concept of conflict-driven clause learning tion with good heuristics can often eficiently solve many
(CDCL), first shown in the GRASP solver [
The distance heuristic pursues a promising approach While the previously described heuristics increase the as described in [31]. This branching heuristic is based scores of variables that appear in reason clauses or on counters like VSIDS and also makes use of decaying. learned clauses, we thought that in our context we could However, the score increment dynamically takes into try something that is much simpler. The conflict heuristic account an estimate of how much a variables contributes is our own variant of VSIDS, where we simply increase to the conflicting assignment under analysis. This is done the scores of variables in the conflicting clause. The by taking into account the position of the variables in intuition behind this procedure is that such variable asthe implication graph that is commonly used in CDCL signments should be fixed as quickly as possible, ideally for analyzing the reasons for a conflicting assignment. to satisfy as many unsatisfied clauses as possible.
An implication graph is a directed acyclic graph. Each
node in the implication graph either represents a clause 3.4. Heuristics based on Pure Literals
that triggered an assignment during unit propagation
(including the empty clause which triggered the conflict Pure literals were already used in the original algorithm
under analysis) or a decision literal. In the implication of Davis and Putnam in the afirmative-negative rule [
The authors hypothesize that the fewer clauses a vari- cation procedure. This is due to the advent of eficient able depends on during the conflict, the higher the prob- data structures for unit propagation which are commonly ability that the variable contributes to a later conflict. used in modern SAT solvers.
Unfortunately, realizing this dependence hypothesis ex- Merlin uses diferent data structures for unit propactly would be too computationally intensive. The dis- agation, primarily due to the additional requirements tance heuristic is an approximation to this idea, in that imposed by incremental user interaction, which requires it determines the number of vertices that are located on the ability to correct assignments deterministically and the longest path in the implication graph from the node non-chronologically. But the non-chronological correcrepresenting the reason of a variable’s assignment to the tion of assignments is also detrimental to the applicability node representing the conflicting clause. of the pure literal rule. At any point in time, a user could
The distance heuristic scores literals diferently de- select a property such that a previously pure literal is no pending on their responsibility for the conflict in con- longer pure. This would not be possible in classical SAT trast to the constant increment of VSIDS. This heuristic solving, where a pure literal appearing under a particular aims to be more precise because of the more elaborate variable assignment remains a pure literal at least for scoring, especially during the beginning of the search all branches below it. However, assigning a pure literal where only few conflicts occurred and none of the deci- explicitly by a branching decision is a valid option. sion heuristics is suficiently initialized yet. However, the authors of the distance heuristic point to the computa- 3.4.1. Pure Literal Heuristic tional overhead of their heuristic as compared to VSIDS.
In their empirical evaluation, they found that it is bet- A first idea for a decision heuristic that utilizes this conter to switch from the distance heuristic to VSIDS after cept can thus try to select pure literals whenever possible 50,000 conflicts. This seems especially fitting for product and thus add them to the partial truth assignment. If configuration because the focus on interactivity means there are no pure literals available, then the remaining that the targeted problems are typically faster to solve variables are handled afterwards with a diferent strategy. compared to some large SAT instances running several In the basic variant this is done by a fixed initial ordering. minutes and resolving tens of thousands of conflicts. 3.4.2. Pure Literal Phase
though be combined with other heuristics as well, where those heuristics proceed instead of the random ordering. Additionally, preferring pure literals can be done in certain phases. So pure literals could only be preferred after a certain amount of conflicts or decisions, up to a certain amount, within a range, or by having alternating phases of favoring pure literals and just the basic heuristic. 3.4.3. State Dependent Pure Literals
and a few other heuristics. In this section we discuss implementation details of VSIDS, CBH and CBH Simplified.
als up-to-date during run time for potential improvement. VSIDS is already part of Merlin and the default heuristic. A heuristic can remember so-called ”almost” pure literals, The concrete realization of VSIDS is quite diferent from which we see as variables that are mostly present in one the ones used in of-the-shelf SAT solvers. One diference polarity, while the other polarity is rare. For every al- is that Merlin initially selects variable’s based on their most pure literal, the configurator also stores the clauses individual occurrence counts in the formula. This is in preventing the literal from being completely pure. If all contrast to most implementations which initialize scores the clauses related to an almost pure literal are marked with zero (cf. CaDiCaL [33], or MiniSat [30]) The variable deleted during unit propagation, then this literal is being occurrence counts and the VSIDS score of a variable are added to the set of pure literals. This would thus increase kept separately. The sum of both scores is then used to the amount of available pure literals. determine the final score used with decisions. During conflict analysis, the VSIDS scores are incre3.4.4. Pureness Variant mented by a bump value which is initially set to 100. The purpose of VSIDS decay is to make previously bumped variables less important over time. In Merlin, this is realized by increasing the bump value over time. Every 15 conflicts the bump value is increased by two percent.
Pureness of literals is another variant of pure literals. The amount of positive versus negative literals of each variable determines a pureness percentage. Variables with a balanced share of positive and negative appearances lead to a low pureness, almost pure literals get a high pureness percentage, and fully pure literals would be 100 percent. The decision heuristic then picks the literal with highest pureness score. Again, diferent heuristics can be used as combination, either as tie breaker or to set multiple scores of against each other.
as it is described in [32] would not suit Merlin’s heuristics, who have to make their decision based on the given set of candidate literals. Therefore, we do not explicitly manage a global clause-list as it is done in the original CBH. 3.5. Clause-Based Heuristic Only initially, a list based on all clauses is created with For the clause-based heuristic (CBH), all clauses are kept the ordering described by the CBH authors. Hereby, we in an ordered list and decision literals are picked from the go through the original set of all clauses and remember top-most unsatisfied clauses in that list according to [ 32]. for each unique literal, in which clauses it was contained. To create an initial ordering of clauses, the priority of a Then we create a new list with every variable, which is clause is calculated based on the number of occurrences sorted regarding the variables’ score based on the counof the literals it contains. To increase the proximity of ters of the variable’s two literals. The paper would now clauses that have literals in common, the ordered list is put the clauses containing the highest scoring variable gradually populated by starting with the clause with the into the clause list, however, we assign a priority to the highest priority and then first increasing the priorities of literals depending on their supposed position in this list all clauses that have literals in common with the clause instead of explicitly storing the clause list for later usage. just added. This process is repeated until all clauses are So in the first step, the highest scoring variable and all added to the list. The ordered list is then update on variables that share a clause with it receive priority -1. each conflict by moving the conflicting clause and the Each variable has two additional local literal counters reason clauses to the front. For the decision heuristic to which get increased for every occurrence of its respective select a literal from the top-most unsatified clauses, each literal as part of a clause added to the clause list. Thereliteral has additional counters to measure its contribution fore, we also increase this local score when setting the to (recent) conflicts, while larger scores are preferred. priority. The priority is afterwards decreased by one for Further details can be found in [32]. the next bunch of clauses. This procedure now continues until every variable was selected, while the local score is always added to the variable’s score.
Updates due to a conflict can then be realized by calculating the conflict responsible clauses. Each literal of [s2te0p0s0] CBH simplified these clauses receives a new priority (starting at zero) Conflict with pure literal phCaBsHe that is one higher than the previous highest priority. This VSIDS procedure is equal to moving clauses to the topmost po- 1500 sition of a clause list. Additionally, these literals get a bump to their conflict counter. The same then happens 1000 to the actual conflict clause with the next priority value.
Choosing a literal can then be done by checking the 500 position of a literal via its priority. The ones with the highest priority (which is equal to the topmost position in a clause list) are preferred. Literals from the supposed 0 topmost clause will receive the same priority, thus the best literal is further selected depending on a variable’s Figure 1: Evaluation with respect to decision count. counters that get bumped for conflicts. The oficial clausebased heuristic seems a bit over-engineered because it keeps counters that get only increased during a conflict and ones that additionally decay periodically. This decay and a method with multiple tests translates to a series seems of questionable importance since we already move of user requests. The most important statistics of the literals that occur in recent conflicts to the top. Thus we formulas used in testing are as follows: 28000 variables, do drop this second counter in our implementation. 127000 clauses, 5000 other constraints.
CBH also operates rather complex in regard to the The performance metrics we consider for the problems diferent counters for the variables because for every in this evaluation are the execution time, averaged over comparison of two variables, several counters need to be three runs, and the sum of the amount of contradictions added and multiplied together for each of the variables. that were encountered plus the number of branches that This may cause unnecessary overhead. The formulas were taken. The number of branches taken due to decithat are used to combine the counters of a positive and sions is a good indicator of the heuristic’s efectiveness. negative literal into a variable’s counter are the main Contradictions happen less often, ideally a few hundreds reason behind CBH’s need for this dynamic calculation. for the most elaborate methods and at most around five In all these formulas, the positive and negative literal get to ten percent the amount of branches. Therefore we added to three times the minimum of the two literals. included it as a small contribution on defining the efecThe reason behind this last term is to punish variables tiveness of the decisions selected. Both numbers should where just one of its literals is important, kind of like the be as low as possible and the sum of them is called ”steps” inverse of pureness. But the CBH authors do not spec- in the following for simplicity. Their advantage is that the ify how strong its impact on the heuristics performance amount of contradictions and branches is deterministic is. So we create a simplified clause-based heuristic re- in every run and hardware agnostic. The only downgarding the scoring functions by removing the minimum side is that potential time-consuming calculations of a component. Consequently, we also drop the distinction heuristic remain hidden when just looking at the step between positive and negative literals in regard to the count. Therefore we also measure the concrete execution score and directly add them up. This means we explic- time (in milliseconds) for certain comparisons where we itly combine values from a positive and negative literal expect overheads from parts of a heuristic. pair into one variable count, since the distinction will be Every metric is always plotted per test method. Cactus unimportant for our simplified heuristic. As a welcome plots – typically seen at SAT and SMT competitions – are side efect, this combination also reduces the number of used whenever more than two heuristics are compared. individual counters that need to be stored. Here, the methods are ordered by importance for each heuristic element displayed in the graph. The top and right borders represent the timeout limit. 5. Evaluation All measurements are performed on an Intel Core i74710MQ CPU at 2.5 GHz with 16 GB of RAM under WinThe evaluation of the heuristics is done on several prob- dows 10, version 21H1. The Merlin CPQ version in use is lems from three rule sets in Merlin CPQ. These rule sets the state of the master branch on 9. December 2021 and are based on the use cases of customers who use Merlin running JDK 11.0.13.8. for product configuration. Our testset contains a total In Figure 1 we can see that the quality of the literals of 241 individual benchmarks across 85 methods of cus- chosen by CBH are rather good, meaning that it takes tomizing trucks. Each test translates to one user wish just a few decisions to finish the algorithm for most tests – typically even less than the pure literal modified VSIDS variants. However, looking at Figure 2 we see that the complicated summation used by CBH comes at a huge penalty for the execution time. The modified and simpliifed alternative eliminates this issue.
The CBH simplified heuristic works as intended. It keeps the strength of CBH’s good decision making while maintaining to reach this conclusion quickly and without too much overhead. The initial priority should also be calculated more eficiently. So the execution time across the whole of rule set 1 is therefore always competitive and often even faster than the best VSIDS variants.
We presented and implemented several heuristics and tweaks that were able to improve the decision making of Merlin CPQ. The largest tests from an industrially used rule set could be significantly improved by an optimized version of the clause-based heuristic. Our idea of a branching heuristic that specializes on the variables causing conflicts and utilized pure literals as preference also performed almost as strong.
In a configurator, the initial weighting of variables is substantial for the performance. The main conclusion for a product configuration heuristic is the significance of selecting interrelated variables. There are several ways a configurator can group them together and take advantage of them. Keeping them united according to their occurrence in clauses is what worked best for our benchmarks.
Other groupings are possible according to concepts like pure literals, the types of literals and their clause type they are contained in, or their appearance in the start configuration. The aim is to ofer a few good heuristics to the people who design the rule sets that are then brought to users who can configure their product. The designers typically test several heuristics with their specific environment and are then able to choose the one that performs best for them.
There are still many promising heuristics that can be tested in the field of product configuration, as well as countless combinations and alternations. The currently popular Learning Rate Branching (LRB) [34] based on reinforcement learning is a prime candidate. However, it is important to consider the limitations of the product configurator’s structure. Some information might not be directly accessible to the decision heuristic and only realizable with major changes to the whole architecture.
Ideas that contain parts which are ineficient to calculate might need to be changed to perform as desired. So a heuristic has to be adopted to the system it is used in, otherwise the configuration system would be in certain aspects designed around the decision heuristic. [13] G. Audemard, L. Simon, Refining restarts strategies [29] C. M. Li, F. Manyà, Maxsat, hard and soft confor sat and unsat, in: CP, 2012. straints, in: Handbook of Satisfiability, 2021. [14] A. Biere, A. Fröhlich, Evaluating cdcl restart [30] N. Sörensson, N. Eén, Minisat v1.13 - a sat solver schemes, in: POS@SAT, 2018. with conflict-clause minimization, 2005. [15] H. A. Kautz, B. Selman, Planning as satisfiability, [31] F. Xiao, C. Li, M. Luo, F. Manyà, Z. Lü, Y. Li, A in: ECAI, 1992. branching heuristic for sat solvers based on com[16] H. A. Kautz, B. Selman, Pushing the envelope: Plan- plete implication graphs, Science China Informaning, propositional logic and stochastic search, in: tion Sciences 62 (2017) 1–13.
AAAI/IAAI, Vol. 2, 1996. [32] N. Dershowitz, Z. Hanna, A. Nadel, A clause-based [17] A. Biere, A. Cimatti, E. M. Clarke, Y. Zhu, Symbolic heuristic for sat solvers, in: SAT, 2005.
model checking without bdds, in: TACAS, 1999. [33] A. Biere, K. Fazekas, M. Fleury, M. Heisinger, CaDi[18] A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, CaL, Kissat, Paracooba, Plingeling and Treengeling Y. Zhu, Bounded model checking, Adv. Comput. 58 entering the SAT Competition 2020, in: T. Balyo, (2003) 117–148. N. Froleyks, M. Heule, M. Iser, M. Järvisalo, M. Suda [19] C. Sinz, A. Kaiser, W. Küchlin, Detection of inconsis- (Eds.), Proc. of SAT Competition 2020 – Solver and tencies in complex product configuration data using Benchmark Descriptions, volume B-2020-1 of Deextended propositional sat-checking, in: FLAIRS partment of Computer Science Report Series B, UniConference, 2001. versity of Helsinki, 2020, pp. 51–53. [20] J. Marques-Silva, The impact of branching heuris- [34] J. H. Liang, V. Ganesh, P. Poupart, K. Czarnecki, tics in propositional satisfiability algorithms, in: Learning rate based branching heuristic for sat EPIA, 1999. solvers, in: SAT, 2016. [21] A. Biere, A. Fröhlich, Evaluating cdcl variable scor
ing schemes, in: SAT, 2015. [22] J. Rintanen, Planning as satisfiability: Heuristics,
Artif. Intell. 193 (2012) 45–86. [23] M. Iser, M. Taghdiri, C. Sinz, Optimizing minisat variable orderings for the relational model finder kodkod - (poster presentation), in: A. Cimatti, R. Sebastiani (Eds.), Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, volume 7317 of Lecture Notes in Computer Science,
Springer, 2012, pp. 483–484. [24] P. Beame, H. A. Kautz, A. Sabharwal, Towards understanding and harnessing the potential of clause learning, CoRR abs/1107.0044 (2011). [25] M. S. Cherif, D. Habet, C. Terrioux, Combining
VSIDS and CHB using restarts in SAT, in: L. D.
Michel (Ed.), 27th International Conference on Principles and Practice of Constraint Programming, CP 2021, Montpellier, France (Virtual Conference), October 25-29, 2021, volume 210 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, pp. 20:1–20:19. [26] D. Speck, A. Biedenkapp, F. Hutter, R. Mattmüller,
M. Lindauer, Learning heuristic selection with dynamic algorithm configuration, in: Proceedings of the International Conference on Automated Planning and Scheduling, volume 31, 2021, pp. 597–605. [27] S. Haug, Graphentheoretische optimierung der satberechnung im anwendungsfall produktkonfiguration, 2021. [28] K. Pipatsrisawat, A. Darwiche, On the power of clause-learning SAT solvers as resolution engines, Artif. Intell. 175 (2011) 512–525.