Connected component (graph theory)

connected-components.chr

// USAGE: init(), then
// path("id1","id2") to add, break("id1","id2") to remove
// path("id1","id1") to add standalone vertex
// fact node_comp("nodeId", X) means "node belongs to component/cluster X"

// nodes from paths; A, B - node ID, C - cluster ID
path(A, B), recolor(C) ==> node_comp(A, C), node_comp(B, C)

// remove duplicates if exist
node_comp(A, C) \ node_comp(A, C) <=> true
path(A, B) \ path(A, B) <=> true
path(A, B) \ path(B, A) <=> true

// uncertain nodes belong to new cluster each; NC - new cluster ID
recolor(C) \ node_comp(A, C), iter(NC) <=> node_comp(A, NC), iter(NC+1)

// merge cluster colors, avoiding cluster being recolored, bidirectional
// OC - cluster during recolor, AC, BC - clusters to merge
recolor(OC), path(A, B), node_comp(A, AC) \ node_comp(B, BC) <=> OC < AC && AC < BC | node_comp(B, AC)
recolor(OC), path(B, A), node_comp(A, AC) \ node_comp(B, BC) <=> OC < AC && AC < BC | node_comp(B, AC)

// break: remove path, set cluster being recolored to cluster where path appeared
node_comp(A, C) \ break(A, B), path(A, B), recolor(O) <=> recolor(C)
node_comp(A, C) \ break(A, B), path(B, A), recolor(O) <=> recolor(C)

// init "variables"
init <=> iter(0), recolor(0)