Definition 1. A configuration model C *is a triple* (**X, D, F**) *where X is a set of variables* {x0, . . . , xn−1}, D = D0 × **. . .** × Dn−1 is the Cartesian product of their finite domains D0**, . . . , D**n−1 and F = {f0**, ..., f**m−1} *is a set of propositional formulae over* atomic propositions xi = v, where v ∈ Di*, specifying conditions on the values of the* variables.

Concretely, every domain can be defined as Di = {0, . . . , |Di| − 1}. An assignment of values v0**, . . . , v**n−1 to variables x0**, . . . , x**n−1 is denoted as an assignment ρ = {(x0, v0), . . . ,(xn−1, vn−1)}. Domain of assignment dom(ρ) is the set of variables which are assigned: dom(ρ) = {xi| ∃v ∈ Di.(xi, v) ∈ ρ} and if dom(ρ) = X
we refer to ρ as a *total assignment*. We say that a total assignment ρ is *valid*, if it satisfies all the rules which is denoted as ρ |= F.

A partial assignment ρ
′
**, dom**(ρ
′
) ⊆ X is *valid* if there is at least one total assignment ρ ⊇ ρ
′
that is valid ρ |= F, i.e. if there is at least one way to successfully finish the existing configuration process.

Example 1. Consider specifying a T-shirt by choosing the color (black, white, red, or blue), the size (small, medium, or large) and the print ("Men In Black" - MIB or "Save The Whales" - STW). There are two rules that we have to observe: if we choose the MIB print then the color black has to be chosen as well, and if we choose the small size then the STW print (including a big picture of a whale) cannot be selected as the large whale does not fit on the small shirt. The configuration problem (**X, D, F**) of the Tshirt example consists of variables X = {x1, x2, x3} representing color, size and print.

Variable domains are D1 = {black , white, red, blue}, D2 = {small, medium, **large**}, and D3 = {MIB, STW }. The two rules translate to F = {f1, f2}, where f1 =
(x3 = MIB) ⇒ (x1 = **black** ) and f2 = (x3 = STW ) ⇒ (x2 6= **small**). There are |D1||D2||D3| = 24 possible assignments. Eleven of these assignments are valid configurations and they form the solution space shown in Fig. 1. ♦

| (black, small, MIB)   | (black, large, STW )   | (red, large, STW )   |
|-----------------------|------------------------|----------------------|
| (black, medium, MIB)  | (white, medium, STW )  | (blue, medium, STW ) |
| (black, medium, STW ) | (white, large, STW )   | (blue, large, STW )  |
| (black, large, MIB)   | (red, medium, STW )    |                      |

Fig. 1. Solution space for the T-shirt example

## 2.1 User Interaction

Configurator assists a user interactively to reach a valid product specification, i.e. to reach total valid assignment. The key operation in this interaction is that of computing, for each unassigned variable xi ∈ X \dom(ρ), the *valid domain* D
ρ i ⊆ Di. The domain is *valid* if it contains those and only those values with which ρ can be extended to become a total valid assignment, i.e. D
ρ i = {v ∈ Di| ∃ρ
′
: ρ
′
|= F ∧ρ∪ {(xi, v)} ⊆ ρ
′}.