theory CDCL_W_Termination
imports CDCL_W
begin
context cdcl⇩W
begin
subsection ‹Termination›
text ‹The condition that no learned clause is a tautology is overkill (in the sense that the
no-duplicate condition is enough), but we can reuse @{term simple_clss}.
The invariant contains all the structural invariants that holds,›
definition cdcl⇩W_all_struct_inv where
"cdcl⇩W_all_struct_inv S =
(no_strange_atm S ∧ cdcl⇩W_M_level_inv S
∧ (∀s ∈# learned_clss S. ¬tautology s)
∧ distinct_cdcl⇩W_state S ∧ cdcl⇩W_conflicting S
∧ all_decomposition_implies_m (init_clss S) (get_all_decided_decomposition (trail S))
∧ cdcl⇩W_learned_clause S)"
lemma cdcl⇩W_all_struct_inv_inv:
assumes "cdcl⇩W S S'" and "cdcl⇩W_all_struct_inv S"
shows "cdcl⇩W_all_struct_inv S'"
unfolding cdcl⇩W_all_struct_inv_def
proof (intro HOL.conjI)
show "no_strange_atm S'"
using cdcl⇩W_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by auto
show "cdcl⇩W_M_level_inv S'"
using cdcl⇩W_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "distinct_cdcl⇩W_state S'"
using cdcl⇩W_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "cdcl⇩W_conflicting S'"
using cdcl⇩W_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "all_decomposition_implies_m (init_clss S') (get_all_decided_decomposition (trail S'))"
using cdcl⇩W_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "cdcl⇩W_learned_clause S'"
using cdcl⇩W_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "∀s∈#learned_clss S'. ¬ tautology s"
using assms(1)[THEN learned_clss_are_not_tautologies] assms(2)
unfolding cdcl⇩W_all_struct_inv_def by fast
qed
lemma rtranclp_cdcl⇩W_all_struct_inv_inv:
assumes "cdcl⇩W⇧*⇧* S S'" and "cdcl⇩W_all_struct_inv S"
shows "cdcl⇩W_all_struct_inv S'"
using assms by induction (auto intro: cdcl⇩W_all_struct_inv_inv)
lemma cdcl⇩W_stgy_cdcl⇩W_all_struct_inv:
"cdcl⇩W_stgy S T ⟹ cdcl⇩W_all_struct_inv S ⟹ cdcl⇩W_all_struct_inv T"
by (meson cdcl⇩W_stgy_tranclp_cdcl⇩W rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_unfold)
lemma rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv:
"cdcl⇩W_stgy⇧*⇧* S T ⟹ cdcl⇩W_all_struct_inv S ⟹ cdcl⇩W_all_struct_inv T"
by (induction rule: rtranclp_induct) (auto intro: cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)
subsection ‹No Relearning of a clause›
lemma cdcl⇩W_o_new_clause_learned_is_backtrack_step:
assumes learned: "D ∈# learned_clss T" and
new: "D ∉# learned_clss S" and
cdcl⇩W: "cdcl⇩W_o S T" and
lev: "cdcl⇩W_M_level_inv S"
shows "backtrack S T ∧ conflicting S = Some D"
using cdcl⇩W lev learned new
proof (induction rule: cdcl⇩W_o_induct_lev2)
case (backtrack K i M1 M2 L C T) note decomp =this(1) and undef = this(6) and T = this(7) and
D_T = this(9) and D_S = this(10)
then have "D = C + {#L#}"
using not_gr0 lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
then show ?case
using T backtrack.hyps(1-5) backtrack.intros by auto
qed auto
lemma cdcl⇩W_cp_new_clause_learned_has_backtrack_step:
assumes learned: "D ∈# learned_clss T" and
new: "D ∉# learned_clss S" and
cdcl⇩W: "cdcl⇩W_stgy S T" and
lev: "cdcl⇩W_M_level_inv S"
shows "∃S'. backtrack S S' ∧ cdcl⇩W_stgy⇧*⇧* S' T ∧ conflicting S = Some D"
using cdcl⇩W learned new
proof (induction rule: cdcl⇩W_stgy.induct)
case (conflict' S')
then show ?case
unfolding full1_def by (metis (mono_tags, lifting) rtranclp_cdcl⇩W_cp_learned_clause_inv
tranclp_into_rtranclp)
next
case (other' S' S'')
then have "D ∈# learned_clss S'"
unfolding full_def by (auto dest: rtranclp_cdcl⇩W_cp_learned_clause_inv)
then show ?case
using cdcl⇩W_o_new_clause_learned_is_backtrack_step[OF _ ‹D ∉# learned_clss S› ‹cdcl⇩W_o S S'›]
‹full cdcl⇩W_cp S' S''› lev by (metis cdcl⇩W_stgy.conflict' full_unfold r_into_rtranclp
rtranclp.rtrancl_refl)
qed
lemma rtranclp_cdcl⇩W_cp_new_clause_learned_has_backtrack_step:
assumes learned: "D ∈# learned_clss T" and
new: "D ∉# learned_clss S" and
cdcl⇩W: "cdcl⇩W_stgy⇧*⇧* S T" and
lev: "cdcl⇩W_M_level_inv S"
shows "∃S' S''. cdcl⇩W_stgy⇧*⇧* S S' ∧ backtrack S' S'' ∧ conflicting S' = Some D ∧
cdcl⇩W_stgy⇧*⇧* S'' T"
using cdcl⇩W learned new
proof (induction rule: rtranclp_induct)
case base
then show ?case by blast
next
case (step T U) note st =this(1) and o = this(2) and IH = this(3) and
D_U = this(4) and D_S = this(5)
show ?case
proof (cases "D ∈# learned_clss T")
case True
then obtain S' S'' where
st': "cdcl⇩W_stgy⇧*⇧* S S'" and
bt: "backtrack S' S''" and
confl: "conflicting S' = Some D" and
st'': "cdcl⇩W_stgy⇧*⇧* S'' T"
using IH D_S by metis
then show ?thesis using o by (meson rtranclp.simps)
next
case False
have "cdcl⇩W_M_level_inv T"
using lev rtranclp_cdcl⇩W_stgy_consistent_inv st by blast
then obtain S' where
bt: "backtrack T S'" and
st': "cdcl⇩W_stgy⇧*⇧* S' U" and
confl: "conflicting T = Some D"
using cdcl⇩W_cp_new_clause_learned_has_backtrack_step[OF D_U False o]
by metis
then have "cdcl⇩W_stgy⇧*⇧* S T" and
"backtrack T S'" and
"conflicting T = Some D" and
"cdcl⇩W_stgy⇧*⇧* S' U"
using o st by auto
then show ?thesis by blast
qed
qed
lemma propagate_no_more_Decided_lit:
assumes "propagate S S'"
shows "Decided K i ∈ set (trail S) ⟷ Decided K i ∈ set (trail S')"
using assms by auto
lemma conflict_no_more_Decided_lit:
assumes "conflict S S'"
shows "Decided K i ∈ set (trail S) ⟷ Decided K i ∈ set (trail S')"
using assms by auto
lemma cdcl⇩W_cp_no_more_Decided_lit:
assumes "cdcl⇩W_cp S S'"
shows "Decided K i ∈ set (trail S) ⟷ Decided K i ∈ set (trail S')"
using assms apply (induct rule: cdcl⇩W_cp.induct)
using conflict_no_more_Decided_lit propagate_no_more_Decided_lit by auto
lemma rtranclp_cdcl⇩W_cp_no_more_Decided_lit:
assumes "cdcl⇩W_cp⇧*⇧* S S'"
shows "Decided K i ∈ set (trail S) ⟷ Decided K i ∈ set (trail S')"
using assms apply (induct rule: rtranclp_induct)
using cdcl⇩W_cp_no_more_Decided_lit by blast+
lemma cdcl⇩W_o_no_more_Decided_lit:
assumes "cdcl⇩W_o S S'" and "cdcl⇩W_M_level_inv S" and "¬decide S S'"
shows "Decided K i ∈ set (trail S') ⟶ Decided K i ∈ set (trail S)"
using assms
proof (induct rule: cdcl⇩W_o_induct_lev2)
case backtrack note decomp = this(1) and undef = this(6) and T =this(7) and lev = this(8)
then show ?case
by (auto simp: cdcl⇩W_M_level_inv_decomp)
next
case (decide L T)
then show ?case by blast
qed auto
lemma cdcl⇩W_new_decided_at_beginning_is_decide:
assumes "cdcl⇩W_stgy S S'" and
lev: "cdcl⇩W_M_level_inv S" and
"trail S' = M' @ Decided L i # M" and
"trail S = M"
shows "∃T. decide S T ∧ no_step cdcl⇩W_cp S"
using assms
proof (induct rule: cdcl⇩W_stgy.induct)
case (conflict' S') note st =this(1) and no_dup = this(2) and S' = this(3) and S = this(4)
have "cdcl⇩W_M_level_inv S'"
using full1_cdcl⇩W_cp_consistent_inv no_dup st by blast
then have "Decided L i ∈ set (trail S')" and "Decided L i ∉ set (trail S)"
using no_dup unfolding S S' cdcl⇩W_M_level_inv_def by (auto simp add: rev_image_eqI)
then have False
using st rtranclp_cdcl⇩W_cp_no_more_Decided_lit[of S S']
unfolding full1_def rtranclp_unfold by blast
then show ?case by fast
next
case (other' T U) note o = this(1) and ns = this(2) and st = this(3) and no_dup = this(4) and
S' = this(5) and S = this(6)
have "cdcl⇩W_M_level_inv U"
by (metis (full_types) lev cdcl⇩W.simps cdcl⇩W_consistent_inv full_def o
other'.hyps(3) rtranclp_cdcl⇩W_cp_consistent_inv)
then have "Decided L i ∈ set (trail U)" and "Decided L i ∉ set (trail S)"
using no_dup unfolding S S' cdcl⇩W_M_level_inv_def by (auto simp add: rev_image_eqI)
then have "Decided L i ∈ set (trail T)"
using st rtranclp_cdcl⇩W_cp_no_more_Decided_lit unfolding full_def by blast
then show ?case
using cdcl⇩W_o_no_more_Decided_lit[OF o] ‹Decided L i ∉ set (trail S)› ns lev by meson
qed
lemma cdcl⇩W_o_is_decide:
assumes "cdcl⇩W_o S' T" and "cdcl⇩W_M_level_inv S'"
"trail T = drop (length M⇩0) M' @ Decided L i # H @ M"and
"¬ (∃M'. trail S' = M' @ Decided L i # H @ M)"
shows "decide S' T"
using assms
proof (induction rule:cdcl⇩W_o_induct_lev2)
case (backtrack K i M1 M2 L D)
then obtain c where "trail S' = c @ M2 @ Decided K (Suc i) # M1"
by auto
then show ?case
using backtrack by (cases "drop (length M⇩0) M'") (auto simp: cdcl⇩W_M_level_inv_def)
next
case decide
show ?case using decide_rule[of S'] decide(1-4) by auto
qed auto
lemma rtranclp_cdcl⇩W_new_decided_at_beginning_is_decide:
assumes "cdcl⇩W_stgy⇧*⇧* R U" and
"trail U = M' @ Decided L i # H @ M" and
"trail R = M" and
"cdcl⇩W_M_level_inv R"
shows
"∃S T T'. cdcl⇩W_stgy⇧*⇧* R S ∧ decide S T ∧ cdcl⇩W_stgy⇧*⇧* T U ∧ cdcl⇩W_stgy⇧*⇧* S U ∧
no_step cdcl⇩W_cp S ∧ trail T = Decided L i # H @ M ∧ trail S = H @ M ∧ cdcl⇩W_stgy S T' ∧
cdcl⇩W_stgy⇧*⇧* T' U"
using assms
proof (induct arbitrary: M H M' i rule: rtranclp_induct)
case base
then show ?case by auto
next
case (step T U) note st = this(1) and IH = this(3) and s = this(2) and
U = this(4) and S = this(5) and lev = this(6)
show ?case
proof (cases "∃M'. trail T = M' @ Decided L i # H @ M")
case False
with s show ?thesis using U s st S
proof induction
case (conflict' W) note cp = this(1) and nd = this(2) and W = this(3)
then obtain M⇩0 where "trail W = M⇩0 @ trail T" and ndecided: "∀l∈set M⇩0. ¬ is_decided l"
using rtranclp_cdcl⇩W_cp_dropWhile_trail unfolding full1_def rtranclp_unfold by meson
then have MV: "M' @ Decided L i # H @ M = M⇩0 @ trail T" unfolding W by simp
then have V: "trail T = drop (length M⇩0) (M' @ Decided L i # H @ M)"
by auto
have "takeWhile (Not o is_decided) M' = M⇩0 @ takeWhile (Not ∘ is_decided) (trail T)"
using arg_cong[OF MV, of "takeWhile (Not o is_decided)"] ndecided
by (simp add: takeWhile_tail)
from arg_cong[OF this, of length] have "length M⇩0 ≤ length M'"
unfolding length_append by (metis (no_types, lifting) Nat.le_trans le_add1
length_takeWhile_le)
then have False using nd V by auto
then show ?case by fast
next
case (other' T' U) note o = this(1) and ns =this(2) and cp = this(3) and nd = this(4)
and U = this(5) and st = this(6)
obtain M⇩0 where "trail U = M⇩0 @ trail T'" and ndecided: "∀l∈set M⇩0. ¬ is_decided l"
using rtranclp_cdcl⇩W_cp_dropWhile_trail cp unfolding full_def by meson
then have MV: "M' @ Decided L i # H @ M = M⇩0 @ trail T'" unfolding U by simp
then have V: "trail T' = drop (length M⇩0) (M' @ Decided L i # H @ M)"
by auto
have "takeWhile (Not o is_decided) M' = M⇩0 @ takeWhile (Not ∘ is_decided) (trail T')"
using arg_cong[OF MV, of "takeWhile (Not o is_decided)"] ndecided
by (simp add: takeWhile_tail)
from arg_cong[OF this, of length] have "length M⇩0 ≤ length M'"
unfolding length_append by (metis (no_types, lifting) Nat.le_trans le_add1
length_takeWhile_le)
then have tr_T': "trail T' = drop (length M⇩0) M' @ Decided L i # H @ M" using V by auto
then have LT': "Decided L i ∈ set (trail T')" by auto
moreover
have "cdcl⇩W_M_level_inv T"
using lev rtranclp_cdcl⇩W_stgy_consistent_inv step.hyps(1) by blast
then have "decide T T'" using o nd tr_T' cdcl⇩W_o_is_decide by metis
ultimately have "decide T T'" using cdcl⇩W_o_no_more_Decided_lit[OF o] by blast
then have 1: "cdcl⇩W_stgy⇧*⇧* R T" and 2: "decide T T'" and 3: "cdcl⇩W_stgy⇧*⇧* T' U"
using st other'.prems(4)
by (metis cdcl⇩W_stgy.conflict' cp full_unfold r_into_rtranclp rtranclp.rtrancl_refl)+
have [simp]: "drop (length M⇩0) M' = []"
using ‹decide T T'› ‹Decided L i ∈ set (trail T')› nd tr_T'
by (auto simp add: Cons_eq_append_conv)
have T': "drop (length M⇩0) M' @ Decided L i # H @ M = Decided L i # trail T"
using ‹decide T T'› ‹Decided L i ∈ set (trail T')› nd tr_T'
by auto
have "trail T' = Decided L i # trail T"
using ‹decide T T'› ‹Decided L i ∈ set (trail T')› tr_T'
by auto
then have 5: "trail T' = Decided L i # H @ M"
using append.simps(1) list.sel(3) local.other'(5) tl_append2 by (simp add: tr_T')
have 6: "trail T = H @ M"
by (metis (no_types) ‹trail T' = Decided L i # trail T›
‹trail T' = drop (length M⇩0) M' @ Decided L i # H @ M› append_Nil list.sel(3) nd
tl_append2)
have 7: "cdcl⇩W_stgy⇧*⇧* T U" using other'.prems(4) st by auto
have 8: "cdcl⇩W_stgy T U" "cdcl⇩W_stgy⇧*⇧* U U"
using cdcl⇩W_stgy.other'[OF other'(1-3)] by simp_all
show ?case apply (rule exI[of _ T], rule exI[of _ T'], rule exI[of _ U])
using ns 1 2 3 5 6 7 8 by fast
qed
next
case True
then obtain M' where T: "trail T = M' @ Decided L i # H @ M" by metis
from IH[OF this S lev] obtain S' S'' S''' where
1: "cdcl⇩W_stgy⇧*⇧* R S'" and
2: "decide S' S''" and
3: "cdcl⇩W_stgy⇧*⇧* S'' T " and
4: "no_step cdcl⇩W_cp S'" and
6: "trail S'' = Decided L i # H @ M" and
7: "trail S' = H @ M" and
8: "cdcl⇩W_stgy⇧*⇧* S' T" and
9: "cdcl⇩W_stgy S' S'''" and
10: "cdcl⇩W_stgy⇧*⇧* S''' T"
by blast
have "cdcl⇩W_stgy⇧*⇧* S'' U" using s ‹cdcl⇩W_stgy⇧*⇧* S'' T › by auto
moreover have "cdcl⇩W_stgy⇧*⇧* S' U" using "8" s by auto
moreover have "cdcl⇩W_stgy⇧*⇧* S''' U" using 10 s by auto
ultimately show ?thesis apply - apply (rule exI[of _ S'], rule exI[of _ S''])
using 1 2 4 6 7 8 9 by blast
qed
qed
lemma rtranclp_cdcl⇩W_new_decided_at_beginning_is_decide':
assumes "cdcl⇩W_stgy⇧*⇧* R U" and
"trail U = M' @ Decided L i # H @ M" and
"trail R = M" and
"cdcl⇩W_M_level_inv R"
shows "∃y y'. cdcl⇩W_stgy⇧*⇧* R y ∧ cdcl⇩W_stgy y y' ∧ ¬ (∃c. trail y = c @ Decided L i # H @ M)
∧ (λa b. cdcl⇩W_stgy a b ∧ (∃c. trail a = c @ Decided L i # H @ M))⇧*⇧* y' U"
proof -
fix T'
obtain S' T T' where
st: "cdcl⇩W_stgy⇧*⇧* R S'" and
"decide S' T" and
TU: "cdcl⇩W_stgy⇧*⇧* T U" and
"no_step cdcl⇩W_cp S'" and
trT: "trail T = Decided L i # H @ M" and
trS': "trail S' = H @ M" and
S'U: "cdcl⇩W_stgy⇧*⇧* S' U" and
S'T': "cdcl⇩W_stgy S' T'" and
T'U: "cdcl⇩W_stgy⇧*⇧* T' U"
using rtranclp_cdcl⇩W_new_decided_at_beginning_is_decide[OF assms] by blast
have n: "¬ (∃c. trail S' = c @ Decided L i # H @ M)" using trS' by auto
show ?thesis
using rtranclp_trans[OF st] rtranclp_exists_last_with_prop[of cdcl⇩W_stgy S' T' _
"λa _. ¬(∃c. trail a = c @ Decided L i # H @ M)", OF S'T' T'U n]
by meson
qed
lemma beginning_not_decided_invert:
assumes A: "M @ A = M' @ Decided K i # H" and
nm: "∀m∈set M. ¬is_decided m"
shows "∃M. A = M @ Decided K i # H"
proof -
have "A = drop (length M) (M' @ Decided K i # H)"
using arg_cong[OF A, of "drop (length M)"] by auto
moreover have "drop (length M) (M' @ Decided K i # H) = drop (length M) M' @ Decided K i # H"
using nm by (metis (no_types, lifting) A drop_Cons' drop_append ann_literal.disc(1) not_gr0
nth_append nth_append_length nth_mem zero_less_diff)
finally show ?thesis by fast
qed
lemma cdcl⇩W_stgy_trail_has_new_decided_is_decide_step:
assumes "cdcl⇩W_stgy S T"
"¬ (∃c. trail S = c @ Decided L i # H @ M)" and
"(λa b. cdcl⇩W_stgy a b ∧ (∃c. trail a = c @ Decided L i # H @ M))⇧*⇧* T U" and
"∃M'. trail U = M' @ Decided L i # H @ M" and
lev: "cdcl⇩W_M_level_inv S"
shows "∃S'. decide S S' ∧ full cdcl⇩W_cp S' T ∧ no_step cdcl⇩W_cp S"
using assms(3,1,2,4,5)
proof induction
case (step T U)
then show ?case by fastforce
next
case base
then show ?case
proof (induction rule: cdcl⇩W_stgy.induct)
case (conflict' T) note cp = this(1) and nd = this(2) and M' =this(3) and no_dup = this(3)
then obtain M' where M': "trail T = M' @ Decided L i # H @ M" by metis
obtain M'' where M'': "trail T = M'' @ trail S" and nm: "∀m∈ set M''. ¬is_decided m"
using cp unfolding full1_def
by (metis rtranclp_cdcl⇩W_cp_dropWhile_trail' tranclp_into_rtranclp)
have False
using beginning_not_decided_invert[of M'' "trail S" M' L i "H @ M"] M' nm nd unfolding M''
by fast
then show ?case by fast
next
case (other' T U') note o = this(1) and ns = this(2) and cp = this(3) and nd = this(4)
and trU' = this(5)
have "cdcl⇩W_cp⇧*⇧* T U'" using cp unfolding full_def by blast
from rtranclp_cdcl⇩W_cp_dropWhile_trail[OF this]
have "∃M'. trail T = M' @ Decided L i # H @ M"
using trU' beginning_not_decided_invert[of _ "trail T" _ L i "H @ M"] by metis
then obtain M' where M': "trail T = M' @ Decided L i # H @ M"
by auto
with o lev nd cp ns
show ?case
proof (induction rule: cdcl⇩W_o_induct_lev2)
case (decide L) note dec = this(1) and cp = this(5) and ns = this(4)
then have "decide S (cons_trail (Decided L (backtrack_lvl S +1)) (incr_lvl S))"
using decide.hyps decide.intros[of S] by force
then show ?case using cp decide.prems by (meson decide_state_eq_compatible ns state_eq_ref
state_eq_sym)
next
case (backtrack K j M1 M2 L' D T) note decomp = this(1) and cp = this(3)
and undef = this(6) and T = this(7) and trT = this(12) and ns = this(4)
obtain MS3 where MS3: "trail S = MS3 @ M2 @ Decided K (Suc j) # M1"
using get_all_decided_decomposition_exists_prepend[OF decomp] by metis
have "tl (M' @ Decided L i # H @ M) = tl M' @ Decided L i # H @ M"
using lev trT T lev undef decomp by (cases M') (auto simp: cdcl⇩W_M_level_inv_decomp)
then have M'': "M1 = tl M' @ Decided L i # H @ M"
using arg_cong[OF trT[simplified], of tl] T decomp undef lev
by (simp add: cdcl⇩W_M_level_inv_decomp)
have False using nd MS3 T undef decomp unfolding M'' by auto
then show ?case by fast
qed auto
qed
qed
lemma rtranclp_cdcl⇩W_stgy_with_trail_end_has_trail_end:
assumes "(λa b. cdcl⇩W_stgy a b ∧ (∃c. trail a = c @ Decided L i # H @ M))⇧*⇧* T U" and
"∃M'. trail U = M' @ Decided L i # H @ M"
shows "∃M'. trail T = M' @ Decided L i # H @ M"
using assms by (induction rule: rtranclp_induct) auto
lemma cdcl⇩W_o_cannot_learn:
assumes
"cdcl⇩W_o y z" and
lev: "cdcl⇩W_M_level_inv y" and
trM: "trail y = c @ Decided Kh i # H" and
DL: "D + {#L#} ∉# learned_clss y" and
DH: "atms_of D ⊆ atm_of `lits_of H" and
LH: "atm_of L ∉ atm_of `lits_of H" and
learned: "∀T. conflicting y = Some T ⟶ trail y ⊨as CNot T" and
z: "trail z = c' @ Decided Kh i # H"
shows "D + {#L#} ∉# learned_clss z"
using assms(1-2) trM DL DH LH learned z
proof (induction rule: cdcl⇩W_o_induct_lev2)
case (backtrack K j M1 M2 L' D' T) note decomp = this(1) and confl = this(3) and levD = this(5)
and undef = this(6) and T = this(7)
obtain M3 where M3: "trail y = M3 @ M2 @ Decided K (Suc j) # M1"
using decomp get_all_decided_decomposition_exists_prepend by metis
have M: "trail y = c @ Decided Kh i # H" using trM by simp
have H: "get_all_levels_of_decided (trail y) = rev [1..<1 + backtrack_lvl y]"
using lev unfolding cdcl⇩W_M_level_inv_def by auto
have "c' @ Decided Kh i # H = Propagated L' (D' + {#L'#}) # trail (reduce_trail_to M1 y)"
using backtrack.prems(6) decomp undef T lev by (force simp: cdcl⇩W_M_level_inv_def)
then obtain d where d: "M1 = d @ Decided Kh i # H"
by (metis (no_types) decomp in_get_all_decided_decomposition_trail_update_trail list.inject
list.sel(3) ann_literal.distinct(1) self_append_conv2 tl_append2)
have "i ∈ set (get_all_levels_of_decided (M3 @ M2 @ Decided K (Suc j) # d @ Decided Kh i # H))"
by auto
then have "i > 0" unfolding H[unfolded M3 d] by auto
show ?case
proof
assume "D + {#L#} ∈# learned_clss T"
then have DLD': "D + {#L#} = D' + {#L'#}"
using DL T neq0_conv undef decomp lev by (fastforce simp: cdcl⇩W_M_level_inv_def)
have L_cKh: "atm_of L ∈ atm_of `lits_of (c @ [Decided Kh i])"
using LH learned M DLD'[symmetric] confl by (fastforce simp add: image_iff)
have "get_all_levels_of_decided (M3 @ M2 @ Decided K (j + 1) # M1)
= rev [1..<1 + backtrack_lvl y]"
using lev unfolding cdcl⇩W_M_level_inv_def M3 by auto
from arg_cong[OF this, of "λa. (Suc j) ∈ set a"] have "backtrack_lvl y ≥ j" by auto
have DD'[simp]: "D = D'"
proof (rule ccontr)
assume "D ≠ D'"
then have "L' ∈# D" using DLD' by (metis add.left_neutral count_single count_union
diff_union_cancelR neq0_conv union_single_eq_member)
then have "get_level (trail y) L' ≤ get_maximum_level (trail y) D"
using get_maximum_level_ge_get_level by blast
moreover {
have "get_maximum_level (trail y) D = get_maximum_level H D"
using DH unfolding M by (simp add: get_maximum_level_skip_beginning)
moreover
have "get_all_levels_of_decided (trail y) = rev [1..<1 + backtrack_lvl y]"
using lev unfolding cdcl⇩W_M_level_inv_def by auto
then have "get_all_levels_of_decided H = rev [1..< i]"
unfolding M by (auto dest: append_cons_eq_upt_length_i
simp add: rev_swap[symmetric])
then have "get_maximum_possible_level H < i"
using get_maximum_possible_level_max_get_all_levels_of_decided[of H] ‹i > 0› by auto
ultimately have "get_maximum_level (trail y) D < i"
by (metis (full_types) dual_order.strict_trans nat_neq_iff not_le
get_maximum_possible_level_ge_get_maximum_level) }
moreover
have "L ∈# D'"
by (metis DLD' ‹D ≠ D'› add.left_neutral count_single count_union diff_union_cancelR
neq0_conv union_single_eq_member)
then have "get_maximum_level (trail y) D' ≥ get_level (trail y) L"
using get_maximum_level_ge_get_level by blast
moreover {
have "get_all_levels_of_decided (c @ [Decided Kh i]) = rev [i..< backtrack_lvl y+1]"
using append_cons_eq_upt_length_i_end[of " rev (get_all_levels_of_decided H)" i
"rev (get_all_levels_of_decided c)" "Suc 0" "Suc (backtrack_lvl y)"] H
unfolding M apply (auto simp add: rev_swap[symmetric])
by (metis (no_types, hide_lams) Nil_is_append_conv Suc_le_eq less_Suc_eq list.sel(1)
rev.simps(2) rev_rev_ident upt_Suc upt_rec)
have "get_level (trail y) L = get_level (c @ [Decided Kh i]) L"
using L_cKh LH unfolding M by simp
have "get_level (c @ [Decided Kh i]) L ≥ i"
using L_cKh
‹get_all_levels_of_decided (c @ [Decided Kh i]) = rev [i..<backtrack_lvl y + 1]›
backtrack.hyps(2) calculation(1,2) by auto
then have "get_level (trail y) L ≥ i"
using M ‹get_level (trail y) L = get_level (c @ [Decided Kh i]) L› by auto }
moreover have "get_maximum_level (trail y) D' < get_level (trail y) L"
using ‹j ≤ backtrack_lvl y› backtrack.hyps(2,5) calculation(1-4) by linarith
ultimately show False using backtrack.hyps(4) by linarith
qed
then have LL': "L = L'" using DLD' by auto
have nd: "no_dup (trail y)" using lev unfolding cdcl⇩W_M_level_inv_def by auto
{ assume D: "D' = {#}"
then have j: "j = 0" using levD by auto
have "∀m ∈ set M1. ¬is_decided m"
using H unfolding M3 j
by (auto simp add: rev_swap[symmetric] get_all_levels_of_decided_no_decided
dest!: append_cons_eq_upt_length_i)
then have False using d by auto
}
moreover {
assume D[simp]: "D' ≠ {#}"
have "i ≤ j"
using H unfolding M3 d by (auto simp add: rev_swap[symmetric]
dest: upt_decomp_lt)
have "j > 0" apply (rule ccontr)
using H ‹ i > 0› unfolding M3 d
by (auto simp add: rev_swap[symmetric] dest!: upt_decomp_lt)
obtain L'' where
"L''∈#D'" and
L''D': "get_level (trail y) L'' = get_maximum_level (trail y) D'"
using get_maximum_level_exists_lit_of_max_level[OF D, of "trail y"] by auto
have L''M: "atm_of L'' ∈ atm_of ` lits_of (trail y)"
using get_rev_level_ge_0_atm_of_in[of 0 "rev (trail y)" L''] ‹j>0› levD L''D' by auto
then have "L'' ∈ lits_of (Decided Kh i # d)"
proof -
{
assume L''H: "atm_of L'' ∈ atm_of ` lits_of H"
have "get_all_levels_of_decided H = rev [1..<i]"
using H unfolding M
by (auto simp add: rev_swap[symmetric] dest!: append_cons_eq_upt_length_i)
moreover have "get_level (trail y) L'' = get_level H L''"
using L''H unfolding M by simp
ultimately have False
using levD ‹j>0› get_rev_level_in_levels_of_decided[of "rev H" 0 L''] ‹i ≤ j›
unfolding L''D'[symmetric] nd by auto
}
then show ?thesis
using DD' DH ‹L'' ∈# D'› atm_of_lit_in_atms_of contra_subsetD by metis
qed
then have False
using DH ‹L''∈#D'› nd unfolding M3 d
by (auto simp add: atms_of_def image_iff image_subset_iff lits_of_def)
}
ultimately show False by blast
qed
qed auto
lemma cdcl⇩W_stgy_with_trail_end_has_not_been_learned:
assumes "cdcl⇩W_stgy y z" and
"cdcl⇩W_M_level_inv y" and
"trail y = c @ Decided Kh i # H" and
"D + {#L#} ∉# learned_clss y" and
DH: "atms_of D ⊆ atm_of `lits_of H" and
LH: "atm_of L ∉ atm_of `lits_of H" and
"∀T. conflicting y = Some T ⟶ trail y ⊨as CNot T" and
"trail z = c' @ Decided Kh i # H"
shows "D + {#L#} ∉# learned_clss z"
using assms
proof induction
case conflict'
then show ?case
unfolding full1_def using tranclp_cdcl⇩W_cp_learned_clause_inv by auto
next
case (other' T U) note o = this(1) and cp = this(3) and lev = this(4) and trY = this(5) and
notin = this(6) and DH = this(7) and LH = this(8) and confl = this(9) and trU = this(10)
obtain c' where c': "trail T = c' @ Decided Kh i # H"
using cp beginning_not_decided_invert[of _ "trail T" c' Kh i H]
rtranclp_cdcl⇩W_cp_dropWhile_trail[of T U] unfolding trU full_def by fastforce
show ?case
using cdcl⇩W_o_cannot_learn[OF o lev trY notin DH LH confl c']
rtranclp_cdcl⇩W_cp_learned_clause_inv cp unfolding full_def by auto
qed
lemma rtranclp_cdcl⇩W_stgy_with_trail_end_has_not_been_learned:
assumes "(λa b. cdcl⇩W_stgy a b ∧ (∃c. trail a = c @ Decided K i # H @ []))⇧*⇧* S z" and
"cdcl⇩W_all_struct_inv S" and
"trail S = c @ Decided K i # H" and
"D + {#L#} ∉# learned_clss S" and
DH: "atms_of D ⊆ atm_of `lits_of H" and
LH: "atm_of L ∉ atm_of `lits_of H" and
"∃c'. trail z = c' @ Decided K i # H"
shows "D + {#L#} ∉# learned_clss z"
using assms(1-4,7)
proof (induction rule: rtranclp_induct)
case base
then show ?case by auto[1]
next
case (step T U) note st = this(1) and s = this(2) and IH = this(3)[OF this(4-6)]
and lev = this(4) and trS = this(5) and DL_S = this(6) and trU = this(7)
obtain c where c: "trail T = c @ Decided K i # H" using s by auto
obtain c' where c': "trail U = c' @ Decided K i # H" using trU by blast
have "cdcl⇩W⇧*⇧* S T"
proof -
have "∀p pa. ∃s sa. ∀sb sc sd se. (¬ p⇧*⇧* (sb::'st) sc ∨ p s sa ∨ pa⇧*⇧* sb sc)
∧ (¬ pa s sa ∨ ¬ p⇧*⇧* sd se ∨ pa⇧*⇧* sd se)"
by (metis (no_types) mono_rtranclp)
then have "cdcl⇩W_stgy⇧*⇧* S T"
using st by blast
then show ?thesis
using rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W by blast
qed
then have lev': "cdcl⇩W_all_struct_inv T"
using rtranclp_cdcl⇩W_all_struct_inv_inv[of S T] lev by auto
then have confl': "∀Ta. conflicting T = Some Ta ⟶ trail T ⊨as CNot Ta"
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def by blast
show ?case
apply (rule cdcl⇩W_stgy_with_trail_end_has_not_been_learned[OF _ _ c _ DH LH confl' c'])
using s lev' IH c unfolding cdcl⇩W_all_struct_inv_def by blast+
qed
lemma cdcl⇩W_stgy_new_learned_clause:
assumes "cdcl⇩W_stgy S T" and
lev: "cdcl⇩W_M_level_inv S" and
"E ∉# learned_clss S" and
"E ∈# learned_clss T"
shows "∃S'. backtrack S S' ∧ conflicting S = Some E ∧ full cdcl⇩W_cp S' T"
using assms
proof induction
case conflict'
then show ?case unfolding full1_def by (auto dest: tranclp_cdcl⇩W_cp_learned_clause_inv)
next
case (other' T U) note o = this(1) and cp = this(3) and not_yet = this(5) and learned = this(6)
have "E ∈# learned_clss T"
using learned cp rtranclp_cdcl⇩W_cp_learned_clause_inv unfolding full_def by auto
then have "backtrack S T" and "conflicting S = Some E"
using cdcl⇩W_o_new_clause_learned_is_backtrack_step[OF _ not_yet o] lev by blast+
then show ?case using cp by blast
qed
lemma cdcl⇩W_stgy_no_relearned_clause:
assumes
invR: "cdcl⇩W_all_struct_inv R" and
st': "cdcl⇩W_stgy⇧*⇧* R S" and
bt: "backtrack S T" and
confl: "conflicting S = Some E" and
already_learned: "E ∈# clauses S" and
R: "trail R = []"
shows False
proof -
have M_lev: "cdcl⇩W_M_level_inv R"
using invR unfolding cdcl⇩W_all_struct_inv_def by auto
have "cdcl⇩W_M_level_inv S"
using M_lev assms(2) rtranclp_cdcl⇩W_stgy_consistent_inv by blast
with bt obtain D L M1 M2_loc K i where
T: "T ∼ cons_trail (Propagated L ((D + {#L#})))
(reduce_trail_to M1 (add_learned_cls (D + {#L#})
(update_backtrack_lvl (get_maximum_level (trail S) D) (update_conflicting None S))))"
and
decomp: "(Decided K (Suc (get_maximum_level (trail S) D)) # M1, M2_loc) ∈
set (get_all_decided_decomposition (trail S))" and
k: "get_level (trail S) L = backtrack_lvl S" and
level: "get_level (trail S) L = get_maximum_level (trail S) (D+{#L#})" and
confl_S: "conflicting S = Some (D + {#L#})" and
i: "i = get_maximum_level (trail S) D" and
undef: "undefined_lit M1 L"
by (induction rule: backtrack_induction_lev2) metis
obtain M2 where
M: "trail S = M2 @ Decided K (Suc i) # M1"
using get_all_decided_decomposition_exists_prepend[OF decomp] unfolding i by (metis append_assoc)
have invS: "cdcl⇩W_all_struct_inv S"
using invR rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W st' by blast
then have conf: "cdcl⇩W_conflicting S" unfolding cdcl⇩W_all_struct_inv_def by blast
then have "trail S ⊨as CNot (D + {#L#})" unfolding cdcl⇩W_conflicting_def confl_S by auto
then have MD: "trail S ⊨as CNot D" by auto
have lev': "cdcl⇩W_M_level_inv S" using invS unfolding cdcl⇩W_all_struct_inv_def by blast
have get_lvls_M: "get_all_levels_of_decided (trail S) = rev [1..<Suc (backtrack_lvl S)]"
using lev' unfolding cdcl⇩W_M_level_inv_def by auto
have lev: "cdcl⇩W_M_level_inv R" using invR unfolding cdcl⇩W_all_struct_inv_def by blast
then have vars_of_D: "atms_of D ⊆ atm_of ` lits_of M1"
using backtrack_atms_of_D_in_M1[OF lev' undef _ decomp _ _ _ T] confl_S conf T decomp k level
lev' i undef unfolding cdcl⇩W_conflicting_def by (auto simp: cdcl⇩W_M_level_inv_def)
have "no_dup (trail S)" using lev' by (auto simp: cdcl⇩W_M_level_inv_decomp)
have vars_in_M1:
"∀x ∈ atms_of D. x ∉ atm_of ` lits_of (M2 @ [Decided K (get_maximum_level (trail S) D + 1)])"
apply (rule vars_of_D distinct_atms_of_incl_not_in_other[of
"M2 @ Decided K (get_maximum_level (trail S) D + 1) # []" M1 D])
using ‹no_dup (trail S)› M vars_of_D by simp_all
have M1_D: "M1 ⊨as CNot D"
using vars_in_M1 true_annots_remove_if_notin_vars[of "M2 @ Decided K (i + 1) # []" M1 "CNot D"]
‹trail S ⊨as CNot D› M by simp
have get_lvls_M: "get_all_levels_of_decided (trail S) = rev [1..<Suc (backtrack_lvl S)]"
using lev' unfolding cdcl⇩W_M_level_inv_def by auto
then have "backtrack_lvl S > 0" unfolding M by (auto split: split_if_asm simp add: upt.simps(2))
obtain M1' K' Ls where
M': "trail S = Ls @ Decided K' (backtrack_lvl S) # M1'" and
Ls: "∀l ∈ set Ls. ¬ is_decided l" and
"set M1 ⊆ set M1'"
proof -
let ?Ls = "takeWhile (Not o is_decided) (trail S)"
have MLs: "trail S = ?Ls @ dropWhile (Not o is_decided) (trail S)"
by auto
have "dropWhile (Not o is_decided) (trail S) ≠ []" unfolding M by auto
moreover
from hd_dropWhile[OF this] have "is_decided(hd (dropWhile (Not o is_decided) (trail S)))"
by simp
ultimately
obtain K' K'k where
K'k: "dropWhile (Not o is_decided) (trail S)
= Decided K' K'k # tl (dropWhile (Not o is_decided) (trail S))"
by (cases "dropWhile (Not ∘ is_decided) (trail S)";
cases "hd (dropWhile (Not ∘ is_decided) (trail S))")
simp_all
moreover have "∀l ∈ set ?Ls. ¬is_decided l" using set_takeWhileD by force
moreover
have "get_all_levels_of_decided (trail S)
= K'k # get_all_levels_of_decided(tl (dropWhile (Not ∘ is_decided) (trail S)))"
apply (subst MLs, subst K'k)
using calculation(2) by (auto simp add: get_all_levels_of_decided_no_decided)
then have "K'k = backtrack_lvl S"
using calculation(2) by (auto split: split_if_asm simp add: get_lvls_M upt.simps(2))
moreover have "set M1 ⊆ set (tl (dropWhile (Not o is_decided) (trail S)))"
unfolding M by (induction M2) auto
ultimately show ?thesis using that MLs by metis
qed
have get_lvls_M: "get_all_levels_of_decided (trail S) = rev [1..<Suc (backtrack_lvl S)]"
using lev' unfolding cdcl⇩W_M_level_inv_def by auto
then have "backtrack_lvl S > 0" unfolding M by (auto split: split_if_asm simp add: upt.simps(2) i)
have M1'_D: "M1' ⊨as CNot D" using M1_D ‹set M1 ⊆ set M1'› by (auto intro: true_annots_mono)
have "-L ∈ lits_of (trail S)" using conf confl_S unfolding cdcl⇩W_conflicting_def by auto
have lvls_M1': "get_all_levels_of_decided M1' = rev [1..<backtrack_lvl S]"
using get_lvls_M Ls by (auto simp add: get_all_levels_of_decided_no_decided M'
split: split_if_asm simp add: upt.simps(2))
have L_notin: "atm_of L ∈ atm_of ` lits_of Ls ∨ atm_of L = atm_of K'"
proof (rule ccontr)
assume "¬ ?thesis"
then have "atm_of L ∉ atm_of ` lits_of (Decided K' (backtrack_lvl S) # rev Ls)" by simp
then have "get_level (trail S) L = get_level M1' L"
unfolding M' by auto
then show False using get_level_in_levels_of_decided[of M1' L] ‹backtrack_lvl S > 0›
unfolding k lvls_M1' by auto
qed
obtain Y Z where
RY: "cdcl⇩W_stgy⇧*⇧* R Y" and
YZ: "cdcl⇩W_stgy Y Z" and
nt: "¬ (∃c. trail Y = c @ Decided K' (backtrack_lvl S) # M1' @ [])" and
Z: "(λa b. cdcl⇩W_stgy a b ∧ (∃c. trail a = c @ Decided K' (backtrack_lvl S) # M1' @ []))⇧*⇧*
Z S"
using rtranclp_cdcl⇩W_new_decided_at_beginning_is_decide'[OF st' _ _ lev, of Ls K'
"backtrack_lvl S" M1' "[]"]
unfolding R M' by auto
have [simp]: "cdcl⇩W_M_level_inv Y"
using RY lev rtranclp_cdcl⇩W_stgy_consistent_inv by blast
obtain M' where trZ: "trail Z = M' @ Decided K' (backtrack_lvl S) # M1'"
using rtranclp_cdcl⇩W_stgy_with_trail_end_has_trail_end[OF Z] M' by auto
have "no_dup (trail Y)"
using RY lev rtranclp_cdcl⇩W_stgy_consistent_inv unfolding cdcl⇩W_M_level_inv_def by blast
then obtain Y' where
dec: "decide Y Y'" and
Y'Z: "full cdcl⇩W_cp Y' Z" and
"no_step cdcl⇩W_cp Y"
using cdcl⇩W_stgy_trail_has_new_decided_is_decide_step[OF YZ nt Z] M' by auto
have trY: "trail Y = M1'"
proof -
obtain M' where M: "trail Z = M' @ Decided K' (backtrack_lvl S) # M1'"
using rtranclp_cdcl⇩W_stgy_with_trail_end_has_trail_end[OF Z] M' by auto
obtain M'' where M'': "trail Z = M'' @ trail Y'" and "∀m∈set M''. ¬is_decided m"
using Y'Z rtranclp_cdcl⇩W_cp_dropWhile_trail' unfolding full_def by blast
obtain M''' where "trail Y' = M''' @ Decided K' (backtrack_lvl S) # M1'"
using M'' unfolding M
by (metis (no_types, lifting) ‹∀m∈set M''. ¬ is_decided m› beginning_not_decided_invert)
then show ?thesis using dec nt by (induction M''') auto
qed
have Y_CT: "conflicting Y = None" using ‹decide Y Y'› by auto
have "cdcl⇩W⇧*⇧* R Y" by (simp add: RY rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W)
then have "init_clss Y = init_clss R" using rtranclp_cdcl⇩W_init_clss[of R Y] M_lev by auto
{ assume DL: "D + {#L#} ∈# clauses Y"
have "atm_of L ∉ atm_of ` lits_of M1"
apply (rule backtrack_lit_skiped[of S])
using decomp i k lev' unfolding cdcl⇩W_M_level_inv_def by auto
then have LM1: "undefined_lit M1 L"
by (metis Decided_Propagated_in_iff_in_lits_of atm_of_uminus image_eqI)
have L_trY: "undefined_lit (trail Y) L"
using L_notin ‹no_dup (trail S)› unfolding defined_lit_map trY M'
by (auto simp add: image_iff lits_of_def)
have "∃ Y'. propagate Y Y'"
using propagate_rule[of Y] DL M1'_D L_trY Y_CT trY DL by (metis state_eq_ref)
then have False using ‹no_step cdcl⇩W_cp Y› propagate' by blast
}
moreover {
assume DL: "D + {#L#} ∉# clauses Y"
have lY_lZ: "learned_clss Y = learned_clss Z"
using dec Y'Z rtranclp_cdcl⇩W_cp_learned_clause_inv[of Y' Z] unfolding full_def
by auto
have invZ: "cdcl⇩W_all_struct_inv Z"
by (meson RY YZ invR r_into_rtranclp rtranclp_cdcl⇩W_all_struct_inv_inv
rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W)
have "D + {#L#} ∉#learned_clss S"
apply (rule rtranclp_cdcl⇩W_stgy_with_trail_end_has_not_been_learned[OF Z invZ trZ])
using DL lY_lZ unfolding clauses_def apply simp
apply (metis (no_types, lifting) ‹set M1 ⊆ set M1'› image_mono order_trans
vars_of_D lits_of_def)
using L_notin ‹no_dup (trail S)› unfolding M' by (auto simp add: image_iff lits_of_def)
then have False
using already_learned DL confl st' M_lev unfolding M'
by (simp add: ‹init_clss Y = init_clss R› clauses_def confl_S
rtranclp_cdcl⇩W_stgy_no_more_init_clss)
}
ultimately show False by blast
qed
lemma rtranclp_cdcl⇩W_stgy_distinct_mset_clauses:
assumes
invR: "cdcl⇩W_all_struct_inv R" and
st: "cdcl⇩W_stgy⇧*⇧* R S" and
dist: "distinct_mset (clauses R)" and
R: "trail R = []"
shows "distinct_mset (clauses S)"
using st
proof (induction)
case base
then show ?case using dist by simp
next
case (step S T) note st = this(1) and s = this(2) and IH = this(3)
from s show ?case
proof (cases rule: cdcl⇩W_stgy.cases)
case conflict'
then show ?thesis
using IH unfolding full1_def by (auto dest: tranclp_cdcl⇩W_cp_no_more_clauses)
next
case (other' S') note o = this(1) and full = this(3)
have [simp]: "clauses T = clauses S'"
using full unfolding full_def by (auto dest: rtranclp_cdcl⇩W_cp_no_more_clauses)
show ?thesis
using o IH
proof (cases rule: cdcl⇩W_o_rule_cases)
case backtrack
moreover
have "cdcl⇩W_all_struct_inv S"
using invR rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv st by blast
then have "cdcl⇩W_M_level_inv S"
unfolding cdcl⇩W_all_struct_inv_def by auto
ultimately obtain E where
"conflicting S = Some E" and
cls_S': "clauses S' = {#E#} + clauses S"
using ‹cdcl⇩W_M_level_inv S›
by (induction rule: backtrack_induction_lev2) (auto simp: cdcl⇩W_M_level_inv_decomp)
then have "E ∉# clauses S"
using cdcl⇩W_stgy_no_relearned_clause R invR local.backtrack st by blast
then show ?thesis using IH by (simp add: distinct_mset_add_single cls_S')
qed auto
qed
qed
lemma cdcl⇩W_stgy_distinct_mset_clauses:
assumes
st: "cdcl⇩W_stgy⇧*⇧* (init_state N) S" and
no_duplicate_clause: "distinct_mset N" and
no_duplicate_in_clause: "distinct_mset_mset N"
shows "distinct_mset (clauses S)"
using rtranclp_cdcl⇩W_stgy_distinct_mset_clauses[OF _ st] assms
by (auto simp: cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def)
subsection ‹Decrease of a measure›
fun cdcl⇩W_measure where
"cdcl⇩W_measure S =
[(3::nat) ^ (card (atms_of_msu (init_clss S))) - card (set_mset (learned_clss S)),
if conflicting S = None then 1 else 0,
if conflicting S = None then card (atms_of_msu (init_clss S)) - length (trail S)
else length (trail S)
]"
lemma length_model_le_vars_all_inv:
assumes "cdcl⇩W_all_struct_inv S"
shows "length (trail S) ≤ card (atms_of_msu (init_clss S))"
using assms length_model_le_vars[of S] unfolding cdcl⇩W_all_struct_inv_def
by (auto simp: cdcl⇩W_M_level_inv_decomp)
end
context cdcl⇩W
begin
lemma learned_clss_less_upper_bound:
fixes S :: "'st"
assumes
"distinct_cdcl⇩W_state S" and
"∀s ∈# learned_clss S. ¬tautology s"
shows "card(set_mset (learned_clss S)) ≤ 3 ^ card (atms_of_msu (learned_clss S))"
proof -
have "set_mset (learned_clss S) ⊆ simple_clss (atms_of_msu (learned_clss S))"
apply (rule simplified_in_simple_clss)
using assms unfolding distinct_cdcl⇩W_state_def by auto
then have "card(set_mset (learned_clss S))
≤ card (simple_clss (atms_of_msu (learned_clss S)))"
by (simp add: simple_clss_finite card_mono)
then show ?thesis
by (meson atms_of_ms_finite simple_clss_card finite_set_mset order_trans)
qed
lemma lexn3[intro!, simp]:
"a < a' ∨ (a = a' ∧ b < b') ∨ (a = a' ∧ b = b' ∧ c < c')
⟹ ([a::nat, b, c], [a', b', c']) ∈ lexn {(x, y). x < y} 3"
apply auto
unfolding lexn_conv apply fastforce
unfolding lexn_conv apply auto
apply (metis append.simps(1) append.simps(2))+
done
lemma cdcl⇩W_measure_decreasing:
fixes S :: "'st"
assumes
"cdcl⇩W S S'" and
no_restart:
"¬(learned_clss S ⊆# learned_clss S' ∧ [] = trail S' ∧ conflicting S' = None)"
and
"learned_clss S ⊆# learned_clss S'" and
no_relearn: "⋀S'. backtrack S S' ⟹ ∀T. conflicting S = Some T ⟶ T ∉# learned_clss S"
and
alien: "no_strange_atm S" and
M_level: "cdcl⇩W_M_level_inv S" and
no_taut: "∀s ∈# learned_clss S. ¬tautology s" and
no_dup: "distinct_cdcl⇩W_state S" and
confl: "cdcl⇩W_conflicting S"
shows "(cdcl⇩W_measure S', cdcl⇩W_measure S) ∈ lexn {(a, b). a < b} 3"
using assms(1) M_level assms(2,3)
proof (induct rule: cdcl⇩W_all_induct_lev2)
case (propagate C L) note undef = this(3) and T = this(4) and conf = this(5)
have propa: "propagate S (cons_trail (Propagated L (C + {#L#})) S)"
using propagate_rule[OF _ propagate.hyps(1,2)] propagate.hyps by auto
then have no_dup': "no_dup (Propagated L ( (C + {#L#})) # trail S)"
by (metis M_level cdcl⇩W_M_level_inv_decomp(2) ann_literal.sel(2) propagate'
r_into_rtranclp rtranclp_cdcl⇩W_cp_consistent_inv trail_cons_trail undef)
let ?N = "init_clss S"
have "no_strange_atm (cons_trail (Propagated L (C + {#L#})) S)"
using alien cdcl⇩W.propagate cdcl⇩W_no_strange_atm_inv propa M_level by blast
then have "atm_of ` lits_of (Propagated L ( (C + {#L#})) # trail S)
⊆ atms_of_msu (init_clss S)"
using undef unfolding no_strange_atm_def by auto
then have "card (atm_of ` lits_of (Propagated L ( (C + {#L#})) # trail S))
≤ card (atms_of_msu (init_clss S))"
by (meson atms_of_ms_finite card_mono finite_set_mset)
then have "length (Propagated L ( (C + {#L#})) # trail S) ≤ card (atms_of_msu ?N)"
using no_dup_length_eq_card_atm_of_lits_of no_dup' by fastforce
then have H: "card (atms_of_msu (init_clss S)) - length (trail S)
= Suc (card (atms_of_msu (init_clss S)) - Suc (length (trail S)))"
by simp
show ?case using conf T undef by (auto simp: H)
next
case (decide L) note conf = this(1) and undef = this(2) and T = this(4)
moreover
have dec: "decide S (cons_trail (Decided L (backtrack_lvl S + 1)) (incr_lvl S))"
using decide.intros decide.hyps by force
then have cdcl⇩W:"cdcl⇩W S (cons_trail (Decided L (backtrack_lvl S + 1)) (incr_lvl S))"
using cdcl⇩W.simps by blast
moreover
have lev: "cdcl⇩W_M_level_inv (cons_trail (Decided L (backtrack_lvl S + 1)) (incr_lvl S))"
using cdcl⇩W M_level cdcl⇩W_consistent_inv[OF cdcl⇩W] by auto
then have no_dup: "no_dup (Decided L (backtrack_lvl S + 1) # trail S)"
using undef unfolding cdcl⇩W_M_level_inv_def by auto
have "no_strange_atm (cons_trail (Decided L (backtrack_lvl S + 1)) (incr_lvl S))"
using M_level alien calculation(4) cdcl⇩W_no_strange_atm_inv by blast
then have "length (Decided L ((backtrack_lvl S) + 1) # (trail S))
≤ card (atms_of_msu (init_clss S))"
using no_dup clauses_def undef
length_model_le_vars[of "cons_trail (Decided L (backtrack_lvl S + 1)) (incr_lvl S)"]
by fastforce
ultimately show ?case using conf by auto
next
case (skip L C' M D) note tr = this(1) and conf = this(2) and T = this(5)
show ?case using conf T unfolding clauses_def by (simp add: tr)
next
case conflict
then show ?case by simp
next
case resolve
then show ?case using finite unfolding clauses_def by simp
next
case (backtrack K i M1 M2 L D T) note decomp = this(1) and conf = this(3) and undef = this(6) and
T =this(7) and lev = this(8)
let ?S' = "T"
have bt: "backtrack S ?S'"
using backtrack.hyps backtrack.intros[of S _ _ _ _ D L K i] by auto
have "D + {#L#} ∉# learned_clss S"
using no_relearn conf bt by auto
then have card_T:
"card (set_mset ({#D + {#L#}#} + learned_clss S)) = Suc (card (set_mset (learned_clss S)))"
by (simp add:)
have "distinct_cdcl⇩W_state ?S'"
using bt M_level distinct_cdcl⇩W_state_inv no_dup other by blast
moreover have "∀s∈#learned_clss ?S'. ¬ tautology s"
using learned_clss_are_not_tautologies[OF cdcl⇩W.other[OF cdcl⇩W_o.bj[OF
cdcl⇩W_bj.backtrack[OF bt]]]] M_level no_taut confl by auto
ultimately have "card (set_mset (learned_clss T)) ≤ 3 ^ card (atms_of_msu (learned_clss T))"
by (auto simp: clauses_def learned_clss_less_upper_bound)
then have H: "card (set_mset ({#D + {#L#}#} + learned_clss S))
≤ 3 ^ card (atms_of_msu ({#D + {#L#}#} + learned_clss S))"
using T undef decomp lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
moreover
have "atms_of_msu ({#D + {#L#}#} + learned_clss S) ⊆ atms_of_msu (init_clss S)"
using alien conf unfolding no_strange_atm_def by auto
then have card_f: "card (atms_of_msu ({#D + {#L#}#} + learned_clss S))
≤ card (atms_of_msu (init_clss S))"
by (meson atms_of_ms_finite card_mono finite_set_mset)
then have "(3::nat) ^ card (atms_of_msu ({#D + {#L#}#} + learned_clss S))
≤ 3 ^ card (atms_of_msu (init_clss S))" by simp
ultimately have "(3::nat) ^ card (atms_of_msu (init_clss S))
≥ card (set_mset ({#D + {#L#}#} + learned_clss S))"
using le_trans by blast
then show ?case using decomp undef diff_less_mono2 card_T T lev
by (auto simp: cdcl⇩W_M_level_inv_decomp)
next
case restart
then show ?case using alien by (auto simp: state_eq_def simp del: state_simp)
next
case (forget C T)
then have "C ∈# learned_clss S" and "C ∉# learned_clss T"
by auto
then show ?case using forget(9) by (simp add: mset_leD)
qed
lemma propagate_measure_decreasing:
fixes S :: "'st"
assumes "propagate S S'" and "cdcl⇩W_all_struct_inv S"
shows "(cdcl⇩W_measure S', cdcl⇩W_measure S) ∈ lexn {(a, b). a < b} 3"
apply (rule cdcl⇩W_measure_decreasing)
using assms(1) propagate apply blast
using assms(1) apply (auto simp add: propagate.simps)[3]
using assms(2) apply (auto simp add: cdcl⇩W_all_struct_inv_def)
done
lemma conflict_measure_decreasing:
fixes S :: "'st"
assumes "conflict S S'" and "cdcl⇩W_all_struct_inv S"
shows "(cdcl⇩W_measure S', cdcl⇩W_measure S) ∈ lexn {(a, b). a < b} 3"
apply (rule cdcl⇩W_measure_decreasing)
using assms(1) conflict apply blast
using assms(1) apply (auto simp add: propagate.simps)[3]
using assms(2) apply (auto simp add: cdcl⇩W_all_struct_inv_def)
done
lemma decide_measure_decreasing:
fixes S :: "'st"
assumes "decide S S'" and "cdcl⇩W_all_struct_inv S"
shows "(cdcl⇩W_measure S', cdcl⇩W_measure S) ∈ lexn {(a, b). a < b} 3"
apply (rule cdcl⇩W_measure_decreasing)
using assms(1) decide other apply blast
using assms(1) apply (auto simp add: propagate.simps)[3]
using assms(2) apply (auto simp add: cdcl⇩W_all_struct_inv_def)
done
lemma trans_le:
"trans {(a, (b::nat)). a < b}"
unfolding trans_def by auto
lemma cdcl⇩W_cp_measure_decreasing:
fixes S :: "'st"
assumes "cdcl⇩W_cp S S'" and "cdcl⇩W_all_struct_inv S"
shows "(cdcl⇩W_measure S', cdcl⇩W_measure S) ∈ lexn {(a, b). a < b} 3"
using assms
proof induction
case conflict'
then show ?case using conflict_measure_decreasing by blast
next
case propagate'
then show ?case using propagate_measure_decreasing by blast
qed
lemma tranclp_cdcl⇩W_cp_measure_decreasing:
fixes S :: "'st"
assumes "cdcl⇩W_cp⇧+⇧+ S S'" and "cdcl⇩W_all_struct_inv S"
shows "(cdcl⇩W_measure S', cdcl⇩W_measure S) ∈ lexn {(a, b). a < b} 3"
using assms
proof induction
case base
then show ?case using cdcl⇩W_cp_measure_decreasing by blast
next
case (step T U) note st = this(1) and step = this(2) and IH =this(3) and inv = this(4)
then have "(cdcl⇩W_measure T, cdcl⇩W_measure S) ∈ lexn {a. case a of (a, b) ⇒ a < b} 3" by blast
moreover have "(cdcl⇩W_measure U, cdcl⇩W_measure T) ∈ lexn {a. case a of (a, b) ⇒ a < b} 3"
using cdcl⇩W_cp_measure_decreasing[OF step] rtranclp_cdcl⇩W_all_struct_inv_inv inv
tranclp_cdcl⇩W_cp_tranclp_cdcl⇩W[OF st]
unfolding trans_def rtranclp_unfold
by blast
ultimately show ?case using lexn_transI[OF trans_le] unfolding trans_def by blast
qed
lemma cdcl⇩W_stgy_step_decreasing:
fixes R S T :: "'st"
assumes "cdcl⇩W_stgy S T" and
"cdcl⇩W_stgy⇧*⇧* R S"
"trail R = []" and
"cdcl⇩W_all_struct_inv R"
shows "(cdcl⇩W_measure T, cdcl⇩W_measure S) ∈ lexn {(a, b). a < b} 3"
proof -
have "cdcl⇩W_all_struct_inv S"
using assms
by (metis rtranclp_unfold rtranclp_cdcl⇩W_all_struct_inv_inv tranclp_cdcl⇩W_stgy_tranclp_cdcl⇩W)
with assms show ?thesis
proof induction
case (conflict' V) note cp = this(1) and inv = this(5)
show ?case
using tranclp_cdcl⇩W_cp_measure_decreasing[OF HOL.conjunct1[OF cp[unfolded full1_def]] inv]
.
next
case (other' T U) note st = this(1) and H= this(4,5,6,7) and cp = this(3)
have "cdcl⇩W_all_struct_inv T"
using cdcl⇩W_all_struct_inv_inv other other'.hyps(1) other'.prems(4) by blast
from tranclp_cdcl⇩W_cp_measure_decreasing[OF _ this]
have le_or_eq: "(cdcl⇩W_measure U, cdcl⇩W_measure T) ∈ lexn {a. case a of (a, b) ⇒ a < b} 3 ∨
cdcl⇩W_measure U = cdcl⇩W_measure T"
using cp unfolding full_def rtranclp_unfold by blast
moreover
have "cdcl⇩W_M_level_inv S"
using cdcl⇩W_all_struct_inv_def other'.prems(4) by blast
with st have "(cdcl⇩W_measure T, cdcl⇩W_measure S) ∈ lexn {a. case a of (a, b) ⇒ a < b} 3"
proof (induction rule:cdcl⇩W_o_induct_lev2)
case (decide T)
then show ?case using decide_measure_decreasing H by blast
next
case (backtrack K i M1 M2 L D T) note decomp = this(1) and undef = this(6) and T = this(7)
have bt: "backtrack S T"
apply (rule backtrack_rule)
using backtrack.hyps by auto
then have no_relearn: "∀T. conflicting S = Some T ⟶ T ∉# learned_clss S"
using cdcl⇩W_stgy_no_relearned_clause[of R S T] H
unfolding cdcl⇩W_all_struct_inv_def clauses_def by auto
have inv: "cdcl⇩W_all_struct_inv S"
using ‹cdcl⇩W_all_struct_inv S› by blast
show ?case
apply (rule cdcl⇩W_measure_decreasing)
using bt cdcl⇩W_bj.backtrack cdcl⇩W_o.bj other apply simp
using bt T undef decomp inv unfolding cdcl⇩W_all_struct_inv_def
cdcl⇩W_M_level_inv_def apply auto[]
using bt T undef decomp inv unfolding cdcl⇩W_all_struct_inv_def
cdcl⇩W_M_level_inv_def apply auto[]
using bt no_relearn apply auto[]
using inv unfolding cdcl⇩W_all_struct_inv_def apply simp
using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def apply simp
using inv unfolding cdcl⇩W_all_struct_inv_def apply simp
using inv unfolding cdcl⇩W_all_struct_inv_def apply simp
using inv unfolding cdcl⇩W_all_struct_inv_def by simp
next
case skip
then show ?case by force
next
case resolve
then show ?case by force
qed
ultimately show ?case
by (metis lexn_transI transD trans_le)
qed
qed
lemma tranclp_cdcl⇩W_stgy_decreasing:
fixes R S T :: 'st
assumes "cdcl⇩W_stgy⇧+⇧+ R S"
"trail R = []" and
"cdcl⇩W_all_struct_inv R"
shows "(cdcl⇩W_measure S, cdcl⇩W_measure R) ∈ lexn {(a, b). a < b} 3"
using assms
apply induction
using cdcl⇩W_stgy_step_decreasing[of R _ R] apply blast
using cdcl⇩W_stgy_step_decreasing[of _ _ R] tranclp_into_rtranclp[of cdcl⇩W_stgy R]
lexn_transI[OF trans_le, of 3] unfolding trans_def by blast
lemma tranclp_cdcl⇩W_stgy_S0_decreasing:
fixes R S T :: 'st
assumes pl: "cdcl⇩W_stgy⇧+⇧+ (init_state N) S" and
no_dup: "distinct_mset_mset N"
shows "(cdcl⇩W_measure S, cdcl⇩W_measure (init_state N)) ∈ lexn {(a, b). a < b} 3"
proof -
have "cdcl⇩W_all_struct_inv (init_state N)"
using no_dup unfolding cdcl⇩W_all_struct_inv_def by auto
then show ?thesis using pl tranclp_cdcl⇩W_stgy_decreasing init_state_trail by blast
qed
lemma wf_tranclp_cdcl⇩W_stgy:
"wf {(S::'st, init_state N)| S N. distinct_mset_mset N ∧ cdcl⇩W_stgy⇧+⇧+ (init_state N) S}"
apply (rule wf_wf_if_measure'_notation2[of "lexn {(a, b). a < b} 3" _ _ cdcl⇩W_measure])
apply (simp add: wf wf_lexn)
using tranclp_cdcl⇩W_stgy_S0_decreasing by blast
end
end