% ACYCLICITY CHECK FOR UNDIRECTED GRAPHS (FORESTS) % % Intuitive readings for predicates: % % node(X) = X is a node % level(L) = L is a level in the deletion of nodes % pair(X,Y) = Ordered pair (X,Y) representing an undirected edge {X,Y} % maps(X,Y,X1,Y1) = Maps nodes of undirected edge {X,Y}={Y,X} to pair (X1,Y1) % del(X,L) = Node X is deleted at level L % edge(X,Y,L) = Edge (X,Y) remains at level L % edge(X,Y) = Edge (X,Y) is initially chosen (to form the forest) #const n = 4. %%% DOMAIN RULES %%% node(1..n). level(0..(n-1)/2). pair(X,Y) :- node(X;Y), X < Y. maps(X,Y,X,Y) :- pair(X,Y). maps(Y,X,X,Y) :- pair(X,Y). %%% CLAUSES DEFINING SOLUTIONS %%% del(X,L) | edge(XX,YY,L) : maps(X,Z,XX,YY) : Y != Z :- maps(X,Y,_,_), level(L). -del(X,L) | -edge(X1,Y1,L) | -edge(X2,Y2,L) :- maps(X,Y,X1,Y1), maps(X,Z,X2,Y2), level(L), Y < Z. edge(X,Y,L) | -edge(X,Y,L-1) | del(X,L-1) | del(Y,L-1) :- pair(X,Y), level(L), 0 < L. -edge(X,Y,L) | edge(X,Y,L-1) :- pair(X,Y), level(L), 0 < L. -edge(X,Y,L) | -del(Z,L-1) :- maps(Z,_,X,Y), level(L), 0 < L. del(X,(n-1)/2) :- node(X). %%% PROJECT SOLUTIONS %%% edge(X,Y) | -edge(X,Y,0) :- pair(X,Y). -edge(X,Y) | edge(X,Y,0) :- pair(X,Y). #hide. #show edge/2. #show -edge/2. #show edge/3. #show -edge/3. #show del/2. #show -del/2.