nonpositiveCycles.ml 2.86 KB
 fpottier committed Mar 01, 2013 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 ``````(* This module uses Floyd and Warshall's algorithm to detect whether a graph with integer-weighted edges contains a simple cycle of negative weight. *) (* The algorithm runs in cubic time in the number of vertices. It may be worthwhile to first use Tarjan's algorithm to obtain the graph's strongly connected components, and use Floyd and Warshall's algorithm only on each component. *) module Run (G : sig type node (* We assume each node has a unique index. Indices must range from \$0\$ to \$n-1\$, where \$n\$ is the number of nodes in the graph. *) val n: int val index: node -> int (* Iterating over a node's immediate successors. Edges are weighted. *) val successors: (int -> node -> unit) -> node -> unit (* Iterating over all nodes. *) val iter: (node -> unit) -> unit end) = struct open G (* Integers with infinity. *) type distance = | Infinity | Finite of int let add d1 d2 = match d1, d2 with | Infinity, _ | _, Infinity -> Infinity | Finite i1, Finite i2 -> Finite (i1 + i2) let min d1 d2 = match d1, d2 with | Infinity, d | d, Infinity -> d | Finite i1, Finite i2 -> Finite (min i1 i2) let le d1 d2 = match d1, d2 with | Infinity, Infinity -> true | Infinity, Finite _ -> false | Finite _, Infinity -> true | Finite i1, Finite i2 -> i1 <= i2 (* Allocate and initialize a distance matrix. At allocation time, every entry is initialized to infinity. Then, we iterate over all edges, and copy them into the distance matrix. *) (* Note that, by default, [d.(i).(i)] is not initialized to zero: it is initialized to infinity. This is because we are looking for paths of non-zero length. In other words, we are computing a transitive closure, not a reflexive, transitive closure. *) let d = Array.init n (fun i -> Array.init n (fun j -> Infinity ) ) let () = iter (fun source -> successors (fun weight target -> (* We use a min operation, so the graph may be a multi-graph, that is, multiple edges between two nodes are permitted. *) let i = index source and j = index target in d.(i).(j) <- min (Finite weight) d.(i).(j) ) source ) (* The algorithm. *) (* Stefan Hougardy notes that, in the presence of negative cycles, distances can grow exponentially fast (towards minus infinity), so there is a risk of overflow. To avoid this, one must check for negative cycles during the computation -- as opposed to waiting until the end. *) exception Detection let graph_has_nonpositive_simple_cycle : bool = try for k = 0 to n-1 do for i = 0 to n-1 do for j = 0 to n-1 do d.(i).(j) <- min d.(i).(j) (add d.(i).(k) d.(k).(j)); if i = j && le d.(i).(j) (Finite 0) then raise Detection done done done; false with Detection -> true end ``````