theory CDCL_W_Termination
imports CDCL_W
begin
context conflict_driven_clause_learning⇩W
begin
subsection ‹Termination›
subsubsection ‹No Relearning of a clause›
text ‹
Because of the conflict minimisation, this version is less clear than the version without:
instead of extracting the clause from the conflicting clause, we must take it from the clause
used to backjump; i.e., the annotation of the first literal of the trail.
We also prove below that no learned clause is subsumed by a (smaller) clause in the clause set.
›
lemma cdcl⇩W_stgy_no_relearned_clause:
assumes
cdcl: ‹backtrack S T› and
inv: ‹cdcl⇩W_all_struct_inv S› and
smaller: ‹no_smaller_propa S›
shows
‹mark_of (hd_trail T) ∉# clauses S›
proof (rule ccontr)
assume n_dist: ‹¬ ?thesis›
obtain K L :: "'v literal" and
M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat and D D' where
confl_S: "conflicting S = Some (add_mset L D)" and
decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
lev_L: "get_level (trail S) L = backtrack_lvl S" and
max_D_L: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
i: "get_maximum_level (trail S) D' ≡ i" and
lev_K: "get_level (trail S) K = i + 1" and
T: "T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S)))" and
D_D': ‹D' ⊆# D› and
‹clauses S ⊨pm add_mset L D'›
using cdcl by (auto elim!: rulesE)
obtain M2' where M2': ‹trail S = (M2' @ M2) @ Decided K # M1›
using decomp by auto
have inv_T: ‹cdcl⇩W_all_struct_inv T›
using cdcl cdcl⇩W_stgy_cdcl⇩W_all_struct_inv inv W_other backtrack bj
cdcl⇩W_all_struct_inv_inv cdcl⇩W_cdcl⇩W_restart by blast
have M1_D': ‹M1 ⊨as CNot D'›
using backtrack_M1_CNot_D'[of S D' ‹i› K M1 M2 L ‹add_mset L D› T
‹Propagated L (add_mset L D')›] inv confl_S decomp i T D_D' lev_K lev_L max_D_L
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def cdcl⇩W_M_level_inv_def
by (auto simp: subset_mset_trans_add_mset)
have ‹undefined_lit M1 L›
using inv_T T decomp unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
by (auto simp: defined_lit_map)
moreover have ‹D' + {#L#} ∈# clauses S›
using n_dist T by (auto simp: clauses_def)
ultimately show False
using smaller M1_D' unfolding no_smaller_propa_def M2' by blast
qed
lemma cdcl⇩W_stgy_no_relearned_larger_clause:
assumes
cdcl: ‹backtrack S T› and
inv: ‹cdcl⇩W_all_struct_inv S› and
smaller: ‹no_smaller_propa S› and
smaller_conf: ‹no_smaller_confl S› and
E_subset: ‹E ⊂# mark_of (hd_trail T)›
shows ‹E ∉# clauses S›
proof (rule ccontr)
assume n_dist: ‹¬ ?thesis›
obtain K L :: "'v literal" and
M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat and D D' where
confl_S: "conflicting S = Some (add_mset L D)" and
decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
lev_L: "get_level (trail S) L = backtrack_lvl S" and
max_D_L: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
i: "get_maximum_level (trail S) D' ≡ i" and
lev_K: "get_level (trail S) K = i + 1" and
T: "T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S)))" and
D_D': ‹D' ⊆# D› and
‹clauses S ⊨pm add_mset L D'›
using cdcl by (auto elim!: rulesE)
obtain M2' where M2': ‹trail S = (M2' @ M2) @ Decided K # M1›
using decomp by auto
have inv_T: ‹cdcl⇩W_all_struct_inv T›
using cdcl cdcl⇩W_stgy_cdcl⇩W_all_struct_inv inv W_other backtrack bj
cdcl⇩W_all_struct_inv_inv cdcl⇩W_cdcl⇩W_restart by blast
have ‹distinct_mset (add_mset L D')›
using inv_T T unfolding cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def
by auto
then have dist_E: ‹distinct_mset E›
using distinct_mset_mono_strict[OF E_subset] T by auto
have M1_D': ‹M1 ⊨as CNot D'›
using backtrack_M1_CNot_D'[of S D' ‹i› K M1 M2 L ‹add_mset L D› T
‹Propagated L (add_mset L D')›] inv confl_S decomp i T D_D' lev_K lev_L max_D_L
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def cdcl⇩W_M_level_inv_def
by (auto simp: subset_mset_trans_add_mset)
have undef_L: ‹undefined_lit M1 L›
using inv_T T decomp unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
by (auto simp: defined_lit_map)
show False
proof (cases ‹L ∈# E›)
case True
then obtain E' where
E: ‹E = add_mset L E'›
by (auto dest: multi_member_split)
then have ‹distinct_mset E'› and ‹L ∉# E'› and E'_E': ‹E' ⊆# D'›
using dist_E T E_subset by auto
then have M1_E': ‹M1 ⊨as CNot E'›
using M1_D' T unfolding true_annots_true_cls_def_iff_negation_in_model
by (auto dest: multi_member_split[of _ E] mset_subset_eq_insertD)
have propa: ‹⋀M' K M L D. trail S = M' @ Decided K # M ⟹
D + {#L#} ∈# clauses S ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D›
using smaller unfolding no_smaller_propa_def by blast
show False
using M1_E' propa[of ‹M2' @ M2› K M1 E', OF M2' _ undef_L] n_dist unfolding E
by auto
next
case False
then have ‹E ⊆# D'›
using E_subset T by (auto simp: subset_add_mset_notin_subset)
then have M1_E: ‹M1 ⊨as CNot E›
using M1_D' T dist_E E_subset unfolding true_annots_true_cls_def_iff_negation_in_model
by (auto dest: multi_member_split[of _ E] mset_subset_eq_insertD)
have confl: ‹⋀M' K M L D. trail S = M' @ Decided K # M ⟹
D ∈# clauses S ⟹ ¬ M ⊨as CNot D›
using smaller_conf unfolding no_smaller_confl_def by blast
show False
using confl[of ‹M2' @ M2› K M1 E, OF M2'] n_dist M1_E
by auto
qed
qed
lemma cdcl⇩W_stgy_no_relearned_highest_subres_clause:
assumes
cdcl: ‹backtrack S T› and
inv: ‹cdcl⇩W_all_struct_inv S› and
smaller: ‹no_smaller_propa S› and
smaller_conf: ‹no_smaller_confl S› and
E_subset: ‹mark_of (hd_trail T) = add_mset (lit_of (hd_trail T)) E›
shows ‹add_mset (- lit_of (hd_trail T)) E ∉# clauses S›
proof (rule ccontr)
assume n_dist: ‹¬ ?thesis›
obtain K L :: "'v literal" and
M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat and D D' where
confl_S: "conflicting S = Some (add_mset L D)" and
decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
lev_L: "get_level (trail S) L = backtrack_lvl S" and
max_D_L: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
i: "get_maximum_level (trail S) D' ≡ i" and
lev_K: "get_level (trail S) K = i + 1" and
T: "T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S)))" and
D_D': ‹D' ⊆# D› and
‹clauses S ⊨pm add_mset L D'›
using cdcl by (auto elim!: rulesE)
obtain M2' where M2': ‹trail S = (M2' @ M2) @ Decided K # M1›
using decomp by auto
have inv_T: ‹cdcl⇩W_all_struct_inv T›
using cdcl cdcl⇩W_stgy_cdcl⇩W_all_struct_inv inv W_other backtrack bj
cdcl⇩W_all_struct_inv_inv cdcl⇩W_cdcl⇩W_restart by blast
have ‹distinct_mset (add_mset L D')›
using inv_T T unfolding cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def
by auto
have M1_D': ‹M1 ⊨as CNot D'›
using backtrack_M1_CNot_D'[of S D' ‹i› K M1 M2 L ‹add_mset L D› T
‹Propagated L (add_mset L D')›] inv confl_S decomp i T D_D' lev_K lev_L max_D_L
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def cdcl⇩W_M_level_inv_def
by (auto simp: subset_mset_trans_add_mset)
have undef_L: ‹undefined_lit M1 L›
using inv_T T decomp unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
by (auto simp: defined_lit_map)
then have undef_uL: ‹undefined_lit M1 (-L)›
by auto
have propa: ‹⋀M' K M L D. trail S = M' @ Decided K # M ⟹
D + {#L#} ∈# clauses S ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D›
using smaller unfolding no_smaller_propa_def by blast
have E[simp]: ‹E = D'›
using E_subset T by (auto dest: multi_member_split)
have propa: ‹⋀M' K M L D. trail S = M' @ Decided K # M ⟹
D + {#L#} ∈# clauses S ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D›
using smaller unfolding no_smaller_propa_def by blast
show False
using T M1_D' propa[of ‹M2' @ M2› K M1 D', OF M2' _ undef_uL] n_dist unfolding E
by auto
qed
lemma cdcl⇩W_stgy_distinct_mset:
assumes
cdcl: ‹cdcl⇩W_stgy S T› and
inv: "cdcl⇩W_all_struct_inv S" and
smaller: ‹no_smaller_propa S› and
dist: ‹distinct_mset (clauses S)›
shows
‹distinct_mset (clauses T)›
proof (rule ccontr)
assume n_dist: ‹¬ distinct_mset (clauses T)›
then have ‹backtrack S T›
using cdcl dist by (auto simp: cdcl⇩W_stgy.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps
elim: propagateE conflictE decideE skipE resolveE)
then show False
using n_dist cdcl⇩W_stgy_no_relearned_clause[of S T] dist
by (auto simp: inv smaller elim!: rulesE)
qed
text ‹
This is a more restrictive version of the previous theorem, but is a better bound for an
implementation that does not do duplication removal (esp. as part of preprocessing).
›
lemma cdcl⇩W_stgy_learned_distinct_mset:
assumes
cdcl: ‹cdcl⇩W_stgy S T› and
inv: "cdcl⇩W_all_struct_inv S" and
smaller: ‹no_smaller_propa S› and
dist: ‹distinct_mset (learned_clss S + remdups_mset (init_clss S))›
shows
‹distinct_mset (learned_clss T + remdups_mset (init_clss T))›
proof (rule ccontr)
assume n_dist: ‹¬ ?thesis›
then have ‹backtrack S T›
using cdcl dist by (auto simp: cdcl⇩W_stgy.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps
elim: propagateE conflictE decideE skipE resolveE)
then show False
using n_dist cdcl⇩W_stgy_no_relearned_clause[of S T] dist
by (auto simp: inv smaller clauses_def elim!: rulesE)
qed
lemma rtranclp_cdcl⇩W_stgy_distinct_mset_clauses:
assumes
st: "cdcl⇩W_stgy⇧*⇧* R S" and
invR: "cdcl⇩W_all_struct_inv R" and
dist: "distinct_mset (clauses R)" and
no_smaller: ‹no_smaller_propa R›
shows "distinct_mset (clauses S)"
using assms by (induction rule: rtranclp_induct)
(auto simp: cdcl⇩W_stgy_distinct_mset rtranclp_cdcl⇩W_stgy_no_smaller_propa
rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)
lemma rtranclp_cdcl⇩W_stgy_distinct_mset_learned_clauses:
assumes
st: "cdcl⇩W_stgy⇧*⇧* R S" and
invR: "cdcl⇩W_all_struct_inv R" and
dist: "distinct_mset (learned_clss R + remdups_mset (init_clss R))" and
no_smaller: ‹no_smaller_propa R›
shows "distinct_mset (learned_clss S + remdups_mset (init_clss S))"
using assms by (induction rule: rtranclp_induct)
(auto simp: cdcl⇩W_stgy_learned_distinct_mset rtranclp_cdcl⇩W_stgy_no_smaller_propa
rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)
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 no_smaller_propa_def)
lemma cdcl⇩W_stgy_learned_distinct_mset_new:
assumes
cdcl: ‹cdcl⇩W_stgy S T› and
inv: "cdcl⇩W_all_struct_inv S" and
smaller: ‹no_smaller_propa S› and
dist: ‹distinct_mset (learned_clss S - A)›
shows ‹distinct_mset (learned_clss T - A)›
proof (rule ccontr)
have [iff]: ‹distinct_mset (add_mset C (learned_clss S) - A) ⟷
C ∉# (learned_clss S) - A› for C
using dist distinct_mset_add_mset[of C ‹learned_clss S - A›]
proof -
have f1: "learned_clss S - A = remove1_mset C (add_mset C (learned_clss S) - A)"
by (metis Multiset.diff_right_commute add_mset_remove_trivial)
have "remove1_mset C (add_mset C (learned_clss S) - A) = add_mset C (learned_clss S) - A ⟶
distinct_mset (add_mset C (learned_clss S) - A)"
by (metis (no_types) Multiset.diff_right_commute add_mset_remove_trivial dist)
then have "¬ distinct_mset (add_mset C (learned_clss S - A)) ∨
distinct_mset (add_mset C (learned_clss S) - A) ≠ (C ∈# learned_clss S - A)"
by (metis (full_types) Multiset.diff_right_commute
distinct_mset_add_mset[of C ‹learned_clss S - A›] add_mset_remove_trivial
diff_single_trivial insert_DiffM)
then show ?thesis
using f1 by (metis (full_types) distinct_mset_add_mset[of C ‹learned_clss S - A›]
diff_single_trivial dist insert_DiffM)
qed
assume n_dist: ‹¬ ?thesis›
then have ‹backtrack S T›
using cdcl dist by (auto simp: cdcl⇩W_stgy.simps cdcl⇩W_o.simps cdcl⇩W_bj.simps
elim: propagateE conflictE decideE skipE resolveE)
then show False
using n_dist cdcl⇩W_stgy_no_relearned_clause[of S T]
by (auto simp: inv smaller clauses_def elim!: rulesE
dest!: in_diffD)
qed
lemma rtranclp_cdcl⇩W_stgy_distinct_mset_clauses_new_abs:
assumes
st: "cdcl⇩W_stgy⇧*⇧* R S" and
invR: "cdcl⇩W_all_struct_inv R" and
no_smaller: ‹no_smaller_propa R› and
‹distinct_mset (learned_clss R - A)›
shows "distinct_mset (learned_clss S - A)"
using assms by (induction rule: rtranclp_induct)
(auto simp: cdcl⇩W_stgy_distinct_mset rtranclp_cdcl⇩W_stgy_no_smaller_propa
rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv
cdcl⇩W_stgy_learned_distinct_mset_new)
lemma rtranclp_cdcl⇩W_stgy_distinct_mset_clauses_new:
assumes
st: "cdcl⇩W_stgy⇧*⇧* R S" and
invR: "cdcl⇩W_all_struct_inv R" and
no_smaller: ‹no_smaller_propa R›
shows "distinct_mset (learned_clss S - learned_clss R)"
using assms by (rule rtranclp_cdcl⇩W_stgy_distinct_mset_clauses_new_abs) auto
subsubsection ‹Decrease of a Measure›
fun cdcl⇩W_restart_measure where
"cdcl⇩W_restart_measure S =
[(3::nat) ^ (card (atms_of_mm (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_mm (init_clss S)) - length (trail S)
else length (trail S)
]"
lemma length_model_le_vars:
assumes
"no_strange_atm S" and
no_d: "no_dup (trail S)" and
"finite (atms_of_mm (init_clss S))"
shows "length (trail S) ≤ card (atms_of_mm (init_clss S))"
proof -
obtain M N U k D where S: "state S = (M, N, U, k, D)" by (cases "state S", auto)
have "finite (atm_of ` lits_of_l (trail S))"
using assms(1,3) unfolding S by (auto simp add: finite_subset)
have "length (trail S) = card (atm_of ` lits_of_l (trail S))"
using no_dup_length_eq_card_atm_of_lits_of_l no_d by blast
then show ?thesis using assms(1) unfolding no_strange_atm_def
by (auto simp add: assms(3) card_mono)
qed
lemma length_model_le_vars_all_inv:
assumes "cdcl⇩W_all_struct_inv S"
shows "length (trail S) ≤ card (atms_of_mm (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)
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_mm (learned_clss S))"
proof -
have "set_mset (learned_clss S) ⊆ simple_clss (atms_of_mm (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_mm (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 cdcl⇩W_restart_measure_decreasing:
fixes S :: 'st
assumes
"cdcl⇩W_restart S S'" and
no_restart:
"¬(learned_clss S ⊆# learned_clss S' ∧ [] = trail S' ∧ conflicting S' = None)"
and
no_forget: "learned_clss S ⊆# learned_clss S'" and
no_relearn: "⋀S'. backtrack S S' ⟹ mark_of (hd_trail S') ∉# 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_restart_measure S', cdcl⇩W_restart_measure S) ∈ lexn less_than 3"
using assms(1) assms(2,3)
proof (induct rule: cdcl⇩W_restart_all_induct)
case (propagate C L) note conf = this(1) and undef = this(5) and T = this(6)
have propa: "propagate S (cons_trail (Propagated L C) S)"
using propagate_rule[OF propagate.hyps(1,2)] propagate.hyps by auto
then have no_dup': "no_dup (Propagated L C # trail S)"
using M_level cdcl⇩W_M_level_inv_decomp(2) undef defined_lit_map by auto
let ?N = "init_clss S"
have "no_strange_atm (cons_trail (Propagated L C) S)"
using alien cdcl⇩W_restart.propagate cdcl⇩W_restart_no_strange_atm_inv propa M_level by blast
then have "atm_of ` lits_of_l (Propagated L C # trail S)
⊆ atms_of_mm (init_clss S)"
using undef unfolding no_strange_atm_def by auto
then have "card (atm_of ` lits_of_l (Propagated L C # trail S))
≤ card (atms_of_mm (init_clss S))"
by (meson atms_of_ms_finite card_mono finite_set_mset)
then have "length (Propagated L C # trail S) ≤ card (atms_of_mm ?N)"
using no_dup_length_eq_card_atm_of_lits_of_l no_dup' by fastforce
then have H: "card (atms_of_mm (init_clss S)) - length (trail S)
= Suc (card (atms_of_mm (init_clss S)) - Suc (length (trail S)))"
by simp
show ?case using conf T undef by (auto simp: H lexn3_conv)
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) S)"
using decide_rule decide.hyps by force
then have "cdcl⇩W_restart S (cons_trail (Decided L) S)"
using cdcl⇩W_restart.simps cdcl⇩W_o.intros by blast } note cdcl⇩W_restart = this
moreover {
have lev: "cdcl⇩W_M_level_inv (cons_trail (Decided L) S)"
using cdcl⇩W_restart M_level cdcl⇩W_restart_consistent_inv[OF cdcl⇩W_restart] by auto
then have no_dup: "no_dup (Decided L # trail S)"
using undef unfolding cdcl⇩W_M_level_inv_def by auto
have "no_strange_atm (cons_trail (Decided L) S)"
using M_level alien calculation(4) cdcl⇩W_restart_no_strange_atm_inv by blast
then have "length (Decided L # (trail S))
≤ card (atms_of_mm (init_clss S))"
using no_dup undef
length_model_le_vars[of "cons_trail (Decided L) S"]
by fastforce }
ultimately show ?case using conf by (simp add: lexn3_conv)
next
case (skip L C' M D) note tr = this(1) and conf = this(2) and T = this(5)
show ?case using conf T by (simp add: tr lexn3_conv)
next
case conflict
then show ?case by (simp add: lexn3_conv)
next
case resolve
then show ?case using finite by (simp add: lexn3_conv)
next
case (backtrack L D K i M1 M2 T D') note conf = this(1) and decomp = this(3) and D_D' = this(7)
and T = this(9)
let ?D' = ‹add_mset L D'›
have bt: "backtrack S T"
using backtrack_rule[OF backtrack.hyps] by auto
have "?D' ∉# learned_clss S"
using no_relearn[OF bt] conf T by auto
then have card_T:
"card (set_mset ({#?D'#} + learned_clss S)) = Suc (card (set_mset (learned_clss S)))"
by simp
have "distinct_cdcl⇩W_state T"
using bt M_level distinct_cdcl⇩W_state_inv no_dup other cdcl⇩W_o.intros cdcl⇩W_bj.intros by blast
moreover have "∀s∈#learned_clss T. ¬ tautology s"
using learned_clss_are_not_tautologies[OF cdcl⇩W_restart.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_mm (learned_clss T))"
by (auto simp: learned_clss_less_upper_bound)
then have H: "card (set_mset ({#?D'#} + learned_clss S))
≤ 3 ^ card (atms_of_mm ({#?D'#} + learned_clss S))"
using T decomp M_level by (simp add: cdcl⇩W_M_level_inv_decomp)
moreover
have "atms_of_mm ({#?D'#} + learned_clss S) ⊆ atms_of_mm (init_clss S)"
using alien conf atms_of_subset_mset_mono[OF D_D'] unfolding no_strange_atm_def
by auto
then have card_f: "card (atms_of_mm ({#?D'#} + learned_clss S))
≤ card (atms_of_mm (init_clss S))"
by (meson atms_of_ms_finite card_mono finite_set_mset)
then have "(3::nat) ^ card (atms_of_mm ({#?D'#} + learned_clss S))
≤ 3 ^ card (atms_of_mm (init_clss S))" by simp
ultimately have "(3::nat) ^ card (atms_of_mm (init_clss S))
≥ card (set_mset ({#?D'#} + learned_clss S))"
using le_trans by blast
then show ?case using decomp diff_less_mono2 card_T T M_level
by (auto simp: cdcl⇩W_M_level_inv_decomp lexn3_conv)
next
case restart
then show ?case using alien by auto
next
case (forget C T) note no_forget = this(9)
then have "C ∈# learned_clss S" and "C ∉# learned_clss T"
using forget.hyps by auto
then have "¬ learned_clss S ⊆# learned_clss T"
by (auto simp add: mset_subset_eqD)
then show ?case using no_forget by blast
qed
lemma cdcl⇩W_stgy_step_decreasing:
fixes S T :: 'st
assumes
cdcl: ‹cdcl⇩W_stgy S T› and
struct_inv: ‹cdcl⇩W_all_struct_inv S› and
smaller: ‹no_smaller_propa S›
shows "(cdcl⇩W_restart_measure T, cdcl⇩W_restart_measure S) ∈ lexn less_than 3"
proof (rule cdcl⇩W_restart_measure_decreasing)
show ‹cdcl⇩W_restart S T›
using cdcl cdcl⇩W_cdcl⇩W_restart cdcl⇩W_stgy_cdcl⇩W by blast
show ‹¬ (learned_clss S ⊆# learned_clss T ∧ [] = trail T ∧ conflicting T = None)›
using cdcl by (cases rule: cdcl⇩W_stgy_cases) (auto elim!: rulesE)
show ‹learned_clss S ⊆# learned_clss T›
using cdcl by (cases rule: cdcl⇩W_stgy_cases) (auto elim!: rulesE)
show ‹mark_of (hd_trail S') ∉# learned_clss S› if ‹backtrack S S'› for S'
using cdcl⇩W_stgy_no_relearned_clause[of S S'] cdcl⇩W_stgy_no_smaller_propa[of S S']
cdcl struct_inv smaller that unfolding clauses_def
by (auto elim!: rulesE)
show ‹no_strange_atm S› and ‹cdcl⇩W_M_level_inv S› and ‹distinct_cdcl⇩W_state S› and
‹cdcl⇩W_conflicting S› and ‹∀s∈#learned_clss S. ¬ tautology s›
using struct_inv unfolding cdcl⇩W_all_struct_inv_def by blast+
qed
lemma empty_trail_no_smaller_propa: ‹trail R = [] ⟹ no_smaller_propa R›
by (simp add: no_smaller_propa_def)
text ‹Roughly corresponds to \cwref{theo:prop:cdcltermlc}{theorem 2.9.15 page 100}
but using a different bound (the bound is below)›
lemma tranclp_cdcl⇩W_stgy_decreasing:
fixes R S T :: 'st
assumes "cdcl⇩W_stgy⇧+⇧+ R S" and
tr: "trail R = []" and
"cdcl⇩W_all_struct_inv R"
shows "(cdcl⇩W_restart_measure S, cdcl⇩W_restart_measure R) ∈ lexn less_than 3"
using assms
apply induction
using empty_trail_no_smaller_propa cdcl⇩W_stgy_no_relearned_clause cdcl⇩W_stgy_step_decreasing
apply blast
using tranclp_into_rtranclp[of cdcl⇩W_stgy R] lexn_transI[OF trans_less_than, of 3]
rtranclp_cdcl⇩W_stgy_no_smaller_propa unfolding trans_def
by (meson cdcl⇩W_stgy_step_decreasing empty_trail_no_smaller_propa
rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)
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_restart_measure S, cdcl⇩W_restart_measure (init_state N)) ∈ lexn less_than 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 less_than 3" _ _ cdcl⇩W_restart_measure])
apply (simp add: wf wf_lexn)
using tranclp_cdcl⇩W_stgy_S0_decreasing by blast
text ‹The following theorems is deeply linked with the strategy: It shows that a decision alone
cannot lead to a conflict. This is obvious but I expect this to be a major part of the proof that
the number of learnt clause cannot be larger that \<^term>‹2^n›.›
lemma no_conflict_after_decide:
assumes
dec: ‹decide S T› and
inv: ‹cdcl⇩W_all_struct_inv T› and
smaller: ‹no_smaller_propa T› and
smaller_confl: ‹no_smaller_confl T›
shows ‹¬conflict T U›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain D where
D: ‹D ∈# clauses T› and
confl: ‹trail T ⊨as CNot D›
by (auto simp: conflict.simps)
obtain L where
‹conflicting S = None› and
undef: ‹undefined_lit (trail S) L› and
‹atm_of L ∈ atms_of_mm (init_clss S)› and
T: ‹T ∼ cons_trail (Decided L) S›
using dec by (auto simp: decide.simps)
have dist: ‹distinct_mset D›
using inv D unfolding cdcl⇩W_all_struct_inv_def distinct_cdcl⇩W_state_def
by (auto dest!: multi_member_split simp: clauses_def)
have L_D: ‹L ∉# D›
using confl undef T
by (auto dest!: multi_member_split simp: Decided_Propagated_in_iff_in_lits_of_l)
show False
proof (cases ‹-L ∈# D›)
case True
have H: ‹trail T = M' @ Decided K # M ⟹
D + {#L#} ∈# clauses T ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D›
for M K M' D L
using smaller unfolding no_smaller_propa_def
by auto
have ‹trail S ⊨as CNot (remove1_mset (-L) D)›
using true_annots_CNot_lit_of_notin_skip[of ‹Decided L› ‹trail S› ‹remove1_mset (-L) D›] T True
dist confl L_D
by (auto dest: multi_member_split)
then show False
using True H[of ‹Nil› L ‹trail S› ‹remove1_mset (-L) D› ‹-L›] T D confl undef
by auto
next
case False
have H: ‹trail T = M' @ Decided K # M ⟹
D ∈# clauses T ⟹ ¬ M ⊨as CNot D›
for M K M' D
using smaller_confl unfolding no_smaller_confl_def
by auto
have ‹trail S ⊨as CNot D›
using true_annots_CNot_lit_of_notin_skip[of ‹Decided L› ‹trail S› D] T False
dist confl L_D
by (auto dest: multi_member_split)
then show False
using False H[of ‹Nil› L ‹trail S› D] T D confl undef
by auto
qed
qed
abbreviation list_weight_propa_trail :: ‹ ('v literal, 'v literal, 'v literal multiset) annotated_lit list ⇒ bool list› where
‹list_weight_propa_trail M ≡ map is_proped M›
definition comp_list_weight_propa_trail :: ‹nat ⇒ ('v literal, 'v literal, 'v literal multiset) annotated_lit list ⇒ bool list› where
‹comp_list_weight_propa_trail b M ≡ replicate (b - length M) False @ list_weight_propa_trail M›
lemma comp_list_weight_propa_trail_append[simp]:
‹comp_list_weight_propa_trail b (M @ M') =
comp_list_weight_propa_trail (b - length M') M @ list_weight_propa_trail M'›
by (auto simp: comp_list_weight_propa_trail_def)
lemma comp_list_weight_propa_trail_append_single[simp]:
‹comp_list_weight_propa_trail b (M @ [K]) =
comp_list_weight_propa_trail (b - 1) M @ [is_proped K]›
by (auto simp: comp_list_weight_propa_trail_def)
lemma comp_list_weight_propa_trail_cons[simp]:
‹comp_list_weight_propa_trail b (K # M') =
comp_list_weight_propa_trail (b - Suc (length M')) [] @ is_proped K # list_weight_propa_trail M'›
by (auto simp: comp_list_weight_propa_trail_def)
fun of_list_weight :: ‹bool list ⇒ nat› where
‹of_list_weight [] = 0›
| ‹of_list_weight (b # xs) = (if b then 1 else 0) + 2 * of_list_weight xs›
lemma of_list_weight_append[simp]:
‹of_list_weight (a @ b) = of_list_weight a + 2^(length a) * of_list_weight b›
by (induction a) auto
lemma of_list_weight_append_single[simp]:
‹of_list_weight (a @ [b]) = of_list_weight a + 2^(length a) * (if b then 1 else 0)›
using of_list_weight_append[of ‹a› ‹[b]›]
by (auto simp del: of_list_weight_append)
lemma of_list_weight_replicate_False[simp]: ‹of_list_weight (replicate n False) = 0›
by (induction n) auto
lemma of_list_weight_replicate_True[simp]: ‹of_list_weight (replicate n True) = 2^n - 1›
apply (induction n)
subgoal by auto
subgoal for m
using power_gt1_lemma[of ‹2 :: nat›]
by (auto simp add: algebra_simps Suc_diff_Suc)
done
lemma of_list_weight_le: ‹of_list_weight xs ≤ 2^(length xs) - 1›
proof -
have ‹of_list_weight xs ≤ of_list_weight (replicate (length xs) True)›
by (induction xs) auto
then show ‹?thesis›
by auto
qed
lemma of_list_weight_lt: ‹of_list_weight xs < 2^(length xs)›
using of_list_weight_le[of xs] by (metis One_nat_def Suc_le_lessD
Suc_le_mono Suc_pred of_list_weight_le zero_less_numeral zero_less_power)
lemma [simp]: ‹of_list_weight (comp_list_weight_propa_trail n []) = 0›
by (auto simp: comp_list_weight_propa_trail_def)
abbreviation propa_weight
:: ‹nat ⇒ ('v literal, 'v literal, 'v literal multiset) annotated_lit list ⇒ nat›
where
‹propa_weight n M ≡ of_list_weight (comp_list_weight_propa_trail n M)›
lemma length_comp_list_weight_propa_trail[simp]: ‹length (comp_list_weight_propa_trail a M) = max (length M) a›
by (auto simp: comp_list_weight_propa_trail_def)
lemma (in -)pow2_times_n:
‹Suc a ≤ n ⟹ 2 * 2^(n - Suc a) = (2::nat)^ (n - a)›
‹Suc a ≤ n ⟹ 2^(n - Suc a) * 2 = (2::nat)^ (n - a)›
‹Suc a ≤ n ⟹ 2^(n - Suc a) * b * 2 = (2::nat)^ (n - a) * b›
‹Suc a ≤ n ⟹ 2^(n - Suc a) * (b * 2) = (2::nat)^ (n - a) * b›
‹Suc a ≤ n ⟹ 2^(n - Suc a) * (2 * b) = (2::nat)^ (n - a) * b›
‹Suc a ≤ n ⟹ 2 * b * 2^(n - Suc a) = (2::nat)^ (n - a) * b›
‹Suc a ≤ n ⟹ 2 * (b * 2^(n - Suc a)) = (2::nat)^ (n - a) * b›
apply (simp_all add: Suc_diff_Suc semiring_normalization_rules(27))
using Suc_diff_le by fastforce+
lemma decide_propa_weight:
‹decide S T ⟹ n ≥ length (trail T) ⟹ propa_weight n (trail S) ≤ propa_weight n (trail T)›
by (auto elim!: decideE simp: comp_list_weight_propa_trail_def
algebra_simps pow2_times_n)
lemma propagate_propa_weight:
‹propagate S T ⟹ n ≥ length (trail T) ⟹ propa_weight n (trail S) < propa_weight n (trail T)›
by (auto elim!: propagateE simp: comp_list_weight_propa_trail_def
algebra_simps pow2_times_n)
text ‹
The theorem below corresponds the bound of \cwref{theo:prop:cdcltermlc}{theorem 2.9.15 page 100}.
In the current version there is no proof of the bound.
The following proof contains an immense amount of stupid bookkeeping. The proof itself
is rather easy and Isabelle makes it extra-complicated.
Let's consider the sequence \<^text>‹S → ... → T›.
The bookkeping part:
▸ We decompose it into its components \<^text>‹f 0 → f 1 → ... → f n›.
▸ Then we extract the backjumps out of it, which are at position \<^text>‹nth_nj 0›,
\<^text>‹nth_nj 1›, ...
▸ Then we extract the conflicts out of it, which are at position \<^text>‹nth_confl 0›,
\<^text>‹nth_confl 1›, ...
Then the simple part:
▸ each backtrack increases \<^term>‹propa_weight›
▸ but \<^term>‹propa_weight› is bounded by \<^term>‹2 ^ (card (atms_of_mm (init_clss S)))›
Therefore, we get the bound.
Comments on the proof:
▪ The main problem of the proof is the number of inductions in the bookkeeping part.
▪ The proof is actually by contradiction to make sure that enough backtrack step exists. This could
probably be avoided, but without change in the proof.
Comments on the bound:
▪ The proof is very very crude: Any propagation also decreases the bound. The lemma
@{thm no_conflict_after_decide} above shows that a decision cannot lead immediately to a
conflict.
▪ TODO: can a backtrack could be immediately followed by another conflict
(if there are several conflicts for the initial backtrack)? If not the bound can be divided by
two.
›
lemma cdcl_pow2_n_learned_clauses:
assumes
cdcl: ‹cdcl⇩W⇧*⇧* S T› and
confl: ‹conflicting S = None› and
inv: ‹cdcl⇩W_all_struct_inv S›
shows ‹size (learned_clss T) ≤ size (learned_clss S) + 2 ^ (card (atms_of_mm (init_clss S)))›
(is ‹_ ≤ _ + ?b›)
proof (rule ccontr)
assume ge: ‹¬ ?thesis›
let ?m = ‹card (atms_of_mm (init_clss S))›
obtain n :: nat where
n: ‹(cdcl⇩W^^n) S T›
using cdcl unfolding rtranclp_power by fast
then obtain f :: ‹nat ⇒ 'st› where
f: ‹⋀i. i < n ⟹ cdcl⇩W (f i) (f (Suc i))› and
[simp]: ‹f 0 = S› and
[simp]: ‹f n = T›
using power_ex_decomp[OF n]
by auto
have cdcl_st_k: ‹cdcl⇩W⇧*⇧* S (f k)› if ‹k ≤ n› for k
using that
apply (induction k)
subgoal by auto
subgoal for k using f[of k] by (auto)
done
let ?g = ‹λi. size (learned_clss (f i))›
have ‹?g 0 = size (learned_clss S)›
by auto
have g_n: ‹?g n > ?g 0 + 2 ^ (card (atms_of_mm (init_clss S)))›
using ge by auto
have g: ‹?g (Suc i) = ?g i ∨ (?g (Suc i) = Suc (?g i) ∧ backtrack (f i) (f (Suc i)))› if ‹i < n›
for i
using f[OF that]
by (cases rule: cdcl⇩W.cases)
(auto elim: propagateE conflictE decideE backtrackE skipE resolveE
simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps)
have g_le: ‹?g i ≤ i + ?g 0› if ‹i ≤ n› for i
using that
apply (induction i)
subgoal by auto
subgoal for i
using g[of i]
by auto
done
from this[of n] have n_ge_m: ‹n > ?b›
using g_n ge by auto
then have n0: ‹n > 0›
using not_add_less1 by fastforce
define nth_bj where
‹nth_bj = rec_nat 0 (λ_ j. (LEAST i. i > j ∧ i < n ∧ backtrack (f i) (f (Suc i))))›
have [simp]: ‹nth_bj 0 = 0›
by (auto simp: nth_bj_def)
have nth_bj_Suc: ‹nth_bj (Suc i) = (LEAST x. nth_bj i < x ∧ x < n ∧ backtrack (f x) (f (Suc x)))›
for i
by (auto simp: nth_bj_def)
have between_nth_bj_not_bt:
‹¬backtrack (f k) (f (Suc k))›
if ‹k < n› ‹k > nth_bj i› ‹k < nth_bj (Suc i) › for k i
using not_less_Least[of k ‹λx. nth_bj i < x ∧ x < n ∧ backtrack (f x) (f (Suc x))›] that
unfolding nth_bj_Suc[symmetric]
by auto
have g_nth_bj_eq:
‹?g (Suc k) = ?g k›
if ‹k < n› ‹k > nth_bj i› ‹k < nth_bj (Suc i)› for k i
using between_nth_bj_not_bt[OF that(1-3)] f[of k, OF that(1)]
by (auto elim: propagateE conflictE decideE backtrackE skipE resolveE
simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)
have g_nth_bj_eq2:
‹?g (Suc k) = ?g (Suc (nth_bj i))›
if ‹k < n› ‹k > nth_bj i› ‹k < nth_bj (Suc i)› for k i
using that
apply (induction k)
subgoal by blast
subgoal for k
using g_nth_bj_eq less_antisym by fastforce
done
have [simp]: ‹?g (Suc 0) = ?g 0›
using confl f[of 0] n0
by (auto elim: propagateE conflictE decideE backtrackE skipE resolveE
simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)
have ‹(?g (nth_bj i) = size (learned_clss S) + (i - 1)) ∧
nth_bj i < n ∧
nth_bj i ≥ i ∧
(i > 0 ⟶ backtrack (f (nth_bj i)) (f (Suc (nth_bj i)))) ∧
(i > 0 ⟶ ?g (Suc (nth_bj i)) = size (learned_clss S) + i) ∧
(i > 0 ⟶ nth_bj i > nth_bj (i-1))›
if ‹i ≤ ?b+1›
for i
using that
proof (induction i)
case 0
then show ?case using n0 by auto
next
case (Suc i)
then have IH: ‹?g (nth_bj i) = size (learned_clss S) + (i - 1)›
‹0 < i ⟹ backtrack (f (nth_bj i)) (f (Suc (nth_bj i)))›
‹0 < i ⟹ ?g (Suc (nth_bj i)) = size (learned_clss S) + i› and
i_le_m: ‹Suc i ≤ ?b+1› and
le_n: ‹nth_bj i < n› and
gei: ‹nth_bj i ≥ i›
by auto
have ex_larger: ‹∃x>nth_bj i. x < n ∧ backtrack (f x) (f (Suc x))›
proof (rule ccontr)
assume ‹¬ ?thesis›
then have [simp]: ‹n>x ⟹ x>nth_bj i ⟹ ?g (Suc x) = ?g x› for x
using g[of x] n_ge_m
by auto
have eq1: ‹nth_bj i < Suc x ⟹ ¬ nth_bj i < x ⟹ x = nth_bj i› and
eq2: ‹nth_bj i < x ⟹ ¬ nth_bj i < x - Suc 0 ⟹ nth_bj i = x - Suc 0›
for x
by simp_all
have ex_larger: ‹n>x ⟹ x>nth_bj i ⟹ ?g (Suc x) = ?g (Suc (nth_bj i))› for x
apply (induction x)
subgoal by auto
subgoal for x
by (cases ‹nth_bj i < x›) (auto dest: eq1)
done
from this[of ‹n-1›] have g_n_nth_bj: ‹?g n = ?g (Suc (nth_bj i))›
using n_ge_m i_le_m le_n
by (cases ‹nth_bj i < n - Suc 0›)
(auto dest: eq2)
then have ‹size (learned_clss (f (Suc (nth_bj i)))) < size (learned_clss T)›
using g_n i_le_m n_ge_m g_le[of ‹Suc (nth_bj i)›] le_n ge
‹?g (nth_bj i) = size (learned_clss S) + (i - 1)›
using Suc.IH by auto
then show False
using g_n i_le_m n_ge_m g_le[of ‹Suc (nth_bj i)›] g_n_nth_bj by auto
qed
from LeastI_ex[OF ex_larger]
have bt: ‹backtrack (f (nth_bj (Suc i))) (f (Suc (nth_bj (Suc i))))› and
le: ‹nth_bj (Suc i) < n› and
nth_mono: ‹nth_bj i < nth_bj (Suc i)›
unfolding nth_bj_Suc[symmetric]
by auto
have g_nth_Suc_g_Suc_nth: ‹?g (nth_bj (Suc i)) = ?g (Suc (nth_bj i))›
using g_nth_bj_eq2[of ‹nth_bj (Suc i) - 1› i] le nth_mono
apply auto
by (metis Suc_pred gr0I less_Suc0 less_Suc_eq less_imp_diff_less)
have H1: ‹size (learned_clss (f (Suc (nth_bj (Suc i))))) =
1 + size (learned_clss (f (nth_bj (Suc i))))› if ‹i = 0›
using bt unfolding that
by (auto simp: that elim: backtrackE)
have ?case if ‹i > 0›
using IH that nth_mono le bt gei
by (auto elim: backtrackE simp: g_nth_Suc_g_Suc_nth)
moreover have ?case if ‹i = 0›
using le bt gei nth_mono IH g_nth_bj_eq2[of ‹nth_bj (Suc i) - 1› i]
g_nth_Suc_g_Suc_nth
apply (intro conjI)
subgoal by (simp add: that)
subgoal by (auto simp: that elim: backtrackE)
subgoal by (auto simp: that elim: backtrackE)
subgoal Hk by (auto simp: that elim: backtrackE)
subgoal using H1 by (auto simp: that elim: backtrackE)
subgoal using nth_mono by auto
done
ultimately show ?case by blast
qed
then have
‹(?g (nth_bj i) = size (learned_clss S) + (i - 1))› and
nth_bj_le: ‹nth_bj i < n› and
nth_bj_ge: ‹nth_bj i ≥ i› and
bt_nth_bj: ‹i > 0 ⟹ backtrack (f (nth_bj i)) (f (Suc (nth_bj i)))› and
‹i > 0 ⟹ ?g (Suc (nth_bj i)) = size (learned_clss S) + i› and
nth_bj_mono: ‹i > 0 ⟹ nth_bj (i - 1) < nth_bj i›
if ‹i ≤ ?b+1›
for i
using that by blast+
have
confl_None: ‹conflicting (f (Suc (nth_bj i))) = None› and
confl_nth_bj: ‹conflicting (f (nth_bj i)) ≠ None›
if ‹i ≤ ?b+1› ‹i > 0›
for i
using bt_nth_bj[OF that] by (auto simp: backtrack.simps)
have conflicting_still_conflicting:
‹conflicting (f k) ≠ None ⟶ conflicting (f (Suc k)) ≠ None›
if ‹k < n› ‹k > nth_bj i› ‹k < nth_bj (Suc i)› for k i
using between_nth_bj_not_bt[OF that] f[OF that(1)]
by (auto elim: propagateE conflictE decideE backtrackE skipE resolveE
simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)
define nth_confl where
‹nth_confl n ≡ LEAST i. i > nth_bj n ∧ i < nth_bj (Suc n) ∧ conflict (f i) (f (Suc i))› for n
have ‹∃i>nth_bj a. i < nth_bj (Suc a) ∧ conflict (f i) (f (Suc i))›
if a_n: ‹a ≤ ?b› ‹a > 0›
for a
proof (rule ccontr)
assume H: ‹¬ ?thesis›
have ‹conflicting (f (nth_bj a + Suc i)) = None›
if ‹nth_bj a + Suc i ≤ nth_bj (Suc a)› for i :: nat
using that
apply (induction i)
subgoal
using confl_None[of a] a_n n_ge_m by auto
subgoal for i
apply (cases ‹Suc (nth_bj a + i) < n›)
using f[of ‹nth_bj a + Suc i›] H
apply (auto elim: propagateE conflictE decideE backtrackE skipE resolveE
simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)[]
using nth_bj_le[of ‹Suc a›] a_n(1) by auto
done
from this[of ‹nth_bj (Suc a) - 1 - nth_bj a›] a_n
show False
using nth_bj_mono[of ‹Suc a›] a_n nth_bj_le[of ‹Suc a›] confl_nth_bj[of ‹Suc a›]
by auto
qed
from LeastI_ex[OF this] have nth_bj_le_nth_confl: ‹nth_bj a < nth_confl a› and
nth_confl: ‹conflict (f (nth_confl a)) (f (Suc (nth_confl a)))› and
nth_confl_le_nth_bj_Suc: ‹nth_confl a < nth_bj (Suc a)›
if a_n: ‹a ≤ ?b› ‹a > 0›
for a
using that unfolding nth_confl_def[symmetric]
by blast+
have nth_confl_conflicting: ‹conflicting (f (Suc (nth_confl a))) ≠ None›
if a_n: ‹a ≤ ?b› ‹a > 0›
for a
using nth_confl[OF a_n]
by (auto simp: conflict.simps)
have no_conflict_before_nth_confl: ‹¬conflict (f k) (f (Suc k))›
if ‹k > nth_bj a› and
‹k < nth_confl a› and
a_n: ‹a ≤ ?b› ‹a > 0›
for k a
using not_less_Least[of k ‹λi. i > nth_bj a ∧ i < nth_bj (Suc a) ∧ conflict (f i) (f (Suc i))›] that
nth_confl_le_nth_bj_Suc[of a]
unfolding nth_confl_def[symmetric]
by auto
have conflicting_after_nth_confl: ‹conflicting (f (Suc (nth_confl a) + k)) ≠ None›
if a_n: ‹a ≤ ?b› ‹a > 0› and
k: ‹Suc (nth_confl a) + k < nth_bj (Suc a)›
for a k
using k
apply (induction k)
subgoal using nth_confl_conflicting[OF a_n] by simp
subgoal for k
using conflicting_still_conflicting[of ‹Suc (nth_confl a + k)› a] a_n
nth_bj_le[of a] nth_bj_le_nth_confl[of a]
apply (cases ‹Suc (nth_confl a + k) < n›)
apply auto
by (metis (no_types, lifting) Suc_le_lessD add.commute le_less less_trans_Suc nth_bj_le
plus_1_eq_Suc)
done
have conflicting_before_nth_confl: ‹conflicting (f (Suc (nth_bj a) + k)) = None›
if a_n: ‹a ≤ ?b› ‹a > 0› and
k: ‹Suc (nth_bj a) + k < nth_confl a›
for a k
using k
apply (induction k)
subgoal using confl_None[of a] a_n by simp
subgoal for k
using f[of ‹Suc (nth_bj a) + k›] no_conflict_before_nth_confl[of a ‹Suc (nth_bj a) + k›] a_n
nth_confl_le_nth_bj_Suc[of a] nth_bj_le[of ‹Suc a›]
apply (cases ‹Suc (nth_bj a + k) < n›)
apply (auto elim!: propagateE conflictE decideE backtrackE skipE resolveE
simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)[]
by linarith
done
have
ex_trail_decomp: ‹∃M. trail (f (Suc (nth_confl a))) = M @ trail (f (Suc (nth_confl a + k)))›
if a_n: ‹a ≤ ?b› ‹a > 0› and
k: ‹Suc (nth_confl a) + k ≤ nth_bj (Suc a)›
for a k
using k
proof (induction k)
case 0
then show ‹?case› by auto
next
case (Suc k)
moreover have ‹nth_confl a + k < n›
proof -
have "nth_bj (Suc a) < n"
by (rule nth_bj_le) (use a_n(1) in simp)
then show ?thesis
using Suc.prems by linarith
qed
moreover have ‹∃Ma. M @ trail (f (Suc (nth_confl a + k))) =
Ma @ tl (trail (f (Suc (nth_confl a + k))))› for M
by (cases ‹trail (f (Suc (nth_confl a + k)))›) auto
ultimately show ?case
using f[of ‹Suc (nth_confl a + k)›] conflicting_after_nth_confl[of a ‹k›, OF a_n] Suc
between_nth_bj_not_bt[of ‹Suc (nth_confl a + k)› ‹a›]
nth_bj_le_nth_confl[of a, OF a_n]
apply (cases ‹Suc (nth_confl a + k) < n›)
subgoal
by (auto elim!: propagateE conflictE decideE skipE resolveE
simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps)[]
subgoal
by (metis (no_types, lifting) Suc_leD Suc_lessI a_n(1) add.commute add_Suc
add_mono_thms_linordered_semiring(1) le_numeral_extra(4) not_le nth_bj_le plus_1_eq_Suc)
done
qed
have propa_weight_decreasing_confl:
‹propa_weight n (trail (f (Suc (nth_bj (Suc a))))) > propa_weight n (trail (f (nth_confl a)))›
if a_n: ‹a ≤ ?b› ‹a > 0› and
n: ‹n ≥ length (trail (f (nth_confl a)))›
for a n
proof -
have pw0: ‹propa_weight n (trail (f (Suc (nth_confl a)))) =
propa_weight n (trail (f (nth_confl a)))› and
[simp]: ‹trail (f (Suc (nth_confl a))) = trail (f (nth_confl a))›
using nth_confl[OF a_n] by (auto elim!: conflictE)
have H: ‹nth_bj (Suc a) = Suc (nth_confl a) ∨ nth_bj (Suc a) ≥ Suc (Suc (nth_confl a))›
using nth_bj_le_nth_confl[of a, OF a_n]
using a_n(1) nth_confl_le_nth_bj_Suc that(2) by force
from ex_trail_decomp[of a ‹nth_bj (Suc a) - (1+nth_confl a)›, OF a_n]
obtain M where
M: ‹trail (f (Suc (nth_confl a))) = M @ trail (f (nth_bj (Suc a)))›
apply -
apply (rule disjE[OF H])
subgoal
by auto
subgoal
using nth_bj_le_nth_confl[of a, OF a_n] nth_bj_ge[of ‹Suc a›] a_n
by (auto simp add: numeral_2_eq_2)
done
obtain K M1 M2 D D' L where
decomp: ‹(Decided K # M1, M2)
∈ set (get_all_ann_decomposition (trail (f (nth_bj (Suc a)))))› and
‹get_maximum_level (trail (f (nth_bj (Suc a)))) (add_mset L D') =
backtrack_lvl (f (nth_bj (Suc a)))› and
‹get_level (trail (f (nth_bj (Suc a)))) L = backtrack_lvl (f (nth_bj (Suc a)))› and
‹get_level (trail (f (nth_bj (Suc a)))) K =
Suc (get_maximum_level (trail (f (nth_bj (Suc a)))) D')› and
‹D' ⊆# D› and
‹clauses (f (nth_bj (Suc a))) ⊨pm add_mset L D'› and
st_Suc: ‹f (Suc (nth_bj (Suc a))) ∼
cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None (f (nth_bj (Suc a))))))›
using bt_nth_bj[of ‹Suc a›] a_n
by (auto elim!: backtrackE)
obtain M3 where
tr: ‹trail (f (nth_bj (Suc a))) = M3 @ M2 @ Decided K # M1›
using decomp by auto
define M2' where
‹M2' = M3 @ M2›
then have
tr: ‹trail (f (nth_bj (Suc a))) = M2' @ Decided K # M1›
using tr by auto
define M' where
‹M' = M @ M2'›
then have tr2: ‹trail (f (nth_confl a)) = M' @ Decided K # M1›
using tr M n
by auto
have [simp]: ‹max (length M) (n - Suc (length M1 + (length M2')))
= (n - Suc (length M1 + (length M2')))›
using tr M st_Suc n by auto
have [simp]: ‹2 *
(of_list_weight (list_weight_propa_trail M1) *
(2 ^ length M2' *
(2 ^ (n - Suc (length M1 + length M2'))))) =
of_list_weight (list_weight_propa_trail M1) * 2 ^ (n - length M1)›
using tr M n by (auto simp: algebra_simps field_simps pow2_times_n
comm_semiring_1_class.semiring_normalization_rules(26))
have n_ge: ‹Suc (length M + (length M2' + length M1)) ≤ n›
using n st_Suc tr M by auto
have WTF: ‹a < b ⟹ b ≤ c ⟹ a < c› and
WTF': ‹a ≤ b ⟹ b < c ⟹ a < c› for a b c :: nat
by auto
have 3: ‹propa_weight (n - Suc (length M1 + (length M2'))) M
≤ 2^(n - Suc (length M1 + length M2')) - 1›
using of_list_weight_le
apply auto
by (metis ‹max (length M) (n - Suc (length M1 + (length M2'))) = n - Suc (length M1 + (length M2'))›
length_comp_list_weight_propa_trail)
have 1: ‹of_list_weight (list_weight_propa_trail M2') *
2 ^ (n - Suc (length M1 + length M2')) < Suc (if M2' = [] then 0
else 2 ^ (n - Suc (length M1)) - 2 ^ (n - Suc (length M1 + length M2')))›
apply (cases ‹M2' = []›)
subgoal by auto
subgoal
apply (rule WTF')
apply (rule Nat.mult_le_mono1[of ‹of_list_weight (list_weight_propa_trail M2')›,
OF of_list_weight_le[of ‹(list_weight_propa_trail M2')›]])
using of_list_weight_le[of ‹(list_weight_propa_trail M2')›] n M tr
by (auto simp add: comm_semiring_1_class.semiring_normalization_rules(26)
algebra_simps)
done
have WTF2:
‹a ≤ a' ⟹ b < b' ⟹ a + b < a' + b'› for a b c a' b' c' :: nat
by auto
have ‹propa_weight (n - Suc (length M1 + length M2')) M +
of_list_weight (list_weight_propa_trail M2') *
2 ^ (n - Suc (length M1 + length M2'))
< 2 ^ (n - Suc (length M1))›
apply (rule WTF)
apply (rule WTF2[OF 3 1])
using n_ge[unfolded nat_le_iff_add] by (auto simp: ac_simps algebra_simps)
then have ‹propa_weight n (trail (f (nth_confl a))) < propa_weight n (trail (f (Suc (nth_bj (Suc a)))))›
using tr2 M st_Suc n tr
by (auto simp: pow2_times_n algebra_simps
comm_semiring_1_class.semiring_normalization_rules(26))
then show ‹?thesis›
using pw0 by auto
qed
have length_trail_le_m: ‹length (trail (f k)) < ?m + 1›
if ‹k ≤ n›
for k
proof -
have ‹cdcl⇩W_all_struct_inv (f k)›
using rtranclp_cdcl⇩W_cdcl⇩W_restart[OF cdcl_st_k[OF that]] inv
rtranclp_cdcl⇩W_all_struct_inv_inv by blast
then have ‹cdcl⇩W_M_level_inv (f k)› and ‹no_strange_atm (f k)›
unfolding cdcl⇩W_all_struct_inv_def by blast+
then have ‹no_dup (trail (f k))› and
incl: ‹atm_of ` lits_of_l (trail (f k)) ⊆ atms_of_mm (init_clss (f k))›
unfolding cdcl⇩W_M_level_inv_def no_strange_atm_def
by auto
have eq: ‹(atms_of_mm (init_clss (f k))) = (atms_of_mm (init_clss S))›
using rtranclp_cdcl⇩W_restart_init_clss[OF rtranclp_cdcl⇩W_cdcl⇩W_restart[OF cdcl_st_k[OF that]]]
by auto
have ‹length (trail (f k)) = card (atm_of ` lits_of_l (trail (f k)))›
using ‹no_dup (trail (f k))› no_dup_length_eq_card_atm_of_lits_of_l by blast
also have ‹card (atm_of ` lits_of_l (trail (f k))) ≤ ?m›
using card_mono[OF _ incl] eq by auto
finally show ?thesis
by linarith
qed
have propa_weight_decreasing_propa:
‹propa_weight ?m (trail (f (nth_confl a))) ≥ propa_weight ?m (trail (f (Suc (nth_bj a))))›
if a_n: ‹a ≤ ?b› ‹a > 0›
for a
proof -
have ppa: ‹propa_weight ?m (trail (f (Suc (nth_bj a) + Suc k)))
≥ propa_weight ?m (trail (f (Suc (nth_bj a) + k)))›
if ‹k < nth_confl a - Suc (nth_bj a)›
for k
proof -
have ‹Suc (nth_bj a + k) < n› and ‹Suc (nth_bj a + k) < nth_confl a›
using that nth_bj_le_nth_confl[OF a_n] nth_confl_le_nth_bj_Suc[OF a_n]
nth_bj_le[of ‹Suc a›] a_n
by auto
then show ?thesis
using f[of ‹(Suc (nth_bj a) + k)›] conflicting_before_nth_confl[OF a_n, of ‹k›]
no_conflict_before_nth_confl[OF _ _ a_n, of ‹Suc (nth_bj a) + k›] that
length_trail_le_m[of ‹Suc (Suc (nth_bj a) + k)›]
by (auto elim!: skipE resolveE backtrackE
simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps cdcl⇩W.simps
dest!: propagate_propa_weight[of _ _ ?m]
decide_propa_weight[of _ _ ?m])
qed
have WTF3: ‹(Suc (nth_bj a + (nth_confl a - Suc (nth_bj a)))) = nth_confl a›
using a_n(1) nth_bj_le_nth_confl that(2) by fastforce
have ‹propa_weight ?m (trail (f (Suc (nth_bj a) + k)))
≥ propa_weight ?m (trail (f (Suc (nth_bj a))))›
if ‹k ≤ nth_confl a - Suc (nth_bj a)›
for k
using that
apply (induction k)
subgoal by auto
subgoal for k using ppa[of k]
apply (cases ‹k < nth_confl a - Suc (nth_bj a)›)
subgoal by auto
subgoal by linarith
done
done
from this[of ‹nth_confl a - (Suc (nth_bj a))›]
show ?thesis
by (auto simp: WTF3)
qed
have propa_weight_decreasing_confl:
‹propa_weight ?m (trail (f (Suc (nth_bj a))))
< propa_weight ?m (trail (f (Suc (nth_bj (Suc a)))))›
if a_n: ‹a ≤ ?b› ‹a > 0›
for a
proof -
have WTF: ‹b < c ⟹ a ≤ b ⟹ a < c› for a b c :: nat by linarith
have ‹nth_confl a < n›
by (metis Suc_le_mono a_n(1) add.commute add_lessD1 less_imp_le nat_le_iff_add
nth_bj_le nth_confl_le_nth_bj_Suc plus_1_eq_Suc that(2))
show ?thesis
apply (rule WTF)
apply (rule propa_weight_decreasing_confl[OF a_n, of ?m])
subgoal using length_trail_le_m[of ‹nth_confl a›] ‹nth_confl a < n› by auto
apply (rule propa_weight_decreasing_propa[OF a_n])
done
qed
have weight1: ‹propa_weight ?m (trail (f (Suc (nth_bj 1)))) ≥ 1›
using bt_nth_bj[of 1]
by (auto simp: elim!: backtrackE intro!: trans_le_add1)
have ‹propa_weight ?m (trail (f (Suc (nth_bj (Suc a))))) ≥
propa_weight ?m (trail (f (Suc (nth_bj 1)))) + a›
if a_n: ‹a ≤ ?b›
for a :: nat
using that
apply (induction a)
subgoal by auto
subgoal for a
using propa_weight_decreasing_confl[of ‹Suc a›]
by auto
done
from this[of ‹?b›] have ‹propa_weight ?m (trail (f (Suc (nth_bj (Suc (?b)))))) ≥ 1 + ?b›
using weight1 by auto
moreover have
‹max (length (trail (f (Suc (nth_bj (Suc ?b)))))) ?m = ?m›
using length_trail_le_m[of ‹(Suc (nth_bj (Suc ?b)))›] Suc_leI nth_bj_le
nth_bj_le[of ‹Suc (?b)›] by (auto simp: max_def)
ultimately show ‹False›
using of_list_weight_le[of ‹comp_list_weight_propa_trail ?m (trail (f (Suc (nth_bj (Suc ?b)))))›]
by (simp del: state_eq_init_clss state_eq_trail)
qed
text ‹Application of the previous theorem to an initial state:›
corollary cdcl_pow2_n_learned_clauses2:
assumes
cdcl: ‹cdcl⇩W⇧*⇧* (init_state N) T› and
inv: ‹cdcl⇩W_all_struct_inv (init_state N)›
shows ‹size (learned_clss T) ≤ 2 ^ (card (atms_of_mm N))›
using assms cdcl_pow2_n_learned_clauses[of ‹init_state N› T]
by auto
end
end