theory CDCL_W_Partial_Optimal_Model
imports CDCL_W_Partial_Encoding
begin
lemma isabelle_should_do_that_automatically: ‹Suc (a - Suc 0) = a ⟷ a ≥ 1›
by auto
lemma (in conflict_driven_clause_learning⇩W_optimal_weight)
conflict_opt_state_eq_compatible:
‹conflict_opt S T ⟹ S ∼ S' ⟹ T ∼ T' ⟹ conflict_opt S' T'›
using state_eq_trans[of T' T
‹update_conflicting (Some (negate_ann_lits (trail S'))) S›]
using state_eq_trans[of T
‹update_conflicting (Some (negate_ann_lits (trail S'))) S›
‹update_conflicting (Some (negate_ann_lits (trail S'))) S'›]
update_conflicting_state_eq[of S S' ‹Some {#}›]
apply (auto simp: conflict_opt.simps state_eq_sym)
using reduce_trail_to_state_eq state_eq_trans update_conflicting_state_eq by blast
context optimal_encoding
begin
definition base_atm :: ‹'v ⇒ 'v› where
‹base_atm L = (if L ∈ Σ - ΔΣ then L else
if L ∈ replacement_neg ` ΔΣ then (SOME K. (K ∈ ΔΣ ∧ L = replacement_neg K))
else (SOME K. (K ∈ ΔΣ ∧ L = replacement_pos K)))›
lemma normalize_lit_Some_simp[simp]: ‹(SOME K. K ∈ ΔΣ ∧ (L⇧↦⇧0 = K⇧↦⇧0)) = L› if ‹L ∈ ΔΣ› for K
by (rule some1_equality) (use that in auto)
lemma base_atm_simps1[simp]:
‹L ∈ Σ ⟹ L ∉ ΔΣ ⟹ base_atm L = L›
by (auto simp: base_atm_def)
lemma base_atm_simps2[simp]:
‹L ∈ (Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ ⟹
K ∈ Σ ⟹ K ∉ ΔΣ ⟹ L ∈ Σ ⟹ K = base_atm L ⟷ L = K›
by (auto simp: base_atm_def)
lemma base_atm_simps3[simp]:
‹L ∈ Σ - ΔΣ ⟹ base_atm L ∈ Σ›
‹L ∈ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ ⟹ base_atm L ∈ ΔΣ›
apply (auto simp: base_atm_def)
by (metis (mono_tags, lifting) tfl_some)
lemma base_atm_simps4[simp]:
‹L ∈ ΔΣ ⟹ base_atm (replacement_pos L) = L›
‹L ∈ ΔΣ ⟹ base_atm (replacement_neg L) = L›
by (auto simp: base_atm_def)
fun normalize_lit :: ‹'v literal ⇒ 'v literal› where
‹normalize_lit (Pos L) =
(if L ∈ replacement_neg ` ΔΣ
then Neg (replacement_pos (SOME K. (K ∈ ΔΣ ∧ L = replacement_neg K)))
else Pos L)› |
‹normalize_lit (Neg L) =
(if L ∈ replacement_neg ` ΔΣ
then Pos (replacement_pos (SOME K. K ∈ ΔΣ ∧ L = replacement_neg K))
else Neg L)›
abbreviation normalize_clause :: ‹'v clause ⇒ 'v clause› where
‹normalize_clause C ≡ normalize_lit `# C›
lemma normalize_lit[simp]:
‹L ∈ Σ - ΔΣ ⟹ normalize_lit (Pos L) = (Pos L)›
‹L ∈ Σ - ΔΣ ⟹ normalize_lit (Neg L) = (Neg L)›
‹L ∈ ΔΣ ⟹ normalize_lit (Pos (replacement_neg L)) = Neg (replacement_pos L)›
‹L ∈ ΔΣ ⟹ normalize_lit (Neg (replacement_neg L)) = Pos (replacement_pos L)›
by auto
definition all_clauses_literals :: ‹'v list› where
‹all_clauses_literals =
(SOME xs. mset xs = mset_set ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ))›
datatype (in -) 'c search_depth =
sd_is_zero: SD_ZERO (the_search_depth: 'c) |
sd_is_one: SD_ONE (the_search_depth: 'c) |
sd_is_two: SD_TWO (the_search_depth: 'c)
abbreviation (in -) un_hide_sd :: ‹'a search_depth list ⇒ 'a list› where
‹un_hide_sd ≡ map the_search_depth›
fun nat_of_search_deph :: ‹'c search_depth ⇒ nat› where
‹nat_of_search_deph (SD_ZERO _) = 0› |
‹nat_of_search_deph (SD_ONE _) = 1› |
‹nat_of_search_deph (SD_TWO _) = 2›
definition opposite_var where
‹opposite_var L = (if L ∈ replacement_pos ` ΔΣ then replacement_neg (base_atm L)
else replacement_pos (base_atm L))›
lemma opposite_var_replacement_if[simp]:
‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ A ∈ ΔΣ ⟹
opposite_var L = replacement_pos A ⟷ L = replacement_neg A›
‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ A ∈ ΔΣ ⟹
opposite_var L = replacement_neg A ⟷ L = replacement_pos A›
‹A ∈ ΔΣ ⟹ opposite_var (replacement_pos A) = replacement_neg A›
‹A ∈ ΔΣ ⟹ opposite_var (replacement_neg A) = replacement_pos A›
by (auto simp: opposite_var_def)
context
assumes [simp]: ‹finite Σ›
begin
lemma all_clauses_literals:
‹mset all_clauses_literals = mset_set ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ)›
‹distinct all_clauses_literals›
‹set all_clauses_literals = ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ)›
proof -
let ?A = ‹mset_set ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪
replacement_pos ` ΔΣ)›
show 1: ‹mset all_clauses_literals = ?A›
using someI[of ‹λxs. mset xs = ?A›]
finite_Σ ex_mset[of ?A]
unfolding all_clauses_literals_def[symmetric]
by metis
show 2: ‹distinct all_clauses_literals›
using someI[of ‹λxs. mset xs = ?A›]
finite_Σ ex_mset[of ?A]
unfolding all_clauses_literals_def[symmetric]
by (metis distinct_mset_mset_set distinct_mset_mset_distinct)
show 3: ‹set all_clauses_literals = ((Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ)›
using arg_cong[OF 1, of set_mset] finite_Σ
by simp
qed
definition unset_literals_in_Σ where
‹unset_literals_in_Σ M L ⟷ undefined_lit M (Pos L) ∧ L ∈ Σ - ΔΣ›
definition full_unset_literals_in_ΔΣ where
‹full_unset_literals_in_ΔΣ M L ⟷
undefined_lit M (Pos L) ∧ L ∉ Σ - ΔΣ ∧ undefined_lit M (Pos (opposite_var L)) ∧
L ∈ replacement_pos ` ΔΣ›
definition full_unset_literals_in_ΔΣ' where
‹full_unset_literals_in_ΔΣ' M L ⟷
undefined_lit M (Pos L) ∧ L ∉ Σ - ΔΣ ∧ undefined_lit M (Pos (opposite_var L)) ∧
L ∈ replacement_neg ` ΔΣ›
definition half_unset_literals_in_ΔΣ where
‹half_unset_literals_in_ΔΣ M L ⟷
undefined_lit M (Pos L) ∧ L ∉ Σ - ΔΣ ∧ defined_lit M (Pos (opposite_var L))›
definition sorted_unadded_literals :: ‹('v, 'v clause) ann_lits ⇒ 'v list› where
‹sorted_unadded_literals M =
(let
M0 = filter (full_unset_literals_in_ΔΣ' M) all_clauses_literals;
― ‹weight is 0›
M1 = filter (unset_literals_in_Σ M) all_clauses_literals;
― ‹weight is 2›
M2 = filter (full_unset_literals_in_ΔΣ M) all_clauses_literals;
― ‹weight is 2›
M3 = filter (half_unset_literals_in_ΔΣ M) all_clauses_literals
― ‹weight is 1›
in
M0 @ M3 @ M1 @ M2)›
definition complete_trail :: ‹('v, 'v clause) ann_lits ⇒ ('v, 'v clause) ann_lits› where
‹complete_trail M =
(map (Decided o Pos) (sorted_unadded_literals M) @ M)›
lemma in_sorted_unadded_literals_undefD:
‹atm_of (lit_of l) ∈ set (sorted_unadded_literals M) ⟹ l ∉ set M›
‹atm_of (l') ∈ set (sorted_unadded_literals M) ⟹ undefined_lit M l'›
‹xa ∈ set (sorted_unadded_literals M) ⟹ lit_of x = Neg xa ⟹ x ∉ set M› and
set_sorted_unadded_literals[simp]:
‹set (sorted_unadded_literals M) =
Set.filter (λL. undefined_lit M (Pos L)) (set all_clauses_literals)›
by (auto simp: sorted_unadded_literals_def undefined_notin all_clauses_literals(1,2)
defined_lit_Neg_Pos_iff half_unset_literals_in_ΔΣ_def full_unset_literals_in_ΔΣ_def
unset_literals_in_Σ_def Let_def full_unset_literals_in_ΔΣ'_def
all_clauses_literals(3))
lemma [simp]:
‹full_unset_literals_in_ΔΣ [] = (λL. L ∈ replacement_pos ` ΔΣ)›
‹full_unset_literals_in_ΔΣ' [] = (λL. L ∈ replacement_neg ` ΔΣ)›
‹half_unset_literals_in_ΔΣ [] = (λL. False)›
‹unset_literals_in_Σ [] = (λL. L ∈ Σ - ΔΣ)›
by (auto simp: full_unset_literals_in_ΔΣ_def
unset_literals_in_Σ_def full_unset_literals_in_ΔΣ'_def
half_unset_literals_in_ΔΣ_def intro!: ext)
lemma filter_disjount_union:
‹(⋀x. x ∈ set xs ⟹ P x ⟹ ¬Q x) ⟹
length (filter P xs) + length (filter Q xs) =
length (filter (λx. P x ∨ Q x) xs)›
by (induction xs) auto
lemma length_sorted_unadded_literals_empty[simp]:
‹length (sorted_unadded_literals []) = length all_clauses_literals›
apply (auto simp: sorted_unadded_literals_def sum_length_filter_compl
Let_def ac_simps filter_disjount_union)
apply (subst filter_disjount_union)
apply auto
apply (subst filter_disjount_union)
apply auto
by (metis (no_types, lifting) Diff_iff UnE all_clauses_literals(3) filter_True)
lemma sorted_unadded_literals_Cons_notin_all_clauses_literals[simp]:
assumes
‹atm_of (lit_of K) ∉ set all_clauses_literals›
shows
‹sorted_unadded_literals (K # M) = sorted_unadded_literals M›
proof -
have [simp]: ‹filter (full_unset_literals_in_ΔΣ' (K # M))
all_clauses_literals =
filter (full_unset_literals_in_ΔΣ' M)
all_clauses_literals›
‹filter (full_unset_literals_in_ΔΣ (K # M))
all_clauses_literals =
filter (full_unset_literals_in_ΔΣ M)
all_clauses_literals›
‹filter (half_unset_literals_in_ΔΣ (K # M))
all_clauses_literals =
filter (half_unset_literals_in_ΔΣ M)
all_clauses_literals›
‹filter (unset_literals_in_Σ (K # M)) all_clauses_literals =
filter (unset_literals_in_Σ M) all_clauses_literals›
using assms unfolding full_unset_literals_in_ΔΣ'_def full_unset_literals_in_ΔΣ_def
half_unset_literals_in_ΔΣ_def unset_literals_in_Σ_def
by (auto simp: sorted_unadded_literals_def undefined_notin all_clauses_literals(1,2)
defined_lit_Neg_Pos_iff all_clauses_literals(3) defined_lit_cons
intro!: ext filter_cong)
show ?thesis
by (auto simp: undefined_notin all_clauses_literals(1,2)
defined_lit_Neg_Pos_iff all_clauses_literals(3) sorted_unadded_literals_def)
qed
lemma sorted_unadded_literals_cong:
assumes ‹⋀L. L ∈ set all_clauses_literals ⟹ defined_lit M (Pos L) = defined_lit M' (Pos L)›
shows ‹sorted_unadded_literals M = sorted_unadded_literals M'›
proof -
have [simp]: ‹filter (full_unset_literals_in_ΔΣ' (M))
all_clauses_literals =
filter (full_unset_literals_in_ΔΣ' M')
all_clauses_literals›
‹filter (full_unset_literals_in_ΔΣ (M))
all_clauses_literals =
filter (full_unset_literals_in_ΔΣ M')
all_clauses_literals›
‹filter (half_unset_literals_in_ΔΣ (M))
all_clauses_literals =
filter (half_unset_literals_in_ΔΣ M')
all_clauses_literals›
‹filter (unset_literals_in_Σ (M)) all_clauses_literals =
filter (unset_literals_in_Σ M') all_clauses_literals›
using assms unfolding full_unset_literals_in_ΔΣ'_def full_unset_literals_in_ΔΣ_def
half_unset_literals_in_ΔΣ_def unset_literals_in_Σ_def
by (auto simp: sorted_unadded_literals_def undefined_notin all_clauses_literals(1,2)
defined_lit_Neg_Pos_iff all_clauses_literals(3) defined_lit_cons
intro!: ext filter_cong)
show ?thesis
by (auto simp: undefined_notin all_clauses_literals(1,2)
defined_lit_Neg_Pos_iff all_clauses_literals(3) sorted_unadded_literals_def)
qed
lemma sorted_unadded_literals_Cons_already_set[simp]:
assumes
‹defined_lit M (lit_of K)›
shows
‹sorted_unadded_literals (K # M) = sorted_unadded_literals M›
by (rule sorted_unadded_literals_cong)
(use assms in ‹auto simp: defined_lit_cons›)
lemma distinct_sorted_unadded_literals[simp]:
‹distinct (sorted_unadded_literals M)›
unfolding half_unset_literals_in_ΔΣ_def
full_unset_literals_in_ΔΣ_def unset_literals_in_Σ_def
sorted_unadded_literals_def
full_unset_literals_in_ΔΣ'_def
by (auto simp: sorted_unadded_literals_def all_clauses_literals(1,2))
lemma Collect_req_remove1:
‹{a ∈ A. a ≠ b ∧ P a} = (if P b then Set.remove b {a ∈ A. P a} else {a ∈ A. P a})› and
Collect_req_remove2:
‹{a ∈ A. b ≠ a ∧ P a} = (if P b then Set.remove b {a ∈ A. P a} else {a ∈ A. P a})›
by auto
lemma card_remove:
‹card (Set.remove a A) = (if a ∈ A then card A - 1 else card A)›
apply (auto simp: Set.remove_def)
by (metis Diff_empty One_nat_def card_Diff_insert card_infinite empty_iff
finite_Diff_insert gr_implies_not0 neq0_conv zero_less_diff)
lemma sorted_unadded_literals_cons_in_undef[simp]:
‹undefined_lit M (lit_of K) ⟹
atm_of (lit_of K) ∈ set all_clauses_literals ⟹
Suc (length (sorted_unadded_literals (K # M))) =
length (sorted_unadded_literals M)›
by (auto simp flip: distinct_card simp: Set.filter_def Collect_req_remove2
card_remove isabelle_should_do_that_automatically
card_gt_0_iff simp flip: less_eq_Suc_le)
lemma no_dup_complete_trail[simp]:
‹no_dup (complete_trail M) ⟷ no_dup M›
by (auto simp: complete_trail_def no_dup_def comp_def all_clauses_literals(1,2)
undefined_notin)
lemma tautology_complete_trail[simp]:
‹tautology (lit_of `# mset (complete_trail M)) ⟷ tautology (lit_of `# mset M)›
by (auto simp: complete_trail_def tautology_decomp' comp_def all_clauses_literals
undefined_notin uminus_lit_swap defined_lit_Neg_Pos_iff
simp flip: defined_lit_Neg_Pos_iff)
lemma atms_of_complete_trail:
‹atms_of (lit_of `# mset (complete_trail M)) =
atms_of (lit_of `# mset M) ∪ (Σ - ΔΣ) ∪ replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ›
by (auto simp add: complete_trail_def all_clauses_literals
image_image image_Un atms_of_def defined_lit_map)
fun depth_lit_of :: ‹('v,_) ann_lit ⇒ ('v, _) ann_lit search_depth› where
‹depth_lit_of (Decided L) = SD_TWO (Decided L)› |
‹depth_lit_of (Propagated L C) = SD_ZERO (Propagated L C)›
fun depth_lit_of_additional_fst :: ‹('v,_) ann_lit ⇒ ('v, _) ann_lit search_depth› where
‹depth_lit_of_additional_fst (Decided L) = SD_ONE (Decided L)› |
‹depth_lit_of_additional_fst (Propagated L C) = SD_ZERO (Propagated L C)›
fun depth_lit_of_additional_snd :: ‹('v,_) ann_lit ⇒ ('v, _) ann_lit search_depth list› where
‹depth_lit_of_additional_snd (Decided L) = [SD_ONE (Decided L)]› |
‹depth_lit_of_additional_snd (Propagated L C) = []›
text ‹
This function is suprisingly complicated to get right. Remember that the last set element
is at the beginning of the list
›
fun remove_dup_information_raw :: ‹('v, _) ann_lits ⇒ ('v, _) ann_lit search_depth list› where
‹remove_dup_information_raw [] = []› |
‹remove_dup_information_raw (L # M) =
(if atm_of (lit_of L) ∈ Σ - ΔΣ then depth_lit_of L # remove_dup_information_raw M
else if defined_lit (M) (Pos (opposite_var (atm_of (lit_of L))))
then if Decided (Pos (opposite_var (atm_of (lit_of L)))) ∈ set (M)
then remove_dup_information_raw M
else depth_lit_of_additional_fst L # remove_dup_information_raw M
else depth_lit_of_additional_snd L @ remove_dup_information_raw M)›
definition remove_dup_information where
‹remove_dup_information xs = un_hide_sd (remove_dup_information_raw xs)›
lemma [simp]: ‹the_search_depth (depth_lit_of L) = L›
by (cases L) auto
lemma length_complete_trail[simp]: ‹length (complete_trail []) = length all_clauses_literals›
unfolding complete_trail_def
by (auto simp: sum_length_filter_compl)
lemma distinct_count_list_if: ‹distinct xs ⟹ count_list xs x = (if x ∈ set xs then 1 else 0)›
by (induction xs) auto
lemma length_complete_trail_Cons:
‹no_dup (K # M) ⟹
length (complete_trail (K # M)) =
(if atm_of (lit_of K) ∈ set all_clauses_literals then 0 else 1) + length (complete_trail M)›
unfolding complete_trail_def by auto
lemma length_complete_trail_eq:
‹no_dup M ⟹ atm_of ` (lits_of_l M) ⊆ set all_clauses_literals ⟹
length (complete_trail M) = length all_clauses_literals›
by (induction M rule: ann_lit_list_induct) (auto simp: length_complete_trail_Cons)
lemma in_set_all_clauses_literals_simp[simp]:
‹atm_of L ∈ Σ - ΔΣ ⟹ atm_of L ∈ set all_clauses_literals›
‹K ∈ ΔΣ ⟹ replacement_pos K ∈ set all_clauses_literals›
‹K ∈ ΔΣ ⟹ replacement_neg K ∈ set all_clauses_literals›
by (auto simp: all_clauses_literals)
lemma [simp]:
‹remove_dup_information [] = []›
by (auto simp: remove_dup_information_def)
lemma atm_of_remove_dup_information:
‹atm_of ` (lits_of_l M) ⊆ set all_clauses_literals ⟹
atm_of ` (lits_of_l (remove_dup_information M)) ⊆ set all_clauses_literals›
unfolding remove_dup_information_def
apply (induction M rule: ann_lit_list_induct)
apply (auto simp: Decided_Propagated_in_iff_in_lits_of_l lits_of_def image_image)
done
primrec remove_dup_information_raw2 :: ‹('v, _) ann_lits ⇒ ('v, _) ann_lits ⇒
('v, _) ann_lit search_depth list› where
‹remove_dup_information_raw2 M' [] = []› |
‹remove_dup_information_raw2 M' (L # M) =
(if atm_of (lit_of L) ∈ Σ - ΔΣ then depth_lit_of L # remove_dup_information_raw2 M' M
else if defined_lit (M @ M') (Pos (opposite_var (atm_of (lit_of L))))
then if Decided (Pos (opposite_var (atm_of (lit_of L)))) ∈ set (M @ M')
then remove_dup_information_raw2 M' M
else depth_lit_of_additional_fst L # remove_dup_information_raw2 M' M
else depth_lit_of_additional_snd L @ remove_dup_information_raw2 M' M)›
lemma remove_dup_information_raw2_Nil[simp]:
‹remove_dup_information_raw2 [] M = remove_dup_information_raw M›
by (induction M) auto
text ‹This can be useful as simp, but I am not certain (yet), because the RHS does not look simpler
than the LHS.›
lemma remove_dup_information_raw_cons:
‹remove_dup_information_raw (L # M2) =
remove_dup_information_raw2 M2 [L] @
remove_dup_information_raw M2›
by (auto simp: defined_lit_append)
lemma remove_dup_information_raw_append:
‹remove_dup_information_raw (M1 @ M2) =
remove_dup_information_raw2 M2 M1 @
remove_dup_information_raw M2›
by (induction M1)
(auto simp: defined_lit_append)
lemma remove_dup_information_raw_append2:
‹remove_dup_information_raw2 M (M1 @ M2) =
remove_dup_information_raw2 (M @ M2) M1 @
remove_dup_information_raw2 M M2›
by (induction M1)
(auto simp: defined_lit_append)
lemma remove_dup_information_subset: ‹mset (remove_dup_information M) ⊆# mset M›
unfolding remove_dup_information_def
apply (induction M rule: ann_lit_list_induct) apply auto
apply (metis add_mset_remove_trivial diff_subset_eq_self subset_mset.dual_order.trans)+
done
lemma no_dup_subsetD: ‹no_dup M ⟹ mset M' ⊆# mset M ⟹ no_dup M'›
unfolding no_dup_def distinct_mset_mset_distinct[symmetric] mset_map
apply (drule image_mset_subseteq_mono[of _ _ ‹atm_of o lit_of›])
apply (drule distinct_mset_mono)
apply auto
done
lemma no_dup_remove_dup_information:
‹no_dup M ⟹ no_dup (remove_dup_information M)›
using no_dup_subsetD[OF _ remove_dup_information_subset] by blast
lemma atm_of_complete_trail:
‹atm_of ` (lits_of_l M) ⊆ set all_clauses_literals ⟹
atm_of ` (lits_of_l (complete_trail M)) = set all_clauses_literals›
unfolding complete_trail_def by (auto simp: lits_of_def image_image image_Un defined_lit_map)
lemmas [simp del] =
remove_dup_information_raw.simps
remove_dup_information_raw2.simps
lemmas [simp] =
remove_dup_information_raw_append
remove_dup_information_raw_cons
remove_dup_information_raw_append2
definition truncate_trail :: ‹('v, _) ann_lits ⇒ _› where
‹truncate_trail M ≡
(snd (backtrack_split M))›
definition ocdcl_score :: ‹('v, _) ann_lits ⇒ _› where
‹ocdcl_score M =
rev (map nat_of_search_deph (remove_dup_information_raw (complete_trail (truncate_trail M))))›
interpretation enc_weight_opt: conflict_driven_clause_learning⇩W_optimal_weight where
state_eq = state_eq and
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state and
ρ = ρ⇩e and
update_additional_info = update_additional_info
apply unfold_locales
subgoal by (rule ρ⇩e_mono)
subgoal using update_additional_info by fast
subgoal using weight_init_state by fast
done
lemma
‹(a, b) ∈ lexn less_than n ⟹ (b, c) ∈ lexn less_than n ∨ b = c ⟹ (a, c) ∈ lexn less_than n›
‹(a, b) ∈ lexn less_than n ⟹ (b, c) ∈ lexn less_than n ∨ b = c ⟹ (a, c) ∈ lexn less_than n›
apply (auto intro: )
apply (meson lexn_transI trans_def trans_less_than)+
done
lemma truncate_trail_Prop[simp]:
‹truncate_trail (Propagated L E # S) = truncate_trail (S)›
by (auto simp: truncate_trail_def)
lemma ocdcl_score_Prop[simp]:
‹ocdcl_score (Propagated L E # S) = ocdcl_score (S)›
by (auto simp: ocdcl_score_def truncate_trail_def)
lemma remove_dup_information_raw2_undefined_Σ:
‹distinct xs ⟹
(⋀L. L ∈ set xs ⟹ undefined_lit M (Pos L) ⟹ L ∈ Σ ⟹ undefined_lit MM (Pos L)) ⟹
remove_dup_information_raw2 MM
(map (Decided ∘ Pos)
(filter (unset_literals_in_Σ M)
xs)) =
map (SD_TWO o Decided ∘ Pos)
(filter (unset_literals_in_Σ M)
xs)›
by (induction xs)
(auto simp: remove_dup_information_raw2.simps
unset_literals_in_Σ_def)
lemma defined_lit_map_Decided_pos:
‹defined_lit (map (Decided ∘ Pos) M) L ⟷ atm_of L ∈ set M›
by (induction M) (auto simp: defined_lit_cons)
lemma remove_dup_information_raw2_full_undefined_Σ:
‹distinct xs ⟹ set xs ⊆ set all_clauses_literals ⟹
(⋀L. L ∈ set xs ⟹ undefined_lit M (Pos L) ⟹ L ∉ Σ - ΔΣ ⟹
undefined_lit M (Pos (opposite_var L)) ⟹ L ∈ replacement_pos ` ΔΣ ⟹
undefined_lit MM (Pos (opposite_var L))) ⟹
remove_dup_information_raw2 MM
(map (Decided ∘ Pos)
(filter (full_unset_literals_in_ΔΣ M)
xs)) =
map (SD_ONE o Decided ∘ Pos)
(filter (full_unset_literals_in_ΔΣ M)
xs)›
unfolding all_clauses_literals
apply (induction xs)
subgoal
by (simp_all add: remove_dup_information_raw2.simps)
subgoal premises p for L xs
using p(1-3) p(4)[of L] p(4)
by (clarsimp simp add: remove_dup_information_raw2.simps
defined_lit_map_Decided_pos
full_unset_literals_in_ΔΣ_def defined_lit_append)
done
lemma full_unset_literals_in_ΔΣ_notin[simp]:
‹La ∈ Σ ⟹ full_unset_literals_in_ΔΣ M La ⟷ False›
‹La ∈ Σ ⟹ full_unset_literals_in_ΔΣ' M La ⟷ False›
apply (metis (mono_tags) full_unset_literals_in_ΔΣ_def
image_iff new_vars_pos)
by (simp add: full_unset_literals_in_ΔΣ'_def image_iff)
lemma Decided_in_definedD: ‹Decided K ∈ set M ⟹ defined_lit M K›
by (simp add: defined_lit_def)
lemma full_unset_literals_in_ΔΣ'_full_unset_literals_in_ΔΣ:
‹L ∈ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⟹
full_unset_literals_in_ΔΣ' M (opposite_var L) ⟷ full_unset_literals_in_ΔΣ M L›
by (auto simp: full_unset_literals_in_ΔΣ'_def full_unset_literals_in_ΔΣ_def
opposite_var_def)
lemma remove_dup_information_raw2_full_unset_literals_in_ΔΣ':
‹(⋀L. L ∈ set (filter (full_unset_literals_in_ΔΣ' M) xs) ⟹ Decided (Pos (opposite_var L)) ∈ set M') ⟹
set xs ⊆ set all_clauses_literals ⟹
(remove_dup_information_raw2
M'
(map (Decided ∘ Pos)
(filter (full_unset_literals_in_ΔΣ' (M))
xs))) = []›
supply [[goals_limit=1]]
apply (induction xs)
subgoal by (auto simp: remove_dup_information_raw2.simps)
subgoal premises p for L xs
using p
by (force simp add: remove_dup_information_raw2.simps
full_unset_literals_in_ΔΣ'_full_unset_literals_in_ΔΣ
all_clauses_literals
defined_lit_map_Decided_pos defined_lit_append image_iff
dest: Decided_in_definedD)
done
lemma
fixes M :: ‹('v, _) ann_lits› and L :: ‹('v, _) ann_lit›
defines ‹n1 ≡ map nat_of_search_deph (remove_dup_information_raw (complete_trail (L # M)))› and
‹n2 ≡ map nat_of_search_deph (remove_dup_information_raw (complete_trail M))›
assumes
lits: ‹atm_of ` (lits_of_l (L # M)) ⊆ set all_clauses_literals› and
undef: ‹undefined_lit M (lit_of L)›
shows
‹(rev n1, rev n2) ∈ lexn less_than n ∨ n1 = n2›
proof -
show ?thesis
using lits
apply (auto simp: n1_def n2_def complete_trail_def prepend_same_lexn)
apply (auto simp: sorted_unadded_literals_def
remove_dup_information_raw2.simps all_clauses_literals(2) defined_lit_map_Decided_pos
remove_dup_information_raw2_undefined_Σ)
subgoal
apply (subst remove_dup_information_raw2_undefined_Σ)
apply (simp_all add: all_clauses_literals(2) defined_lit_map_Decided_pos
remove_dup_information_raw2_undefined_Σ)
apply (subst remove_dup_information_raw2_full_undefined_Σ)
apply (auto simp: all_clauses_literals(2))
apply (subst remove_dup_information_raw2_full_unset_literals_in_ΔΣ')
apply (auto simp: full_unset_literals_in_ΔΣ'_full_unset_literals_in_ΔΣ)[2]
oops
lemma
defines ‹n ≡ card Σ›
assumes
‹init_clss S = penc N› and
‹enc_weight_opt.cdcl_bnb_stgy S T› and
struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)› and
smaller_propa: ‹no_smaller_propa S› and
smaller_confl: ‹cdcl_bnb_stgy_inv S›
shows ‹(ocdcl_score (trail T), ocdcl_score (trail S)) ∈ lexn less_than n ∨
ocdcl_score (trail T) = ocdcl_score (trail S)›
using assms(3)
proof (cases)
case cdcl_bnb_conflict
then show ?thesis by (auto elim!: rulesE)
next
case cdcl_bnb_propagate
then show ?thesis
by (auto elim!: rulesE)
next
case cdcl_bnb_improve
then show ?thesis
by (auto elim!: enc_weight_opt.improveE)
next
case cdcl_bnb_conflict_opt
then show ?thesis
by (auto elim!: enc_weight_opt.conflict_optE)
next
case cdcl_bnb_other'
then show ?thesis
proof cases
case bj
then show ?thesis
proof cases
case skip
then show ?thesis by (auto elim!: rulesE)
next
case resolve
then show ?thesis by (cases ‹trail S›) (auto elim!: rulesE)
next
case backtrack
then obtain M1 M2 :: ‹('v, 'v clause) ann_lits› and K L :: ‹'v literal› and
D D' :: ‹'v clause› where
confl: ‹conflicting S = Some (add_mset L D)› and
decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and
‹get_maximum_level (trail S) (add_mset L D') = local.backtrack_lvl S› and
‹get_level (trail S) L = local.backtrack_lvl S› and
lev_K: ‹get_level (trail S) K = Suc (get_maximum_level (trail S) D')› and
D'_D: ‹D' ⊆# D› and
‹set_mset (clauses S) ∪ set_mset (enc_weight_opt.conflicting_clss S) ⊨p
add_mset L D'› 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)))›
by (auto simp: enc_weight_opt.obacktrack.simps)
have
tr_D: ‹trail S ⊨as CNot (add_mset L D)› and
‹distinct_mset (add_mset L D)› and
‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)› and
n_d: ‹no_dup (trail S)›
using struct confl
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
have tr_D': ‹trail S ⊨as CNot (add_mset L D')›
using D'_D tr_D
by (auto simp: true_annots_true_cls_def_iff_negation_in_model)
have ‹trail S ⊨as CNot D' ⟹ trail S ⊨as CNot (normalize2 D')›
if ‹get_maximum_level (trail S) D' < backtrack_lvl S›
for D'
oops
end
interpretation enc_weight_opt: conflict_driven_clause_learning⇩W_optimal_weight where
state_eq = state_eq and
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state and
ρ = ρ⇩e and
update_additional_info = update_additional_info
apply unfold_locales
subgoal by (rule ρ⇩e_mono)
subgoal using update_additional_info by fast
subgoal using weight_init_state by fast
done
inductive simple_backtrack_conflict_opt :: ‹'st ⇒ 'st ⇒ bool› where
‹simple_backtrack_conflict_opt S T›
if
‹backtrack_split (trail S) = (M2, Decided K # M1)› and
‹negate_ann_lits (trail S) ∈# enc_weight_opt.conflicting_clss S› and
‹conflicting S = None› and
‹T ∼ cons_trail (Propagated (-K) (DECO_clause (trail S)))
(add_learned_cls (DECO_clause (trail S)) (reduce_trail_to M1 S))›
inductive_cases simple_backtrack_conflict_optE: ‹simple_backtrack_conflict_opt S T›
lemma simple_backtrack_conflict_opt_conflict_analysis:
assumes ‹simple_backtrack_conflict_opt S U› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)›
shows ‹∃T T'. enc_weight_opt.conflict_opt S T ∧ resolve⇧*⇧* T T'
∧ enc_weight_opt.obacktrack T' U›
using assms
proof (cases rule: simple_backtrack_conflict_opt.cases)
case (1 M2 K M1)
have tr: ‹trail S = M2 @ Decided K # M1›
using 1 backtrack_split_list_eq[of ‹trail S›]
by auto
let ?S = ‹update_conflicting (Some (negate_ann_lits (trail S))) S›
have ‹enc_weight_opt.conflict_opt S ?S›
by (rule enc_weight_opt.conflict_opt.intros[OF 1(2,3)]) auto
let ?T = ‹λn. update_conflicting
(Some (negate_ann_lits (drop n (trail S))))
(reduce_trail_to (drop n (trail S)) S)›
have proped_M2: ‹is_proped (M2 ! n)› if ‹n < length M2› for n
using that 1(1) nth_length_takeWhile[of ‹Not ∘ is_decided› ‹trail S›]
length_takeWhile_le[of ‹Not ∘ is_decided› ‹trail S›]
unfolding backtrack_split_takeWhile_dropWhile
apply auto
by (metis annotated_lit.exhaust_disc comp_apply nth_mem set_takeWhileD)
have is_dec_M2[simp]: ‹filter_mset is_decided (mset M2) = {#}›
using 1(1) nth_length_takeWhile[of ‹Not ∘ is_decided› ‹trail S›]
length_takeWhile_le[of ‹Not ∘ is_decided› ‹trail S›]
unfolding backtrack_split_takeWhile_dropWhile
apply (auto simp: filter_mset_empty_conv)
by (metis annotated_lit.exhaust_disc comp_apply nth_mem set_takeWhileD)
have n_d: ‹no_dup (trail S)› and
le: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (enc_weight_opt.abs_state S)› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (enc_weight_opt.abs_state S)› and
decomp_imp: ‹all_decomposition_implies_m (clauses S + (enc_weight_opt.conflicting_clss S))
(get_all_ann_decomposition (trail S))› and
learned: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (enc_weight_opt.abs_state S)›
using inv
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
then have [simp]: ‹K ≠ lit_of (M2 ! n)› if ‹n < length M2› for n
using that unfolding tr
by (auto simp: defined_lit_nth)
have n_d_n: ‹no_dup (drop n M2 @ Decided K # M1)› for n
using n_d unfolding tr
by (subst (asm) append_take_drop_id[symmetric, of _ n])
(auto simp del: append_take_drop_id dest: no_dup_appendD)
have mark_dist: ‹distinct_mset (mark_of (M2!n))› if ‹n < length M2› for n
using dist that proped_M2[OF that] nth_mem[OF that]
unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def tr
by (cases ‹M2!n›) (auto simp: tr)
have [simp]: ‹undefined_lit (drop n M2) K› for n
using n_d defined_lit_mono[of ‹drop n M2› K M2]
unfolding tr
by (auto simp: set_drop_subset)
from this[of 0] have [simp]: ‹undefined_lit M2 K›
by auto
have [simp]: ‹count_decided (drop n M2) = 0› for n
apply (subst count_decided_0_iff)
using 1(1) nth_length_takeWhile[of ‹Not ∘ is_decided› ‹trail S›]
length_takeWhile_le[of ‹Not ∘ is_decided› ‹trail S›]
unfolding backtrack_split_takeWhile_dropWhile
by (auto simp: dest!: in_set_dropD set_takeWhileD)
from this[of 0] have [simp]: ‹count_decided M2 = 0› by simp
have proped: ‹⋀L mark a b.
a @ Propagated L mark # b = trail S ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark›
using le
unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by auto
have mark: ‹drop (Suc n) M2 @ Decided K # M1 ⊨as
CNot (mark_of (M2 ! n) - unmark (M2 ! n)) ∧
lit_of (M2 ! n) ∈# mark_of (M2 ! n)›
if ‹n < length M2› for n
using proped_M2[OF that] that
append_take_drop_id[of n M2, unfolded Cons_nth_drop_Suc[OF that, symmetric]]
proped[of ‹take n M2› ‹lit_of (M2 ! n)› ‹mark_of (M2 ! n)›
‹drop (Suc n) M2 @ Decided K # M1›]
unfolding tr by (cases ‹M2!n›) auto
have confl: ‹enc_weight_opt.conflict_opt S ?S›
by (rule enc_weight_opt.conflict_opt.intros) (use 1 in auto)
have res: ‹resolve⇧*⇧* ?S (?T n)› if ‹n ≤ length M2› for n
using that unfolding tr
proof (induction n)
case 0
then show ?case
using get_all_ann_decomposition_backtrack_split[THEN iffD1, OF 1(1)]
1
by (cases ‹get_all_ann_decomposition (trail S)›) (auto simp: tr)
next
case (Suc n)
have [simp]: ‹¬ Suc (length M2 - Suc n) < length M2 ⟷ n = 0›
using Suc(2) by auto
have [simp]: ‹reduce_trail_to (drop (Suc 0) M2 @ Decided K # M1) S = tl_trail S›
apply (subst reduce_trail_to.simps)
using Suc by (auto simp: tr )
have [simp]: ‹reduce_trail_to (M2 ! 0 # drop (Suc 0) M2 @ Decided K # M1) S = S›
apply (subst reduce_trail_to.simps)
using Suc by (auto simp: tr )
have [simp]: ‹(Suc (length M1) -
(length M2 - n + (Suc (length M1) - (n - length M2)))) = 0›
‹(Suc (length M2 + length M1) -
(length M2 - n + (Suc (length M1) - (n - length M2)))) =n›
‹length M2 - n + (Suc (length M1) - (n - length M2)) = Suc (length M2 + length M1) - n›
using Suc by auto
have [symmetric,simp]: ‹M2 ! n = Propagated (lit_of (M2 ! n)) (mark_of (M2 ! n))›
using Suc proped_M2[of n]
by (cases ‹M2 ! n›) (auto simp: tr trail_reduce_trail_to_drop hd_drop_conv_nth
intro!: resolve.intros)
have ‹- lit_of (M2 ! n) ∈# negate_ann_lits (drop n M2 @ Decided K # M1)›
using Suc in_set_dropI[of ‹n› ‹map (uminus o lit_of) M2› n]
by (simp add: negate_ann_lits_def comp_def drop_map
del: nth_mem)
moreover have ‹get_maximum_level (drop n M2 @ Decided K # M1)
(remove1_mset (- lit_of (M2 ! n)) (negate_ann_lits (drop n M2 @ Decided K # M1))) =
Suc (count_decided M1)›
using Suc(2) count_decided_ge_get_maximum_level[of ‹drop n M2 @ Decided K # M1›
‹(remove1_mset (- lit_of (M2 ! n)) (negate_ann_lits (drop n M2 @ Decided K # M1)))›]
by (auto simp: negate_ann_lits_def tr max_def ac_simps
remove1_mset_add_mset_If get_maximum_level_add_mset
split: if_splits)
moreover have ‹lit_of (M2 ! n) ∈# mark_of (M2 ! n)›
using mark[of n] Suc by auto
moreover have ‹(remove1_mset (- lit_of (M2 ! n))
(negate_ann_lits (drop n M2 @ Decided K # M1)) ∪#
(mark_of (M2 ! n) - unmark (M2 ! n))) = negate_ann_lits (drop (Suc n) (trail S))›
apply (rule distinct_set_mset_eq)
using n_d_n[of n] n_d_n[of ‹Suc n›] no_dup_distinct_mset[OF n_d_n[of n]] Suc
mark[of n] mark_dist[of n]
by (auto simp: tr Cons_nth_drop_Suc[symmetric, of n]
entails_CNot_negate_ann_lits
dest: in_diffD intro: distinct_mset_minus)
moreover { have 1: ‹(tl_trail
(reduce_trail_to (drop n M2 @ Decided K # M1) S)) ∼
(reduce_trail_to (drop (Suc n) M2 @ Decided K # M1) S)›
apply (subst Cons_nth_drop_Suc[symmetric, of n M2])
subgoal using Suc by (auto simp: tl_trail_update_conflicting)
subgoal
apply (rule state_eq_trans)
apply simp
apply (cases ‹length (M2 ! n # drop (Suc n) M2 @ Decided K # M1) < length (trail S)›)
apply (auto simp: tl_trail_reduce_trail_to_cons tr)
done
done
have ‹update_conflicting
(Some (negate_ann_lits (drop (Suc n) M2 @ Decided K # M1)))
(reduce_trail_to (drop (Suc n) M2 @ Decided K # M1) S) ∼
update_conflicting
(Some (negate_ann_lits (drop (Suc n) M2 @ Decided K # M1)))
(tl_trail
(update_conflicting (Some (negate_ann_lits (drop n M2 @ Decided K # M1)))
(reduce_trail_to (drop n M2 @ Decided K # M1) S)))›
apply (rule state_eq_trans)
prefer 2
apply (rule update_conflicting_state_eq)
apply (rule tl_trail_update_conflicting[THEN state_eq_sym[THEN iffD1]])
apply (subst state_eq_sym)
apply (subst update_conflicting_update_conflicting)
apply (rule 1)
by fast }
ultimately have ‹resolve (?T n) (?T (n+1))› apply -
apply (rule resolve.intros[of _ ‹lit_of (M2 ! n)› ‹mark_of (M2 ! n)›])
using Suc
get_all_ann_decomposition_backtrack_split[THEN iffD1, OF 1(1)]
in_get_all_ann_decomposition_trail_update_trail[of ‹Decided K› M1 ‹M2› ‹S›]
by (auto simp: tr trail_reduce_trail_to_drop hd_drop_conv_nth
intro!: resolve.intros intro: update_conflicting_state_eq)
then show ?case
using Suc by (auto simp add: tr)
qed
have ‹get_maximum_level (Decided K # M1) (DECO_clause M1) = get_maximum_level M1 (DECO_clause M1)›
by (rule get_maximum_level_cong)
(use n_d in ‹auto simp: tr get_level_cons_if atm_of_eq_atm_of
DECO_clause_def Decided_Propagated_in_iff_in_lits_of_l lits_of_def›)
also have ‹... = count_decided M1›
using n_d unfolding tr apply -
apply (induction M1 rule: ann_lit_list_induct)
subgoal by auto
subgoal for L M1'
apply (subgoal_tac ‹∀La∈#DECO_clause M1'. get_level (Decided L # M1') La = get_level M1' La›)
subgoal
using count_decided_ge_get_maximum_level[of ‹M1'› ‹DECO_clause M1'›]
get_maximum_level_cong[of ‹DECO_clause M1'› ‹Decided L # M1'› ‹M1'›]
by (auto simp: get_maximum_level_add_mset tr atm_of_eq_atm_of
max_def)
subgoal
by (auto simp: DECO_clause_def
get_level_cons_if atm_of_eq_atm_of Decided_Propagated_in_iff_in_lits_of_l
lits_of_def)
done
subgoal for L C M1'
apply (subgoal_tac ‹∀La∈#DECO_clause M1'. get_level (Propagated L C # M1') La = get_level M1' La›)
subgoal
using count_decided_ge_get_maximum_level[of ‹M1'› ‹DECO_clause M1'›]
get_maximum_level_cong[of ‹DECO_clause M1'› ‹Propagated L C # M1'› ‹M1'›]
by (auto simp: get_maximum_level_add_mset tr atm_of_eq_atm_of
max_def)
subgoal
by (auto simp: DECO_clause_def
get_level_cons_if atm_of_eq_atm_of Decided_Propagated_in_iff_in_lits_of_l
lits_of_def)
done
done
finally have max: ‹get_maximum_level (Decided K # M1) (DECO_clause M1) = count_decided M1› .
have ‹trail S ⊨as CNot (negate_ann_lits (trail S))›
by (auto simp: true_annots_true_cls_def_iff_negation_in_model
negate_ann_lits_def lits_of_def)
then have ‹clauses S + (enc_weight_opt.conflicting_clss S) ⊨pm DECO_clause (trail S)›
unfolding DECO_clause_def apply -
apply (rule all_decomposition_implies_conflict_DECO_clause[OF decomp_imp,
of ‹negate_ann_lits (trail S)›])
using 1
by auto
have neg: ‹trail S ⊨as CNot (mset (map (uminus o lit_of) (trail S)))›
by (auto simp: true_annots_true_cls_def_iff_negation_in_model
lits_of_def)
have ent: ‹clauses S + enc_weight_opt.conflicting_clss S ⊨pm DECO_clause (trail S)›
unfolding DECO_clause_def
by (rule all_decomposition_implies_conflict_DECO_clause[OF decomp_imp,
of ‹mset (map (uminus o lit_of) (trail S))›])
(use neg 1 in ‹auto simp: negate_ann_lits_def›)
have deco: ‹DECO_clause (M2 @ Decided K # M1) = add_mset (- K) (DECO_clause M1)›
by (auto simp: DECO_clause_def)
have eg: ‹reduce_trail_to M1 (reduce_trail_to (Decided K # M1) S) ∼
reduce_trail_to M1 S›
apply (subst reduce_trail_to_compow_tl_trail_le)
apply (solves ‹auto simp: tr›)
apply (subst (3)reduce_trail_to_compow_tl_trail_le)
apply (solves ‹auto simp: tr›)
apply (auto simp: tr)
apply (cases ‹M2 = []›)
apply (auto simp: reduce_trail_to_compow_tl_trail_le reduce_trail_to_compow_tl_trail_eq tr)
done
have U: ‹cons_trail (Propagated (- K) (DECO_clause (M2 @ Decided K # M1)))
(add_learned_cls (DECO_clause (M2 @ Decided K # M1))
(reduce_trail_to M1 S)) ∼
cons_trail (Propagated (- K) (add_mset (- K) (DECO_clause M1)))
(reduce_trail_to M1
(add_learned_cls (add_mset (- K) (DECO_clause M1))
(update_conflicting None
(update_conflicting (Some (add_mset (- K) (negate_ann_lits M1)))
(reduce_trail_to (Decided K # M1) S)))))›
unfolding deco
apply (rule cons_trail_state_eq)
apply (rule state_eq_trans)
prefer 2
apply (rule state_eq_sym[THEN iffD1])
apply (rule reduce_trail_to_add_learned_cls_state_eq)
apply (solves ‹auto simp: tr›)
apply (rule add_learned_cls_state_eq)
apply (rule state_eq_trans)
prefer 2
apply (rule state_eq_sym[THEN iffD1])
apply (rule reduce_trail_to_update_conflicting_state_eq)
apply (solves ‹auto simp: tr›)
apply (rule state_eq_trans)
prefer 2
apply (rule state_eq_sym[THEN iffD1])
apply (rule update_conflicting_state_eq)
apply (rule reduce_trail_to_update_conflicting_state_eq)
apply (solves ‹auto simp: tr›)
apply (rule state_eq_trans)
prefer 2
apply (rule state_eq_sym[THEN iffD1])
apply (rule update_conflicting_update_conflicting)
apply (rule eg)
apply (rule state_eq_trans)
prefer 2
apply (rule state_eq_sym[THEN iffD1])
apply (rule update_conflicting_itself)
by (use 1 in auto)
have bt: ‹enc_weight_opt.obacktrack (?T (length M2)) U›
apply (rule enc_weight_opt.obacktrack.intros[of _ ‹-K› ‹negate_ann_lits M1› K M1 ‹[]›
‹DECO_clause M1› ‹count_decided M1›])
subgoal by (auto simp: tr)
subgoal by (auto simp: tr)
subgoal by (auto simp: tr)
subgoal
using count_decided_ge_get_maximum_level[of ‹Decided K # M1› ‹DECO_clause M1›]
by (auto simp: tr get_maximum_level_add_mset max_def)
subgoal using max by (auto simp: tr)
subgoal by (auto simp: tr)
subgoal by (auto simp: DECO_clause_def negate_ann_lits_def
image_mset_subseteq_mono)
subgoal using ent by (auto simp: tr DECO_clause_def)
subgoal
apply (rule state_eq_trans [OF 1(4)])
using 1(4) U by (auto simp: tr)
done
show ?thesis
using confl res[of ‹length M2›, simplified] bt
by blast
qed
inductive conflict_opt0 :: ‹'st ⇒ 'st ⇒ bool› where
‹conflict_opt0 S T›
if
‹count_decided (trail S) = 0› and
‹negate_ann_lits (trail S) ∈# enc_weight_opt.conflicting_clss S› and
‹conflicting S = None› and
‹T ∼ update_conflicting (Some {#}) (reduce_trail_to ([] :: ('v, 'v clause) ann_lits) S)›
inductive_cases conflict_opt0E: ‹conflict_opt0 S T›
inductive cdcl_dpll_bnb_r :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
cdcl_conflict: "conflict S S' ⟹ cdcl_dpll_bnb_r S S'" |
cdcl_propagate: "propagate S S' ⟹ cdcl_dpll_bnb_r S S'" |
cdcl_improve: "enc_weight_opt.improvep S S' ⟹ cdcl_dpll_bnb_r S S'" |
cdcl_conflict_opt0: "conflict_opt0 S S' ⟹ cdcl_dpll_bnb_r S S'" |
cdcl_simple_backtrack_conflict_opt:
‹simple_backtrack_conflict_opt S S' ⟹ cdcl_dpll_bnb_r S S'› |
cdcl_o': "ocdcl⇩W_o_r S S' ⟹ cdcl_dpll_bnb_r S S'"
inductive cdcl_dpll_bnb_r_stgy :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
cdcl_dpll_bnb_r_conflict: "conflict S S' ⟹ cdcl_dpll_bnb_r_stgy S S'" |
cdcl_dpll_bnb_r_propagate: "propagate S S' ⟹ cdcl_dpll_bnb_r_stgy S S'" |
cdcl_dpll_bnb_r_improve: "enc_weight_opt.improvep S S' ⟹ cdcl_dpll_bnb_r_stgy S S'" |
cdcl_dpll_bnb_r_conflict_opt0: "conflict_opt0 S S' ⟹ cdcl_dpll_bnb_r_stgy S S'" |
cdcl_dpll_bnb_r_simple_backtrack_conflict_opt:
‹simple_backtrack_conflict_opt S S' ⟹ cdcl_dpll_bnb_r_stgy S S'› |
cdcl_dpll_bnb_r_other': "ocdcl⇩W_o_r S S' ⟹ no_confl_prop_impr S ⟹ cdcl_dpll_bnb_r_stgy S S'"
lemma no_dup_dropI:
‹no_dup M ⟹ no_dup (drop n M)›
by (cases ‹n < length M›) (auto simp: no_dup_def drop_map[symmetric])
lemma tranclp_resolve_state_eq_compatible:
‹resolve⇧+⇧+ S T ⟹T ∼ T' ⟹ resolve⇧+⇧+ S T'›
apply (induction arbitrary: T' rule: tranclp_induct)
apply (auto dest: resolve_state_eq_compatible)
by (metis resolve_state_eq_compatible state_eq_ref tranclp_into_rtranclp tranclp_unfold_end)
lemma conflict_opt0_state_eq_compatible:
‹conflict_opt0 S T ⟹ S ∼ S' ⟹ T ∼ T' ⟹ conflict_opt0 S' T'›
using state_eq_trans[of T' T
‹update_conflicting (Some {#}) (reduce_trail_to ([]::('v,'v clause) ann_lits) S)›]
using state_eq_trans[of T
‹update_conflicting (Some {#}) (reduce_trail_to ([]::('v,'v clause) ann_lits) S)›
‹update_conflicting (Some {#}) (reduce_trail_to ([]::('v,'v clause) ann_lits) S')›]
update_conflicting_state_eq[of S S' ‹Some {#}›]
apply (auto simp: conflict_opt0.simps state_eq_sym)
using reduce_trail_to_state_eq state_eq_trans update_conflicting_state_eq by blast
lemma conflict_opt0_conflict_opt:
assumes ‹conflict_opt0 S U› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)›
shows ‹∃T. enc_weight_opt.conflict_opt S T ∧ resolve⇧*⇧* T U›
proof -
have
1: ‹count_decided (trail S) = 0› and
neg: ‹negate_ann_lits (trail S) ∈# enc_weight_opt.conflicting_clss S› and
confl: ‹conflicting S = None› and
U: ‹U ∼ update_conflicting (Some {#}) (reduce_trail_to ([]::('v,'v clause)ann_lits) S)›
using assms by (auto elim: conflict_opt0E)
let ?T = ‹update_conflicting (Some (negate_ann_lits (trail S))) S›
have confl: ‹enc_weight_opt.conflict_opt S ?T›
using neg confl
by (auto simp: enc_weight_opt.conflict_opt.simps)
let ?T = ‹λn. update_conflicting
(Some (negate_ann_lits (drop n (trail S))))
(reduce_trail_to (drop n (trail S)) S)›
have proped_M2: ‹is_proped (trail S ! n)› if ‹n < length (trail S)› for n
using 1 that by (auto simp: count_decided_0_iff is_decided_no_proped_iff)
have n_d: ‹no_dup (trail S)› and
le: ‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (enc_weight_opt.abs_state S)› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (enc_weight_opt.abs_state S)› and
decomp_imp: ‹all_decomposition_implies_m (clauses S + (enc_weight_opt.conflicting_clss S))
(get_all_ann_decomposition (trail S))› and
learned: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (enc_weight_opt.abs_state S)›
using inv
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
have proped: ‹⋀L mark a b.
a @ Propagated L mark # b = trail S ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark›
using le
unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by auto
have [simp]: ‹count_decided (drop n (trail S)) = 0› for n
using 1 unfolding count_decided_0_iff
by (cases ‹n < length (trail S)›) (auto dest: in_set_dropD)
have [simp]: ‹get_maximum_level (drop n (trail S)) C = 0› for n C
using count_decided_ge_get_maximum_level[of ‹drop n (trail S)› C]
by auto
have mark_dist: ‹distinct_mset (mark_of (trail S!n))› if ‹n < length (trail S)› for n
using dist that proped_M2[OF that] nth_mem[OF that]
unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
by (cases ‹trail S!n›) auto
have res: ‹resolve (?T n) (?T (Suc n))› if ‹n < length (trail S)› for n
proof -
define L and E where
‹L = lit_of (trail S ! n)› and
‹E = mark_of (trail S ! n)›
have ‹hd (drop n (trail S)) = Propagated L E› and
tr_Sn: ‹trail S ! n = Propagated L E›
using proped_M2[OF that]
by (cases ‹trail S ! n›; auto simp: that hd_drop_conv_nth L_def E_def; fail)+
have ‹L ∈# E› and
ent_E: ‹drop (Suc n) (trail S) ⊨as CNot (remove1_mset L E)›
using proped[of ‹take n (trail S)› L E ‹drop (Suc n) (trail S)›]
that unfolding tr_Sn[symmetric]
by (auto simp: Cons_nth_drop_Suc)
have 1: ‹negate_ann_lits (drop (Suc n) (trail S)) =
(remove1_mset (- L) (negate_ann_lits (drop n (trail S))) ∪#
remove1_mset L E)›
apply (subst distinct_set_mset_eq_iff[symmetric])
subgoal
using n_d by (auto simp: no_dup_dropI)
subgoal
using n_d mark_dist[OF that] unfolding tr_Sn
by (auto intro: distinct_mset_mono no_dup_dropI
intro!: distinct_mset_minus)
subgoal
using ent_E unfolding tr_Sn[symmetric]
by (auto simp: negate_ann_lits_def that
Cons_nth_drop_Suc[symmetric] L_def lits_of_def
true_annots_true_cls_def_iff_negation_in_model
uminus_lit_swap
dest!: multi_member_split)
done
have ‹update_conflicting (Some (negate_ann_lits (drop (Suc n) (trail S))))
(reduce_trail_to (drop (Suc n) (trail S)) S) ∼
update_conflicting
(Some
(remove1_mset (- L) (negate_ann_lits (drop n (trail S))) ∪#
remove1_mset L E))
(tl_trail
(update_conflicting (Some (negate_ann_lits (drop n (trail S))))
(reduce_trail_to (drop n (trail S)) S)))›
unfolding 1[symmetric]
apply (rule state_eq_trans)
prefer 2
apply (rule state_eq_sym[THEN iffD1])
apply (rule update_conflicting_state_eq)
apply (rule tl_trail_update_conflicting)
apply (rule state_eq_trans)
prefer 2
apply (rule state_eq_sym[THEN iffD1])
apply (rule update_conflicting_update_conflicting)
apply (rule state_eq_ref)
apply (rule update_conflicting_state_eq)
using that
by (auto simp: reduce_trail_to_compow_tl_trail funpow_swap1)
moreover have ‹L ∈# E›
using proped[of ‹take n (trail S)› L E ‹drop (Suc n) (trail S)›]
that unfolding tr_Sn[symmetric]
by (auto simp: Cons_nth_drop_Suc)
moreover have ‹- L ∈# negate_ann_lits (drop n (trail S))›
by (auto simp: negate_ann_lits_def L_def
in_set_dropI that)
term ‹get_maximum_level (drop n (trail S))›
ultimately show ?thesis apply -
by (rule resolve.intros[of _ L E])
(use that in ‹auto simp: trail_reduce_trail_to_drop
‹hd (drop n (trail S)) = Propagated L E››)
qed
have ‹resolve⇧*⇧* (?T 0) (?T n)› if ‹n ≤ length (trail S)› for n
using that
apply (induction n)
subgoal by auto
subgoal for n
using res[of n] by auto
done
from this[of ‹length (trail S)›] have ‹resolve⇧*⇧* (?T 0) (?T (length (trail S)))›
by auto
moreover have ‹?T (length (trail S)) ∼ U›
apply (rule state_eq_trans)
prefer 2 apply (rule state_eq_sym[THEN iffD1], rule U)
by auto
moreover have False if ‹(?T 0) = (?T (length (trail S)))› and ‹length (trail S) > 0›
using arg_cong[OF that(1), of conflicting] that(2)
by (auto simp: negate_ann_lits_def)
ultimately have ‹length (trail S) > 0 ⟶ resolve⇧*⇧* (?T 0) U›
using tranclp_resolve_state_eq_compatible[of ‹?T 0›
‹?T (length (trail S))› U] by (subst (asm) rtranclp_unfold) auto
then have ?thesis if ‹length (trail S) > 0›
using confl that by auto
moreover have ?thesis if ‹length (trail S) = 0›
using that confl U
enc_weight_opt.conflict_opt_state_eq_compatible[of S ‹(update_conflicting (Some {#}) S)› S U]
by (auto simp: state_eq_sym)
ultimately show ?thesis
by blast
qed
lemma backtrack_split_some_is_decided_then_snd_has_hd2:
‹∃l∈set M. is_decided l ⟹ ∃M' L' M''. backtrack_split M = (M'', Decided L' # M')›
by (metis backtrack_split_snd_hd_decided backtrack_split_some_is_decided_then_snd_has_hd
is_decided_def list.distinct(1) list.sel(1) snd_conv)
lemma no_step_conflict_opt0_simple_backtrack_conflict_opt:
‹no_step conflict_opt0 S ⟹ no_step simple_backtrack_conflict_opt S ⟹
no_step enc_weight_opt.conflict_opt S›
using backtrack_split_some_is_decided_then_snd_has_hd2[of ‹trail S›]
count_decided_0_iff[of ‹trail S›]
by (fastforce simp: conflict_opt0.simps simple_backtrack_conflict_opt.simps
enc_weight_opt.conflict_opt.simps
annotated_lit.is_decided_def)
lemma no_step_cdcl_dpll_bnb_r_cdcl_bnb_r:
assumes ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)›
shows
‹no_step cdcl_dpll_bnb_r S ⟷ no_step cdcl_bnb_r S› (is ‹?A ⟷ ?B›)
proof
assume ?A
show ?B
using ‹?A› no_step_conflict_opt0_simple_backtrack_conflict_opt[of S]
by (auto simp: cdcl_bnb_r.simps
cdcl_dpll_bnb_r.simps all_conj_distrib)
next
assume ?B
show ?A
using ‹?B› simple_backtrack_conflict_opt_conflict_analysis[OF _ assms]
by (auto simp: cdcl_bnb_r.simps cdcl_dpll_bnb_r.simps all_conj_distrib assms
dest!: conflict_opt0_conflict_opt)
qed
lemma cdcl_dpll_bnb_r_cdcl_bnb_r:
assumes ‹cdcl_dpll_bnb_r S T› and
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)›
shows ‹cdcl_bnb_r⇧*⇧* S T›
using assms
proof (cases rule: cdcl_dpll_bnb_r.cases)
case cdcl_simple_backtrack_conflict_opt
then obtain S1 S2 where
‹enc_weight_opt.conflict_opt S S1›
‹resolve⇧*⇧* S1 S2› and
‹enc_weight_opt.obacktrack S2 T›
using simple_backtrack_conflict_opt_conflict_analysis[OF _ assms(2), of T]
by auto
then have ‹cdcl_bnb_r S S1›
‹cdcl_bnb_r⇧*⇧* S1 S2›
‹cdcl_bnb_r S2 T›
using mono_rtranclp[of resolve enc_weight_opt.cdcl_bnb_bj]
mono_rtranclp[of enc_weight_opt.cdcl_bnb_bj ocdcl⇩W_o_r]
mono_rtranclp[of ocdcl⇩W_o_r cdcl_bnb_r]
ocdcl⇩W_o_r.intros enc_weight_opt.cdcl_bnb_bj.resolve
cdcl_bnb_r.intros
enc_weight_opt.cdcl_bnb_bj.intros
by (auto 5 4 dest: cdcl_bnb_r.intros conflict_opt0_conflict_opt)
then show ?thesis
by auto
next
case cdcl_conflict_opt0
then obtain S1 where
‹enc_weight_opt.conflict_opt S S1›
‹resolve⇧*⇧* S1 T›
using conflict_opt0_conflict_opt[OF _ assms(2), of T]
by auto
then have ‹cdcl_bnb_r S S1›
‹cdcl_bnb_r⇧*⇧* S1 T›
using mono_rtranclp[of resolve enc_weight_opt.cdcl_bnb_bj]
mono_rtranclp[of enc_weight_opt.cdcl_bnb_bj ocdcl⇩W_o_r]
mono_rtranclp[of ocdcl⇩W_o_r cdcl_bnb_r]
ocdcl⇩W_o_r.intros enc_weight_opt.cdcl_bnb_bj.resolve
cdcl_bnb_r.intros
enc_weight_opt.cdcl_bnb_bj.intros
by (auto 5 4 dest: cdcl_bnb_r.intros conflict_opt0_conflict_opt)
then show ?thesis
by auto
qed (auto 5 4 dest: cdcl_bnb_r.intros conflict_opt0_conflict_opt simp: assms)
lemma resolve_no_prop_confl: ‹resolve S T ⟹ no_step propagate S ∧ no_step conflict S›
by (auto elim!: rulesE)
lemma cdcl_bnb_r_stgy_res:
‹resolve S T ⟹ cdcl_bnb_r_stgy S T›
using enc_weight_opt.cdcl_bnb_bj.resolve[of S T]
ocdcl⇩W_o_r.intros[of S T]
cdcl_bnb_r_stgy.intros[of S T]
resolve_no_prop_confl[of S T]
by (auto 5 4 dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt)
lemma rtranclp_cdcl_bnb_r_stgy_res:
‹resolve⇧*⇧* S T ⟹ cdcl_bnb_r_stgy⇧*⇧* S T›
using mono_rtranclp[of resolve cdcl_bnb_r_stgy]
cdcl_bnb_r_stgy_res
by (auto)
lemma obacktrack_no_prop_confl: ‹enc_weight_opt.obacktrack S T ⟹ no_step propagate S ∧ no_step conflict S›
by (auto elim!: rulesE enc_weight_opt.obacktrackE)
lemma cdcl_bnb_r_stgy_bt:
‹enc_weight_opt.obacktrack S T ⟹ cdcl_bnb_r_stgy S T›
using enc_weight_opt.cdcl_bnb_bj.backtrack[of S T]
ocdcl⇩W_o_r.intros[of S T]
cdcl_bnb_r_stgy.intros[of S T]
obacktrack_no_prop_confl[of S T]
by (auto 5 4 dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt)
lemma cdcl_dpll_bnb_r_stgy_cdcl_bnb_r_stgy:
assumes ‹cdcl_dpll_bnb_r_stgy S T› and
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)›
shows ‹cdcl_bnb_r_stgy⇧*⇧* S T›
using assms
proof (cases rule: cdcl_dpll_bnb_r_stgy.cases)
case cdcl_dpll_bnb_r_simple_backtrack_conflict_opt
then obtain S1 S2 where
‹enc_weight_opt.conflict_opt S S1›
‹resolve⇧*⇧* S1 S2› and
‹enc_weight_opt.obacktrack S2 T›
using simple_backtrack_conflict_opt_conflict_analysis[OF _ assms(2), of T]
by auto
then have ‹cdcl_bnb_r_stgy S S1›
‹cdcl_bnb_r_stgy⇧*⇧* S1 S2›
‹cdcl_bnb_r_stgy S2 T›
using enc_weight_opt.cdcl_bnb_bj.resolve
by (auto dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt
rtranclp_cdcl_bnb_r_stgy_res cdcl_bnb_r_stgy_bt)
then show ?thesis
by auto
next
case cdcl_dpll_bnb_r_conflict_opt0
then obtain S1 where
‹enc_weight_opt.conflict_opt S S1›
‹resolve⇧*⇧* S1 T›
using conflict_opt0_conflict_opt[OF _ assms(2), of T]
by auto
then have ‹cdcl_bnb_r_stgy S S1›
‹cdcl_bnb_r_stgy⇧*⇧* S1 T›
using enc_weight_opt.cdcl_bnb_bj.resolve
by (auto dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt
rtranclp_cdcl_bnb_r_stgy_res cdcl_bnb_r_stgy_bt)
then show ?thesis
by auto
qed (auto 5 4 dest: cdcl_bnb_r_stgy.intros conflict_opt0_conflict_opt)
lemma cdcl_bnb_r_stgy_cdcl_bnb_r:
‹cdcl_bnb_r_stgy S T ⟹ cdcl_bnb_r S T›
by (auto simp: cdcl_bnb_r_stgy.simps cdcl_bnb_r.simps)
lemma rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r:
‹cdcl_bnb_r_stgy⇧*⇧* S T ⟹ cdcl_bnb_r⇧*⇧* S T›
by (induction rule: rtranclp_induct)
(auto dest: cdcl_bnb_r_stgy_cdcl_bnb_r)
context
fixes S :: 'st
assumes S_Σ: ‹atms_of_mm (init_clss S) = Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
begin
lemma cdcl_dpll_bnb_r_stgy_all_struct_inv:
‹cdcl_dpll_bnb_r_stgy S T ⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S) ⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state T)›
using cdcl_dpll_bnb_r_stgy_cdcl_bnb_r_stgy[of S T]
rtranclp_cdcl_bnb_r_all_struct_inv[OF S_Σ]
rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r[of S T]
by auto
end
lemma cdcl_bnb_r_stgy_cdcl_dpll_bnb_r_stgy:
‹cdcl_bnb_r_stgy S T ⟹ ∃T. cdcl_dpll_bnb_r_stgy S T›
by (meson cdcl_bnb_r_stgy.simps cdcl_dpll_bnb_r_conflict cdcl_dpll_bnb_r_conflict_opt0
cdcl_dpll_bnb_r_other' cdcl_dpll_bnb_r_propagate cdcl_dpll_bnb_r_simple_backtrack_conflict_opt
cdcl_dpll_bnb_r_stgy.intros(3) no_step_conflict_opt0_simple_backtrack_conflict_opt)
context
fixes S :: 'st
assumes S_Σ: ‹atms_of_mm (init_clss S) = Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
begin
lemma rtranclp_cdcl_dpll_bnb_r_stgy_cdcl_bnb_r:
assumes ‹cdcl_dpll_bnb_r_stgy⇧*⇧* S T› and
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)›
shows ‹cdcl_bnb_r_stgy⇧*⇧* S T›
using assms
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for T U
using cdcl_dpll_bnb_r_stgy_cdcl_bnb_r_stgy[of T U]
rtranclp_cdcl_bnb_r_all_struct_inv[OF S_Σ, of T]
rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r[of S T]
by auto
done
lemma rtranclp_cdcl_dpll_bnb_r_stgy_all_struct_inv:
‹cdcl_dpll_bnb_r_stgy⇧*⇧* S T ⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S) ⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state T)›
using rtranclp_cdcl_dpll_bnb_r_stgy_cdcl_bnb_r[of T]
rtranclp_cdcl_bnb_r_all_struct_inv[OF S_Σ, of T]
rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r[of S T]
by auto
lemma full_cdcl_dpll_bnb_r_stgy_full_cdcl_bnb_r_stgy:
assumes ‹full cdcl_dpll_bnb_r_stgy S T› and
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)›
shows ‹full cdcl_bnb_r_stgy S T›
using no_step_cdcl_dpll_bnb_r_cdcl_bnb_r[of T]
rtranclp_cdcl_dpll_bnb_r_stgy_cdcl_bnb_r[of T]
rtranclp_cdcl_dpll_bnb_r_stgy_all_struct_inv[of T] assms
rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_r[of S T]
by (auto simp: full_def
dest: cdcl_bnb_r_stgy_cdcl_bnb_r cdcl_bnb_r_stgy_cdcl_dpll_bnb_r_stgy)
end
lemma replace_pos_neg_not_both_decided_highest_lvl:
assumes
struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)› and
smaller_propa: ‹no_smaller_propa S› and
smaller_confl: ‹no_smaller_confl S› and
dec0: ‹Pos (A⇧↦⇧0) ∈ lits_of_l (trail S)› and
dec1: ‹Pos (A⇧↦⇧1) ∈ lits_of_l (trail S)› and
add: ‹additional_constraints ⊆# init_clss S› and
[simp]: ‹A ∈ ΔΣ›
shows ‹get_level (trail S) (Pos (A⇧↦⇧0)) = backtrack_lvl S ∧
get_level (trail S) (Pos (A⇧↦⇧1)) = backtrack_lvl S›
proof (rule ccontr)
assume neg: ‹¬?thesis›
let ?L0 = ‹get_level (trail S) (Pos (A⇧↦⇧0))›
let ?L1 = ‹get_level (trail S) (Pos (A⇧↦⇧1))›
define KL where ‹KL = (if ?L0 > ?L1 then (Pos (A⇧↦⇧1)) else (Pos (A⇧↦⇧0)))›
define KL' where ‹KL' = (if ?L0 > ?L1 then (Pos (A⇧↦⇧0)) else (Pos (A⇧↦⇧1)))›
then have ‹get_level (trail S) KL < backtrack_lvl S› and
le: ‹?L0 < backtrack_lvl S ∨ ?L1 < backtrack_lvl S›
‹?L0 ≤ backtrack_lvl S ∧ ?L1 ≤ backtrack_lvl S›
using neg count_decided_ge_get_level[of ‹trail S› ‹Pos (A⇧↦⇧0)›]
count_decided_ge_get_level[of ‹trail S› ‹Pos (A⇧↦⇧1)›]
unfolding KL_def
by force+
have ‹KL ∈ lits_of_l (trail S)›
using dec1 dec0 by (auto simp: KL_def)
have add: ‹additional_constraint A ⊆# init_clss S›
using add multi_member_split[of A ‹mset_set ΔΣ›] by (auto simp: additional_constraints_def
subset_mset.dual_order.trans)
have n_d: ‹no_dup (trail S)›
using struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
have H: ‹⋀M K M' D L.
trail S = M' @ Decided K # M ⟹
D + {#L#} ∈# additional_constraint A ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D› and
H': ‹⋀M K M' D L.
trail S = M' @ Decided K # M ⟹
D ∈# additional_constraint A ⟹ ¬ M ⊨as CNot D›
using smaller_propa add smaller_confl unfolding no_smaller_propa_def no_smaller_confl_def clauses_def
by auto
have L1_L0: ‹?L1 = ?L0›
proof (rule ccontr)
assume neq: ‹?L1 ≠ ?L0›
define i where ‹i ≡ min ?L1 ?L0›
obtain K M1 M2 where
decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and
‹get_level (trail S) K = Suc i›
using backtrack_ex_decomp[OF n_d, of i] neq le
by (cases ‹?L1 < ?L0›) (auto simp: min_def i_def)
have ‹get_level (trail S) KL ≤ i› and ‹get_level (trail S) KL' > i›
using neg neq le by (auto simp: KL_def KL'_def i_def)
then have ‹undefined_lit M1 KL'›
using n_d decomp ‹get_level (trail S) K = Suc i›
count_decided_ge_get_level[of ‹M1› KL']
by (force dest!: get_all_ann_decomposition_exists_prepend
simp: get_level_append_if get_level_cons_if atm_of_eq_atm_of
dest: defined_lit_no_dupD
split: if_splits)
moreover have ‹{#-KL', -KL#} ∈# additional_constraint A›
using neq by (auto simp: additional_constraint_def KL_def KL'_def)
moreover have ‹KL ∈ lits_of_l M1›
using ‹get_level (trail S) KL ≤ i› ‹get_level (trail S) K = Suc i›
n_d decomp ‹KL ∈ lits_of_l (trail S)›
count_decided_ge_get_level[of ‹M1› KL]
by (auto dest!: get_all_ann_decomposition_exists_prepend
simp: get_level_append_if get_level_cons_if atm_of_eq_atm_of
dest: defined_lit_no_dupD in_lits_of_l_defined_litD
split: if_splits)
ultimately show False
using H[of _ K M1 ‹{#-KL#}› ‹-KL'›] decomp
by force
qed
obtain K M1 M2 where
decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and
lev_K: ‹get_level (trail S) K = Suc ?L1›
using backtrack_ex_decomp[OF n_d, of ?L1] le
by (cases ‹?L1 < ?L0›) (auto simp: min_def L1_L0)
then obtain M3 where
M3: ‹trail S = M3 @ Decided K # M1›
by auto
then have [simp]: ‹undefined_lit M3 (Pos (A⇧↦⇧1))› ‹undefined_lit M3 (Pos (A⇧↦⇧0))›
by (solves ‹use n_d L1_L0 lev_K M3 in auto›)
(solves ‹use n_d L1_L0[symmetric] lev_K M3 in auto›)
then have [simp]: ‹Pos (A⇧↦⇧0) ∉ lits_of_l M3› ‹Pos (A⇧↦⇧1) ∉ lits_of_l M3›
using Decided_Propagated_in_iff_in_lits_of_l by blast+
have ‹Pos (A⇧↦⇧1) ∈ lits_of_l M1› ‹Pos (A⇧↦⇧0) ∈ lits_of_l M1›
using n_d L1_L0 lev_K dec0 dec1 Decided_Propagated_in_iff_in_lits_of_l
by (auto dest!: get_all_ann_decomposition_exists_prepend
simp: M3 get_level_cons_if
split: if_splits)
then show False
using H'[of M3 K M1 ‹{#Neg (A⇧↦⇧0), Neg (A⇧↦⇧1)#}›]
by (auto simp: additional_constraint_def M3)
qed
lemma cdcl_dpll_bnb_r_stgy_clauses_mono:
‹cdcl_dpll_bnb_r_stgy S T ⟹ clauses S ⊆# clauses T›
by (cases rule: cdcl_dpll_bnb_r_stgy.cases, assumption)
(auto elim!: rulesE obacktrackE enc_weight_opt.improveE
conflict_opt0E simple_backtrack_conflict_optE odecideE
enc_weight_opt.obacktrackE
simp: ocdcl⇩W_o_r.simps enc_weight_opt.cdcl_bnb_bj.simps)
lemma rtranclp_cdcl_dpll_bnb_r_stgy_clauses_mono:
‹cdcl_dpll_bnb_r_stgy⇧*⇧* S T ⟹ clauses S ⊆# clauses T›
by (induction rule: rtranclp_induct) (auto dest!: cdcl_dpll_bnb_r_stgy_clauses_mono)
lemma cdcl_dpll_bnb_r_stgy_init_clss_eq:
‹cdcl_dpll_bnb_r_stgy S T ⟹ init_clss S = init_clss T›
by (cases rule: cdcl_dpll_bnb_r_stgy.cases, assumption)
(auto elim!: rulesE obacktrackE enc_weight_opt.improveE
conflict_opt0E simple_backtrack_conflict_optE odecideE
enc_weight_opt.obacktrackE
simp: ocdcl⇩W_o_r.simps enc_weight_opt.cdcl_bnb_bj.simps)
lemma rtranclp_cdcl_dpll_bnb_r_stgy_init_clss_eq:
‹cdcl_dpll_bnb_r_stgy⇧*⇧* S T ⟹ init_clss S = init_clss T›
by (induction rule: rtranclp_induct) (auto dest!: cdcl_dpll_bnb_r_stgy_init_clss_eq)
context
fixes S :: 'st and N :: ‹'v clauses›
assumes S_Σ: ‹init_clss S = penc N›
begin
lemma replacement_pos_neg_defined_same_lvl:
assumes
struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)› and
A: ‹A ∈ ΔΣ› and
lev: ‹get_level (trail S) (Pos (replacement_pos A)) < backtrack_lvl S› and
smaller_propa: ‹no_smaller_propa S› and
smaller_confl: ‹cdcl_bnb_stgy_inv S›
shows
‹Pos (replacement_pos A) ∈ lits_of_l (trail S) ⟹
Neg (replacement_neg A) ∈ lits_of_l (trail S)›
proof -
have n_d: ‹no_dup (trail S)›
using struct
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
have H: ‹⋀M K M' D L.
trail S = M' @ Decided K # M ⟹
D + {#L#} ∈# additional_constraint A ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D› and
H': ‹⋀M K M' D L.
trail S = M' @ Decided K # M ⟹
D ∈# additional_constraint A ⟹ ¬ M ⊨as CNot D›
using smaller_propa S_Σ A smaller_confl unfolding no_smaller_propa_def clauses_def penc_def
additional_constraints_def cdcl_bnb_stgy_inv_def no_smaller_confl_def by fastforce+
show ‹Neg (replacement_neg A) ∈ lits_of_l (trail S)›
if Pos: ‹Pos (replacement_pos A) ∈ lits_of_l (trail S)›
proof -
obtain M1 M2 K where
‹trail S = M2 @ Decided K # M1› and
‹Pos (replacement_pos A) ∈ lits_of_l M1›
using lev n_d Pos by (force dest!: split_list elim!: is_decided_ex_Decided
simp: lits_of_def count_decided_def filter_empty_conv)
then show ‹Neg (replacement_neg A) ∈ lits_of_l (trail S)›
using H[of M2 K M1 ‹{#Neg (replacement_pos A)#}› ‹Neg (replacement_neg A)›]
H'[of M2 K M1 ‹{#Neg (replacement_pos A), Neg (replacement_neg A)#}›]
by (auto simp: additional_constraint_def Decided_Propagated_in_iff_in_lits_of_l)
qed
qed
lemma replacement_pos_neg_defined_same_lvl':
assumes
struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)› and
A: ‹A ∈ ΔΣ› and
lev: ‹get_level (trail S) (Pos (replacement_neg A)) < backtrack_lvl S› and
smaller_propa: ‹no_smaller_propa S› and
smaller_confl: ‹cdcl_bnb_stgy_inv S›
shows
‹Pos (replacement_neg A) ∈ lits_of_l (trail S) ⟹
Neg (replacement_pos A) ∈ lits_of_l (trail S)›
proof -
have n_d: ‹no_dup (trail S)›
using struct
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
have H: ‹⋀M K M' D L.
trail S = M' @ Decided K # M ⟹
D + {#L#} ∈# additional_constraint A ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D› and
H': ‹⋀M K M' D L.
trail S = M' @ Decided K # M ⟹
D ∈# additional_constraint A ⟹ ¬ M ⊨as CNot D›
using smaller_propa S_Σ A smaller_confl unfolding no_smaller_propa_def clauses_def penc_def
additional_constraints_def cdcl_bnb_stgy_inv_def no_smaller_confl_def by fastforce+
show ‹Neg (replacement_pos A) ∈ lits_of_l (trail S)›
if Pos: ‹Pos (replacement_neg A) ∈ lits_of_l (trail S)›
proof -
obtain M1 M2 K where
‹trail S = M2 @ Decided K # M1› and
‹Pos (replacement_neg A) ∈ lits_of_l M1›
using lev n_d Pos by (force dest!: split_list elim!: is_decided_ex_Decided
simp: lits_of_def count_decided_def filter_empty_conv)
then show ‹Neg (replacement_pos A) ∈ lits_of_l (trail S)›
using H[of M2 K M1 ‹{#Neg (replacement_neg A)#}› ‹Neg (replacement_pos A)›]
H'[of M2 K M1 ‹{#Neg (replacement_neg A), Neg (replacement_pos A)#}›]
by (auto simp: additional_constraint_def Decided_Propagated_in_iff_in_lits_of_l)
qed
qed
end
definition all_new_literals :: ‹'v list› where
‹all_new_literals = (SOME xs. mset xs = mset_set (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ))›
lemma set_all_new_literals[simp]:
‹set all_new_literals = (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ)›
using finite_Σ apply (simp add: all_new_literals_def)
apply (metis (mono_tags) ex_mset finite_Un finite_Σ finite_imageI finite_set_mset_mset_set set_mset_mset someI)
done
text ‹This function is basically resolving the clause with all the additional clauses \<^term>‹{#Neg (replacement_pos L), Neg (replacement_neg L)#}›.›
fun resolve_with_all_new_literals :: ‹'v clause ⇒ 'v list ⇒ 'v clause› where
‹resolve_with_all_new_literals C [] = C› |
‹resolve_with_all_new_literals C (L # Ls) =
remdups_mset (resolve_with_all_new_literals (if Pos L ∈# C then add_mset (Neg (opposite_var L)) (removeAll_mset (Pos L) C) else C) Ls)›
abbreviation normalize2 where
‹normalize2 C ≡ resolve_with_all_new_literals C all_new_literals›
lemma Neg_in_normalize2[simp]: ‹Neg L ∈# C ⟹ Neg L ∈# resolve_with_all_new_literals C xs›
by (induction arbitrary: C rule: resolve_with_all_new_literals.induct) auto
lemma Pos_in_normalize2D[dest]: ‹Pos L ∈# resolve_with_all_new_literals C xs ⟹ Pos L ∈# C›
by (induction arbitrary: C rule: resolve_with_all_new_literals.induct) (force split: if_splits)+
lemma opposite_var_involutive[simp]:
‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ opposite_var (opposite_var L) = L›
by (auto simp: opposite_var_def)
lemma Neg_in_resolve_with_all_new_literals_Pos_notin:
‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ set xs ⊆ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹
Pos (opposite_var L) ∉# C ⟹ Neg L ∈# resolve_with_all_new_literals C xs ⟷ Neg L ∈# C›
apply (induction arbitrary: C rule: resolve_with_all_new_literals.induct)
apply clarsimp+
subgoal premises p
using p(2-)
by (auto simp del: Neg_in_normalize2 simp: eq_commute[of _ ‹opposite_var _›])
done
lemma Pos_in_normalize2_Neg_notin[simp]:
‹L ∈ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹
Pos (opposite_var L) ∉# C ⟹ Neg L ∈# normalize2 C ⟷ Neg L ∈# C›
by (rule Neg_in_resolve_with_all_new_literals_Pos_notin) (auto)
lemma all_negation_deleted:
‹L ∈ set all_new_literals ⟹ Pos L ∉# normalize2 C›
apply (induction arbitrary: C rule: resolve_with_all_new_literals.induct)
subgoal by auto
subgoal by (auto split: if_splits)
done
lemma Pos_in_resolve_with_all_new_literals_iff_already_in_or_negation_in:
‹L ∈ set all_new_literals ⟹set xs ⊆ (replacement_neg ` ΔΣ ∪ replacement_pos ` ΔΣ) ⟹ Neg L ∈# resolve_with_all_new_literals C xs⟹
Neg L ∈# C ∨ Pos (opposite_var L) ∈# C›
apply (induction arbitrary: C rule: resolve_with_all_new_literals.induct)
subgoal by auto
subgoal premises p for C La Ls Ca
using p
by (auto split: if_splits dest: simp: Neg_in_resolve_with_all_new_literals_Pos_notin)
done
lemma Pos_in_normalize2_iff_already_in_or_negation_in:
‹L ∈ set all_new_literals ⟹ Neg L ∈# normalize2 C ⟹
Neg L ∈# C ∨ Pos (opposite_var L) ∈# C›
using Pos_in_resolve_with_all_new_literals_iff_already_in_or_negation_in[of L ‹all_new_literals› C]
by auto
text ‹This proof makes it hard to measure progress because I currently do not see a way to
distinguish between \<^term>‹add_mset (replacement_pos A) C› and \<^term>‹add_mset (replacement_pos A)
(add_mset (replacement_neg A) C)›. ›
lemma
assumes
‹enc_weight_opt.cdcl_bnb_stgy S T› and
struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S)› and
dist: ‹distinct_mset (normalize_clause `# learned_clss S)› and
smaller_propa: ‹no_smaller_propa S› and
smaller_confl: ‹cdcl_bnb_stgy_inv S›
shows ‹distinct_mset (remdups_mset (normalize2 `# learned_clss T))›
using assms(1)
proof (cases)
case cdcl_bnb_conflict
then show ?thesis using dist by (auto elim!: rulesE)
next
case cdcl_bnb_propagate
then show ?thesis using dist by (auto elim!: rulesE)
next
case cdcl_bnb_improve
then show ?thesis using dist by (auto elim!: enc_weight_opt.improveE)
next
case cdcl_bnb_conflict_opt
then show ?thesis using dist by (auto elim!: enc_weight_opt.conflict_optE)
next
case cdcl_bnb_other'
then show ?thesis
proof cases
case decide
then show ?thesis using dist by (auto elim!: rulesE)
next
case bj
then show ?thesis
proof cases
case skip
then show ?thesis using dist by (auto elim!: rulesE)
next
case resolve
then show ?thesis using dist by (auto elim!: rulesE)
next
case backtrack
then obtain M1 M2 :: ‹('v, 'v clause) ann_lits› and K L :: ‹'v literal› and
D D' :: ‹'v clause› where
confl: ‹conflicting S = Some (add_mset L D)› and
decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and
‹get_maximum_level (trail S) (add_mset L D') = local.backtrack_lvl S› and
‹get_level (trail S) L = local.backtrack_lvl S› and
lev_K: ‹get_level (trail S) K = Suc (get_maximum_level (trail S) D')› and
D'_D: ‹D' ⊆# D› and
‹set_mset (clauses S) ∪ set_mset (enc_weight_opt.conflicting_clss S) ⊨p
add_mset L D'› 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)))›
by (auto simp: enc_weight_opt.obacktrack.simps)
have
tr_D: ‹trail S ⊨as CNot (add_mset L D)› and
‹distinct_mset (add_mset L D)› and
‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)› and
n_d: ‹no_dup (trail S)›
using struct confl
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
have tr_D': ‹trail S ⊨as CNot (add_mset L D')›
using D'_D tr_D
by (auto simp: true_annots_true_cls_def_iff_negation_in_model)
have ‹trail S ⊨as CNot D' ⟹ trail S ⊨as CNot (normalize2 D')›
if ‹get_maximum_level (trail S) D' < backtrack_lvl S›
for D'
oops
find_theorems get_level Pos Neg
end
end