Calculating valid domains is an important feature of an interactive product configurator. Since it is an NP hard problem, it is necessary (for large real-world instances) to calculate valid domains only approximately in order to keep the response time low. In this paper, we present a new fast and accurate approximation algorithm to calculate the valid domains in a satisfiability based interactive product configurator. The algorithm is based on building a full implication graph during unit propagation and performing a search in that implication graph in order to approximate whether a domain value is valid. We experimentally compared our new algorithm to the algorithm used by the commercial SAT-based configurator CAS Merlin and measured speedups of up to 18-fold while maintaining the same accuracy.
With the ever increasing number of products available on the market,
customers increasingly demand products that are tailored to their
specific needs. The goal of mass customization is to deliver products and
services that best meet individual customers needs with near mass
production efficiency[
In this paper, we focus on configuration systems that offer an
interactive configuration process. In such systems, the configurator
provides feedback on the current configuration after every new user
decision [
The main contribution of this paper is a new algorithm that is able
to approximate valid domains in the context of interactive product
configuration. We experimentally compared our new algorithm to the
algorithm used in the commercial configurator CAS Merlin [
2.0.1
A propositional variable can be either assigned the value true or f alse. A literal is a propositional variable (e.g. x1) or its negation (e.g. :x1). A disjunction (or, _) of literals is called a clause (e.g. (x1 _ :x2 _ : : :)) and a conjunction (and, ^) of clauses is called a conjunctive normal form (CNF) formula, or just formula (e.g. (x1 _ :x2) ^ (:x3) ^ : : :).
The satisfiability problem (SAT) is the task to decide whether a given formula F has a variable assignment that evaluates F to true (i.e. satisfies F , or F is satisfiable). An assignment satisfies F if it satisfies at least one literal in each of F ’s clauses. An assignment satisfies a positive (resp. negative) literal if the corresponding variable is assigned the value true (resp. f alse).
A SAT solver is a tool which solves a given SAT instance. The
state of the art technique used in modern SAT solvers is conflict
driven clause learning (CDCL) [
As input, UP takes a partial variable assignment and a formula Fcnf . The UP algorithm then iterates over all unit clauses (clauses with exactly one literal) in Fcnf and checks for each unit clause whether the corresponding literal is part of any other clause in Fcnf . If a clause contains the corresponding literal, that clause is satisfied and does not have to be considered anymore. It can be removed from the clause set. If the corresponding literal is negated part of any clause, the negated literal will never evaluate to true and thus can be removed from the clause. Removing literals from a clause can produce new unit clauses which will subsequently be processed by UP as well. The algorithm terminates when there are no unit clauses left or a conflict is detected. 2.0.2
A configuration task T is defined as the triplet (V; D; C) where V = fv1; v2; :::; vng represents a finite set of finite domain variables and D = fD1; D2; :::; Dng represents a set of values corresponding to the variables (i.e., dom(v1) = D1). Furthermore, C = PKB [ CR represents constraints, where PKB represents the product knowledge and CR represents a set of user requirements (both represented as CNF formulas). A configuration is a selection of values for all variables in the product model. Given a set of variables V = fv1; :::; vng and their corresponding domains D = fD1; D2; :::; Dng, a configuration is an instantiation I = fv1 = fi11; :::g; v2 = fi21; :::g; :::; vn = fin1; :::ggg where ikj is an element of dom(vk) 2 D. A configuration is called partial, if it does not contain a selection for all variables, otherwise it is called complete. A configuration is called valid when it is complete and consistent, as that the assignments do not contradict the product model.
A product configurator assists the user during the selection of
domain values in order to configure a product which fits the user’s
requirements best. A single selection of a domain value is called a user
decision [
Calculating valid domains using satisfiability as the consistency
criteria is an NP-hard problem [
Underestimating the set of valid domains means that domain
values could be displayed to the user as invalid, even though they would
not lead to a contradiction. Underestimating the set of valid
domains also means that a user is not able to use the full potential of
the configurability of the product and is restricted rather by
technical limitations of the product configurator. A configurator which
does not underestimate the set of valid domains is called complete.
Overestimating the set of valid domains means that domain values
which would lead to a contradiction could be displayed to the user as
valid nonetheless. By selecting such a domain value, a contradiction
would arise even though the user would not expect this. A
configurator which does not overestimate the set of valid domains is called
backtrack-free [
In this paper we will present an algorithm that overestimates valid domains, therefore the configurator using our method is complete but not backtrack-free. 2.1
Overestimating the set of valid domains can also be seen as underestimating the set of invalid domains. An invalid domain only contains values which are guaranteed to lead to a contradiction when selected by the user. A possible way to calculate the underestimated set of invalid domains is to only consider invalid domain values which are implied through unit propagation by all previously made user decisions. We call such domain values unit-provable invalid domain values. A domain that only contains unit-provable invalid domain values is called a unit-provable invalid domain.
Definition 1 (unit-provable invalid domain). Given the configuration task T = (V; D; C) and a variable v 2 V , the unit-provable invalid domain domiunv(v) for variable v is defined as domiunv(v) = fd j :d 2 up(V; D; C [ fv = dg), d 2 domunsel(v)g; v 2 V .
up is a configurator which returns a configuration that only contains the user selected domain values and through unit propagation additionally implied domain values. domunsel(v) refers to the domain values d 2 dom(v) for variable v which are currently not selected by the user. Consequently, a unit-provable invalid domain only contains values that the user could have selected in the next step.
As a side note: Another way of overestimating the set of valid
domains is to calculate the set of 1-provable invalid domains.
1provability was developed by Pipatsrisawat and Darwiche [
In a configurator it is desirable to handle a certain type of conflicts differently when calculating invalid domains. When a user selects a value from a domain with an at-most-one constraint then all the other values become invalid. However, in this case, we make an exception and do not mark the other values invalid. The reason is that the user selecting another value usually intends to change his selection and not attempting to select both values at once. Therefore we can automatically resolve these kinds of conflicts by removing the originally selected value first and then adding the newly selected value.
Next we provide a definition for a unit-provable invalid domain, which considers the previously mentioned type of conflict. We call such a domain an ar-unit-provable invalid domain. The prefix ar is added in order to indicate that conflicts arising from alternative relations are considered.
Definition 2 (ar-unit-provable invalid domain). Given a configuration task T = (V; D; C) and a variable v 2 V , an ar-unit-provable invalid domain domianrv(v) for variable v is, except in one case, identical to a unit-provable invalid domain: domianrv(v) = domiunv(v) (1)
The only case in which a ar-unit-provable invalid domain differs from the unit-provable invalid domain is when the corresponding variable v (1) is a max-one variable (there is an at-most-one constraint bound to its domain) and (2) a value is already assigned to v by the user. In this case, domianrv(v) only contains invalid domain values that stay unit-provable invalid even if v would not be a maxone variable but could be assigned multiple values.
The ar-unit-provable invalid domain of a max-one variable v thus only contains invalid values that would stay invalid even if the user would manually deselect the already assigned value to v before making his new decision. For any other variable, there is no value that the user could deselect before making a new decision in order to avoid an obvious but undesired conflict. Thus all other ar-unit-provable invalid domains are identical to unit-provable invalid domains. Example 1 (ar-unit-provable invalid domains). Consider a product model consisting of the variables V = fv1; v2g with domains dom(v1) = fd1; d2; d3g and dom(v2) = fd4; d5; d6g, where v1 is a max-one variable and a single constraint: d4 excludes d2. The user assigns d1 to v1 and d4 to v2. The formula Fcnf represents the product model. Performing unit propagation on Fcnf with = fd1; d4g as the initial assignment leads to the implied negative literals f:d2; :d3g. Those negative literals are then extracted from the solution and since they correspond to a domain value in the product model, they form the unit-provable invalid domain domiunv(v1) = fd2; d3g for v1. The unit-provable invalid domain for v2 is empty. But since v2 is not a max-one variable, its arunit-provable invalid domain is empty as well. v1, on the other hand, is a max-one variable and was assigned a value by the user. Thus, its ar-unit-provable domain differs from its unit-provable invalid domain. In order to determine the ar-unit-provable invalid domain for v1, the domain value assigned to variable v1 is removed from the configuration and unit propagation is performed again with the initial assignment = fd4g. Only d2 is negatively implied again and thus forms the ar-unit-provable invalid domain domianrv(v1) = fd2g of v1.
Definition 2 can be generalized to ar-invalid domains and also to ar-valid domain by using satisfiability as the consistency criteria instead of only considering domain values that are implied by the currently selected values and unit propagation. 3
In this Section, we will look at related work for calculating the set of (in)valid domains. Methods for calculating the set of valid domains can be generally grouped into online and offline methods. The goal of offline methods is to solve the hard part (NP-hard) of calculating valid domains before the interactive configuration process is started. This in turn allows to check whether a domain value is valid in polynomial time during the configuration process.
There are three main kinds of offline methods in the literature.
The first method is the translation of the configuration problem into
a binary decision diagram (BDD) [
The second and third approach rely on the representation of the
configuration problem as a constraint satisfaction problem (CSP).
Checking whether a partial configuration can be extended to a valid
configuration corresponds to checking whether the sub-CSP induced
by the corresponding partial variable assignment is satisfiable. As
checking satisfiability is NP-complete, researchers have developed
several preprocessing methods for CSPs [
Adaptive consistency is a decomposition method for
preprocessing CSPs. By ensuring adaptive consistency, a solution can be found
in polynomial time by guaranteeing a backtrack-free solution
calculation when given a fixed variable assignment order. Adaptive
consistency is ensured by adding additional constraints to the CSP and
finding a solution to it in polynomial time is, however, only possible
if adaptive consistency does not increase the size of the CSP
superpolynomially [
Beck et al. [
Input: configuration task T = (V; D; C) 1 Initialize valid domains domval(v) = ; for all v 2 V 2 foreach unselected domain value d, d 2 dom(v) do
4 Add d to domval(v) 5 end 6 end 7 return domval(V )
Algorithm 1: Naive approach for calculating valid domains
Online methods do not do any preprocessing but solve an
NPhard problem after each configuration step in order to guarantee a
backtrack-free configuration process. Algorithm 1 shows the pseudo
code for calculating the set of valid domains using satisfiability as
the consistency criteria. To achieve an approximation we can just use
unit propagation instead of SAT solving (at line 3 of Algorithm 1),
which is the basic idea behind the algorithm used in the commercial
product configurator Merlin [
Our algorithm calculates the ar-unit-provable invalid domains. In the following, we assume that the product model is a Boolean formula Fcnf and the variable assignment which corresponds to the user selected domain values is denoted with . We call the literals in the root literals.
Given a domain value d which is implied by when is used as the initial assignment for Fcnf , there may exist several subsets fS1; S2; :::; Sng; Si which would also imply d if Si would be used as the initial assignment instead of . If Si is minimal, then we call Si an implication possibility of d. For each Si there is a minimal subset C Fcnf of clauses such that C implies d through unit propagation when using Si as the initial assignment. We define two types of equality between two implications possibilities S1; S2: Type-1: Two implication possibilities S1; S2 are equal, iff their corresponding minimal clause sets C1; C2 are equal (denoted by S1 =C S2) and Type-2: Two implication possibilities S1; S2 are equal, iff the literals in both sets are equal (denoted by S1 = S2). It is easy to see that S1 =C S2 implies S1 = S2, but not the other way around. Example 2 (Implication possibility). Given Fcnf = (:d1 _ d2) ^ (:d2_d4)^(:d1_:d3_d4) an initial assignment = fd1; d2; d3g, and a literal d4 2= . Then, three implication possibilities for d4 exist: S = fS1 = fd1g; S2 = fd2g; S3 = fd1; d3gg.
Any literal which is not in the intersection of all implication possibilities of l can be removed from and l will remain implied. Contrary, removing any literal from the intersection results in l being no longer implied. We call the intersection of all implication possibilities of l the required root literals of l, denoted by req(l). Input: configuration task T = (V; D; C), required root literals req(D) F = product model formula
= initial assignment corresponding to the user decisions 1 8v 2 V calculate unit-provable invalid domains domiunv(v) using F and 2 8v 2 V Initialize ar-unit-provable invalid domains
domianrv(v) = domiunv(v) 3 foreach user selected domain value d that is assigned to a max-one variable v do 4 5 foreach d^ 2 domiunv(v) do if d 2 req(d^) then
Remove d^ from domianrv(v)
Now, with the definition of required root literals at hand, we can connect ar-unit-provable invalid domain values to required root literals.
Theorem 1. Given a Boolean formula Fcnf , an initial assignment , a variable v 2 V with domain dom(v) = fd1; :::; dng and dk 2 with an arbitrary but fix k 2 [1; n] which is assigned to v. If v is a multivalue variable (variable which can be assigned multiple values) or v was not assigned by the user, then domianrv(v) and domiunv(v) are identical. On the other hand, if v is a max-one variable and was assigned by the user then a domain value d 2 domiunv(v) is ar-unitprovable invalid if and only if dk 2= req(d).
Proof. Assume that v is a max-one variable and was assigned the value l by the user. A domain value d 2 domiunv(v) is also arunit-provable invalid iff it stays negatively implied even if the user would deselect l. Deselecting l means that l is removed from . Deciding whether d is ar-unit-provable invalid thus means that it has to be checked whether :d stays implied if l is removed from . A required root literal of :d is a literal that has to be part of in order for :d to be implied. So if l is a required root literal of :d, and the user would deselect l, :d would not stay implied and thus d would not be ar-unit-provable invalid. If l is not a required root literal of :d, and the user would deselect l, :d would stay implied and thus d would be ar-unit-provable invalid.
If v was not assigned by the user or is not a max-one variable, then domianrv(v) and domiunv(v) are identical by definition 2.
Algorithm 2 makes use of Theorem 1 for calculating the set of ar-unit-provable invalid domains. First, the unit-provable invalid domains are calculated (line 1). In line 2, the ar-unit-provable invalid domains are initialized with the unit-provable invalid domains. The foreach loop in line 3 iterates over all user assigned max-one variables to check whether the previously calculated unit-provable invalid domain values of those variables are also ar-unit-provable invalid. The foreach loop in line 4 iterates over each unit-provable invalid domain value of v in order to check whether each individual value is ar-unit-provable invalid. In line 5, it is checked whether d is a required root literal of d^. If this is the case, d^is not ar-unit-provable invalid and removed from domianrv(v). The general approach is to create an implication graph during unit propagation which allows us to retrace by which literals each literal was implied. This consequently also allows us to calculate which literals of the initial assignment lead to the implication of certain other literals. Note that calculating the complete set of required root literals for each literal is not necessary in order to correctly execute Algorithm 2. Checking whether d is part of the required root literals of d^ can be performed by using the implication graph to enumerate all type-1 distinct implication possibilities of d^ until one is found that does not contain d. If such an implication possibility was found, it has been proven that d is not a required root literal of d^. The reason is that d has to be contained in all implication possibilities S1; :::; Sn in order to be in the intersection S1 \ ::: \ Sn.
An implication graph is a directed acyclic graph and represents
which literals implied which other literals during unit propagation
[
Definition 3 (Full implication graph). Adapted from [
The full implication graph is built in the same way during unit propagation as the conventional implication graph with the difference that satisfied clauses must not be ignored. 4.1.1
We developed an algorithm that considers each implication possibility one by one by performing a depth first search on a full implication graph. However, instead of calculating each implication possibility individually, our algorithm makes use of theorem 2 to directly decide for each traversed literal, whether l is a required root literal of that literal.
For a literal x let C be the clause which became unit during unit propagation and implied x. By predecessor clause we mean the set of literals C n fxg. Example: for (:a_:b_x) and x the predecessor clause would be fa; bg.
Theorem 2. Let C = fC1; :::; Cng be a set predecessor clauses of an arbitrary literal x. An arbitrary root literal l is not a required root literal of a predecessor clause Ci = fvi1; :::g, iff no literal vij 2 Ci has l as a required root literal. If at least one literal vij 2 Ci exists, that has l as a required root literal, then l is a required root literal of Ci as well. l is not a required root literal of x, iff at least one predecessor clause Ci exists that does not have l as a required root literal. On the other hand, l is a required root literal of x, iff all predecessor clauses of x have l as a required root literal. In the case that C is empty (i.e., x has no predecessor clauses and thus is a root literal), l is not a required root literal of x iff l 6= x. l is a required root literal of x, iff l = x.
Proof. Follows from the definition of required root literals.
Theorem 2 is recursively applied to each traversed literal during the depth first search in the full implication graph in order to eventually decide whether l is a required root literal of k.
The algorithm (see Algorithm 3 for a pseudo-code) iterates over all predecessor clauses of k. First, it is assumed, that l is not a required root literal of the currently processed predecessor clause C. Then we iterate over each literal in C in order to falsify this assumption. This is done by recursively calling the algorithm in order to evaluate whether l is a required root literal of the currently processed literal. If this is the case, the assumption was falsified and it was proven that l is also a required root literal of C. Consequently, no more literals in C have to be evaluated and the next predecessor clause can be processed. If the assumption could not be falsified, then it was proven that at least one predecessor clause of k exists where all literals do not have l as a required root literal and thus k does not have l as a required root literal. Consequently, the algorithm returns f alse. If all predecessor clauses have l as a required root literal, the algorithm cannot return early and has to iterate over all predecessor clauses. In this case, l is a required root literal of k and true is returned. The termination condition of our recursive algorithm is either that k is a root literal and we return (according to Theorem 2) f alse if k is not equal to l. If, on the other hand, k equals l, the algorithm cannot return true immediately because k could have predecessor clauses since root literals can imply other root literals.
Contrary to a conventional implication graph, a full implication
graph can contain cycles [
root literal of x, even if predecessor clauses that contain cycles are skipped during the search.
Proof. Let x be the literal that was assigned to parameter k in the initial call to the algorithm. Each implication possibility of x is associated with a distinct set of clauses. This set of clauses is sufficient in combination with the corresponding set of root literals to imply x through unit propagation. Since this set of clauses is minimal, each literal is implied only once during unit propagation. Consequently, the resulting full implication graph is acyclic. A correct solution can be found for x when searching in an acyclic full implication graph since the clause set that belongs to an implication possibility is a subset of the original clause set. The resulting full implication graph of that subset is also a sub graph of the original full implication graph. Further, each full implication graph induced by each individual implication possibility is contained in the original full implication graph 12 as well. Thus, the algorithm can find each implication possibility in the original full implication graph by traversing the original full implication graph in the correct order. The algorithm is thus also able to traverse all induced full implication graphs with a single continuous acyclic search order. With a known acyclic continuous order, the algorithm would be able to reconstruct all implication possibilities of x, which in turn allows the algorithm to prove that l is not a required root literal. Thus, skipping cycles during the search has no effect on whether the algorithm is able to find a correct result.
This proof requires that Algorithm 3 traverses the implication graph in a certain order. But since it is not possible to know this order beforehand, each possible order has to be tried. The algorithm chooses the next clause or literal to process by whichever clause or literal was not tried yet. This in turn can have the effect that the algorithm selects a wrong search order and thus reaches a dead end where only cycles are detected or a different order has to be tried in order to find additional implication possibilities. In such a case, the algorithm has to backtrack. For this reason, literal k is removed from V isited in line 20 and 24. This allows the algorithm to process the same literal again at a later point but in the context of a different order. However, the downside of this approach is, that it requires an exponential amount of operations in the worst case.
If all different orders have been tried without being able to prove that l is not a required root literal of x, the algorithm returns true. In line 25, it is checked whether V isited is empty. If this is the case, the currently processed literal is x. Since the check is performed after each predecessor clause was processed, it can be concluded that all different orders have been tried and we return true.
On a last note regarding cycles: The algorithm is also able to correctly determine that l is a required root literal of k, if no cycles were encountered at all while processing all predecessor clause of k and the corresponding literals. In such a case, the algorithm would not have to return uncertain but could return true instead. But since the return value true would be handled the same way as uncertain is, we do not differentiate between those two return values and stick to uncertain. 4.1.2
So far, we have discussed how the algorithm works. But due to cycles in the full implication graph, the algorithm is required to perform en exponential amount of operations in the worst case. In this section, we will present two optimizations that minimize the amount of operations that the algorithm has to perform.
Optimization 1: It is sufficient to find a single predecessor clause of literal k where each literal does not have l as a required root literal in order to prove that k does not have l as a required root literal as well. Since evaluating k at a later point during the search again would yield the same result, this result can be saved. The next time the algorithm encounters k, the saved result can be used instead of having to search the full implication graph again.
Optimization 2: Algorithm 2 uses Alorithm 3 to decide whether d^ is a required root literal of d. The set of literals that do not have d^as a required root literal can be passed to Algorithm 2 as parameter. This set can be reused between independent calls to Algorithm 2 as long as the literal assigned to parameter d^ is the same. This is the case in Algorithm 2 for each call to Algorithm 3. This way, each subsequent call to Algorithm 3 terminates faster since the evaluation result of more literals is already known. 5
In this Section we present the results of our experimental evaluation of Algorithm 2 regarding its runtime and accuracy.
As benchmarks we will use feature models as product models.
Mendonca provides a repository of real-world and generated feature
models [
For the accuracy evaluation we used five real world feature
models [
For the performance evaluation experiments we will use the following algorithms. Each implemented by us in Java.
Naive algorithm: The naive approach for calculating the ar-unitprovable invalid domains – running unit propagation for each candidate separately.
Merlin algorithm: An algorithm used by the commercial product configurator Merlin. It is an optimized variant of the naive approach that reduces redundant unit-propagations.
RRL algorithm: The algorithm introduced in this paper – Algorithm 2.
For our accuracy experiments, we will use the RRL algorithm to calculate the ar-unit-provable invalid domain values, the naive approach for calculating the ar-1-provable invalid domain values and the adapted SAT Online algorithm (Algorithm 1) for calculating arinvalid domain values.
All experiments were performed on a Computer with Intel(R) Xeon(R) CPU E3-1231 v3 @ 3.40GHz, 8GB RAM, NixOS 20.03 operating system and Java 11 (OpenJDK).
Figure 1 shows the results of the performance measurement. The naive algorithm is clearly the slowest one and needs 135ms for 500 asserted features and 309ms for 1,000 asserted features. The second slowest algorithm is Merlin’s algorithm which needs 81ms at the 500 mark and 169 at the 1,000 mark. The RRL algorithm needs 5ms at the 500 mark and 9ms at the 1,000 mark. This corresponds to a speedup at the 500 and 1,000 mark of roughly 18 compared to the Merlin algorithm and a speedup of roughly 34 compared to the naive algorithm.
Our algorithm has in the worst case an exponential time complexity, But it still outperforms the naive and Merlin’s algorithm even though they have a linear worst case time complexity. We argue, that the reason for that is, that most traversed literals evaluate to f alse. This allows the algorithm, due to our optimization to reuse evaluation results instead of having to search the implication graph again at a later point. Another probable reason is that the implication graph most likely never has to be traversed completely in order to decide whether a literal is a required root literal.
Figure 2 shows the measured sizes of the set of ar-unit-provable invalid domain values, ar-1-provable invalid domain values and arinvalid domain values for the SubseaControlSystem and ubuntu1410 feature models. For the other three feature models the set of ar-unitprovable invalid domain values is identical to both the set of ar-1provable invalid domain values and ar-invalid domain values.
For the SubseaControlSystem the set of ar-invalid domain values is identical to the set of ar-1-provable values. The set of ar-1-provable invalid domain values differs from the set of unit-provable invalid domain values in 10 of the 60 test cases, the maximum difference in size is 7. In case of ubuntu1410 the set of ar-1-provable invalid domain values differs from the set of unit-provable invalid domain values in 29 of 150 test cases, the maximum difference in size is 4.
The results indicate that the ar-unit-provable invalid domain values are most of the time identical to the ar-invalid domain values. Only in two feature models additional ar-1-provable invalid domains were detected. We do believe that our results are representative for small feature models with few constraints. But due to the available tools and our limited time frame we were not able to measure big feature models with many constraints. 6
The challenge of calculating valid domains is that this problem is NPhard but we need to calculate them for hundreds of variables within milliseconds. For this reason, we developed an algorithm that approximates the valid domains. A further challenge is to consider the automatic resolution of conflicts that arise from selecting a second value within an alternative relation as domain values could become valid that would be invalid otherwise.
We developed our algorithm based on the idea of required root literals. Our algorithm has to perform unit propagation only once and then relies on the full implication graph for further calculations. Even though this approach induces an exponential worst case complexity, we could not observe it in our experiments. Instead, we found that the calculation time of our algorithm appears to grow linearly with the the amount of asserted features. In future work, the average case complexity of our algorithm should be determined and it should be analyzed, under which circumstances the algorithm might require an exponential computation time.
We additionally measured the accuracy of the approximation achieved by our method. We found that for small feature models with few constraints this approximation is very accurate. These results are, however, not transferable to large feature models with many constraints. Additional measurements have to be performed in future work in order to get a better understanding of the accuracy.