
   0 | module Data.Graph.Indexed.Util.Bipartite
   1 | 
   2 | import Data.Graph.Indexed
   3 | import Data.Graph.Indexed.Subgraph
   4 | import Data.Linear.List
   5 | import Data.Linear.Token
   6 | import Data.Linear.Traverse1
   7 | import Data.Queue
   8 | 
   9 | %default total
  10 | 
  11 | data Color = Unset | Even | Odd
  12 | 
  13 | toBool : Color -> Bool
  14 | toBool Odd = False
  15 | toBool _   = True
  16 | 
  17 | not : Color -> Color
  18 | not Even = Odd
  19 | not _    = Even
  20 | 
  21 | matches : Color -> Color -> Bool
  22 | matches Even Even = True
  23 | matches Odd  Odd  = True
  24 | matches _    _    = False
  25 | 
  26 | parameters (g  : IGraph k e n)
  27 |            (cs : MArray s k Color)
  28 | 
  29 |   setc : Fin k -> Color -> Queue (Color,Fin k) -> F1 s (Queue (Color,Fin k))
  30 |   setc x c q t =
  31 |    let _ # t := set cs x c t
  32 |     in enqueueAll q ((not c,) <$> neighbours g x) # t
  33 | 
  34 |   bfs : Queue (Color,Fin k) -> F1 s Bool
  35 |   bfs q t =
  36 |     case dequeue q of
  37 |       Nothing         => True # t
  38 |       Just ((c,x),q2) => case Core.get cs x t of
  39 |         Unset # t => let q3 # t := setc x c q2 t in bfs (assert_smaller q q3) t
  40 |         col   # t => case matches c col of
  41 |           True  => bfs (assert_smaller q q2) t
  42 |           False => False # t
  43 | 
  44 | ||| Tries to color a graph with only two colors, so that all
  45 | ||| edges in the graph connect nodes of distinct colors.
  46 | |||
  47 | ||| Returns the coloring in case of a success and `Nothing` otherwise.
  48 | export
  49 | bipartite : {k : _} -> IGraph k e n -> Maybe (IArray k Bool)
  50 | bipartite g = alloc k Unset (go $ nodes g)
  51 |   where
  52 |     go : List (Fin k) -> MArray s k Color -> F1 s (Maybe $ IArray k Bool)
  53 |     go []        cs t =
  54 |      let ci # t := unsafeFreeze cs t
  55 |       in Just (map toBool ci) # t
  56 |     go (x :: xs) cs t =
  57 |      let Unset # t := Core.get cs x t                 | _ # t => go xs cs t
  58 |          True  # t := bfs g cs (fromList [(Odd,x)]) t | _ # t => Nothing # t
  59 |       in go xs cs t
  60 | 
  61 | --------------------------------------------------------------------------------
  62 | -- Matches on bipartite graphs
  63 | --------------------------------------------------------------------------------
  64 | 
  65 | ||| Finds a maximal matching for a bipartite graph. Returns `Nothing`
  66 | ||| in case the graph is not bipartite.
  67 | export
  68 | match : {k : _} -> IGraph k e n -> Maybe (IArray k (Maybe $ Fin k))
  69 | -- implementation below
  70 | 
  71 | ||| Tries to find a perfect matching for a bipartite graph.
  72 | ||| Returns `Nothing` in case the graph is not bipartite or no
  73 | ||| perfect matching exists.
  74 | export
  75 | perfectMatch : {k : _} -> IGraph k e n -> Maybe (IArray k (Fin k))
  76 | perfectMatch g = match g >>= sequence
  77 | 
  78 | ||| Finds the edges of a maximal matching in a graph.
  79 | export
  80 | matchEdges : {k : _} -> IGraph k e n -> List (Edge k e)
  81 | matchEdges g = maybe [] (\a => mapMaybe (edg a) (nodes g)) (match g)
  82 |   where
  83 |     edg : IArray k (Maybe $ Fin k) -> Fin k -> Maybe (Edge k e)
  84 |     edg a x = at a x >>= \y => if x < y then edge g x y else Nothing
  85 | 
  86 | ||| Finds the edges of a maximal matching in a subgraph.
  87 | export
  88 | matchEdgesWhere :
  89 |      {k : _}
  90 |   -> IGraph k e n
  91 |   -> (pred : Fin k -> Bool)
  92 |   -> List (Edge k e)
  93 | matchEdgesWhere g pred =
  94 |  let G _ sg := subgraphL g (filter pred $ nodes g)
  95 |   in mapMaybe (originEdge sg) (matchEdges sg)
  96 | 
  97 | --------------------------------------------------------------------------------
  98 | -- Hopcroft-Karp: Implementation
  99 | --------------------------------------------------------------------------------
 100 | 
 101 | 0 Q : Nat -> Type
 102 | Q k = Queue (Fin k)
 103 | 
 104 | 0 MDist : Type -> Nat -> Type
 105 | MDist s k = MArray s k Nat
 106 | 
 107 | 0 Dist : Nat -> Type
 108 | Dist k = IArray k Nat
 109 | 
 110 | 0 Pair : Type -> Nat -> Type
 111 | Pair s k = MArray s k (Maybe $ Fin k)
 112 | 
 113 | %inline
 114 | link : Pair s k => Fin k -> F1 s (Maybe $ Fin k)
 115 | link @{p} = Core.get p
 116 | 
 117 | %inline
 118 | isFree : Pair s k => Fin k -> F1 s Bool
 119 | isFree x t =
 120 |   case link x t of
 121 |     Nothing # t => True # t
 122 |     _       # t => False # t
 123 | 
 124 | %inline
 125 | doLink : Pair s k => (x,y : Fin k) -> F1 s Bool
 126 | doLink @{p} x y t =
 127 |  let _ # t := Core.set p x (Just y) t
 128 |      _ # t := Core.set p y (Just x) t
 129 |   in True # t
 130 | 
 131 | %inline
 132 | dist : MDist s k => Fin k -> F1 s Nat
 133 | dist @{d} = Core.get d
 134 | 
 135 | %inline
 136 | putDist : MDist s k => Fin k -> Nat -> F1' s
 137 | putDist @{d} = Core.set d
 138 | 
 139 | enq : Pair s k => MDist s k => Nat -> List (Fin k) -> Q k -> F1 s (Q k)
 140 | enq _ []      q t = q # t
 141 | enq l (v::vs) q t =
 142 |  let Just u # t := link v t | _ # t => enq l vs q t
 143 |      Z      # t := dist u t | _ # t => enq l vs q t
 144 |      _      # t := putDist u l t
 145 |   in enq l vs (enqueue q u) t
 146 | 
 147 | parameters {0 s,e,n : Type}
 148 |            (g    : IGraph k e n)
 149 | 
 150 |   layers : (d : MDist s k) => Pair s k => Q k -> F1 s (Dist k)
 151 |   layers q t =
 152 |     case dequeue q of
 153 |       Nothing     => unsafeFreeze d t
 154 |       Just (u,q2) =>
 155 |        let du # t := dist u t
 156 |            q3 # t := enq (S du) (neighbours g u) q2 t
 157 |         in layers (assert_smaller q q3) t
 158 | 
 159 |   dfs : Pair s k => Dist k -> Fin k -> F1 s Bool
 160 |   dfs dist u t = go (neighbours g u) t
 161 |     where
 162 |       go : List (Fin k) -> F1 s Bool
 163 |       go []      t = False # t
 164 |       go (v::vs) t =
 165 |        let Just w # t := link v t                        | _ # t => doLink u v t
 166 |            True       := at dist w == S (at dist u)      | False => go vs t
 167 |            True # t   := dfs dist (assert_smaller u w) t | _ # t => go vs t
 168 |         in doLink u v t
 169 | 
 170 | match g =
 171 |   map
 172 |     (\cs => alloc k Nothing $ \x => loop @{x} (filter (at cs) (nodes g)))
 173 |     (bipartite g)
 174 |   where
 175 |     loop : Pair s k => List (Fin k) -> F1 s (IArray k (Maybe $ Fin k))
 176 |     loop @{p} es t =
 177 |      let fs # t := filter1 isFree es t
 178 |          md # t := marray1 k Z t
 179 |          _  # t := for1_ fs (\x => putDist x 1) t
 180 |          ds # t := layers g (fromList fs) t
 181 |          [] # t := filter1 (dfs g ds) fs t | _ # t => loop (assert_smaller es fs) t
 182 |       in unsafeFreeze p t
 183 |