Modulealgebraic-graphs-0.8Haskell2010

Algebra.Graph.AdjacencyMap.Algorithm

Alga is a library for algebraic construction and manipulation of graphs in Haskell. See this paper for the motivation behind the library, the underlying theory, and implementation details.

This module provides basic graph algorithms, such as depth-first search, implemented for the Algebra.Graph.AdjacencyMap data type.

1 type
11 values

Packagealgebraic-graphs-0.8
Exports12
LanguageHaskell2010
LicenceMIT
SourceAlgorithm.hs

Algorithms

9 declarations

valuebfsForest :: Ord a => AdjacencyMap a -> [a] -> Forest a

Compute the breadth-first search forest of a graph, such that adjacent vertices are explored in increasing order according to their Ord instance. The search is seeded by a list of vertices that will become the roots of the resulting forest. Duplicates in the list will have their first occurrence explored and subsequent ones ignored. The seed vertices that do not belong to the graph are also ignored.

Complexity: O((L + m) * log n) time and O(n) space, where L is the number of seed vertices.

forest $ bfsForest (edge 1 2) [0]        == empty
forest $ bfsForest (edge 1 2) [1]        == edge 1 2
forest $ bfsForest (edge 1 2) [2]        == vertex 2
forest $ bfsForest (edge 1 2) [0,1,2]    == vertices [1,2]
forest $ bfsForest (edge 1 2) [2,1,0]    == vertices [1,2]
forest $ bfsForest (edge 1 1) [1]        == vertex 1
isSubgraphOf (forest $ bfsForest x vs) x == True
bfsForest x (vertexList x)               == map (\v -> Node v []) (nub $ vertexList x)
bfsForest x []                           == []
bfsForest empty vs                       == []
bfsForest (3 * (1 + 4) * (1 + 5)) [1,4]  == [ Node { rootLabel = 1
                                                   , subForest = [ Node { rootLabel = 5
                                                                        , subForest = [] }]}
                                            , Node { rootLabel = 4
                                                   , subForest = [] }]
forest $ bfsForest (circuit [1..5] + circuit [5,4..1]) [3] == path [3,2,1] + path [3,4,5]

valuebfs :: Ord a => AdjacencyMap a -> [a] -> [[a]]

A version of bfsForest where the resulting forest is converted to a level structure. Adjacent vertices are explored in the increasing order according to their Ord instance. Flattening the result via concat . bfs x gives an enumeration of reachable vertices in the breadth-first search order.

Complexity: O((L + m) * min(n,W)) time and O(n) space, where L is the number of seed vertices.

bfs (edge 1 2) [0]                == []
bfs (edge 1 2) [1]                == [[1], [2]]
bfs (edge 1 2) [2]                == [[2]]
bfs (edge 1 2) [1,2]              == [[1,2]]
bfs (edge 1 2) [2,1]              == [[2,1]]
bfs (edge 1 1) [1]                == [[1]]
bfs empty vs                      == []
bfs x []                          == []
bfs (1 * 2 + 3 * 4 + 5 * 6) [1,2] == [[1,2]]
bfs (1 * 2 + 3 * 4 + 5 * 6) [1,3] == [[1,3], [2,4]]
bfs (3 * (1 + 4) * (1 + 5)) [3]   == [[3], [1,4,5]]

bfs (circuit [1..5] + circuit [5,4..1]) [3]          == [[2], [1,3], [5,4]]
concat $ bfs (circuit [1..5] + circuit [5,4..1]) [3] == [3,2,4,1,5]
map concat . transpose . map levels . bfsForest x    == bfs x

valuedfsForest :: Ord a => AdjacencyMap a -> Forest a

Compute the depth-first search forest of a graph, where adjacent vertices are explored in the increasing order according to their Ord instance.

Complexity: O((n + m) * min(n,W)) time and O(n) space.

forest $ dfsForest empty              == empty
forest $ dfsForest (edge 1 1)         == vertex 1
forest $ dfsForest (edge 1 2)         == edge 1 2
forest $ dfsForest (edge 2 1)         == vertices [1,2]
isSubgraphOf (forest $ dfsForest x) x == True
isDfsForestOf (dfsForest x) x         == True
dfsForest . forest . dfsForest        == dfsForest
dfsForest (vertices vs)               == map (\v -> Node v []) (nub $ sort vs)
dfsForest $ 3 * (1 + 4) * (1 + 5)     == [ Node { rootLabel = 1
                                                , subForest = [ Node { rootLabel = 5
                                                                     , subForest = [] }]}
                                         , Node { rootLabel = 3
                                                , subForest = [ Node { rootLabel = 4
                                                                     , subForest = [] }]}]
forest (dfsForest $ circuit [1..5] + circuit [5,4..1]) == path [1,2,3,4,5]

valuedfsForestFrom :: Ord a => AdjacencyMap a -> [a] -> Forest a

Compute the depth-first search forest of a graph starting from the given seed vertices, where adjacent vertices are explored in the increasing order according to their Ord instance. Note that the resulting forest does not necessarily span the whole graph, as some vertices may be unreachable. The seed vertices which do not belong to the graph are ignored.

Complexity: O((L + m) * log n) time and O(n) space, where L is the number of seed vertices.

forest $ dfsForestFrom empty      vs             == empty
forest $ dfsForestFrom (edge 1 1) [1]            == vertex 1
forest $ dfsForestFrom (edge 1 2) [0]            == empty
forest $ dfsForestFrom (edge 1 2) [1]            == edge 1 2
forest $ dfsForestFrom (edge 1 2) [2]            == vertex 2
forest $ dfsForestFrom (edge 1 2) [1,2]          == edge 1 2
forest $ dfsForestFrom (edge 1 2) [2,1]          == vertices [1,2]
isSubgraphOf (forest $ dfsForestFrom x vs) x     == True
isDfsForestOf (dfsForestFrom x (vertexList x)) x == True
dfsForestFrom x (vertexList x)                   == dfsForest x
dfsForestFrom x []                               == []
dfsForestFrom (3 * (1 + 4) * (1 + 5)) [1,4]      == [ Node { rootLabel = 1
                                                           , subForest = [ Node { rootLabel = 5
                                                                                , subForest = [] }
                                                    , Node { rootLabel = 4
                                                           , subForest = [] }]
forest $ dfsForestFrom (circuit [1..5] + circuit [5,4..1]) [3] == path [3,2,1,5,4]

valuedfs :: Ord a => AdjacencyMap a -> [a] -> [a]

Return the list vertices visited by the depth-first search in a graph, starting from the given seed vertices. Adjacent vertices are explored in the increasing order according to their Ord instance.

Complexity: O((L + m) * log n) time and O(n) space, where L is the number of seed vertices.

dfs empty      vs    == []
dfs (edge 1 1) [1]   == [1]
dfs (edge 1 2) [0]   == []
dfs (edge 1 2) [1]   == [1,2]
dfs (edge 1 2) [2]   == [2]
dfs (edge 1 2) [1,2] == [1,2]
dfs (edge 1 2) [2,1] == [2,1]
dfs x          []    == []

Data.List.and [ hasVertex v x | v <- dfs x vs ]       == True
dfs (3 * (1 + 4) * (1 + 5)) [1,4]           == [1,5,4]
dfs (circuit [1..5] + circuit [5,4..1]) [3] == [3,2,1,5,4]

valuereachable :: Ord a => AdjacencyMap a -> a -> [a]

Return the list of vertices reachable from a source vertex in a graph. The vertices in the resulting list appear in the depth-first search order.

Complexity: O(m * log n) time and O(n) space.

reachable empty              x == []
reachable (vertex 1)         1 == [1]
reachable (edge 1 1)         1 == [1]
reachable (edge 1 2)         0 == []
reachable (edge 1 2)         1 == [1,2]
reachable (edge 1 2)         2 == [2]
reachable (path    [1..8]  ) 4 == [4..8]
reachable (circuit [1..8]  ) 4 == [4..8] ++ [1..3]
reachable (clique  [8,7..1]) 8 == [8] ++ [1..7]

Data.List.and [ hasVertex v x | v <- reachable x y ] == True

valuetopSort :: Ord a => AdjacencyMap a -> Either (Cycle a) [a]

Compute a topological sort of a graph or discover a cycle.

Vertices are explored in the decreasing order according to their Ord instance. This gives the lexicographically smallest topological ordering in the case of success. In the case of failure, the cycle is characterized by being the lexicographically smallest up to rotation with respect to Ord (Dual Int) in the first connected component of the graph containing a cycle, where the connected components are ordered by their largest vertex with respect to Ord a.

Complexity: O((n + m) * min(n,W)) time and O(n) space.

topSort (1 * 2 + 3 * 1)                    == Right [3,1,2]
topSort (path [1..5])                      == Right [1..5]
topSort (3 * (1 * 4 + 2 * 5))              == Right [3,1,2,4,5]
topSort (1 * 2 + 2 * 1)                    == Left (2 :| [1])
topSort (path [5,4..1] + edge 2 4)         == Left (4 :| [3,2])
topSort (circuit [1..3])                   == Left (3 :| [1,2])
topSort (circuit [1..3] + circuit [3,2,1]) == Left (3 :| [2])
topSort (1 * 2 + (5 + 2) * 1 + 3 * 4 * 3)  == Left (1 :| [2])
fmap (flip isTopSortOf x) (topSort x)      /= Right False
isRight . topSort                          == isAcyclic
topSort . vertices                         == Right . nub . sort

valueisAcyclic :: Ord a => AdjacencyMap a -> Bool

Check if a given graph is acyclic.

Complexity: O((n+m)*log n) time and O(n) space.

isAcyclic (1 * 2 + 3 * 1) == True
isAcyclic (1 * 2 + 2 * 1) == False
isAcyclic . circuit       == null
isAcyclic                 == isRight . topSort

valuescc :: Ord a => AdjacencyMap a -> AdjacencyMap (AdjacencyMap a)

Compute the condensation of a graph, where each vertex corresponds to a strongly-connected component of the original graph. Note that component graphs are non-empty, and are therefore of type Algebra.Graph.NonEmpty.AdjacencyMap.

Details about the implementation can be found at gabow-notes.

Complexity: O((n+m)*log n) time and O(n+m) space.

scc empty               == empty
scc (vertex x)          == vertex (NonEmpty.vertex x)
scc (vertices xs)       == vertices (map vertex xs)
scc (edge 1 1)          == vertex (NonEmpty.edge 1 1)
scc (edge 1 2)          == edge   (NonEmpty.vertex 1) (NonEmpty.vertex 2)
scc (circuit (1:xs))    == vertex (NonEmpty.circuit1 (1 :| xs))
scc (3 * 1 * 4 * 1 * 5) == edges  [ (NonEmpty.vertex  3      , NonEmpty.vertex  5      )
                                  , (NonEmpty.vertex  3      , NonEmpty.clique1 [1,4,1])
                                  , (NonEmpty.clique1 [1,4,1], NonEmpty.vertex  5      ) ]
isAcyclic . scc == const True
isAcyclic x     == (scc x == gmap NonEmpty.vertex x)

Correctness properties

2 declarations

valueisDfsForestOf :: Ord a => Forest a -> AdjacencyMap a -> Bool

Check if a given forest is a correct depth-first search forest of a graph. The implementation is based on the paper "Depth-First Search and Strong Connectivity in Coq" by François Pottier.

isDfsForestOf []                              empty            == True
isDfsForestOf []                              (vertex 1)       == False
isDfsForestOf [Node 1 []]                     (vertex 1)       == True
isDfsForestOf [Node 1 []]                     (vertex 2)       == False
isDfsForestOf [Node 1 [], Node 1 []]          (vertex 1)       == False
isDfsForestOf [Node 1 []]                     (edge 1 1)       == True
isDfsForestOf [Node 1 []]                     (edge 1 2)       == False
isDfsForestOf [Node 1 [], Node 2 []]          (edge 1 2)       == False
isDfsForestOf [Node 2 [], Node 1 []]          (edge 1 2)       == True
isDfsForestOf [Node 1 [Node 2 []]]            (edge 1 2)       == True
isDfsForestOf [Node 1 [], Node 2 []]          (vertices [1,2]) == True
isDfsForestOf [Node 2 [], Node 1 []]          (vertices [1,2]) == True
isDfsForestOf [Node 1 [Node 2 []]]            (vertices [1,2]) == False
isDfsForestOf [Node 1 [Node 2 [Node 3 []]]]   (path [1,2,3])   == True
isDfsForestOf [Node 1 [Node 3 [Node 2 []]]]   (path [1,2,3])   == False
isDfsForestOf [Node 3 [], Node 1 [Node 2 []]] (path [1,2,3])   == True
isDfsForestOf [Node 2 [Node 3 []], Node 1 []] (path [1,2,3])   == True
isDfsForestOf [Node 1 [], Node 2 [Node 3 []]] (path [1,2,3])   == False

valueisTopSortOf :: Ord a => [a] -> AdjacencyMap a -> Bool

Check if a given list of vertices is a correct topological sort of a graph.

isTopSortOf [3,1,2] (1 * 2 + 3 * 1) == True
isTopSortOf [1,2,3] (1 * 2 + 3 * 1) == False
isTopSortOf []      (1 * 2 + 3 * 1) == False
isTopSortOf []      empty           == True
isTopSortOf [x]     (vertex x)      == True
isTopSortOf [x]     (edge x x)      == False

Type synonyms

1 declaration

typetype Cycle = NonEmpty