Constraint solver generates invalid solutions
Markus Triska <[email protected]> Fri, 18 Feb 2011 19:38:01 +0100
| Newsgroups | gmane.comp.gnu.prolog.bugs |
|---|---|
| Message-ID | <[email protected]> |
On a 2009 iMac (2.66 Intel Core 2 Duo, 4 GB RAM) with OSX 10.5.8, gprolog 1.3.1 produces invalid solutions (that is, they do not satisfy all posted constraints) to a finite domain constraint problem, as you can verify with the attached programs. The first program, fd_decompose.pl, solves a certain combinatorial problem (it enumerates all supersimple 16-4-2 designs that are decomposable, that is, each of them is the union of two 16-4-1 designs; "supersimple" means that every two blocks share at most two points). The second program, fd_decompose_verify.pl, is almost identical to the first program, except that it does not generate solutions, but reads them from standard input and uses the exact same constraint formulation to check whether the solution (is ground and) satisfies all constraints; a simple counter displays how many solutions were already read and checked. Compile both programs as usual with "gplc fd_decompose.pl" and "gplc fd_decompose_verify.pl", and then use them together with: $ ./fd_decompose | ./fd_decompose_verify The first few generated solutions are all valid: 0 1 2 3 4 ... but, after about 2 weeks of computation time, I get an invalid one: ... 22218 22219 wrong - ([[0, 1, 5, 14], [0, 2, 8, 13], [0, 3, 7, 11], [0, 4, 9, 12], [0, 6, 10, 15], [1, 2, 4, 6], [1, 3, 8, 9], [1, 7, 10, 12], [1, 11, 13, 15], [2, 3, 5, 12], [2, 7, 9, 15], [2, 10, 11, 14], [3, 4, 5, 6], [3, 4, 5, 6], [3, 4, 5, 6], [3, 4, 5, 6], [3, 4, 5, 6], [3, 4, 5, 6], [3, 4, 5, 6], [3, 4, 5, 6]] - [[0, 1, 7, 9], [0, 2, 12, 14], [0, 3, 5, 15], [0, 4, 6, 8], [0, 10, 11, 13], [1, 2, 10, 15], [1, 3, 4, 13], [1, 5, 8, 12], [1, 6, 11, 14], [2, 3, 7, 8], [2, 4, 9, 11], [2, 5, 6, 13], [3, 6, 10, 12], [3, 5, 7, 10], [3, 5, 7, 10], [3, 5, 7, 10], [3, 5, 7, 10], [3, 5, 7, 10], [3, 5, 7, 10], [3, 5, 7, 14]]). Please let me know if you need any further information. Thank you and all the best, Markus _______________________________________________ Bug-prolog mailing list [email protected] http://lists.gnu.org/mailman/listinfo/bug-prolog
fd_decompose.pl
(application/octet-stream, 4 KB)
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
construct supersimple (16-4-2) designs from two 16-4-1 designs
(every two blocks share at most TWO points)
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
run :- decomposable(40, Sol, Vs), fd_labelingff(Vs), portray_clause(Sol), format("\n", []), flush_output, fail.
decomposable(N, D1-D2, Vs) :-
N1 #= N / 2,
solution_(N1, D1, Vs1),
solution_(N1, D2, Vs2),
at_most_two_in_common(D1, D2),
D1 = [[_,_,X,_]|_],
D2 = [[_,_,Y,_]|_],
X #< Y,
append(Vs1, Vs2, Vs).
at_most_two_in_common([], _).
at_most_two_in_common([Block|Blocks], D2) :-
at_most_two_each(D2, Block),
at_most_two_in_common(Blocks, D2).
at_most_two_each([], _).
at_most_two_each([B|Bs], Block) :-
phrase(in_common(B, Block), Cs),
sum(Cs, #=, N),
N #< 3,
at_most_two_each(Bs, Block).
sum([], _, 0).
sum([V|Vs], _, N) :- sum(Vs, _, N1), N #= N1 + V.
in_common([], _) --> [].
in_common([X|Xs], Block) -->
in_common_(Block, X),
in_common(Xs, Block).
in_common_([], _) --> [].
in_common_([X|Xs], Y) -->
{ X #= Y #<=> B },
[B],
in_common_(Xs, Y).
five_times(Vs, N) :- fd_exactly(5, Vs, N).
length_(L, Ls) :- length(Ls, L).
chain([], _).
chain([V|Vs], Rel) :-
chain(Vs, V, Rel).
chain([], _, _).
chain([V|Vs], X, Rel) :-
call(Rel, X, V),
chain(Vs, V, Rel).
maplist(G, List) :-
all_call(List, G).
maplist(G, Ls1, Ls2) :-
all_call(Ls1, G, Ls2).
all_call([], _, []).
all_call([L|Ls], G, [X|Xs]) :-
call(G, L, X),
all_call(Ls, G, Xs).
all_call([], _).
all_call([A|As], G) :-
call(G, A),
all_call(As, G).
solution_(L, Schedule, Vars) :-
fd_set_vector_max(500),
length(Schedule, L),
maplist(length_(4), Schedule),
maplist(group, Schedule),
maplist(nth0(0), Schedule, Firsts),
chain(Firsts, #=<),
length(Five, 5),
append(Five, [F1,F2,F3,F4,F5,F6,F7|_], Schedule),
Schedule = [[0,1,_,_]|_],
ordered_by_second(Schedule),
maplist(first_is(0), Five),
maplist(first_is(1), [F1,F2,F3,F4]),
maplist(first_is(2), [F5,F6,F7]),
append(Schedule, Vars),
numlist(0, 15, Players),
maplist(five_times(Vars), Players),
players_meet_disjoint(Schedule),
rests_diff(Five),
rests_diff([F1,F2,F3,F4]),
rests_diff([F5,F6,F7]).
numlist(X, X, [X]) :- !.
numlist(A, B, [A|Rest]) :-
A1 is A + 1,
numlist(A1, B, Rest).
rests_diff(Ls) :-
maplist(rest, Ls, Rests),
append(Rests, Diff),
fd_all_different(Diff).
ordered_by_second([]).
ordered_by_second([_]) :- !.
ordered_by_second([[A,B|_],Second|Rest]) :-
Second = [C,D|_],
A #= C #==> B #< D,
ordered_by_second([Second|Rest]).
group(Group) :- chain(Group, #<).
rest([_|Rest], Rest).
first_is(N, [N|_]).
players_meet_disjoint(Groups) :-
phrase(groups_meets(Groups), Tuples),
findall([A,B,P], (fd_domain([A,B], 0, 15), A #< B,
P #= A*16+B, fd_labeling([A,B])), Table),
all_fd_relation(Tuples, Table),
maplist(nth0(2), Tuples, MeetVars),
fd_all_different(MeetVars).
all_fd_relation([], _).
all_fd_relation([T|Ts], Table) :-
fd_relation(Table, T),
all_fd_relation(Ts, Table).
groups_meets([]) --> [].
groups_meets([G|Gs]) --> group_meets(G), groups_meets(Gs).
group_meets([]) --> [].
group_meets([P|Ps]) --> group_meets(Ps, P), group_meets(Ps).
group_meets([], _) --> [].
group_meets([Q|Qs], P) --> [[P,Q,_]], group_meets(Qs, P).
append1([]) --> [].
append1([A|Rest]) --> list(A), append1(Rest).
list([]) --> [].
list([L|Ls]) --> [L], list(Ls).
append(A, B) :- phrase(append1(A), B).
nth0(0, [E|_], E) :- !.
nth0(N, [_|Rs], E) :-
N1 is N - 1,
nth0(N1, Rs, E).
:- initialization((run;halt)).
fd_decompose_verify.pl
(application/octet-stream, 4.5 KB)
/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
test supersimple (16-4-2) designs from two 16-4-1 designs
(every two blocks share at most TWO points)
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
:- dynamic(count/1).
count(0).
run :-
repeat,
count(N0),
format("~w ", [N0]),
N1 is N0 + 1,
retract(count(_)),
assertz(count(N1)),
read(Sol),
( nonvar(Sol), Sol = D1-D2, nonvar(D1), nonvar(D2),
maplist(valid_group, D1), maplist(valid_group, D2) ->
( decomposable(40, Sol, _) -> true
; portray_clause(wrong-Sol), halt
)
; portray_clause(indadmissible-Sol), halt
),
fail.
valid_group(G) :- nonvar(G), maplist(integer, G).
decomposable(N, D1-D2, Vs) :-
N1 #= N / 2,
solution_(N1, D1, Vs1),
solution_(N1, D2, Vs2),
at_most_two_in_common(D1, D2),
D1 = [[_,_,X,_]|_],
D2 = [[_,_,Y,_]|_],
X #< Y,
append(Vs1, Vs2, Vs).
at_most_two_in_common([], _).
at_most_two_in_common([Block|Blocks], D2) :-
at_most_two_each(D2, Block),
at_most_two_in_common(Blocks, D2).
at_most_two_each([], _).
at_most_two_each([B|Bs], Block) :-
phrase(in_common(B, Block), Cs),
sum(Cs, #=, N),
N #< 3,
at_most_two_each(Bs, Block).
sum([], _, 0).
sum([V|Vs], _, N) :- sum(Vs, _, N1), N #= N1 + V.
in_common([], _) --> [].
in_common([X|Xs], Block) -->
in_common_(Block, X),
in_common(Xs, Block).
in_common_([], _) --> [].
in_common_([X|Xs], Y) -->
{ X #= Y #<=> B },
[B],
in_common_(Xs, Y).
five_times(Vs, N) :- fd_exactly(5, Vs, N).
length_(L, Ls) :- length(Ls, L).
chain([], _).
chain([V|Vs], Rel) :-
chain(Vs, V, Rel).
chain([], _, _).
chain([V|Vs], X, Rel) :-
call(Rel, X, V),
chain(Vs, V, Rel).
maplist(G, List) :-
all_call(List, G).
maplist(G, Ls1, Ls2) :-
all_call(Ls1, G, Ls2).
all_call([], _, []).
all_call([L|Ls], G, [X|Xs]) :-
call(G, L, X),
all_call(Ls, G, Xs).
all_call([], _).
all_call([A|As], G) :-
call(G, A),
all_call(As, G).
solution_(L, Schedule, Vars) :-
fd_set_vector_max(500),
length(Schedule, L),
maplist(length_(4), Schedule),
maplist(group, Schedule),
maplist(nth0(0), Schedule, Firsts),
chain(Firsts, #=<),
length(Five, 5),
append(Five, [F1,F2,F3,F4,F5,F6,F7|_], Schedule),
Schedule = [[0,1,_,_]|_],
ordered_by_second(Schedule),
maplist(first_is(0), Five),
maplist(first_is(1), [F1,F2,F3,F4]),
maplist(first_is(2), [F5,F6,F7]),
append(Schedule, Vars),
numlist(0, 15, Players),
maplist(five_times(Vars), Players),
players_meet_disjoint(Schedule),
rests_diff(Five),
rests_diff([F1,F2,F3,F4]),
rests_diff([F5,F6,F7]).
numlist(X, X, [X]) :- !.
numlist(A, B, [A|Rest]) :-
A1 is A + 1,
numlist(A1, B, Rest).
rests_diff(Ls) :-
maplist(rest, Ls, Rests),
append(Rests, Diff),
fd_all_different(Diff).
ordered_by_second([]).
ordered_by_second([_]) :- !.
ordered_by_second([[A,B|_],Second|Rest]) :-
Second = [C,D|_],
A #= C #==> B #< D,
ordered_by_second([Second|Rest]).
group(Group) :- chain(Group, #<).
rest([_|Rest], Rest).
first_is(N, [N|_]).
players_meet_disjoint(Groups) :-
phrase(groups_meets(Groups), Tuples),
findall([A,B,P], (fd_domain([A,B], 0, 15), A #< B,
P #= A*16+B, fd_labeling([A,B])), Table),
all_fd_relation(Tuples, Table),
maplist(nth0(2), Tuples, MeetVars),
fd_all_different(MeetVars).
all_fd_relation([], _).
all_fd_relation([T|Ts], Table) :-
fd_relation(Table, T),
all_fd_relation(Ts, Table).
groups_meets([]) --> [].
groups_meets([G|Gs]) --> group_meets(G), groups_meets(Gs).
group_meets([]) --> [].
group_meets([P|Ps]) --> group_meets(Ps, P), group_meets(Ps).
group_meets([], _) --> [].
group_meets([Q|Qs], P) --> [[P,Q,_]], group_meets(Qs, P).
append1([]) --> [].
append1([A|Rest]) --> list(A), append1(Rest).
list([]) --> [].
list([L|Ls]) --> [L], list(Ls).
append(A, B) :- phrase(append1(A), B).
nth0(0, [E|_], E) :- !.
nth0(N, [_|Rs], E) :-
N1 is N - 1,
nth0(N1, Rs, E).
:- initialization((run;halt)).