scc.nmo

% strongly connected components

% example from sedgewick, algorithms in C++, part 5, figure 19.28, §19.8, p. 207
% edge(from, to)
e(0,1). e(0,5). e(0,6).
e(2,0). e(2,3).
e(3,2). e(3,5).
e(4,2). e(4,3). e(4,11).
e(5,4).
e(6,4). e(6,9).
e(7,6). e(7,8).
e(8,7). e(8,9).
e(9,10). e(9,11).
e(10,12).
e(11,12).
e(12,9).

% all vertices seen by e()
v(?x) :- e(?x,?y).
v(?x) :- e(?y,?x).

% which paths exist
path(?x, ?x) :- v(?x).
path(?x, ?z) :- e(?x, ?y), path(?y, ?z).

% which edges have no path back?
% these edges are truly directed-acyclical and denote SCC boundaries
% they also give us the sources and sinks of each SCC
de(?x, ?y) :- e(?x, ?y), ~path(?y, ?x).

% vertices which are entry points for SCCs
dsource(?y) :- de(?x, ?y).
% vertices which are exit points for SCCs
dsink(?x) :- de(?x, ?y).

% which edges are therefore cyclical? this graph intra-connects SCC components
ce(?x, ?x) :- v(?x).
ce(?x, ?y) :- e(?x, ?y), ~de(?x, ?y).

% which intra-cyclical paths exist (separated by SCC)
xpath(?x, ?x) :- v(?x).
xpath(?x, ?z) :- xpath(?x, ?y), ce(?y, ?z).

% assign each vertex to an arbitrary canonical vertex which represents the SCC group
scc(#min(?x), ?y) :- xpath(?x, ?y), ?x <= ?y.

% SCC distance: how many SCCs must be crossed to connect two vertices?
scc_dist(0, ?x, ?x) :- v(?x).
scc_dist(1, ?x, ?y) :- de(?x, ?y).
% same distance if in same SCC
scc_dist(?n, ?x, ?z) :- scc_dist(?n, ?x, ?y), ce(?y, ?z).
% +1 if not - truly directed, and therefore guaranteed to terminate
scc_dist(?n + 1, ?x, ?z) :- scc_dist(?n, ?x, ?y), de(?y, ?z).

% SCC topological sort: in what order to process SCCs?
scc_toposort(#max(?n), ?g) :- scc_dist(?n, ?y, ?x), scc(?g, ?x).
% include SCCs that aren't connected to anything
scc_toposort(0, ?g) :- scc(?g, ?x), ~scc_dist(?n, ?y, ?x).

@export scc_toposort :- csv{resource = ""}.