Theory Fifo_Push_Relabel
section ‹FIFO Push Relabel Algorithm›
theory Fifo_Push_Relabel
imports
Flow_Networks.Refine_Add_Fofu
Generic_Push_Relabel
begin
text ‹The FIFO push-relabel algorithm maintains a first-in-first-out queue
of active nodes. As long as the queue is not empty, it discharges the
first node of the queue.
Discharging repeatedly applied push operations from the node.
If no more push operations are possible, and the node is still active,
it is relabeled and enqueued.
Moreover, we implement the gap heuristics, which may accelerate relabeling
if there is a gap in the label values, i.e., a label value that is assigned
to no node.
›
subsection ‹Implementing the Discharge Operation›
context Network
begin
text ‹
First, we implement push and relabel operations that maintain
a queue of all active nodes.
›
definition "fifo_push f l Q ≡ λ(u,v). do {
assert (push_precond f l (u,v));
assert (Labeling c s t f l);
let Q = (if v≠s ∧ v≠t ∧ excess f v = 0 then Q@[v] else Q);
return (push_effect f (u,v),Q)
}"
text ‹For the relabel operation, we assume that
only active nodes are relabeled, and enqueue the relabeled node.
›
definition "fifo_gap_relabel f l Q u ≡ do {
assert (u∈V-{s,t});
assert (Height_Bounded_Labeling c s t f l);
let Q = Q@[u];
assert (relabel_precond f l u);
assert (l u < 2*card V ∧ relabel_effect f l u u < 2*card V);
let l = gap_relabel_effect f l u;
return (l,Q)
}"
text ‹The discharge operation iterates over the edges, and pushes
flow, as long as then node is active. If the node is still active after all
edges have been saturated, the node is relabeled.
›
definition "fifo_discharge f⇩0 l Q ≡ do {
assert (Q≠[]);
let u=hd Q; let Q=tl Q;
assert (u∈V ∧ u≠s ∧ u≠t);
(f,l,Q) ← FOREACHc {v . (u,v)∈cfE_of f⇩0} (λ(f,l,Q). excess f u ≠ 0) (λv (f,l,Q). do {
if (l u = l v + 1) then do {
(f',Q) ← fifo_push f l Q (u,v);
assert (∀v'. v'≠v ⟶ cf_of f' (u,v') = cf_of f (u,v'));
return (f',l,Q)
} else return (f,l,Q)
}) (f⇩0,l,Q);
if excess f u ≠ 0 then do {
(l,Q) ← fifo_gap_relabel f l Q u;
return (f,l,Q)
} else do {
return (f,l,Q)
}
}"
text ‹
We will show that the discharge operation maintains the invariant that the queue
is disjoint and contains exactly the active nodes:
›
definition "Q_invar f Q ≡ distinct Q ∧ set Q = { v∈V-{s,t}. excess f v ≠ 0 }"
text ‹Inside the loop of the discharge operation, we will use the following
version of the invariant:›
definition "QD_invar u f Q ≡ u∈V-{s,t} ∧ distinct Q ∧ set Q = { v∈V-{s,t,u}. excess f v ≠ 0 }"
lemma Q_invar_when_discharged1: "⟦QD_invar u f Q; excess f u = 0⟧ ⟹ Q_invar f Q"
unfolding Q_invar_def QD_invar_def by auto
lemma Q_invar_when_discharged2: "⟦QD_invar u f Q; excess f u ≠ 0⟧ ⟹ Q_invar f (Q@[u])"
unfolding Q_invar_def QD_invar_def
by auto
lemma (in Labeling) push_no_activate_pres_QD_invar:
fixes v
assumes INV: "QD_invar u f Q"
assumes PRE: "push_precond f l (u,v)"
assumes VC: "s=v ∨ t=v ∨ excess f v ≠ 0"
shows "QD_invar u (push_effect f (u,v)) Q"
proof -
interpret push_effect_locale c s t f l u v
using PRE by unfold_locales
from excess_non_negative Δ_positive have "excess f v + Δ ≠ 0" if "v∉{s,t}"
using that by force
thus ?thesis
using VC INV
unfolding QD_invar_def
by (auto simp: excess'_if split!: if_splits)
qed
lemma (in Labeling) push_activate_pres_QD_invar:
fixes v
assumes INV: "QD_invar u f Q"
assumes PRE: "push_precond f l (u,v)"
assumes VC: "s≠v" "t≠v" and [simp]: "excess f v = 0"
shows "QD_invar u (push_effect f (u,v)) (Q@[v])"
proof -
interpret push_effect_locale c s t f l u v
using PRE by unfold_locales
show ?thesis
using VC INV Δ_positive
unfolding QD_invar_def
by (auto simp: excess'_if split!: if_splits)
qed
text ‹Main theorem for the discharge operation:
It maintains a height bounded labeling, the invariant for the FIFO queue,
and only performs valid steps due to the generic push-relabel algorithm with
gap-heuristics.
›
theorem fifo_discharge_correct[THEN order_trans, refine_vcg]:
assumes DINV: "Height_Bounded_Labeling c s t f l"
assumes QINV: "Q_invar f Q" and QNE: "Q≠[]"
shows "fifo_discharge f l Q ≤ SPEC (λ(f',l',Q').
Height_Bounded_Labeling c s t f' l'
∧ Q_invar f' Q'
∧ ((f',l'),(f,l))∈gap_algo_rel⇧+
)"
proof -
from QNE obtain u Qr where [simp]: "Q=u#Qr" by (cases Q) auto
from QINV have U: "u∈V-{s,t}" "QD_invar u f Qr" and XU_orig: "excess f u ≠ 0"
by (auto simp: Q_invar_def QD_invar_def)
have [simp, intro!]: "finite {v. (u, v) ∈ cfE_of f}"
apply (rule finite_subset[where B=V])
using cfE_of_ss_VxV
by auto
show ?thesis
using U
unfolding fifo_discharge_def fifo_push_def fifo_gap_relabel_def
apply (simp only: split nres_monad_laws)
apply (rewrite in "FOREACHc _ _ ⌑ _" vcg_intro_frame)
apply (rewrite in "if excess _ _ ≠ 0 then ⌑ else _" vcg_intro_frame)
apply (refine_vcg FOREACHc_rule[where
I="λit (f',l',Q').
Height_Bounded_Labeling c s t f' l'
∧ QD_invar u f' Q'
∧ ((f',l'),(f,l))∈gap_algo_rel⇧*
∧ it ⊆ {v. (u,v) ∈ cfE_of f' }
∧ (excess f' u≠0 ⟶ (∀v∈{v. (u,v) ∈ cfE_of f' }-it. l' u ≠ l' v + 1)
)
"
])
apply (vc_solve simp: DINV QINV it_step_insert_iff split del: if_split)
subgoal for v it f' l' Q' proof -
assume HBL: "Height_Bounded_Labeling c s t f' l'"
then interpret l': Height_Bounded_Labeling c s t f' l' .
assume X: "excess f' u ≠ 0" and UI: "u ∈ V" "u ≠ s" "u ≠ t"
and QDI: "QD_invar u f' Q'"
assume "v ∈ it" and ITSS: "it ⊆ {v. (u, v) ∈ l'.cf.E}"
hence UVE: "(u,v) ∈ l'.cf.E" by auto
assume REL: "((f', l'), f, l) ∈ gap_algo_rel⇧*"
assume SAT_EDGES: "∀v∈{v. (u, v) ∈ cfE_of f'} - it. l' u ≠ Suc (l' v)"
from X UI l'.excess_non_negative have X': "excess f' u > 0" by force
have PP: "push_precond f' l' (u, v)" if "l' u = l' v + 1"
unfolding push_precond_def using that UVE X' by auto
show ?thesis
apply (rule vcg_rem_frame)
apply (rewrite in "if _ then (assert _ ⪢ ⌑) else _" vcg_intro_frame)
apply refine_vcg
apply (vc_solve simp: REL solve: PP l'.push_pres_height_bound HBL QDI split del: if_split)
subgoal proof -
assume [simp]: "l' u = Suc (l' v)"
assume PRE: "push_precond f' l' (u, v)"
then interpret pe: push_effect_locale c s t f' l' u v by unfold_locales
have UVNE': "l'.cf (u, v) ≠ 0"
using l'.resE_positive by fastforce
show ?thesis
apply (rule vcg_rem_frame)
apply refine_vcg
apply (vc_solve simp: l'.push_pres_height_bound[OF PRE])
subgoal by unfold_locales
subgoal by (auto simp: pe.cf'_alt augment_edge_cf_def)
subgoal
using l'.push_activate_pres_QD_invar[OF QDI PRE]
using l'.push_no_activate_pres_QD_invar[OF QDI PRE]
by auto
subgoal
by (meson gap_algo_rel.push REL PRE converse_rtrancl_into_rtrancl HBL)
subgoal for x proof -
assume "x∈it" "x≠v"
with ITSS have "(u,x)∈l'.cf.E" by auto
thus ?thesis
using ‹x≠v›
unfolding pe.f'_alt
apply (simp add: augment_edge_cf')
unfolding Graph.E_def
by (auto)
qed
subgoal for v' proof -
assume "excess f' u ≠ pe.Δ"
hence PED: "pe.Δ = l'.cf (u,v)"
unfolding pe.Δ_def by auto
hence E'SS: "pe.l'.cf.E ⊆ (l'.cf.E ∪ {(v,u)}) - {(u,v)}"
unfolding pe.f'_alt
apply (simp add: augment_edge_cf')
unfolding Graph.E_def
by auto
assume "v' ∈ it ⟶ v' = v" and UV'E: "(u, v') ∈ pe.l'.cf.E" and LUSLV': "l' v = l' v'"
with E'SS have "v'∉it" by auto
moreover from UV'E E'SS pe.uv_not_eq(2) have "(u,v')∈l'.cf.E" by auto
ultimately have "l' u ≠ Suc (l' v')" using SAT_EDGES by auto
with LUSLV' show False by simp
qed
done
qed
subgoal using ITSS by auto
subgoal using SAT_EDGES by auto
done
qed
subgoal premises prems for f' l' Q' proof -
from prems interpret l': Height_Bounded_Labeling c s t f' l' by simp
from prems have UI: "u∈V" "u≠s" "u≠t"
and X: "excess f' u ≠ 0"
and QDI: "QD_invar u f' Q'"
and REL: "((f', l'), f, l) ∈ gap_algo_rel⇧*"
and NO_ADM: "∀v. (u, v) ∈ l'.cf.E ⟶ l' u ≠ Suc (l' v)"
by simp_all
from X have X': "excess f' u > 0" using l'.excess_non_negative UI by force
from X' UI NO_ADM have PRE: "relabel_precond f' l' u"
unfolding relabel_precond_def by auto
from l'.height_bound ‹u∈V› card_V_ge2 have [simp]: "l' u < 2*card V" by auto
from l'.relabel_pres_height_bound[OF PRE]
interpret l'': Height_Bounded_Labeling c s t f' "relabel_effect f' l' u" .
from l''.height_bound ‹u∈V› card_V_ge2 have [simp]: "relabel_effect f' l' u u < 2*card V" by auto
show ?thesis
apply (rule vcg_rem_frame)
apply refine_vcg
apply (vc_solve
simp: UI PRE
simp: l'.gap_relabel_pres_hb_labeling[OF PRE]
simp: Q_invar_when_discharged2[OF QDI X])
subgoal by unfold_locales
subgoal
by (meson PRE REL gap_algo_rel.relabel l'.Height_Bounded_Labeling_axioms rtrancl_into_trancl2)
done
qed
subgoal by (auto simp: Q_invar_when_discharged1 Q_invar_when_discharged2)
subgoal using XU_orig by (metis Pair_inject rtranclD)
subgoal by (auto simp: Q_invar_when_discharged1)
subgoal using XU_orig by (metis Pair_inject rtranclD)
done
qed
end
subsection ‹Main Algorithm›
context Network
begin
text ‹The main algorithm initializes the flow, labeling, and the queue,
and then applies the discharge operation until the queue is empty:
›
definition "fifo_push_relabel ≡ do {
let f = pp_init_f;
let l = pp_init_l;
Q ← spec l. distinct l ∧ set l = {v∈V - {s,t}. excess f v ≠ 0};
(f,l,_) ← while⇩T (λ(f,l,Q). Q ≠ []) (λ(f,l,Q). do {
fifo_discharge f l Q
}) (f,l,Q);
assert (Height_Bounded_Labeling c s t f l);
return f
}"
text ‹Having proved correctness of the discharge operation, the correctness
theorem of the main algorithm is straightforward:
As the discharge operation implements the generic algorithm, the loop
will terminate after finitely many steps.
Upon termination, the queue that contains exactly the active nodes is empty.
Thus, all nodes are inactive, and the resulting preflow is actually a maximal
flow.
›
theorem fifo_push_relabel_correct:
"fifo_push_relabel ≤ SPEC isMaxFlow"
unfolding fifo_push_relabel_def
apply (refine_vcg
WHILET_rule[where
I="λ(f,l,Q). Height_Bounded_Labeling c s t f l ∧ Q_invar f Q"
and R="inv_image (gap_algo_rel⇧+) (λ(f,l,Q). ((f,l)))"
]
)
apply (vc_solve solve: pp_init_height_bound)
subgoal by (blast intro: wf_lex_prod wf_trancl)
subgoal unfolding Q_invar_def by auto
subgoal for initQ f l proof -
assume "Height_Bounded_Labeling c s t f l"
then interpret Height_Bounded_Labeling c s t f l .
assume "Q_invar f []"
hence "∀u∈V-{s,t}. excess f u = 0" unfolding Q_invar_def by auto
thus "isMaxFlow f" by (rule no_excess_imp_maxflow)
qed
done
end
end