Search code examples
prologclpfd

CLPFD and infinite countable domains

I #> 0, I #< 10, indomain(I).

The previous code obviously does the following:

I = 1 ;
I = 2 ;
I = 3 ;
I = 4 ;
I = 5 ;
I = 6 ;
I = 7 ;
I = 8 ;
I = 9.

The following code does not work (arguments are not sufficiently instantiated):

I #> 0, indomain(I).

Now I understand that there are in this case an infinite number of possible bindings for I, and that CLPFD works for finite domains as its name suggests.

However I don't understand why this limitation exists in this particular case. Isn't it possible to enumerate possible solutions from smallest to biggest norm, and get the following:

I = 1 ;
I = 2 ;
I = 3 ;
.
.
.

Even for problems where there are more than one variables, say:

0 #< I, I #< J, label([I,J]).

Why wouldn't it be possible to implement it such that the following behavior occurs:

I = 1,
J = 2 ;
I = 1,
J = 3 ;
I = 2,
J = 3 ;
I = 1,
J = 4 ;
.
.
.

In short: why doesn't CLPFD still work for infinite domains if those domains are easily countable using amplitude?

Solution

  • The reason for this is that CLP(FD) preserves the following important property:

    If a predicate p(Vs) terminates universally, then ?- p(Vs), label(Vs). also terminates universally.

    A goal G terminates universally iff ?- G, false. terminates.

    Why is this so important? Because a CLP(FD) program typically consists of two parts:

    1. posting all constraints
    2. the search for solutions.

    It is often easy to show, by simple inspection, that the modeling part (1) terminates universally. But (2) is the tough part that usually takes most of the computation time, and often we do not know a priori whether there even is a single solution. The search part may run for days, months or years without yielding results.

    Many Prolog beginners describe a search task, run it, and after a few seconds complain that Prolog is slow. In reality, as it turns out, they often accidentally write programs that do not terminate, and can never find a solution.

    For such reasons, it is encouraging that if you can only show (as you typically can, and also rather easily) that part (1) terminates, then your whole program—part (1) and part (2)—also terminates.

    You are completely right that any countably infinite search space can be systematically covered to any finite extent in one of the ways you are describing. However, doing so would break this fundamental invariant. You must be able to count on the following property for the above reasoning to apply:

    label/1, labeling/2 and indomain/1 always terminate.

    In SWI-Prolog and YAP, this is ensured by design. In other systems it holds to varying degrees.