# Encoding bst.dlv

Name bst.dlv [Root]    Unclassified (114) Martin Gebser A DLV encoding for BST, with bstedge as output predicate. 2009-03-30 13:03 2008-11-29 00:10 No % DLV encoding for bounded spanning tree % By Wolfgang Faber %Check all subgraphs. bstedge(X,Y) v nbstedge(X,Y) :- edge(X,Y). % The input graph is interpreted as being directed. % The subgraph is a tree if its undirected shadow has no circle. % Create the shadow. ubstedge(X,Y) :- bstedge(X,Y). ubstedge(Y,X) :- bstedge(X,Y). % Define reachability (without using the first edge to go back) on the shadow. ustpath_f(X,Y,Y,X) :- ubstedge(X,Y). ustpath_f(X,Y,Xf,Yf) :- ustpath_f(X,Z,Xf,Yf), ubstedge(Z,Y), not eq_edge(Z,Y,Xf,Yf). % Auxiliary: Edge equivalence. eq_edge(X,Y,X,Y) :- vtx(X),vtx(Y). % No node shall be reachable (modulo trivially going back) from itself if it % is a tree. :- ustpath_f(X,X,_,_). reached(X) :- bstedge(_,X). % A tree must have exactly one root. :- #count{ X: vtx(X), not reached(X) } < 1. :- #count{ X: vtx(X), not reached(X) } > 1. % The tree should be spanning. connected(X,Y) :- ustpath_f(X,Y,_,_). :- vtx(X), vtx(Y), X != Y, not connected(X,Y). % Enforce the bound on outgoing edges. :- vtx(X), #count{ Y: bstedge(X,Y) } > D, bound(D).