

![0_image_0.png](0_image_0.png) 
assignment ρ = ρold ∪ {(**x, v**)}. For every variable xi ∈ X, old valid domains are denoted as D
ρold i, i = 0**, . . . , n** − 1. and the old BDD Bρold is reduced to the restricted BDD, Bρ(V, E, Xb**, var**). The **CV D** functionality is to calculate valid domains D
ρ i for remaining unassigned variables xi 6∈ dom(ρ) by extracting values from the newly restricted BDD Bρ(V, E, Xb**, var**).

To simplify the following discussion, we will analyze the isolated execution of the CV D algorithms over a given BDD B(V, E, Xb**, var**). The task is to calculate valid domains V Di from the starting domains Di. The user-configurator interaction can be modelled as a sequence of these executions over restricted BDDs Bρ, where the valid domains are D
ρ i and the starting domains are D
ρold i.

The **CV D** functionality is delivered by executing two algorithms presented in Fig.

5 and Fig. 6. The first algorithm is based on the key idea that if there is an edge e =
(u1, u2) crossing over Vj , i.e. var1(u1) **< j < var**1(u2) then we can include all the values from Dj into a valid domain V Dj ← Dj .

We refer to e as a *long edge* of length var1(u2) − var1(u1). Note that it skips var(u2) − var(u1) Boolean variables, and therefore compactly represents the part of a solution space of size 2 var(u2)−var(u1).

For the remaining variables xi, whose valid domain was not copied by **CV D** −
Skipped, we execute CV D(**B, x**i) from Fig. 6. There, for each value j in a domain D′i we check whether it can be part of the domain Di. The key idea is that if j ∈ Dithen there must be u ∈ Vi such that traversing the BDD from u with binary encoding of j