Toggle navigation
?
users online
Logout
Open hangout
Open chat for current file
% Un programme SWI-Prolog résolvant naivement les problèmes NP-complets HC, VC, and SAT :- use_module(library(lists)). % Un graphe simple non-orienté est représenté par sa liste de sommets et d'arêtes. % 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 problème 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 ≤ à 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 problème SAT % une variable propositionnelle est représenté 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 négatif). % Par exemple : p(a), n(x) % Une clause est représentée par la liste de ses littéraux. % Par exemple : a ∨ ¬ b ∨ c se note [p(a),n(b),p(c)] % Une CNF est représentée par la liste des ses clauses. % Par exemple : (¬ a ∨ b) ∧ (¬ b ∨ 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 ∨ y) ∧ (x ∨ ¬ z) ∧ (¬ x ∨ y) ∧ (y ∨ z) f3([[p(x),p(y)],[p(x),n(z)],[n(x),p(y)],[p(y),p(z)]]). % (x ∨ y) ∧ (z ∨ ¬ t) ∧ (x ∨ t) ∧ (x ∨ z) ∧ (¬ y ∨ 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 ∨ b, ¬ b ∨ ¬ 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 interprétation qui valide CNF, % ie, I est une interprétation des variables de CNF qui est un modèle 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). */