Theory EdmondsKarp_Algo
theory EdmondsKarp_Algo
imports EdmondsKarp_Termination_Abstract FordFulkerson_Algo
begin
text ‹
In this theory, we formalize an abstract version of
Edmonds-Karp algorithm, which we obtain by refining the
Ford-Fulkerson algorithm to always use shortest augmenting paths.
Then, we show that the algorithm always terminates within $O(VE)$ iterations.
›
subsection ‹Algorithm›
context Network
begin
text ‹First, we specify the refined procedure for finding augmenting paths›
definition "find_shortest_augmenting_spec f ≡ assert (NFlow c s t f) ⪢
(select p. Graph.isShortestPath (residualGraph c f) s p t)"
text ‹We show that our refined procedure is actually a refinement›
thm SELECT_refine
lemma find_shortest_augmenting_refine[refine]:
"(f',f)∈Id ⟹ find_shortest_augmenting_spec f' ≤ ⇓(⟨Id⟩option_rel) (find_augmenting_spec f)"
unfolding find_shortest_augmenting_spec_def find_augmenting_spec_def
apply (refine_vcg)
apply (auto
simp: NFlow.shortest_is_augmenting RELATESI
dest: NFlow.augmenting_path_imp_shortest)
done
text ‹Next, we specify the Edmonds-Karp algorithm.
Our first specification still uses partial correctness,
termination will be proved afterwards. ›
definition "edka_partial ≡ do {
let f = (λ_. 0);
(f,_) ← while⇗fofu_invar⇖
(λ(f,brk). ¬brk)
(λ(f,_). do {
p ← find_shortest_augmenting_spec f;
case p of
None ⇒ return (f,True)
| Some p ⇒ do {
assert (p≠[]);
assert (NPreflow.isAugmentingPath c s t f p);
assert (Graph.isShortestPath (residualGraph c f) s p t);
let f = NFlow.augment_with_path c f p;
assert (NFlow c s t f);
return (f, False)
}
})
(f,False);
assert (NFlow c s t f);
return f
}"
lemma edka_partial_refine[refine]: "edka_partial ≤ ⇓Id fofu"
unfolding edka_partial_def fofu_def
apply (refine_rcg bind_refine')
apply (refine_dref_type)
apply (vc_solve simp: find_shortest_augmenting_spec_def)
done
end
subsubsection ‹Total Correctness›
context Network begin
text ‹We specify the total correct version of Edmonds-Karp algorithm.›
definition "edka ≡ do {
let f = (λ_. 0);
(f,_) ← while⇩T⇗fofu_invar⇖
(λ(f,brk). ¬brk)
(λ(f,_). do {
p ← find_shortest_augmenting_spec f;
case p of
None ⇒ return (f,True)
| Some p ⇒ do {
assert (p≠[]);
assert (NPreflow.isAugmentingPath c s t f p);
assert (Graph.isShortestPath (residualGraph c f) s p t);
let f = NFlow.augment_with_path c f p;
assert (NFlow c s t f);
return (f, False)
}
})
(f,False);
assert (NFlow c s t f);
return f
}"
text ‹Based on the measure function, it is easy to obtain a well-founded
relation that proves termination of the loop in the Edmonds-Karp algorithm:›
definition "edka_wf_rel ≡ inv_image
(less_than_bool <*lex*> measure (λcf. ek_analysis_defs.ekMeasure cf s t))
(λ(f,brk). (¬brk,residualGraph c f))"
lemma edka_wf_rel_wf[simp, intro!]: "wf edka_wf_rel"
unfolding edka_wf_rel_def by auto
text ‹The following theorem states that the total correct
version of Edmonds-Karp algorithm refines the partial correct one.›
theorem edka_refine[refine]: "edka ≤ ⇓Id edka_partial"
unfolding edka_def edka_partial_def
apply (refine_rcg bind_refine'
WHILEIT_refine_WHILEI[where V=edka_wf_rel])
apply (refine_dref_type)
apply (simp; fail)
subgoal
txt ‹Unfortunately, the verification condition for introducing
the variant requires a bit of manual massaging to be solved:›
apply (simp)
apply (erule bind_sim_select_rule)
apply (auto split: option.split
simp: NFlow.augment_with_path_def
simp: assert_bind_spec_conv Let_def
simp: find_shortest_augmenting_spec_def
simp: edka_wf_rel_def NFlow.shortest_path_decr_ek_measure
; fail) []
done
txt ‹The other VCs are straightforward›
apply (vc_solve)
done
subsubsection ‹Complexity Analysis›
text ‹For the complexity analysis, we additionally show that the measure
function is bounded by $O(VE)$. Note that our absolute bound is not as
precise as possible, but clearly $O(VE)$.›
lemma ekMeasure_upper_bound:
"ek_analysis_defs.ekMeasure (residualGraph c (λ_. 0)) s t
< 2 * card V * card E + card V"
proof -
interpret NFlow c s t "(λ_. 0)"
by unfold_locales (auto simp: s_node t_node cap_non_negative)
interpret ek: ek_analysis cf
by unfold_locales auto
have cardV_positive: "card V > 0" and cardE_positive: "card E > 0"
using card_0_eq[OF finite_V] V_not_empty apply blast
using card_0_eq[OF finite_E] E_not_empty apply blast
done
show ?thesis proof (cases "cf.connected s t")
case False hence "ek.ekMeasure = 0" by (auto simp: ek.ekMeasure_def)
with cardV_positive cardE_positive show ?thesis
by auto
next
case True
have "cf.min_dist s t > 0"
apply (rule ccontr)
apply (auto simp: Graph.min_dist_z_iff True s_not_t[symmetric])
done
have "cf = c"
unfolding residualGraph_def E_def
by auto
hence "ek.uE = E∪E¯" unfolding ek.uE_def by simp
from True have "ek.ekMeasure
= (card cf.V - cf.min_dist s t) * (card ek.uE + 1) + (card (ek.spEdges))"
unfolding ek.ekMeasure_def by simp
also from
mlex_bound[of "card cf.V - cf.min_dist s t" "card V",
OF _ ek.card_spEdges_less]
have "… < card V * (card ek.uE+1)"
using ‹cf.min_dist s t > 0› ‹card V > 0›
by (auto simp: resV_netV)
also have "card ek.uE ≤ 2*card E" unfolding ‹ek.uE = E∪E¯›
apply (rule order_trans)
apply (rule card_Un_le)
by auto
finally show ?thesis by (auto simp: algebra_simps)
qed
qed
text ‹Finally, we present a version of the Edmonds-Karp algorithm
which is instrumented with a loop counter, and asserts that
there are less than $2|V||E|+|V| = O(|V||E|)$ iterations.
Note that we only count the non-breaking loop iterations.
›
text ‹The refinement is achieved by a refinement relation, coupling the
instrumented loop state with the uninstrumented one›
definition "edkac_rel ≡ {((f,brk,itc), (f,brk)) | f brk itc.
itc + ek_analysis_defs.ekMeasure (residualGraph c f) s t
< 2 * card V * card E + card V
}"
definition "edka_complexity ≡ do {
let f = (λ_. 0);
(f,_,itc) ← while⇩T
(λ(f,brk,_). ¬brk)
(λ(f,_,itc). do {
p ← find_shortest_augmenting_spec f;
case p of
None ⇒ return (f,True,itc)
| Some p ⇒ do {
let f = NFlow.augment_with_path c f p;
return (f, False,itc + 1)
}
})
(f,False,0);
assert (itc < 2 * card V * card E + card V);
return f
}"
lemma edka_complexity_refine: "edka_complexity ≤ ⇓Id edka"
proof -
have [refine_dref_RELATES]:
"RELATES edkac_rel"
by (auto simp: RELATES_def)
show ?thesis
unfolding edka_complexity_def edka_def
apply (refine_rcg)
apply (refine_dref_type)
apply (vc_solve simp: edkac_rel_def "NFlow.augment_with_path_def")
subgoal using ekMeasure_upper_bound by auto []
subgoal by (drule (1) NFlow.shortest_path_decr_ek_measure; auto)
done
qed
text ‹We show that this algorithm never fails, and computes a maximum flow.›
theorem "edka_complexity ≤ (spec f. isMaxFlow f)"
proof -
note edka_complexity_refine
also note edka_refine
also note edka_partial_refine
also note fofu_partial_correct
finally show ?thesis .
qed
end
end