Re: [eclipse-clp-users] ECLiPSe - Real variables domain propagation problem

From: Joachim Schimpf <joachim.schimpf_at_infotech.monash.edu.au>
Date: Fri, 24 Jul 2009 11:38:36 +1000
Wayne Mac Adams wrote:
> Or even just a simpler way to represent it is to just focus on the
> following query(assuming the ic librarby is loaded)
> 
> ?- A :: 0.0 .. 0.5, [B, C] :: 0.0 .. 1.0, A $= eval(B + C - B * C).
> A = A{0.0 .. 0.5}
> B = B{0.0 .. 1.0}
> C = C{0.0 .. 1.0}
> There are 4 delayed goals.
> Yes (0.00s cpu)
> 
> If i had
> ?- A :: 0.0 .. 0.5, [B, C] :: 0.0 .. 1.0, A $= eval(B + C).
> A = A{0.0 .. 0.5}
> B = B{0.0 .. 0.5}
> C = C{0.0 .. 0.5}
> There is 1 delayed goal.
> Yes (0.00s cpu)
> 
> it propagates correctly.
> 
> I have been told( by Helmut Simonis, and I hope I paraphrase this
> correctly!) it is because ECLiPSe treats B+C and B*C as seperate and not
> foesn't see the it as as the same terms being used.

There are two aspects here:
(1)  you seem to expect too much from propagation generally
(2)  A $= B+C-B*C could propagate more than it actually does


As for (1), all that constraint propagation does is to remove
"impossible" values from the domains, i.e. values that do not
occur in any solution to the problem.  But there is no guarantee
that propagation removes _all_ impossible values.  In fact, as
soon as you have more than a single constraint, you can be almost
certain that this is not the case.  Even if the individual constraints
have this property (i.e. achieve "generalised arc consistency"),
an arbitrary combination of them will not (in general).
To prove that a value is part of a solution, you have to find
a concrete solution with this value, you cannot rely on propagation
alone.


As for (2): individual constraints can often be implemented such
that they achieve "generalised arc consistency", i.e. remove all
impossible domain values.  But even that is not always done,
simply because it may be too computationally expensive, or,
like in this particular case, because what looks like a single
constraint in your model is actually implemented by decomposition:
The source constraint

  A $= B+C-B*C

is broken up into two constraints, representing the linear
and the nonlinear part of your equation separately:

  A $= B+C-Aux,  Aux $= B*C

If you look at these two constraints separately, you see that none
of them (individually) can achieve more propagation than it does:

  Aux{0.0 .. 1.0} - C{0.0 .. 1.0} - B{0.0 .. 1.0} + A{0.0 .. 0.5} $= 0,
  Aux{0.0 .. 1.0} $= B{0.0 .. 1.0} * C{0.0 .. 1.0}

Although it would be possible to make an implementation of A $= B+C-B*C
without decomposition that achieves full arc consistency, the example
shows that as soon as you add other constraints, you lose the property
again.


>...
> 
>     Does anyone know how to solve this problem?
>     It forms part of a larger problem in which I am getting an incorrect
>     result because of the domains staying between 0.0..1.0.

The issue is that you are not interpreting the "result" correctly: the fact
that there are "delayed goals" left at the end of the computation implies
that the problem is not actually solved, and the domains may or may not
contain solutions.  The only guarantee you have is that any solutions
(should they exist) are within the computed domains.

In an integer problem you would at this point use labeling/indomain to
find concrete integer solution values.  Since you are working with reals,
it is more tricky, because of numerical inaccuracies - some of it is
discussed in http://eclipse-clp.org/doc/tutorial/tutorial063.html

To get more restricted domains in your example, you could use

?- A::0.0..0.5, [B,C]::0.0..1.0, A $= B+C-B*C, squash([A,B,C], 0.001, log).
A = A{0.0 .. 0.5}
B = B{0.0 .. 0.50091762095689774}
C = C{0.0 .. 0.50091762095689774}
There are 4 delayed goals.
Yes (0.00s cpu)

squash/3 is a search procedure that splits domains and excludes ranges
if they can be shown not to contain any solutions.


-- Joachim
Received on Fri Jul 24 2009 - 02:39:27 CEST

This archive was generated by hypermail 2.2.0 : Thu Feb 02 2012 - 02:31:58 CET