Documentation

Mathlib.Data.MLList.BestFirst

Best first search #

We perform best first search of a tree or graph, where the neighbours of a vertex are provided by a lazy list α → MLList m α.

We maintain a priority queue of visited-but-not-exhausted nodes, and at each step take the next child of the highest priority node in the queue.

This is useful in meta code for searching for solutions in the presence of alternatives. It can be nice to represent the choices via a lazy list, so the later choices don't need to be evaluated while we do depth first search on earlier choices.

Options:

def bestFirstSearchAux {m : Type u → Type u} {α : Type u} [Monad m] [Alternative m] [Ord α] (f : NatαMLList m α) (maxQueued : optParam (Option Nat) none) :
Std.RBMap α (Nat × MLList m α) comparem (Std.RBMap α (Nat × MLList m α) compare × List α)

Auxiliary function for bestFirstSearch, that updates the internal state, consisting of a priority queue of triples α × Nat × MLList m α. We remove the next element from the list contained in the best triple (discarding the triple if there is no next element), enqueue it and return it.

Instances For
    def bestFirstSearch {m : Type u → Type u} {α : Type u} [Monad m] [Alternative m] [Ord α] (f : αMLList m α) (a : α) (maxDepth : optParam (Option Nat) none) (maxQueued : optParam (Option Nat) none) (removeDuplicates : optParam Bool true) :
    MLList m α

    A lazy list recording the best first search of a graph generated by a function f : α → MLList m α.

    We maintain a priority queue of visited-but-not-exhausted nodes, and at each step take the next child of the highest priority node in the queue.

    The option maxDepth limits the search depth.

    The option maxQueued bounds the size of the priority queue, discarding the lowest priority nodes as needed. This implements a "beam" search, which may be incomplete but uses bounded memory.

    The option removeDuplicates keeps an RBSet of previously visited nodes. Otherwise, if the graph is not a tree then nodes will be visited multiple times.

    Instances For