SWI Prolog vs. GNU Prolog - CLP(FD) issues under SWI

Question

I wrote a quick predicate in Prolog trying out CLP(FD) and its ability to solve systems of equations.

problem(A, B) :-
    A-B #= 320,
    A #= 21*B.

When I call it in SWI, I get:

?- problem(A,B).
320+B#=A,
21*B#=A.

Whereas in GNU, I get the correct answer of:

| ?- problem(A,B).

A = 336
B = 16

What's going on here? Ideally I'd like to get the correct results in SWI as it's a much more robust environment.

Answer 1

This is a good observation.

At first glance, it will no doubt appear to be a shortcoming of SWI that it fails to propagate as strongly as GNU Prolog.

However, there are also other factors at play here.

The core issue

To start, please try the following query in GNU Prolog:

| ?- X #= X.

Declaratively, the query can be read as: X is an integer. The reasons are:

• (#=)/2 only holds for integers
• X #= X does not constrain the domain of the integer X in any way.

However, at least on my machine, GNU Prolog answers with:

X = _#0(0..268435455)

So, in fact, the domain of the integer X has become finite even though we have not restricted it in any way!

For comparison, we get for example in SICStus Prolog:

?- X #= X.
X in inf..sup.

This shows that the domain of the integer X has not been restricted in any way.

Replicating the result with CLP(Z)

Let us level the playing field. We can simulate the above situation with SWI-Prolog by artificially restricting the variables' domains to, say, the finite interval 0..2⁶⁴:

?- problem(A, B),
   Upper #= 2^64,
   [A,B] ins 0..Upper.

In response, we now get with SWI-Prolog:

A = 336,
B = 16,
Upper = 18446744073709551616.

So, restricting the domain to a finite subset of integers has allowed us to replicate the result we know from GNU Prolog also with the CLP(FD) solver of SWI-Prolog or its successor, CLP(Z).

The reason for this

The ambition of CLP(Z) is to completely replace low-level arithmetic predicates in user programs by high-level declarative alternatives that can be used as true relations and of course also as drop-in replacements. For this reason, CLP(Z) supports unbounded integers, which can grow as large as your computer's memory allows. In CLP(Z), the default domain of all integer variables is the set of all integers. This means that certain propagations that are applied for bounded domains are not performed as long as one of the domains is infinite.

For example:

?- X #> Y, Y #> X.
X#=<Y+ -1,
Y#=<X+ -1.

This is a conditional answer: The original query is satisfiable iff the so-called residual constraints are satisfiable.

In contrast, we get with finite domains:

?- X #> Y, Y #> X, [X,Y] ins -5000..2000.
false.

As long as all domains are finite, we expect roughly the same propagation strength from the involved systems.

An inherent limitation

Solving equations over integers is undecidable in general. So, for CLP(Z), we know that there is no decision algorithm that always yields correct results.

For this reason, you sometimes get residual constraints instead of an unconditional answer. Over finite sets of integers, equations are of course decidable: If all domains are finite and you do not get a concrete solution as answer, use one of the enumeration predicates to exhaustively search for solutions.

In systems that can reason over infinite sets of integers, you will sooner or later, and necessarily, encounter such phenomena.