Four-color theorem in Prolog (using a dynamic predicate)

I'm working on coloring a map according to the four-color theorem (http://en.wikipedia.org/wiki/Four_color_theorem) with SWI-Prolog. So far my program looks like this:

colour(red).
colour(blue).

map_color(A,B,C) :- colour(A),
         colour(B),
         colour(C),
         C \= B,
         C \= A.

(the actual progam would be more complex, with 4 colors and more fields, but I thought I'd start out with a simple case)

Now, I want to avoid double solutions that have the same structure. E.g. for a map with three fields, the solution "red, red, blue" would ha开发者_如何学编程ve the same structure as "blue, blue, red", just with different color names, and I don't want both of them displayed.

So I thought I would have a dynamic predicate solution/3, and call assert(solution(A,B,C)) at the end of my map_color predicate. And then, for each solution, check if they already exist as a solution/3 fact. The problem is that I would have to assert something like solution(Color1,Color1,Color2), i.e. with variables in order to make a unification check. And I can't think of a way to achieve this.

So, the question is, what is the best way to assert a found solution and then make a unification test so that "red, red, blue" would unify with "blue, blue, red"?

To build relation between variables:

mask_helper(_, _, [], []).
mask_helper(A, B, [A|_], [B|_]):- !.
mask_helper(A, B, [X|Xs], [_|Ys]):-
    A \= X,
    mask_helper(A, B, Xs, Ys).

mask([], []).
mask([X|Xs], [Y|Ys]):-
    mask_helper(X,Y,Xs,Ys),
    mask(Xs, Ys).

and you can build your mask:

?- mask([red,red,blue],X).
X = [_G300, _G300, _G306] .

but:

?- mask([red,red,blue],X), mask([blue,red,red],Y), X=Y.
X = [_G27, _G27, _G27],
Y = [_G27, _G27, _G27].

I.e. there is no relation about Color1 \= Color2 if you will use assert (without rule body).

You may consider somethin like ordering of assigning colours (pretty popular approach):

colour(red). colour(green). colour(blue).

colour_order(red, red).
colour_order(red, green).
colour_order(red, blue).
colour_order(green, green).
colour_order(green, blue).

colour_code([]).
colour_code([X]):- colour(X).
colour_code([X|[Y|T]]):-
    colour_order(X,Y),
    colour_code([Y|T]).

map_color(A,B,C):-
    colour_code([A,B,C]),
    C \= B, C \= A.

But again you will never get result "red, blue, red" if your conditions will be A \= B, B \= C.

Think about:

unify([], [], _).
unify([X|Xs], [Y|Ys], M):-
    member((X=Z), M), !,
    Z = Y,
    unify(Xs, Ys, M).

unify([X|Xs], [Y|Ys], M):-
    % X is not assigned yet
    not(member((_=Y),M)), % Y is not used as well
    unify(Xs, Ys, [(X=Y)|M]).

Than you can compare:

?- unify([red,red,blue],[blue,blue,red],[]).
true.

?- unify([red,red,blue],[blue,blue,blue],[]).
false.

?- unify([red,red,blue],[blue,red,red],[]).
false.

I think that the simplest solution is to say that A has always the color red (for example).