Re: Constraint solver generates invalid solutions

Hi Daniel,

Daniel Diaz <[email protected]> writes:

>   DATE++;
>   if (DATE < 0)
>      DATE = 1;

I noticed you included this change in GNU Prolog 1.4.1. I have now
constructed a simpler test case which shows that this does not fix the
problem. GNU Prolog 1.4.1 still emits wrong answers within 5 days on an
iMac (2.66 GHz) with the following test case, which uses only a single
fd_all_different/1 constraint:

   run :-
           L = 20,
           length(Ls, L),
           fd_domain(Ls, 1, L),
           fd_all_different(Ls),
           fd_labeling(Ls),
           portray_clause(Ls),
           false.

I'm attaching two files that let you reproduce the problem:

   alldif.pl: Posts fd_all_different/1, labels and emits all solutions

   alldif_verify.pl: Reads solutions from stdin and verifies them

Just compile them as usual with "gplc alldif.pl" and "gplc
alldif_verify", and then use them together with:

   $ ./alldif | ./alldif_verify

alldif_verify emits a line every 10.000th solution. The first few
million solutions are all valid:

   0.
   1.
   2.
   3.
   ....

but after about 5 days, GNU Prolog 1.4.1 emits an answer that does not
satisfy the fd_all_different/1 constraint:

   ...
   124964.
   124965.
   false - [1, 2, 3, 4, 5, 6, 7, 10, 16, 12, 14, 8, 18, 11, 20, 17, 19, 13, 9, 13].

Please let me know if you need any further information.

Thank you and all the best,
Markus

_______________________________________________
Bug-prolog mailing list
[email protected]
https://lists.gnu.org/mailman/listinfo/bug-prolog

run :-
        L = 20,
        length(Ls, L),
        fd_domain(Ls, 1, L),
        fd_all_different(Ls),
        fd_labeling(Ls),
        portray_clause(Ls),
        false.

:- initialization(run).

:- dynamic(count/1).
:- dynamic(count_mod/1).

count(0).

count_mod(0).

run :-
        repeat,
        count(N0),
        retract(count(_)),
        (   N0 =:= 10000 ->
            assertz(count(0)),
            count_mod(M0),
            retract(count_mod(_)),
            M1 is M0 + 1,
            assertz(count_mod(M1)),
            format("~w.\n", [M0])
        ;   N1 is N0 + 1,
            assertz(count(N1))
        ),
        read(Ls),
        (   nonvar(Ls), fd_all_different(Ls) ->
            true
        ;   portray_clause(false-Ls), halt
        ),
        false.

:- initialization(run).