! MinSpanForest.ax - specification axioms for minimum spanning forest function
! - result will be a minimum spanning tree if the input graph is connected
! - will be compared to Kruskal's and Prim's algorithms in C and other langs
!---+----x----+----x----+----x----+----x----+----x----+----x----+----x----+----8
!/
top-level predicate:
(MSF )
- input weighted undirected graph
= (.. ..) -- sequence (set) of >=0 weighted undirected edges
- weighted undirected edge
= ( ) -- edge between vertices A and B with weight wt
-- order of vertices for undirected edge doesn't matter
- symbol for a vertex X
(just equality and inequality between vertex symbols is needed)
- natural number weight given as an unsigned decimal number symbol
-- Note that the set of vertices is implied by the set of edges.
(Thus, we can't represent isolated vertices without edges.)
-- We allow a multigraph where there can be >1 edges (with or without
different weights) between two vertices. The edges may have the
vertices in different orders. (The minimum spanning forest, of course,
would only contain the/an edge of minimum weight.) We also allow
loops where an edge goes to and from the same vertex. (The minimum
spanning forest, of course, would exclude these edges.)
- output weighted undirected graph representing minimum spanning forest
-- same format as the input weighted undirected graph
-- The output graph is just a subset of the input edges and we keep the
same edge order and the same vertex order for each edge.
-- If there is more than one minimum spanning forest (with the same
minimum weight), our output graph can nondeterministically be any
one of those solutions.
example wug:
((B F 7) (G C 8) (D H 7) (A E 4) (A F 2) (E B 9) (F C 5)
(A B 8) (E F 6) (G F 9))
(A)--8---(B) (C) (D)
| \ / | / | |
| 2 9 | 5 | |
4 \/ 7 / 8 7
| /\ | / | |
| / \ | / | |
| / \ | / | |
(E)--6---(F)--9---(G) (H)
minimum spanning forest:
((B F 7) (G C 8) (D H 7) (A E 4) (A F 2) (F C 5))
(A) (B) (C) (D)
| \ | / | |
| 2 | 5 | |
4 \ 7 / 8 7
| \ | / | |
| \ | / | |
| \ | / | |
(E) (F) (G) (H)
See utilities directory for utility function definitions.
!\
! MSF - Minimum Spanning Forest
(MSF %wug %wugMSF)<
((filter edge-verts-differ?) %wug %wugll), ! get loop-less version of graph
! -- we need this to eliminate isolated vertices with loop edges
(all_subsets %wugll %wugsubs), ! get all (loop-less) subgraphs
! -- we get all edge subsets
((filter (same-components? %wugll)) %wugsubs %wugspan),
! -- get spanning subgraphs (same connected components as original)
((min graph-weight+) %wugspan %wugMSF). ! get spanning subgr w min weight
! non-deterministic if more than one minimum!
! components - connected components of an undirected graph
! (returns partition of the set of vertices obtained from sequence of edges)
(components %wug %components)<
((map pre2) %wug %edge_verts),
! -- init "components" to separate 2-vertex subsets for each edge
! (we remove the weights)
! (since tbere are no loop edges, the end vertices are distinct)
((repeat merge_sets) %edge_verts %components),
! -- repeatedly merge vertex subsets that have a vertex in common
! (gives larger vertex subsets that are connected)
(partition %components). ! the vertex subsets form a partition
! -- at this point no two vertex subsets have a vertex in common
! -- thus the vertex subsets are all the connected components
! some supporting graph function definitions
(define_func edge-verts-differ? (comp not (1 ==?) pre2)).
! returns `t if edge end-vertices differ
(define_func (same-components? %wug)
(comp =ssets? (constr (comp components (`' %wug)) components))).
! tests if input graph has same components as graph in function
(define_func edge-weight (comp dec_sym sel2)). ! edge wt as natural number
(define_func edge-weight+ (comp (partial plus (s 0)) edge-weight)).
! get incremented edge weight
! -- This makes sure that 0-weight edges have a positive weight;
! otherwise, they might be left in the minimum weight graph.
(define_func graph-weight+ (comp sum (map edge-weight+))).
! sum of incremented weights
!/ alternative (with same number of lines):
(define_func graph-weight+
(comp plus (constr (comp plus (map edge-weight)) length))).
! -- uses graph length to add 1 to each edge weight
! -- Note that plus has been generalized to add a sequence of numbers.
!\