graphlogic-programminganswer-set-programmingspanning-tree

Spanning Trees in Answer Set Programming


For the undirected graph described below, I am trying to get its spanning trees and then separate its leaves from the internal nodes. Could you please help me with my code ?

What I expect to see after running the code is something like :

Answer 1 : spanTree(1,2), spanTree(2,3), spanTree(3,4), leaf(1), leaf(4), internal(2), internal(3).

Answer 2 : spanTree(1,2), spanTree(1,3), spanTree(3,4), leaf(2), leaf(4), internal(1), internal(3).

% undirected graph
edge(1,2).
edge(2,3).
edge(1,3).
edge(3,4).
vertex(X):- edge(X,Y).
vertex(X):- edge(Y,X).

%find spanning trees
spanTree(X,Y):- edge(X,Y).
spanTree(X,Y):- edge(Y,X).

start(1).

reached(X):-start(X).
reached(X):-reached(Y), spanTree(Y,X).
    
:-spanTree(X,Y), start(Y).
:-spanTree(X,Y), spanTree(X1,Y), X != X1.
:-vertex(X), not reached(X).

% degree of vertex
degree(X,D) :- vertex(X),D=#count {Y :spanTree(X,Y)}.

% leaves and internal vertices
{leaf(X):- spanTree(X,_),degree(X,D), D=1}:- vertex(X).
{internal(X):- spanTree(X,_),degree(X,D), D>1}:- vertex(X).

Solution

  • I would avoid counting unless necessary. I mirrored the edges at start to implement the undirected graph and guessing the spanTree is also important. I made a shortcut here: instead of saying, an edge might be a spantree-edge, when "building" I say: for every node (except root) choose exactly one ingoing edge to be the spantree-edge.
    The reached part is pretty much copy & paste (good job here), but I left out the first two constraints because they are already covered.
    The internal/leaf classification can also be simplified. Deriving internal nodes is easy, leafs can be covered by not being internals.

    edge(1,2). edge(2,3). edge(1,3). edge(3,4).
    % mirror edges
    edge(Y,X) :- edge(X,Y).
    vertex(X) :- edge(_,X).
    
    % every node Y except root has exactly one ingoing edge
    { spanTree(X,Y) : edge(X,Y) } == 1:- vertex(Y), not root(Y).
    
    root(1).
    reached(X) :- root(X).
    reached(X) :- reached(Y), spanTree(Y,X).
        
    :- vertex(X), not reached(X).
    
    % an internal node has an outgoing edge
    internal(X) :- spanTree(X,_).
    % a vertex which is not an internal is a leaf
    leaf(X) :- vertex(X), not internal(X).
    
    #show spanTree/2.
    #show leaf/1.
    #show internal/1.
    

    Output

    Answer: 1
    internal(3) leaf(2) leaf(4) internal(1) spanTree(3,2) spanTree(1,3) spanTree(3,4)
    Answer: 2
    internal(3) leaf(2) leaf(4) internal(1) spanTree(1,2) spanTree(1,3) spanTree(3,4)
    Answer: 3
    internal(3) leaf(4) internal(1) spanTree(1,2) internal(2) spanTree(2,3) spanTree(3,4)
    SATISFIABLE