Graph Search Invariants

General Graph Search Invariants

Consider the following graph search loop:

    do whatever you need to do with v
    record that v has been visited
    put the edges leaving v into the dispenser
    while the dispenser is not empty
        retrieve and remove edge e from the dispenser
        let w be the head of e
        if w has not been visited
            do whatever you need to do with e
            do whatever you need to do with w
            record that w has been visited
            put the edges leaving w into the dispenser
        endif
    endwhile
    

This loop has the following invariants:

1. 1. Every edge in the dispenser originates from a visited vertex.
2. 2. Every edge from a visited vertex to an unvisited vertex is in the dispenser.

As a consequence of the above invariants, we get a third invariant:

1. 3. Visited edges form a tree for the visited vertices.

This means that the edges connect the visited vertices and they do not form any cycles.

Optimizing Graph Search Invariants

For some optimization conditions, MST and SSSP, for example, we can use a priority queue for the dispenser and set up the prioritization so that the third invariant can be strengthened to the following:

1. 3′. Visited edges form an optimal tree for the visited vertices.