% Un programme SWI-Prolog resolvant naivement les problemes NP-complets HC, VC, and SAT

:- use_module(library(lists)).
	
% Un graphe simple non-oriente est represente par sa liste de sommets et d'aretes.
% Voici deux tels graphes :

ge1(graph([a,b,c,d,e],[a-b,a-c,a-d,b-c,b-d,b-a,c-d,d-e,e-a])).
ge2(graph([a,b,c,d,e],[a-b,a-c,a-d,b-c,b-d,b-a,c-d,d-a])).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% hc(G,HC) ssi HC est un circuit hamiltonien de G
% ie, HC est une permutation des sommets de G qui est un circuit de G.

hc(G,HC) :- 
    G = graph(Vs,_),
    % NB : le probleme n'a pas de solution pour les graphes avec 1 ou 2 sommets
    length(Vs,N), N > 2, 
    permutation(Vs,Ws),
    Ws = [X|_], 
    append(Ws,[X],HC),
    circuit(HC,G).

circuit(Circuit,G) :-
    G = graph(_,Es),
	forall(append(_,[V1,V2|_],Circuit),
           (member(V1-V2,Es) ; member(V2-V1,Es))).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% vc(G,Max,C) ssi C est une couverture de sommets de G de taille =< a Max
% ie, C est un sous-ensemble des sommets de G de taille =< Max qui couvre G.

vc(G,Max,C) :- 
    G=graph(Vs,_),
    between(1,Max,N),
    length(C,N),
    is_subset(C,Vs),
    cover(C,G).

is_subset([],_).
is_subset([X|Xs],[X|Ys]) :- is_subset(Xs,Ys).
is_subset([X|Xs],[_|Ys]) :- is_subset([X|Xs],Ys).

cover(C,G) :-
    G = graph(_,Es),
    forall(member(X-Y,Es),
           (member(X,C) ; member(Y,C))).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Le probleme SAT

% une variable propositionnelle est represente par une suite non vide de minuscules.
% Par exemple : a, b, c, ab, p, q, x, y, z, xyz, 
% Un litteral est un terme de la forme p(VP) (litteral positif) ou n(VP) (litteral negatif).
% Par exemple : p(a), n(x) 
% Une clause est representee par la liste de ses litteraux.
% Par exemple : a v -b v c se note [p(a),n(b),p(c)]
% Une CNF est representee par la liste des ses clauses.
% Par exemple : (-a v b) ^ (-b v a) se note [[n(a),p(b)],[n(b),p(a)]]
% Voici d'autres CNF :

% p v -p
f1([[p(p),n(p)]]).    

% (p) ^ (-p)
f2([[p(p)],[n(p)]]).  

% (x v y) ^ (x v -z) ^(-x v y ) ^ (y v z)
f3([[p(x),p(y)],[p(x),n(z)],[n(x),p(y)],[p(y),p(z)]]).

% (x v y) ^ (z v -t) ^ (x ^ t) ^ (x v z) ^ (-y v t )
f4([[p(x),p(y)],[p(z),n(t)],[p(x),p(t)],[p(x),p(z)],[n(y),p(t)]]).

% a => b, b => c, c => a
f5([[n(a),p(b)],[n(b),p(c)],[n(c),p(a)]]).

% a => b, b => c, c => a, a v b, -b v -c
f6([[n(a),p(b)],[n(b),p(c)],[n(c),p(a)],[p(a),p(b)],[n(b),n(c)]]).

% sat(CNF,I) ssi I est une interpretation qui valide CNF,
% ie, I est une interpretation des variables de CNF qui est un modele de CNF.

sat(CNF,I) :- 
    vars(CNF,Vars), 
    interpretation(Vars,I), 
    models(I,CNF).

vars([],[]).
vars([D|Ds],Ws) :- varsd(D,V), vars(Ds,Vs), union(V,Vs,Ws).

varsd([],[]).
varsd([p(I)|Ls],Vs) :- varsd(Ls,Ws), union([I],Ws,Vs).
varsd([n(I)|Ls],Vs) :- varsd(Ls,Ws), union([I],Ws,Vs).

interpretation([],[]).
interpretation([I|Is],[I-Bool|Inters]) :- bool(Bool), interpretation(Is,Inters).

bool(0). 
bool(1).

models(I,CNF) :- and_model(CNF,I).

and_model([],_).
and_model([D|Ds],I) :- or_model(D,I), and_model(Ds,I).

or_model([p(N)|_],I)    :- member(N-1,I).
or_model([p(N)|Disj],I) :- member(N-0,I), or_model(Disj,I).
or_model([n(N)|_],I)    :- member(N-0,I).
or_model([n(N)|Disj],I) :- member(N-1,I), or_model(Disj,I).
  


/** <examples>
?- ge1(G).
?- ge2(G).
?- ge1(G),hc(G,HC).
?- ge2(G),hc(G,HC).
?- ge1(G),vc(G,3,C).
?- ge1(G),vc(G,2,C).
?- f1(F),sat(F,I).
?- f2(F),sat(F,I).
?- f3(F),sat(F,I).
?- f4(F),sat(F,I).
?- f5(F),sat(F,I).
?- f6(F),sat(F,I).
*/

