diff --git a/lib/sasacore/localSearch.ml b/lib/sasacore/localSearch.ml new file mode 100644 index 0000000000000000000000000000000000000000..0dfae38d4f8e3556a67e7ee9213d5964912fd6f6 --- /dev/null +++ b/lib/sasacore/localSearch.ml @@ -0,0 +1,61 @@ + +type ('n, 'tv, 'v) t = { + init : 'n * 'tv * 'v; + succ : 'n -> 'n list; (* returns (all or some) neighbors *) + + is_goal : 'n -> bool; (* is the node a solution of the problem *) + stop : 'n -> 'n -> bool; (* [stop pre_sol n] to stop the search before all nodes are visited *) + cut: 'n -> 'n -> bool; (* if [cut pre_sol n] is true, stop exploring n *) + + push : 'tv -> 'n -> 'tv; (* add the node in the set of nodes to visit *) + pop : 'tv -> ('n * 'tv) option; (* pick a node to visit *) + + visiting : 'n -> 'v -> 'v; (* mark a node as visited *) + visited : 'n -> 'v -> bool; (* check if a node has been visited *) +} + + +type 'n sol = Stopped | NoMore | Sol of 'n * 'n moresol +and 'n moresol = 'n option -> 'n sol + + +let debug = false + +let cut_nb = ref 0 +let sol_nb = ref 0 + +let (run : ('n, 'tv, 'v) t -> 'n option -> 'n sol) = + fun g pre_sol -> + let cut sol_opt n = match sol_opt with + | None -> false + | Some sol -> + let res = g.cut sol n in + if res then incr cut_nb; + res + in + let pre_process sol_opt (v, tv) n = + if g.visited n v || cut sol_opt n then (v, tv) else (g.visiting n v, g.push tv n) + in + let rec loop ps n tv v psol = + let do_succ_cont s = + if g.stop ps n then Stopped else loop2 n tv v s + in (* to avoid code duplication *) + if not (g.is_goal n) then + do_succ_cont psol + else + (incr sol_nb; Sol(n, do_succ_cont)) + and loop2 n tv v psol = (* look at the n successors *) + if debug then Printf.printf "look at successors\n%!"; + let v, tv = List.fold_left (pre_process psol) (v, tv) (g.succ n) in + (match g.pop tv with + | None -> NoMore + | Some (next_n, tv) -> loop n next_n tv v psol + ) + in + let n, tv, v = g.init in + loop n n tv v pre_sol + +let stat log = + Printf.fprintf log "\n- local search stat:\n\t- cut: %d\n\t- sol nb: %d\n%!" !cut_nb !sol_nb + + diff --git a/lib/sasacore/localSearch.mli b/lib/sasacore/localSearch.mli new file mode 100644 index 0000000000000000000000000000000000000000..591475d21a38e5e74e0ab3b6104af39cc0fdc3f9 --- /dev/null +++ b/lib/sasacore/localSearch.mli @@ -0,0 +1,48 @@ +(* Time-stamp: <modified the 27/10/2021 (at 12:08) by Erwan Jahier> *) + +(** A generic module to implement local searches + https://en.wikipedia.org/wiki/Local_search_(optimization) +*) + +(** Parameterized by node, nodes to visit later, already visited (+ to visit) nodes + +- 'tv: nodes to visit late can be implemented by lists, or priority queues +- 'v: visited nodes can be implemented by lists, or sets +*) +type ('n, 'tv, 'v) t = { + init : 'n * 'tv * 'v; + succ : 'n -> 'n list; (* returns (all or some) neighbors *) + + is_goal : 'n -> bool; (* is the node a solution of the problem *) + stop : 'n -> 'n -> bool; (* if [stop pre_sol n], stop the search *) + cut: 'n -> 'n -> bool; (* if [cut pre_sol n], don't explore n *) + + push : 'tv -> 'n -> 'tv; (* add the node in the set of nodes to visit *) + pop : 'tv -> ('n * 'tv) option; (* pick a node to visit *) + + visiting : 'n -> 'v -> 'v; (* mark a node as visited *) + visited : 'n -> 'v -> bool; (* check if a node has been visited *) +} + + + +type 'n sol = Stopped | NoMore | Sol of 'n * 'n moresol +and 'n moresol = 'n option -> 'n sol + + (** [explore g] the graph induced by [g.succ] until either + - [pop tv]~>None, then it returns NoMore + - [stop pre_s s]~> true and is_goal s~>false, then it returns [Stopped] + - [is_goal s]~>true, then it returns [Sol(sol, cont)] + + When a valid node (a.k.a., a solution) is found, [run] returns it plus + a continuation to carry on the search. + + The optional argument of ['n moresol] ought to contain a previously obtained + solution (i.e., a node n for which [is_goal n=true]) that can be used by [cut] + to cut branches. + + nb: no cost function is required. But of course, the [push] or the [cut] + functions might use one. +*) +val run : ('n, 'tv, 'v) t -> 'n moresol +val stat : out_channel -> unit