0
$\begingroup$

I am trying to find a correct invariant of BFS. If we represent a queue as $ Q = [a_0;...; a_n]$ such that : $Q.pop() = a_n$ then I found the following invariant which I think is correct (we denote by $Q$ the queue used to run the BFS, $s$ the node in the graph from which we begin the BFS and $d$ the distance between two nodes in the graph):

  • all elements in $Q$ are in decreasing order (i.e., for all $i <j$, $d(s,a_i) \geq d(s, a_j)$ ) and $d(s,a_n) \leq d(s,a_0) \leq d(s,a_n)+1$.

So in the queue there aren't three nodes $a_i, a_j, a_k$ that are all at distinct distances from $s$.

So is this invariant correct? Is it the common invariant to use or we generally use a "simpler" invariant? (In this case It would be very nice if you can give this invariant.)

Thank you very much!

$\endgroup$
  • $\begingroup$ @Apass.Jack Thank you, you are right I meant nodes not edges. I 've edited, hope it's better now. $\endgroup$ – Name_is_anonyme Mar 4 at 15:31
  • $\begingroup$ I'd suggest looking through a good algorithms textbook; it's likely to have a proof of correctness for BFS. That proof is likely to contain an invariant (either explicitly or implicitly); see what they use. That should let you figure out what is common/normal to use. I'm not sure your sufficient will be strong enough to prove the algorithm correct, but that's how to test whether your algorithm is "correct"; try proving BFS is correct using proof by induction, and see if your invariant is enough that such a proof goes through. $\endgroup$ – D.W. Mar 4 at 21:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.