[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: A question on FD solver
Re: A question on FD solver
Tue, 25 Mar 2003 12:21:32 +0100
Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.0.2) Gecko/20021120 Netscape/7.01
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,...).
X #=< D + V,
X #>= D + 2.
D <--- X --->
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):
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)
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)
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:
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:
LD1 = [X1,X2,X3,X4],
LD2 = [D1,D2],
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
- 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.
Ce message a subi une analyse antivirus
par MailScanner ; il est vraisemblablement