CLPB: sat does not make input variables unify but instead uses fresh variables

[jasagredo]

I have been some time trying to solve the last problem in Advent of Code, and after a lot of debugging I came across this behavior of CLPB which I find extremely surprising.

First of all, this works as expected, A is unified with 1.

?- sat(card([1], [A])).
   A = 1.

Now if I print the variable A before and after the call to sat, it seems correct too:

?- write(A), nl, sat(card([1], [A])), write(A).
_912647
1   A = 1.

But if A is not fully constrained by the call to sat, I get the following response:

?- write(A), nl, sat(card([0,1], [A])), write(A).
_912647
_913236   clpb:sat(A=:=A).

Notice how the variable for A before and after the call to sat is a different variable.
In my attempt to solve the puzzle, I have a set of variables on which I assert constraints using sat on them, but the reality is that whatever I assert does not make the list of variables I carry around unify with anything. Fresh variables are using for the results of the sat calls.

I tried using portray_clause/1 to see if the variable names before and after were rewritten to different names, and they are not, although it rewrites X to A:

?- portray_clause((write(X), nl, sat(card([0,1], [X])), write(X))).
(write(A),nl,sat(card([0,1],[A])),write(A)).
   true.

I defined this as a predicate and asked for the listing/1 of it:

?- listing(foo/0).
foo :-
   write(A),
   nl,
   sat(card([0,1],[A])),
   write(A).
   true.

and it still refers to the same variable name A.

The code in my solution looks for example like this:

write(sat(card([0,1], Vs))), nl,
sat(card([0,1], Vs)),
write(nooverlap2(Vs)), nl

and I get this:

sat(card([0,1],[_918411]))
nooverlap2([_920752])

[jasagredo]

I deleted a comment because I have done a rookie mistake in the example which would never succeed and was only adding noise.

I think I might have found the cause. This code:

a(X) :-
    member(A, X),
    write(a(A)), nl,
    sat(card([1], [A])),
    write(a(A)), nl.

b(X) :-
    member(A, X),
    write(b(A)), nl,
    sat(card([0], [A])),
    write(b(A)), nl.

foo :-
    X = [_],
    write(X), nl,
    a(X),
    write(X), nl,
    b(X),
    write(X), nl.

fails as expected:

?- foo.
[_863241]
a(_863241)
a(1)
[1]
b(1)
   false.

but this other code, succeeds:

a(X) :-
    forall(
        member(A, X),
        ( write(a(A)), nl,
          sat(card([1], [A])),
          write(a(A)), nl
        )
    ).

b(X) :-
    forall(
        member(A, X),
        ( write(b(A)), nl,
          sat(card([0], [A])),
          write(b(A)), nl
        )
    ).

foo :-
    X = [_],
    write(X), nl,
    a(X),
    write(X), nl,
    b(X),
    write(X), nl.

?- foo.
[_864972]
a(_864972)
a(1)
[_864972]
b(_864972)
b(0)
[_864972]
   true.

And it seems like it would be unifying _864972 with 1 and later on with 0. However in the previous example in this same message it can be seen that the call to sat replaces all the references it knows about with the new variable, in particular the one in the original list. But with the forall/2 pattern it seems it doesn't know that the variable it is using is in some other structure in other place.

I can concieve that forall/2 being one of those special meta-predicates, generates fresh variables on each attempt, but the weird thing is that the variable it picks and is given to sat is precisely the one in X, in this case _864972 and yet it breaks the relation.

[triska]

I think there are two separate questions:

First, why does the character sequence representing the variable change? We have:

7.10.5 Writing a term

When a term Term is output using write_term/3 (8.14.2)
the action which is taken is defined by the rules below:

  a) If Term is a variable, a character sequence repre-
  senting that variable is output. The sequence begins
  with _ (underscore) and the remaining characters are
  implementation dependent. The same character sequence
  is used for each occurrence of a particular variable in
  Term. A different character sequence is used for each
  distinct variable in Term.

So, it is perfectly conforming behaviour to print a different sequence, even for the same variable, every time write/1 is used. In practice, there may of course be little reason for an implementation to randomly change the output sequence for the same variable. But what if something in fact did change, affecting the variable? For example, we have:

?- write(A), clpb:put_visited(A), write(A).
_95_477   clpb:put_atts(A,clpb_visited(true)).

Where put_visited/1 is defined as:

put_visited(V) :- put_attr(V, clpb_visited, true).

In this case, a so-called attribute was attached to the variable, and that apparently had an effect on the output. Perfectly OK, write/1 still satisfies all guarantees we need to reliably read such a term back when needed. If needed, the variable_names/1 option can be used for writing to guarantee specific names:

?- write_term(A, [variable_names(['A'=A])]),
   clpb:put_visited(A),
   write_term(A, [variable_names(['A'=A])]).
AA   clpb:put_atts(A,clpb_visited(true)).

[jasagredo]

I see. In the past I have used the numbers of the variables to track whether I was looking at the same variable or not. I expected it to be implementation dependent but this was the first time I can remember I mutated something in place where it was not a unification (and since then I would not see the variable numbers).

Thanks for the explanation.

[triska]

See also the current standard, which has the variable_names/1 option:

https://www.complang.tuwien.ac.at/ulrich/iso-prolog/draft-7.10.5#a2

[triska]

The second question pertains to forall/2:

In my opinion, forall/2 should be removed from library(iso_ext), since its name suggests more than it provides, I think there is also a discussion about this, even though I see no open issue about it at the moment.