29 lines
1.2 KiB
Plaintext
29 lines
1.2 KiB
Plaintext
%#show path/7.
|
|
#show satisfiable/0.
|
|
#show unsatisfiable/0.
|
|
dom(a). dom(b). dom(c).
|
|
%tri(a,a,a). tri(a,b,c).
|
|
%tri(b,b,b). tri(b,c,a).
|
|
%tri(c,c,c). tri(c,a,b).
|
|
tri(a,b,c). tri(a,c,b).
|
|
tri(b,a,a). tri(b,b,b).
|
|
tri(c,a,c). tri(c,c,a).
|
|
|
|
same(X,Y,Z, X,Y,Z) :- tri(X,Y,Z).
|
|
|
|
% There is an edge if two triplet have a common letter
|
|
edge(X,Y,Z, X1,Y1,Z1) :- tri(X,Y,Z), tri(X1,Y1,Z1), not same(X,Y,Z, X1,Y1,Z1), X = X1.
|
|
edge(X,Y,Z, X1,Y1,Z1) :- tri(X,Y,Z), tri(X1,Y1,Z1), not same(X,Y,Z, X1,Y1,Z1), Y = Y1.
|
|
edge(X,Y,Z, X1,Y1,Z1) :- tri(X,Y,Z), tri(X1,Y1,Z1), not same(X,Y,Z, X1,Y1,Z1), Z = Z1.
|
|
|
|
%path(X,Y,Z, XF,YF,ZF) :- edge(X,Y,Z, X1,Y1,Z1), edge(X1,Y1,Z1, X2,Y2,Z2), edge(X2,Y2,Z2, XF,YF,ZF), not same(X1,Y1,Z1, XF,YF,ZF), not same(X,Y,Z, X2,Y2,Z2).
|
|
|
|
% The 1 and 0 are used to diferentiate the two type of vertice
|
|
% If it is 0 the path stoped in the first type and must then go to the other type and vice versa
|
|
path(X,Y,Z, XF,YF,ZF, 1) :- edge(X,Y,Z, XF,YF,ZF).
|
|
path(X,Y,Z, XF,YF,ZF, 0) :- path(X,Y,Z, X1,Y1,Z1, 1), edge(X1,Y1,Z1, XF,YF,ZF).
|
|
path(X,Y,Z, XF,YF,ZF, 1) :- path(X,Y,Z, X1,Y1,Z1, 0), edge(X1,Y1,Z1, XF,YF,ZF).
|
|
|
|
satisfiable() :- tri(X,Y,Z), not path(X,Y,Z, X,Y,Z, 1).
|
|
unsatisfiable() :- tri(X,Y,Z), path(X,Y,Z, X,Y,Z, 1).
|