how to prove correctness of this BFS algorithm?

Question

Given an undirected connected graph, I wrote the following algorithm based on BFS. The algorithm detects wether this graph contains a cycle. If it contains a cycle then prints it. I'm pretty sure that it works just fine, but I don't really know how to prove its correctness properly. Here is the pseudo-code:

Let s be the root
set parent[s]=s and parent[v]=null for all other v
create queue q ;
enqueue(s,q);
cycle=false;
while (!isEmpty(q) && !cycle) {
 u=front(q);
 for every edge (u,v) incident to u {
 if (parent[v]==null){
  parent[v]=u;
  enqueue(v);
 }
 else if (parent[u]!=v){
   cycle=true;
   keep the edge (u,v)
 }
dequeue(q);
if (cycle){
 print edge (u,v)
 while (parent[u]!=parent[v])&& (parent[v]!=u)&&(parent[u]!=v){
        print edge (u,parent[u]) and  edge (v,parent[v]) 
        u=parent[u];
        v=parent[v];
    }
    if (parent[u]==parent[v])
        print edge (u,parent[u]) and edge (v,parent[v]) 
    else
        print edge (u,v) 
}
/**************************************************/
/**************************************************/

I've been working on the proof but i can't get through it. First i want to prove that if G contains a cycle then the algorithm does detect it. My idea is the following: Let s be the root of the bfs. We know that G contains a cycle, so there is a node such that there are two different paths from s to such a node. Let u be the first node that satisfies this. Since that BFS visits all the nodes, and explores each edge once, and also marks as visited all nodes that were visited, it will reach a step in which it is about to visit the node u for the second time and then it finds the cycle.

Then I want to prove that in the afirmative case, the edges that it prints does forms a cycle, but i'm really stuck with this.

Answer 1

I believe your problem has been resolved as this is an old question, but here is a solution just to add up to your knowledge.

Proof of Correctness of BFS

First, two kinds of annoying lemmas. These help us formalize what’s going on as the algorithm is running.

Lemma 1. At end of BFS, for all $v ∈ V$, $\newcommand{\dist}{\operatorname{dist}}\dist(v)$ is at least the distance from $s$ to $v$.

Proof. Will show by induction that at each iteration of loop, this holds for all $v$.

Base Case: 0th iteration.

Inductive Hypothesis: Assume true for the $k$th iteration.

Inductive Case: Consider the vertex $v$ removed from queue on $(k + 1)$st iteration.

• Only changes $\dist(u)$ for a few vertices, and only if $u$ is adjacent to $v$.
• For vertices not changed, use IH.
• Otherwise,
  ∗ distance from $s$ to $v$
  ∗ ≤ distance from $s$ to $u + 1$
  ∗ ≤ $\dist(u)+1$
  ∗ = $\dist(v)$.

Lemma 2. For any $k$, let $(v_1, \dots , v_r)$ be the elements of the queue at iteration $k$. At this iteration,

1. $\dist(v_1) ≥ \dist(v_r) − 1$
2. For any $i < j$, $\dist(v_i) < \dist(v_j)$

Proof. Induction

Base Case: Initially, queue is empty.

Inductive Hypothesis: Assume true for $k$th iteration.

Inductive Case: Consider $(k + 1)$st iteration.

• Remove $v_1$ from queue. New front is $v_2$.
• Enqueue neighbors of $v_1$.
  ∗ Let $u$ be a neighbor.
  ∗ $\dist(u)$ is set to $\dist(v_1) + 1 ≥ \dist(v_r) − 1 + 1 = \dist(v_r)$, so 2. still holds.
  ∗ $\dist(v_2) ≥ \dist(v_1) = \dist(u) − 1$, so 1. still holds.

Corollary: Let $v_k$ be the $k$th vertex to have $\dist(v)$ set. $\dist(v_k)$ is increasing in $k$.

Finally, the proof of correctness. At the termination of BFS, if BFS explores $v$, then $\dist(v)$ is the distance from $s$ to $v$.

Proof by contradiction.

• Assume there’s some vertex with $\dist()$ not equal to the distance from $s$.
• Let $v$ be such a vertex which is the smallest distance from $s$.
• Let $u$ be its predecessor on shortest path from $v$ to $u$.
• By lemma 1, $\dist(v) > $ distance from $s$ to $v$
• = (distance from $s$ to $u$)$ + 1 = \dist(u) + 1$
• Consider when $u$ was dequeued. We’ll contradict the above chain of inequalities in any of the three cases:
  – If $v$ wasn’t explored yet, $v$ would have been enqueued with $\dist(v)=\dist(u)+1$. Contradiction to above inequalities.
  – If $v$ is on the queue, then $\operatorname{parent}(v)$ has lower $\dist$ than $u$ does, by corollary to lemma 2. Then $\dist(v) = \dist(\operatorname{parent}(v)) + 1 ≤ \dist(u) + 1$, again contradicting the inequalities.
  – If v has already been dequeued, then $\dist(v) ≤ \dist(u)$. Contradiction again.

Watch the video for clear understanding, along with visual description

Answer 2

Assuming the graph has no cycles in it, the graph is hence a tree. Since in a tree, there is a unique path between two vertices, we will never encounter a visited vertex and hence our algorithm will not detect a cycle.

Now assuming there is at least one cycle in the graph. Consider the set $S$ of vertices, that belong to a cycle and have the least possible distance to $s$. Any two vertices in $S$ can not belong to the same cycle, since then they will form a cycle with a vertex with a smaller depth in the BFS-tree, which contradicts the assumption that they are closest possible to $s$. All these vertices belong to the same level of the BFS-tree since they have the same distance to $s$. The BFS-tree branches at each of them to at least two branches. Sice they all belong to cycles in the graph, there must exist an edge between two branches from the subtree rooted at one of them. This edge has its endpoints between two nodes on the same level in the tree, since else, one of them could have been visited by the other and get a smaller depth. When visiting this edge, our algorithm detects a cycle. The Cycle is hence this edge along with both paths in the BFS-tree from a vertex $v \in S$, to the endpoints of this edge. We output exactly these edges, where we start by printing this edge and backtrack on both branches until we reach back the vertex $v$ .