Re: Problem with CLP

[Lars Riis Olsen]

Fergus Henderson wrote:

> In general, a CLP system can give three kinds of results to a query:
>
> 1. the query is definitely satisfiable
> 2. the query is possibly satisfiable, subject to some constraints
> 3. the query is definitely unsatisfiable
>
> These three cases correspond to "yes", "maybe", and "no", respectively.
>
> A good CLP system will distinguish between cases 1 and 2 in its 
responses,
> for example by printing out a representation of the remaining unresolved
> constraints for case 2.  However, many CLP systems -- including GNU
> Prolog -- fail to distinguish these cases.  GNU Prolog just prints out
> the variable bindings, and some information about the maximum possible
> ranges of constrained variables, but it does not print out any remaining
> unresolved constraints or indeed give any indication that there might
> be unresolved constraints, and instead of printing out "maybe" for 
case 2,
> it misleadingly prints "yes".
>
> This is IMHO a significant flaw in the GNU Prolog user interface.
>
> > From the query it should be clear that it is indeed not satisfiable.
> > Furthermore to recheck this I tried to further constraint the value of
> > the variable X to be eg. 0. In this case it comes up with the correct
> > answer (no). The same happens if X is instead constrained to 1,2,3...
> > and so forth.
>
> Once you bind the variables, the unresolved constraints can be evaluated.
> Then the query results will be either in category 1 or 3, and will match
> what you expect.

So if I am understanding you correctly there is no way of determining 
whether a "yes" result returned by GNU Prolog is correct. Maybe except 
from binding one of the variables with each of its possible values to 
check whether any of them returns "yes" (which obviuosly is immensely 
ugly and not at all feasable for large ranges.). Is this correct a 
correct interpretation of your previous post?.

In that case, do you know of any free constraint satisfiability 
package(s), with a C interface, that does not have this limitation?.

\Lars