Re: A question on FD solver

[Daniel Diaz]

There is no bug here, FD constraint solving is based on consistency 
techniques and propagation. Meaning that the domain of each variables is 
updated (reduced) when constraints are added. This only ensures that, 
for each variable, all solutions are in the current domain (but not the 
reverse: some values are not solutions). The domain of a variable is 
then an approximation of the set of all solutions. For classical 
arithmetic constraints only the bounds of the variables are propagated 
(the min..max) (called 	arc-consistency). This is done for each 
constraint independently of all other constraints.

To find actual solutions among values in the domain we have to try each 
of them one by one. This is done by the labeling phase. For a variable X 
with a domain D1, D2,..., Dn this phase tries to unify X with D1, with 
D2,... by backtraking. It is then equivalent to (X=D1; X=D2;...;X=Dn).

Here is a simplified version of your example (basically V is Va, all 
domains are 0..4, V is Va, X is X3, D is D2, X1 has been replaced by 0, 
X4 is replaced by 2+D2,...).

eq(X,D,V):-
        fd_domain([X,D,V],0,4),
        X #=< D + V,
        X #>= D + 2.
I.e.

D  <--- X --->
|--|---------|
  +2        +V

This has a solution iif V >= 2 but this is not discovered by simple 
arc-consistency as shown below:

| ?- eq(X,D,V).

D = _#25(0..2)
V = _#47(0..4)
X = _#3(2..4)

V is 0..4

The arc-consistency deduces (briefly):

for X:
  max(X) <= max(D) + max(V)
  (which is greater than 4, given by fd_domain), so noting is deduced.
  min(X) >= min(D) + 2. Thus X is in 2..4 (i.e. X >= 2)

for D:
  min(D) >= min(X) - max(V) = 0-2 = -2 (less than 0, nothing deduced)
  max(D) <= max(X) - 2 = 4-2 = 2. Thus D is in 0..2 (i.e. D <= 2)

for V:
  min(V) >= min(X) - max(D) = 2 - 2 = 0
  max(V) is not constrained, Thus V is in 0..4 (not reduced)

Thus for V, arc-consistency does not discover V>=2. For this we would 
have to combine both constraints:
we have  X<=D+V ie. V>=X-D
we also have  X>=D+2  ie.  X-D>=D+2-D ie X-D>=2
from V>=X-D and X-D>=2 we can deduce V>=2
But arc-consistency does not perform this kind of deduction (it would 
need to have a global view of all constraints, instead arc-consistency 
has only a local view but... it is also fast for this reason :-)).

We then need a labeling pahse to discover solutions (with V >= 2).

I hope this clarifies things.


Xiaohua Kong wrote:
> Hi,
>  
> I am using FD solver to work on some verification problem that is 
> modeled as CSP problem. Since most constraints are linear, I choose 
> partial consistency operators in FD solver.
> Here is a small example:
>  
> ========================
> ieq(LD1,LD2,Va):-
> LD1 = [X1,X2,X3,X4],
> LD2 = [D1,D2],
> fd_domain(LD1,0,20),
> fd_domain(LD2,1,12),
> Va #=<5,
> Va #>=0,
> X1 #= 0,
> X2 #=< X1+4,
> X2 #>= X1+2,
> X3 #= X1+D1,
> X4 #= X2+D2,
> D1 #=< D2+Va,
> D1 #>= D2-Va,
> X4 #=< X3.
> ===========================
> By asking ieq(LD1,LD2,Va).
> The solver gives answer:
> LD1 = [0,_#25(2..4),_#47(3..12),_#69(3..12)]
> LD2 = [_#91(3..12),_#113(1..10)]
> Va = _#134(0..5)
> However, there is no assignment exsits if Va=0.
> Actually, labeling Va will return give answer that Va could b [2,5].
> ==============================================
>  
> Several questions on this penominon:
> - Is there any problem with the code? Or it is a problem that caused by 
> the algrithm.
> - Without labeling, if the solver gives answer "yes" and return a 
> domain, does that means there exist at least one solution? (Even though 
> the answer of the variable domains is not accurate).
> - The computation cost of labeling.
>  
> Thanks
> Xiaohua Kong



--
Ce message a subi une analyse antivirus 
par MailScanner ; il est vraisemblablement
sans danger.