Re: Problem with CLP

[Fergus Henderson]

On 22-Sep-2003, Lars Riis Olsen <address@hidden> wrote:
> I am new to GNU Prolog and I have run into a problem concerning its CLP 
> extension. I don't know whether it is a bug or whether it is just me who 
> have misunderstood something. The problem is that GNU Prolog says that 
> the following query is satisfiable:
> 
> fd_domain(X,0,15), fd_domain(Y,0,15), (((X #< Y) #/\ ((Y-X) #> 8))   
> #\/   ((X #> Y) #/\ ((X - Y) #< 8))) #/\   (((X #< Y) #/\ ((Y-X) #< 
> 8))   #\/   ((X #> Y) #/\ ((X - Y) #> 8))).
> 
> more specifically it returns the following answer:
> 
> X = _#3(0..15)
> Y = _#25(0..15)

Furthermore, after printing that out, it also prints out "yes".

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.

-- 
Fergus Henderson <address@hidden>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.