=Paper=
{{Paper
|id=None
|storemode=property
|title=Enumeration of Valid Partial Configurations
|pdfUrl=https://ceur-ws.org/Vol-755/paper04.pdf
|volume=Vol-755
|dblpUrl=https://dblp.org/rec/conf/confws/VoronovAE11
}}
==Enumeration of Valid Partial Configurations==
https://ceur-ws.org/Vol-755/paper04.pdf
Enumeration of valid partial configurations
Alexey Voronov, Knut Åkesson, Fredrik Ekstedt
Chalmers University of Technology, Göteborg, Sweden
{voronov, knut}@chalmers.se
Fraunhofer-Chalmers Research Centre for Industrial Mathematics, Göteborg, Sweden
fredrik.ekstedt@fcc.chalmers.se
Abstract know which combinations of variable assignments for a sub-
set of the variables might result in a product that satisfies all
Models of configurable products can have hundreds constraints, that is to know valid partial configurations. This
of variables and thousands of configuration con- is important because it helps the engineer to develop solu-
straints. A product engineer usually has a limited tions only for those combinations that can actually be built
responsibility area, and thus is interested in only and sold. Overestimation of these solutions will lead to engi-
a small subset of the variables that are relevant to neer doing unnecessary designs. Underestimation can lead to
the responsibility area. It is important for the en- costly delays if an overlooked configuration is requested by a
gineer to have an overview of possible products customer afterwards.
with respect to the responsibility area, with all ir- Computing the exact set of valid partial configurations is
relevant information omitted. Configurations with generally hard. Simply taking configurations of the complete
some variables omitted we will call partial config- products and projecting them on relevant variables is not fea-
urations, and we will call a partial configuration sible, as practical problems can have 10120 and more build-
valid if it can be extended to a complete configura- able complete products.
tion satisfying all configuration constraints. In this
One of the ways to get exact set of valid partial configura-
paper we consider exact ways to compute valid par-
tions is to existentially quantify all irrelevant variables from
tial configurations: we present two new algorithms
the formula that represents the conjunction of all configura-
based on Boolean satisfiability solvers, as well as
tion constraints, for example using resolution inference rule
ways to use knowledge compilation methods (Bi- [Robinson, 1965; Davis and Putnam, 1960], and then use a
nary Decision Diagrams and Decomposable Nega-
standard algorithm to enumerate all (complete) assignments
tion Normal Form) to compute valid partial config-
of the new simplified formula. A simple enumeration of com-
urations. We also show that the proposed methods
plete assignments searches for a satisfying assignment, adds it
are feasible on configuration data from two auto-
to the result, and also adds it to the current set of constraints as
motive companies.
a blocking constraint, forbidding future search from returning
it again. The disadvantage of this approach is that the formula
size can grow significantly after quantification. In this paper
1 Introduction we present a modification of this enumeration algorithm that
Within the automotive industry it is common to have a few does not require existential quantification of variables to enu-
general platforms where each platform are highly config- merate partial configurations (Section 4.1). Similar algorithm
urable to adapt to the needs on different markets but also to can be found in [Gebser et al., 2009].
satisfy the needs of individual customers. Having highly con- The problem of partial configurations can also be tackled
figurable products put high demands on the engineering sys- by the widely used interactive configurators. In an interac-
tems to support the engineers during the development of the tive configurator a user selects values for variables one by
platforms. While having a configurable product or platform it one. The configurator should guide the user so that at any
is inevitable to also have constraints that specify what can be point there exist at least one way to complete the configura-
allowed together and what is not allowed together. These con- tion without changing any of the earlier decisions, in this case
straints can, in many situations, be defined as a set of Boolean a configurator is backtrack-free. Configurator should also be
formulas defined over finite domain variables. complete meaning that if a configuration is allowed accord-
Development of complex products—like in the automo- ing to the constraints, configurator should allow it. Having
tive industry—is done in large teams, where each engineer such complete and backtrack-free configurator, it is possible
is working with only a limited part of the product. For the to automatically check all (partial) assignments of values to
individual engineer only a small subset of the variables from the relevant variables, and the configurator will show which
those that describe the full product, are of immediate inter- of them are valid. If a configurator is not backtrack-free, it
est. However, an important problem for the engineer is to can overestimate allowed partial configurations. If it is not
complete, it will underestimate them. 3 Motivating example
Previous work on methods for building interactive con- Configuration problems describing complete products can
figurators started as extensions of Constraint Satisfaction have thousands of variables and hundreds of thousands con-
Problem (CSP) with conditional and dynamic formulations straints. An engineer, or a group of engineers, is usually re-
[Dechter and Dechter, 1988; Mittal and Falkenhainer, 1990; sponsible only for a subset of the variables. It could be that it
Soininen and Gelle, 1999; Sabin and Freuder, 1998; Gott- is a requirement to design all possible solutions within the re-
lob et al., 2007]. However, supported implementations of sponsibility area, in case someone will order such a product.
these algorithms are not readily available. Binary Decision In such a case it can be expensive to have overestimated set
Diagrams (BDDs) [Bryant, 1986] is a knowledge compi- of valid configurations, since engineers will spend time de-
lation method [Darwiche and Marquis, 2002] successfully signing forbidden ones. Underestimations are also bad, since
used for configuration [Hadzic et al., 2004], especially for they lead to delays for designing a solution for ordered, but
real-time interactive configuration. However, BDDs suffer missed configuration.
from memory explosion for many datasets of practical size. The problem can be illustrated by the following ex-
Other knowledge compilation methods used for configuration ample of a simple car configuration. Let X =
include automata representation [Amilhastre et al., 2002], {body, engine, transmission} be the set of variables, and
Tree-of-BDDs [Subbarayan, 2005], Joint Matched CSP [Sub- D = {{mini, sedan, suv}, {gasoline, diesel, electric},
barayan and Andersen, 2005], Decomposable Negation Nor- {manual, auto, evt}} be the set of corresponding domains.
mal Form (DNNF) [Darwiche and Marquis, 2002] (espe- Let the following be the set of constraints C:
cially Deterministic DNNF for model counting [Kübler et
al., 2010]), as well as combinations of search and BDDs • ¬((body = mini) ∧ (engine = gasoline))
[Norgaard et al., 2009]. Recently, Boolean Satisfiability • ¬((body = mini) ∧ (engine = diesel))
Solvers (SAT-solvers) emerged as an alternative to work with
configurations [Sinz et al., 2003; Küchlin and Sinz, 2000; • ¬((body = sedan) ∧ (engine = electric))
Sinz et al., 2006; Janota, 2008], including interactive con- • ¬((body = suv) ∧ (engine = gasoline))
figurators [Janota, 2010]. • (engine = electric) → (transmission = evt)
In this paper we show how a SAT-solver can be used to enu-
merate partial configurations based on modification of stan- • (transmission = evt) → (engine = electric)
dard enumeration algorithm, and based on checking every Valid assignments of P = hX, D, Ci can be presented, for
partial assignment inspired by interactive configuration. We example, in a tabular form, as shown in Table 1. Each row
also show how existing DNNF algorithms can be used to enu- in the table corresponds to an assignment, and each column
merate partial configurations. We show feasibility of a SAT- corresponds to a variable. Each cell contains a value assigned
solver based implementation on configuration data from two to the corresponding variable.
automotive companies. Let us suppose that there is a group of engineers that
The paper is organized as following. Section 2 covers for- are interested only in connection between body and trans-
mal preliminaries, Section 3 gives a motivating example, Sec- mission, and they would like to disregard all information
tion 4 presents the algorithms. Section 5 provides experimen- about engine. So they define the limited scope to be S =
tal results and discussion, and Section 6 concludes the paper. {body, transmission}. Valid partial assignments for S are
presented in Table 2.
One way to get the partial assignments is to enumerate all
2 Preliminaries complete assignments, project them onto the relevant vari-
ables (remove the irrelevant columns from the table), and re-
The configuration problem is a triple P = hX, D, Ci, move duplicate partial assignments (rows). This approach is
where X = {x1 , x2 , . . . , xK } is a set of variables, D = infeasible in practice, as some industrial examples from au-
{D1 , D2 , . . . , DK } is a set of corresponding finite domains, tomotive industry have 10120 allowed complete assignments.
and C = {C1 , C2 , . . . , CJ } is a set of propositional formulas However, scopes of interest for the engineers may have less
over atomic propositions xk = v where v ∈ Dk , specifying
conditions that the variable assignments have to satisfy. Table 1: Valid complete assignments
A complete assignment to a configuration problem P is a
function A : X → D which is defined for all xk ∈ X. A body engine transmission
valid complete assignment (or solution) to P is a complete
mini electric evt
assignment A for which each Cj is satisfied. A partial as-
sedan gasoline manual
signment to P is a partial function B : X → D defined for
sedan gasoline automatic
variables xk ∈ Y ⊆ X. We will write vars(B) = Y ⊆ X
sedan diesel manual
to denote the set of variables of B, or the scope of B. We
sedan diesel automatic
will call a partial assignment valid iff it can be extended to a
suv diesel manual
valid complete assignment. We will use P[B] to denote the
suv diesel automatic
simplified problem obtained by setting the variables defined
suv electric evt
in B.
Table 2: Valid partial assignments Algorithm 1 Search for complete, then forbid partial
body transmission input: problem P = hX, D, Ci, relevant variables S ⊆ X
C0 ← C
mini evt P0 ← P
sedan manual result ← {}
sedan automatic while sat(P): /∗ ask solver ∗/
suv manual A ← assignment(P) /∗ assignment from solver ∗/
suv automatic B ← A projected on S
suv evt result ← result ∪B
C 0 ← C 0 ∧ ¬(B as constraint)
P 0 ← hX, D, C 0 )i
than a thousand valid partial assignments, which is com- return result
putable using methods presented below. Approximations of
this approach are found in practice, where instead of all valid
assignments, only the ones that correspond to the products
built during the last year (for example) are considered, which the complete scope. The solver can be used as following:
gives an underestimation of the answer. Clearly, there is a each partial assignment is added as an extra constraint to the
need for a better method. set of configuration constraints, and removed after the solver
has returned an answer. The key to the good performance in
4 Enumerating valid partial assignments this method is in the ability of the solver to cheaply add and
retract constraints consisting of atomic propositions; again,
This sections presents two algorithms adopted to solve the Minisat-like solvers have this feature.
problem based on satisfiability solvers. By a satisfiability
solver we mean a tool that is able to answer whether an in-
Algorithm 2 Enumerate partial, then extend
stance of a configuration problem has at least one valid com-
plete assignment, and provides one if such exists. For exam- input: problem P = hX, D, Ci, relevant variables S ⊆ X
ple, tools for solving Constraint Satisfaction Problems (CSP- output: valid partial assignments
solvers) and Boolean Satisfiability Problems (SAT-solvers) result ← {}
can be used for this purpose. This section also shows how for B in allAssignments(S):
DNNF algorithms can be used to enumerate valid partial con- if sat( P[B] ):
figurations. result ← result ∪B
return result
4.1 Searching for complete, then forbidding
partial
One way to enumerate all valid complete assignments is to An example illustrating this method is presented in Table 3.
iteratively search for any valid complete assignment, and in The columns for body and transmission contain all possible
addition to adding it to the result, add a negation of it as a (not only valid) partial assignments for S. The table must be
blocking constraint to the existing set of constraints. This extended with the columns for variables (X \ S), in this case
algorithm can be modified to enumerate valid partial assign- it is only one, engine. If there is at least one valid complete
ments, as shown in Algorithm 1. When a solver returns the assignment that contains the partial one for the row, the values
first complete assignment, the assignment is projected onto for all variables are written in the row. Otherwise, a “—”
the relevant scope. This partial assignment is returned as the indicates that there is no such valid complete assignment, and
first element of the result, and also added as a blocking con- the partial assignment is not valid.
straint, ensuring that the solver will not return any (complete)
assignment that will contain the partial one. Then this process
is repeated. Table 3: Illustration of Algorithm 2 (Enumerate partial, then
The ability of the solver to incrementally add blocking con- extend).
straints, while still keeping previously inferred information,
is very important for the good performance of this algorithm. body transmission engine
This is supported by, for example, Minisat-like solvers [Een
and Sörensson, 2004; Een and Sörensson, 2003]. mini manual —
mini autmatic —
4.2 Enumerating partial, then extending mini evt electric
sedan manual gasoline
In this approach it is necessary to enumerate all partial as-
sedan automatic gasoline
signments, and try to extend each of them to a valid complete
sedan evt —
assignment using a solver. Just checking a partial assignment
suv manual diesel
against each of the constraints in isolation is not enough, be-
suv automatic diesel
cause there could be dependencies between variables that are
suv evt electric
not visible within the local scope, but are only visible within
An advantage of Algorithm 1 compared to Algorithm 2 is Enumeration of assignments of DNNFs is shown in Algo-
that it builds upon heuristics of an underlying solver to skip rithm 4 [Darwiche, 2000], where each assignment is repre-
checking many of the non-allowed assignments. A disadvan- sented as a set of literals, and × is a Cartesian product on
tage is that to find the next partial assignment, it is necessary them:
to process a larger (increased by one) set of constraints; this
{N1 , . . . , Nn }×{M1 , . . . , Mm } = {N1 ∪M1 , . . . , Nn ∪Mm }.
could be a problem when it is necessary to produce millions
of partial assignments. But when there is a small number of The complexity of enumerating the models of a smooth
valid partial assignments, or a user specifically asked for the DNNF f is O(mn2 ), where m is the size of f and n =
first hundred of assignments as a sample, and there are many |MODELS(f )| [Darwiche, 1998].
non-allowed configurations, Algorithm 1 can be beneficial.
Algorithm 4 MODELS – enumerating assignments of DNNF
4.3 Knowledge compilation: DNNF
input: smooth DNNF f
Knowledge compilation is a family of approaches that ad- output: (complete) valid assignments of f , as sets of literals
dresses intractability of many Artificial Intelligence prob- if f is a Literal l:
lems. A propositional model is compiled in an off-line phase return {{l}};
in order to support some queries in polytime [Darwiche and else if f is a conjunction a1 ∧ · · · ∧ an :
Marquis, 2002]. Binary Decision Diagrams (BDDs) [Bryant, return MODELS(a1 )× · · · × MODELS(an );
1986] belong to this family and received substantial attention else if f is a disjunction a1 ∨ · · · ∨ an :
as a tool for configuration problems [Hadzic et al., 2004]. return MODELS(a1 )∪ · · · ∪ MODELS(an ).
Decomposable Negation Normal Form (DNNF) [Darwiche,
2001] is a data structure used in knowledge compilation for
which BDD is a special case. It is more succinct than BDDs The overall process of using DNNF is shown in Algo-
and its compilation time is often shorter than that of BDDs rithm 5. DNNF for the car example is shown on Figure 1a.
[Subbarayan et al., 2007]. DNNF supports smaller number DNNF with variable engine forgotten is shown on Figure 1b,
of tractable operations than BDD, while still allowing poly- and its valid partial assignments can be found in Table 2.
time existential quantification (forgetting) and assignments
enumeration, which together allow polytime partial assign- Algorithm 5 Knowledge compilation based approach
ments enumeration once DNNF is compiled.
Formally, a propositional formula a is in negation normal input: problem P = hX, D, Ci, relevant variables S ⊆ X
form (NNF) if and only if a is either a positive or negative output: valid partial assignments
atomic proposition (a literal); a conjunction ∧i ai ; or a dis- f1 ← COMPILE(P)
junction ∨i ai where each ai is in negation normal form. A f2 ← FORGET(S, f1 ) /* see Algorithm 3 ∗ /
formula in NNF f is decomposable (DNNF) if and only if for m ← MODELS(f2 ) /* see Algorithm 4 ∗ /
any conjunction a = a1 ∧ · · · ∧ an no atomic propositions are return m
shared by any conjuncts in a: ATOMS(ai ) ∩ ATOMS(aj ) = ∅
for every i 6= j. A formula in NNF is smooth if for every
disjunction a = a1 ∨ · · · ∨ an , ATOMS(a) = ATOMS(ai ) for Polynomial time guarantee for assignments enumeration
every i. operation is an advantage of DNNF. However, the compi-
Existential quantification of variables from DNNF is pre- lation time of arbitrary constraints into DNNF is in general
sented in Algorithm 3 [Darwiche, 2001]. Every occurence exponential. When the data changes rarely, this time is amor-
of irrelevant variable is replaced by true, and the formula is tized among multiple queries, but when the data changes very
simplified accordingly. This procedure preserves decompos- often, this off-line stage does not pays off.
ability, and its running time is linear in the DNNF size. DNNF have an important advantage: if it is smooth and
deterministic, it can be used to count the assignments [Dar-
wiche, 2000]. An NNF formula a is deterministic if for every
Algorithm 3 FORGET – existential quantification on DNNF disjunction a = a1 ∨ · · · ∨ an , every pair of disjuncts in a
input: relevant variables S ⊆ X, DNNF f is logically inconsistent; that is, ai ∧ aj |= f alse for every
output: DNNF with variables X \ S existentially quantified i 6= j. Unfortunately, operation FORGET does not preserve
if f is a Literal l: determinism, and counting in such case will give overesti-
if VAR(l) ∈ S: mated answer. However, even overestimated answer can be
return f useful in some cases. It is also possible to recompile the re-
else sulting DNNF again into a deterministic one. Some practical
return true applications of counting for configuration using DNNF were
else if f is a conjunction a1 ∧ · · · ∧ an : considered in [Kübler et al., 2010].
return FORGET(a1 ) ∧ . . . ∧ FORGET(an )
else if f is a disjunction a1 ∨ · · · ∨ an : 5 Experimental results
return FORGET(a1 ) ∨ . . . ∨ FORGET(an ) We analyzed the data from two automotive companies: three
datasets from the first company, and one dataset from the sec-
(a) Full DNNF. (b) DNNF with variable engine existentially quantified.
Figure 1: DNNFs for the car example.
ond, denoted as A, B, C and D, respectively. Details about Table 4: Problem properties.
datasets are presented in Table 4.
We implemented Algorithms 2 and 1 on top of Sat4j solver A B C D
[Le Berre and Parrain, 2010].
Variables 511 446 92 217
A knowledge compilation tool was developed based on Domain size, average 6.3 2.4 6.1 3.3
BDD package BuDDy [Lind-Nielsen, 2002]. The pre- Domain size, max 108 82 75 59
ordering algorithms from [Narodytska and Walsh, 2007] were # of assignments 10150 1087 1055 1085
implemented for sorting variables and restrictions, using in- # of valid assignments 10124 1057 1049 1033
flation parameter r = 1.5 in the clustering step. A simplified CNF clauses 65183 1121 341 9010
version of the MCL clustering algorithm [van Dongen, 2000] DNNF nodes n/a 5071 5009 528583
was used, skipping the truncation heuristics and the sparse
matrix multiplication tools. No post-ordering of the variables Partial scope, variables 6 17 3 8
was included. The tool was able to handle only the smallest # of valid partial assignments 200 13770 25 382
dataset.
Another attempt to use knowledge compilation involved
c2d compiler [Darwiche, 2004] that compiles propositional the BDD was successfully built, is the fastest. The reason
formulas to deterministic DNNF. Algorithms 3 (FORGET) and why DNNF-based method appears to be slow could be a non-
4 (MODELS) were implemented to work with the DNNF out- optimal implementation of Algorithms 3 and 4.
put of c2d. Using another DNNF compiler sharpSAT [Muise
et al., 2010] resulted in segmentation faults on some of the 6 Conclusions
datasets, and its debugging is underway.
In this paper we looked at the problem of computing allowed
Sat4j and c2d require the input to be in Conjunctive Normal
partial combinations, which is important for engineers work-
Form (CNF), that is it have to be a conjunction of clauses, and
ing with product development. We presented several algo-
each clause is a disjunction of literals. Each literal is either
rithms, two of which are suitable for SAT-solvers, and one
a positive or negative atomic proposition. Constraints were
that is based on DNNF. Our experiments showed that SAT-
converted to CNF using Tseitin encoding [Tseitin, 1968].
based implementation can handle large datasets from automo-
Two times were measured. The first time measured was tive industry quite efficiently. Preliminary experiments with
preprocessing or off-line time. This included, for example, knowledge compilation tools showed that available DNNF
DNNF compilation, and initial constraint propagation. The compilers cannot handle the largest dataset within the mem-
results are presented in Table 5. BDD-based implementation ory and time limits. However, DNNF-based method has
was not able to complete the compilation process of larger
instances. c2d compiler ran out of 2 GB memory limit (it is
available only as a 32 bit application) compiling the largest Table 5: Time for compilation/initial clause learning, sec-
dataset A. onds.
The second time measured was the on-line time, or the time
to actually compute the valid partial configurations for one A B C D
given scope, while utilizing results from the off-line phase.
Sat4j, Alg 1 2 2 1 2
The results are presented in Table 6. SAT-based solution is
BuDDy timeout timeout 40 timeout
very robust on the datasets, even without having theoretical
c2d out-of-mem 240 2 20
guarantees on running times. The BDD-based solution, when
Table 6: Time to compute valid partial assignments [Een and Sörensson, 2004] Niklas Een and Niklas Sörens-
(FORGET + MODELS), seconds. son. An Extensible SAT-solver. Theory and Applications
of Satisfiability Testing, 2919/2004:502–518, 2004.
A B C D [Gebser et al., 2009] Martin Gebser, Benjamin Kaufmann,
Sat4j, Alg 1 10 29 0.12 3 and Torsten Schaub. Solution enumeration for projected
BuDDy n/a n/a 0.01 n/a Boolean search problems. Integration of AI and OR Tech-
DNNF from c2d n/a 681∗ 0.15∗ 22∗ niques in Constraint Programming for Combinatorial Op-
∗
Based on own, unoptimized implementation. timization Problems, pages 71–86, 2009.
[Gottlob et al., 2007] Georg Gottlob, Gianluigi Greco, and
the advantages of polynomial time guarantee on the on-line Toni Mancini. Conditional Constraint Satisfaction: Logi-
phase, and the ability to count the assignments when DNNF cal Foundations and Complexity. In Manuela M. Veloso,
is determenistic. editor, IJCAI-2007, pages 88–93, Hyderabad, India, Jan-
uary 2007.
Acknowledgements [Hadzic et al., 2004] Tarik Hadzic, Sathiamoorthy Sub-
barayan, R.M. Jensen, Henrik Reif Andersen, J. Mø ller,
This work was carried out at the Wingquist Laboratory VINN
and H. Hulgaard. Fast backtrack-free product configu-
Excellence Centre within the Area of Advance — Produc-
ration using a precompiled solution space representation.
tion at Chalmers, supported by the Swedish Governmental
PETO conference, 2004.
Agency for Innovation Systems (VINNOVA). The support is
gratefully acknowledged. [Janota, 2008] Mikolas Janota. Do SAT solvers make good
configurators? 12th International Software Product Line
References Conference. First Workshop on Analyses of Software Prod-
uct Lines, pages 1–5, 2008.
[Amilhastre et al., 2002] Jérôme Amilhastre, Helene
Fargier, and Pierre Marquis. Consistency restoration [Janota, 2010] Mikolas Janota. SAT Solving in Interactive
and explanations in dynamic CSPs — Application to Configuration (PhD thesis). PhD thesis, University Col-
configuration. Artificial Intelligence, 135:199–234, 2002. lege Dublin, 2010.
[Bryant, 1986] Randal E. Bryant. Graph-Based Algorithms [Kübler et al., 2010] Andreas Kübler, Christoph Zengler,
for Boolean Function Manipulation. IEEE Trans. Comput., and Wolfgang Küchlin. Model Counting in Product Con-
35(8):677–691, August 1986. figuration. Electronic Proceedings in Theoretical Com-
[Darwiche and Marquis, 2002] Adnan Darwiche and Pierre puter Science, 29(LoCoCo):44–53, July 2010.
Marquis. A knowledge compilation map. Journal of Arti- [Küchlin and Sinz, 2000] Wolfgang Küchlin and Carsten
ficial Intelligence Research, 17(1):229–264, 2002. Sinz. Proving Consistency Assertions for Automotive
[Darwiche, 1998] Adnan Darwiche. Model-Based Diagnosis Product Data Management. Journal of Automated Rea-
using Structured System Descriptions. Journal of Arti cial soning, 24(1):145–163, February 2000.
Intelligence Research, 8:165–222, 1998. [Le Berre and Parrain, 2010] Daniel Le Berre and Anne Par-
[Darwiche, 2000] Adnan Darwiche. On the tractable count- rain. The Sat4j library , release 2.2 system description.
ing of theory models and its application to belief revision Journal on Satisfiability, Boolean Modeling and Compu-
and truth maintenance. Journal of Applied Non-Classical tation, 7:59–64, 2010.
Logics, 2000. [Lind-Nielsen, 2002] Jø rn Lind-Nielsen. BuDDy: A BDD
[Darwiche, 2001] Adnan Darwiche. Decomposable negation package. http://buddy.sourceforge.net, 2002.
normal form. Journal of the ACM, 48(4):608–647, July [Mittal and Falkenhainer, 1990] Sanjay Mittal and Brian
2001. Falkenhainer. Dynamic Constraint Satisfaction Problems.
[Darwiche, 2004] Adnan Darwiche. New Advances in Com- In AAAI-90, pages 25–32, 1990.
piling CNF to Decomposable Negation Normal Form. In [Muise et al., 2010] Christian Muise, Sheila McIlraith,
ECAI 2004, 2004. J.Christopher Beck, and Eric Hsu. Fast d-DNNF Com-
[Davis and Putnam, 1960] Martin Davis and Hilary Putnam. pilation with sharpSAT. In AAAI 2010, pages 54–60,
A Computing Procedure for Quantification Theory. Jour- 2010.
nal of the ACM, 7(3):201–215, July 1960. [Narodytska and Walsh, 2007] Nina Narodytska and Toby
[Dechter and Dechter, 1988] Rina Dechter and Avi Dechter. Walsh. Constraint and variable ordering heuristics for
Belief maintenance in Dynamic Constraint Networks. In compiling configuration problems. In Proceedings of the
AAAI-88, pages 37–42, 1988. 20th international joint conference on Artifical intelli-
[Een and Sörensson, 2003] Niklas Een and Niklas Sörens- gence, pages 149–154, Hyderabad, India, 2007. Morgan
son. Temporal Induction by Incremental SAT Solv- Kaufmann Publishers Inc.
ing. Electronic Notes in Theoretical Computer Science, [Norgaard et al., 2009] Andreas Hau Norgaard, Morten Ri-
89(4):543–560, 2003. iskjaer Boysen, Rune Moller Jensen, and Peter Tiede-
mann. Combining Binary Decision Diagrams and Back-
tracking Search for Scalable Backtrack-Free Interactive
Product Configuration. In Proceedings of the 21st Interna-
tional Joint Conferences on Artificial Intelligence(IJCAI-
09) Workshop on Configuration, 2009.
[Robinson, 1965] J. A. Robinson. A Machine-Oriented
Logic Based on the Resolution Principle. Journal of the
ACM, 12(1):23–41, January 1965.
[Sabin and Freuder, 1998] Mihaela Sabin and Eugene C.
Freuder. Detecting and resolving inconsistency and redun-
dancy in conditional constraint satisfaction problems. In
Proceeding of Constraint Programming (CP-98), 1998.
[Sinz et al., 2003] Carsten Sinz, Andreas Kaiser, and Wolf-
gang Küchlin. Formal methods for the validation of au-
tomotive product configuration data. Artificial Intelli-
gence for Engineering Design, Analysis and Manufactur-
ing, 17(01):75–97, August 2003.
[Sinz et al., 2006] Carsten Sinz, Wolfgang Küchlin, Dieter
Feichtinger, and Georg Görtler. Checking Consistency and
Completeness of On-Line Product Manuals. Journal of
Automated Reasoning, 37(1):45–66, August 2006.
[Soininen and Gelle, 1999] Timo Soininen and Esther Gelle.
Dynamic Constraint Satisfaction in Configuration. In
AAAI-99, Workshop on Configuration, pages 95–100,
1999.
[Subbarayan and Andersen, 2005] Sathiamoorthy Sub-
barayan and Henrik Reif Andersen. Linear Functions
for Interactive Configuration Using Join Matching and
CSP Tree Decomposition. In Configuration Workshop at
IJCAI’05, pages 7–12, 2005.
[Subbarayan et al., 2007] Sathiamoorthy Subbarayan, Lucas
Bordeaux, and Youssef Hamadi. Knowledge Compilation
Properties of Tree-of-BDDs. In AAAI 2007, pages 502–
507, 2007.
[Subbarayan, 2005] Sathiamoorthy Subbarayan. Integrating
CSP Decomposition Techniques and BDDs for Compiling
Configuration Problems. Integration of AI and OR Tech-
niques in Constraint Programming for Combinatorial Op-
timization Problems, 3524/2005:351–365, 2005.
[Tseitin, 1968] Gregory S. Tseitin. On the complexity of
derivation in propositional calculus. In A.O. Slisenko, ed-
itor, Structures in Constructive Mathematics and Mathe-
matical Logic, Part II, Seminars in Mathematics (trans-
lated from Russian), pages 234–259. Steklov Mathemati-
cal Institute, 1968.
[van Dongen, 2000] Stijn van Dongen. A cluster algorithm
for graphs. Technical Report INS-R0010., 2000.