About tarjan's algorithm for finding scc

Question

I'm a senior student learing informatics olympiad on algorithms, and this is my first question on stackoverflow.

In tarjan's dfs search getting lowlink(u):

low[u]=min(low[u],low[v]) (v isn't visited)

or

low[u]=min(low[u],dfn[v]) (v is still in the stack)

My question is, is it still ok to replace dfn[v] for low[v] in the second case? I know this is incorrect, but I failed finding a counter-example. Could anyone help explain this?

thx:)

Answer 1

It's correct, actually.

The proof of correctness depends on two properties of low. The first is that, for all v, there exists w reachable from v such that dfn[w] <= low[v] <= dfn[v]. The second is that, when determining whether v is a root, we have for all w reachable from v that low[v] <= dfn[w].

We can prove inductively that the first property still holds by the fact that, if there's a path from u to v and a path from v to w, then there's a path from u to w. As for the second, let low be the original array and low' be yours. It's not hard to show that, for all v, at all times, low'[v] <= low[v], so at the critical moment for v, for all w reachable from v, it holds that low'[v] <= low[v] <= dfn[w].

I imagine that the algorithm is presented the way it is to avoid the need to consider intermediate values of low.