theory CDCL_W_Covering_Models
imports CDCL_W_Optimal_Model
begin
section ‹Covering Models›
text ‹I am only interested in the extension of CDCL to find covering mdoels, not in the required
subsequent extraction of the minimal covering models.›
type_synonym 'v cov = ‹'v literal multiset multiset›
lemma true_clss_cls_in_susbsuming:
‹C' ⊆# C ⟹ C' ∈ N ⟹ N ⊨p C›
by (metis subset_mset.le_iff_add true_clss_cls_in true_clss_cls_mono_r)
locale covering_models =
fixes
ρ :: ‹'v ⇒ bool›
begin
definition model_is_dominated :: ‹'v literal multiset ⇒ 'v literal multiset ⇒ bool› where
‹model_is_dominated M M' ⟷
filter_mset (λL. is_pos L ∧ ρ (atm_of L)) M ⊆# filter_mset (λL. is_pos L ∧ ρ (atm_of L)) M'›
lemma model_is_dominated_refl: ‹model_is_dominated I I›
by (auto simp: model_is_dominated_def)
lemma model_is_dominated_trans:
‹model_is_dominated I J ⟹ model_is_dominated J K ⟹ model_is_dominated I K›
by (auto simp: model_is_dominated_def)
definition is_dominating :: ‹'v literal multiset multiset ⇒ 'v literal multiset ⇒ bool› where
‹is_dominating ℳ I ⟷ (∃M∈#ℳ. ∃J. I ⊆# J ∧ model_is_dominated J M)›
lemma
is_dominating_in:
‹I ∈# ℳ ⟹ is_dominating ℳ I› and
is_dominating_mono:
‹is_dominating ℳ I ⟹ set_mset ℳ ⊆ set_mset ℳ' ⟹ is_dominating ℳ' I› and
is_dominating_mono_model:
‹is_dominating ℳ I ⟹ I' ⊆# I ⟹ is_dominating ℳ I'›
using multiset_filter_mono[of I' I ‹λL. is_pos L ∧ ρ (atm_of L)›]
by (auto 5 5 simp: is_dominating_def model_is_dominated_def
dest!: multi_member_split)
lemma is_dominating_add_mset:
‹is_dominating (add_mset x ℳ) I ⟷
is_dominating ℳ I ∨ (∃J. I ⊆# J ∧ model_is_dominated J x)›
by (auto simp: is_dominating_def)
definition is_improving_int
:: ‹('v, 'v clause) ann_lits ⇒ ('v, 'v clause) ann_lits ⇒ 'v clauses ⇒ 'v cov ⇒ bool›
where
‹is_improving_int M M' N ℳ ⟷
M = M' ∧ (∀I ∈# ℳ. ¬model_is_dominated (lit_of `# mset M) I) ∧
total_over_m (lits_of_l M) (set_mset N) ∧
lit_of `# mset M ∈ simple_clss (atms_of_mm N) ∧
lit_of `# mset M ∉# ℳ ∧
M ⊨asm N ∧
no_dup M›
text ‹This criteria is a bit more general than Weidenbach's version.›
abbreviation conflicting_clauses_ent where
‹conflicting_clauses_ent N ℳ ≡
{#pNeg {#L ∈# x. ρ (atm_of L)#}.
x ∈# filter_mset (λx. is_dominating ℳ x ∧ atms_of x = atms_of_mm N)
(mset_set (simple_clss (atms_of_mm N)))#}+ N›
definition conflicting_clauses
:: ‹'v clauses ⇒ 'v cov ⇒ 'v clauses›
where
‹conflicting_clauses N ℳ =
{#C ∈# mset_set (simple_clss (atms_of_mm N)).
conflicting_clauses_ent N ℳ ⊨pm C#}›
lemma conflicting_clauses_insert:
assumes ‹M ∈ simple_clss (atms_of_mm N)› and ‹atms_of M = atms_of_mm N›
shows ‹pNeg M ∈# conflicting_clauses N (add_mset M w)›
using assms true_clss_cls_in_susbsuming[of ‹pNeg {#L ∈# M. ρ (atm_of L)#}›
‹pNeg M› ‹set_mset (conflicting_clauses_ent N (add_mset M w))›]
is_dominating_in
by (auto simp: conflicting_clauses_def simple_clss_finite
pNeg_def image_mset_subseteq_mono)
lemma is_dominating_in_conflicting_clauses:
assumes ‹is_dominating ℳ I› and
atm: ‹atms_of_s (set_mset I) = atms_of_mm N› and
‹set_mset I ⊨m N› and
‹consistent_interp (set_mset I)› and
‹¬tautology I› and
‹distinct_mset I›
shows
‹pNeg I ∈# conflicting_clauses N ℳ›
proof -
have simpI: ‹I ∈ simple_clss (atms_of_mm N)›
using assms by (auto simp: simple_clss_def atms_of_s_def atms_of_def)
obtain I' J where ‹J ∈# ℳ› and ‹model_is_dominated I' J› and ‹I ⊆# I'›
using assms(1) unfolding is_dominating_def
by auto
then have ‹I ∈ {x ∈ simple_clss (atms_of_mm N).
(is_dominating A x ∨ (∃Ja. x ⊆# Ja ∧ model_is_dominated Ja J)) ∧
atms_of x = atms_of_mm N}›
using assms(1) atm
by (auto simp: conflicting_clauses_def simple_clss_finite simpI atms_of_def
pNeg_mono true_clss_cls_in_susbsuming is_dominating_add_mset atms_of_s_def
dest!: multi_member_split)
then show ?thesis
using assms(1)
by (auto simp: conflicting_clauses_def simple_clss_finite simpI
pNeg_mono is_dominating_add_mset
dest!: multi_member_split
intro!: true_clss_cls_in_susbsuming[of ‹(λx. pNeg {#L ∈# x. ρ (atm_of L)#}) I›])
qed
end
locale conflict_driven_clause_learning⇩W_covering_models =
conflict_driven_clause_learning⇩W
state_eq
state
trail init_clss learned_clss conflicting
cons_trail tl_trail add_learned_cls remove_cls
update_conflicting
init_state +
covering_models ρ
for
state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) and
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'v cov × 'b" and
trail :: "'st ⇒ ('v, 'v clause) ann_lits" and
init_clss :: "'st ⇒ 'v clauses" and
learned_clss :: "'st ⇒ 'v clauses" and
conflicting :: "'st ⇒ 'v clause option" and
cons_trail :: "('v, 'v clause) ann_lit ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_learned_cls :: "'v clause ⇒ 'st ⇒ 'st" and
remove_cls :: "'v clause ⇒ 'st ⇒ 'st" and
update_conflicting :: "'v clause option ⇒ 'st ⇒ 'st" and
init_state :: "'v clauses ⇒ 'st" and
ρ :: ‹'v ⇒ bool› +
fixes
update_additional_info :: ‹'v cov × 'b ⇒ 'st ⇒ 'st›
assumes
update_additional_info:
‹state S = (M, N, U, C, ℳ) ⟹ state (update_additional_info K' S) = (M, N, U, C, K')› and
weight_init_state:
‹⋀N :: 'v clauses. fst (additional_info (init_state N)) = {#}›
begin
definition update_weight_information :: ‹('v, 'v clause) ann_lits ⇒ 'st ⇒ 'st› where
‹update_weight_information M S =
update_additional_info (add_mset (lit_of `# mset M) (fst (additional_info S)), snd (additional_info S)) S›
lemma
trail_update_additional_info[simp]: ‹trail (update_additional_info w S) = trail S› and
init_clss_update_additional_info[simp]:
‹init_clss (update_additional_info w S) = init_clss S› and
learned_clss_update_additional_info[simp]:
‹learned_clss (update_additional_info w S) = learned_clss S› and
backtrack_lvl_update_additional_info[simp]:
‹backtrack_lvl (update_additional_info w S) = backtrack_lvl S› and
conflicting_update_additional_info[simp]:
‹conflicting (update_additional_info w S) = conflicting S› and
clauses_update_additional_info[simp]:
‹clauses (update_additional_info w S) = clauses S›
using update_additional_info[of S] unfolding clauses_def
by (subst (asm) state_prop; subst (asm) state_prop; auto; fail)+
lemma
trail_update_weight_information[simp]:
‹trail (update_weight_information w S) = trail S› and
init_clss_update_weight_information[simp]:
‹init_clss (update_weight_information w S) = init_clss S› and
learned_clss_update_weight_information[simp]:
‹learned_clss (update_weight_information w S) = learned_clss S› and
backtrack_lvl_update_weight_information[simp]:
‹backtrack_lvl (update_weight_information w S) = backtrack_lvl S› and
conflicting_update_weight_information[simp]:
‹conflicting (update_weight_information w S) = conflicting S› and
clauses_update_weight_information[simp]:
‹clauses (update_weight_information w S) = clauses S›
using update_additional_info[of S] unfolding update_weight_information_def by auto
definition covering :: ‹'st ⇒ 'v cov› where
‹covering S = fst (additional_info S)›
lemma
additional_info_update_additional_info[simp]:
"additional_info (update_additional_info w S) = w"
unfolding additional_info_def using update_additional_info[of S]
by (cases ‹state S›; auto; fail)+
lemma
covering_cons_trail2[simp]: ‹covering (cons_trail L S) = covering S› and
clss_tl_trail2[simp]: "covering (tl_trail S) = covering S" and
covering_add_learned_cls_unfolded:
"covering (add_learned_cls U S) = covering S"
and
covering_update_conflicting2[simp]: "covering (update_conflicting D S) = covering S" and
covering_remove_cls2[simp]:
"covering (remove_cls C S) = covering S" and
covering_add_learned_cls2[simp]:
"covering (add_learned_cls C S) = covering S" and
covering_update_covering_information2[simp]:
"covering (update_weight_information M S) = add_mset (lit_of `# mset M) (covering S)"
by (auto simp: update_weight_information_def covering_def)
sublocale conflict_driven_clause_learning⇩W 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
by unfold_locales
sublocale conflict_driven_clause_learning_with_adding_init_clause_cost⇩W_no_state
where
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
weight = covering and
update_weight_information = update_weight_information and
is_improving_int = is_improving_int and
conflicting_clauses = conflicting_clauses
by unfold_locales
lemma state_additional_info2':
‹state S = (trail S, init_clss S, learned_clss S, conflicting S, covering S, additional_info' S)›
unfolding additional_info'_def by (cases ‹state S›; auto simp: state_prop covering_def)
lemma state_update_weight_information:
‹state S = (M, N, U, C, w, other) ⟹
∃w'. state (update_weight_information T S) = (M, N, U, C, w', other)›
unfolding update_weight_information_def by (cases ‹state S›; auto simp: state_prop covering_def)
lemma conflicting_clss_incl_init_clss:
‹atms_of_mm (conflicting_clss S) ⊆ atms_of_mm (init_clss S)›
unfolding conflicting_clss_def conflicting_clauses_def
apply (auto simp: simple_clss_finite)
by (auto simp: simple_clss_def atms_of_ms_def split: if_splits)
lemma conflict_clss_update_weight_no_alien:
‹atms_of_mm (conflicting_clss (update_weight_information M S))
⊆ atms_of_mm (init_clss S)›
by (auto simp: conflicting_clss_def conflicting_clauses_def atms_of_ms_def
cdcl⇩W_restart_mset_state simple_clss_finite
dest: simple_clssE)
lemma distinct_mset_mset_conflicting_clss2: ‹distinct_mset_mset (conflicting_clss S)›
unfolding conflicting_clss_def conflicting_clauses_def distinct_mset_set_def
apply (auto simp: simple_clss_finite)
by (auto simp: simple_clss_def)
lemma total_over_m_atms_incl:
assumes ‹total_over_m M (set_mset N)›
shows
‹x ∈ atms_of_mm N ⟹ x ∈ atms_of_s M›
by (meson assms contra_subsetD total_over_m_alt_def)
lemma negate_ann_lits_simple_clss_iff[iff]:
‹negate_ann_lits M ∈ simple_clss N ⟷ lit_of `# mset M ∈ simple_clss N›
unfolding negate_ann_lits_def
by (subst uminus_simple_clss_iff[symmetric]) auto
lemma conflicting_clss_update_weight_information_in2:
assumes ‹is_improving M M' S›
shows ‹negate_ann_lits M' ∈# conflicting_clss (update_weight_information M' S)›
proof -
have
[simp]: ‹M' = M› and
‹∀I∈#covering S. ¬ model_is_dominated (lit_of `# mset M) I› and
tot: ‹total_over_m (lits_of_l M) (set_mset (init_clss S))› and
simpI: ‹lit_of `# mset M ∈ simple_clss (atms_of_mm (init_clss S))› and
‹lit_of `# mset M ∉# covering S› and
‹no_dup M› and
‹M ⊨asm init_clss S›
using assms unfolding is_improving_int_def by auto
have ‹pNeg {#L ∈# lit_of `# mset M. ρ (atm_of L)#}
∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm (init_clss S)).
is_dominating (add_mset (lit_of `# mset M) (covering S)) x}›
using is_dominating_in[of ‹lit_of `# mset M› ‹add_mset (lit_of `# mset M) (covering S)›]
by (auto simp: simple_clss_finite multiset_filter_mono2 pNeg_mono
conflicting_clauses_def conflicting_clss_def is_improving_int_def
simpI)
moreover have ‹atms_of (lit_of `# mset M) = atms_of_mm (init_clss S)›
using tot simpI
by (auto simp: simple_clss_finite multiset_filter_mono2 pNeg_mono
conflicting_clauses_def conflicting_clss_def is_improving_int_def
total_over_m_alt_def atms_of_s_def lits_of_def image_image atms_of_def
simple_clss_def)
ultimately have ‹(∃x. x ∈ simple_clss (atms_of_mm (init_clss S)) ∧
is_dominating (add_mset (lit_of `# mset M) (covering S)) x ∧
atms_of x = atms_of_mm (init_clss S) ∧
pNeg {#L ∈# lit_of `# mset M. ρ (atm_of L)#} =
pNeg {#L ∈# x. ρ (atm_of L)#})›
by (auto intro: exI[of _ ‹lit_of `# mset M›] simp add: simpI is_dominating_in)
then show ?thesis
using is_dominating_in
true_clss_cls_in_susbsuming[of ‹pNeg {#L ∈# lit_of `# mset M. ρ (atm_of L)#}›
‹pNeg (lit_of `# mset M)› ‹set_mset (conflicting_clauses_ent
(init_clss S) (covering (update_weight_information M' S)))›]
by (auto simp: simple_clss_finite multiset_filter_mono2 simpI
conflicting_clauses_def conflicting_clss_def pNeg_mono
negate_ann_lits_pNeg_lit_of image_iff image_mset_subseteq_mono)
qed
lemma is_improving_conflicting_clss_update_weight_information: ‹is_improving M M' S ⟹
conflicting_clss S ⊆# conflicting_clss (update_weight_information M' S)›
by (auto simp: is_improving_int_def conflicting_clss_def conflicting_clauses_def
simp: multiset_filter_mono2 le_less true_clss_cls_tautology_iff simple_clss_finite
is_dominating_add_mset filter_disj_eq image_Un
intro!: image_mset_subseteq_mono
intro: true_clss_cls_subsetI
dest: simple_clssE
split: enat.splits)
sublocale state⇩W_no_state
where
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
by unfold_locales
sublocale state⇩W_no_state 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
by unfold_locales
sublocale conflict_driven_clause_learning⇩W 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
by unfold_locales
sublocale conflict_driven_clause_learning_with_adding_init_clause_cost⇩W_ops
where
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
weight = covering and
update_weight_information = update_weight_information and
is_improving_int = is_improving_int and
conflicting_clauses = conflicting_clauses
apply unfold_locales
subgoal by (rule state_additional_info2')
subgoal by (rule state_update_weight_information)
subgoal by (rule conflicting_clss_incl_init_clss)
subgoal by (rule distinct_mset_mset_conflicting_clss2)
subgoal by (rule is_improving_conflicting_clss_update_weight_information)
subgoal by (rule conflicting_clss_update_weight_information_in2)
done
definition covering_simple_clss where
‹covering_simple_clss N S ⟷ (set_mset (covering S) ⊆ simple_clss (atms_of_mm N)) ∧
distinct_mset (covering S) ∧
(∀M ∈# covering S. total_over_m (set_mset M) (set_mset N))›
lemma [simp]: ‹covering (init_state N) = {#}›
by (simp add: covering_def weight_init_state)
lemma ‹covering_simple_clss N (init_state N)›
by (auto simp: covering_simple_clss_def)
lemma cdcl_bnb_covering_simple_clss:
‹cdcl_bnb S T ⟹ init_clss S = N ⟹ covering_simple_clss N S ⟹ covering_simple_clss N T›
by (auto simp: cdcl_bnb.simps covering_simple_clss_def is_improving_int_def
model_is_dominated_refl ocdcl⇩W_o.simps cdcl_bnb_bj.simps
lits_of_def
elim!: rulesE improveE conflict_optE obacktrackE
dest!: multi_member_split[of _ ‹covering S›])
lemma rtranclp_cdcl_bnb_covering_simple_clss:
‹cdcl_bnb⇧*⇧* S T ⟹ init_clss S = N ⟹ covering_simple_clss N S ⟹ covering_simple_clss N T›
by (induction rule: rtranclp_induct)
(auto simp: cdcl_bnb_covering_simple_clss simp: rtranclp_cdcl_bnb_no_more_init_clss
cdcl_bnb_no_more_init_clss)
lemma wf_cdcl_bnb_fixed:
‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ∧ cdcl_bnb S T
∧ covering_simple_clss N S ∧ init_clss S = N}›
apply (rule wf_cdcl_bnb_with_additional_inv[of
‹covering_simple_clss N›
N id ‹{(T, S). (T, S) ∈ {(ℳ', ℳ). ℳ ⊂# ℳ' ∧ distinct_mset ℳ'
∧ set_mset ℳ' ⊆ simple_clss (atms_of_mm N)}}›])
subgoal
by (auto simp: improvep.simps is_improving_int_def covering_simple_clss_def
add_mset_eq_add_mset model_is_dominated_refl
dest!: multi_member_split)
subgoal
apply (rule wf_bounded_set[of _ ‹λ_. simple_clss (atms_of_mm N)› set_mset])
apply (auto simp: distinct_mset_subset_iff_remdups[symmetric] simple_clss_finite
simp flip: remdups_mset_def)
by (metis distinct_mset_mono distinct_mset_set_mset_ident)
subgoal
by (rule cdcl_bnb_covering_simple_clss)
done
lemma can_always_improve:
assumes
ent: ‹trail S ⊨asm clauses S› and
total: ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))› and
n_s: ‹no_step conflict_opt S› and
confl: ‹conflicting S = None› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹Ex (improvep S)›
proof -
have ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)› and
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)›
using all_struct
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then have n_d: ‹no_dup (trail S)›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
have [simp]:
‹atms_of_mm (CDCL_W_Abstract_State.init_clss (abs_state S)) = atms_of_mm (init_clss S)›
unfolding abs_state_def init_clss.simps
by auto
let ?M = ‹(lit_of `# mset (trail S))›
have trail_simple: ‹?M ∈ simple_clss (atms_of_mm (init_clss S))›
using n_d alien
by (auto simp: simple_clss_def cdcl⇩W_restart_mset.no_strange_atm_def
lits_of_def image_image atms_of_def
dest: distinct_consistent_interp no_dup_not_tautology
no_dup_distinct)
then have [simp]: ‹atms_of ?M = atms_of_mm (init_clss S)›
using total
by (auto simp: total_over_m_alt_def simple_clss_def atms_of_def image_image
lits_of_def atms_of_s_def clauses_def)
then have K: ‹is_dominating (covering S) ?M ⟹ pNeg {#L ∈# lit_of `# mset (trail S). ρ (atm_of L)#}
∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm (init_clss S)).
is_dominating (covering S) x ∧
atms_of x = atms_of_mm (init_clss S)}›
by (auto simp: image_iff trail_simple
intro!: exI[of _ ‹lit_of `# mset (trail S)›])
have H: ‹I ∈# covering S ⟹
model_is_dominated ?M I ⟹
pNeg {#L ∈# ?M. ρ (atm_of L)#}
∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm (init_clss S)).
is_dominating (covering S) x}› for I
using is_dominating_in[of ‹lit_of `# mset M› ‹add_mset (lit_of `# mset M) (covering S)›]
trail_simple
by (auto 5 5 simp: simple_clss_finite multiset_filter_mono2 pNeg_mono
conflicting_clauses_def conflicting_clss_def is_improving_int_def
is_dominating_add_mset filter_disj_eq image_Un
dest!: multi_member_split)
have ‹I ∈# covering S ⟹
model_is_dominated ?M I ⟹ False› for I
using n_s confl H[of I] K
true_clss_cls_in_susbsuming[of ‹pNeg {#L ∈# ?M. ρ (atm_of L)#}›
‹pNeg ?M› ‹set_mset (conflicting_clauses_ent
(init_clss S) (covering S))›]
by (auto simp: conflict_opt.simps simple_clss_finite
conflicting_clss_def conflicting_clauses_def is_dominating_def
is_dominating_add_mset filter_disj_eq image_Un pNeg_mono
multiset_filter_mono2 negate_ann_lits_pNeg_lit_of
intro: trail_simple)
moreover have False if ‹lit_of `# mset (trail S) ∈# covering S›
using n_s confl that trail_simple by (auto simp: conflict_opt.simps
conflicting_clauses_insert conflicting_clss_def simple_clss_finite
negate_ann_lits_pNeg_lit_of
dest!: multi_member_split)
ultimately have imp: ‹is_improving (trail S) (trail S) S›
unfolding is_improving_int_def
using assms trail_simple n_d by (auto simp: clauses_def)
show ?thesis
by (rule exI) (rule improvep.intros[OF imp confl state_eq_ref])
qed
lemma exists_model_with_true_lit_entails_conflicting:
assumes
L_I: ‹Pos L ∈ I› and
L: ‹ρ L› and
L_in: ‹L ∈ atms_of_mm (init_clss S)› and
ent: ‹I ⊨m init_clss S› and
cons: ‹consistent_interp I› and
total: ‹total_over_m I (set_mset N)› and
no_L: ‹¬(∃J∈# covering S. Pos L ∈# J)› and
cov: ‹covering_simple_clss N S› and
NS: ‹atms_of_mm N = atms_of_mm (init_clss S)›
shows ‹I ⊨m conflicting_clss S› and
‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state S)›
proof -
show ‹I ⊨m conflicting_clss S›
unfolding conflicting_clss_def conflicting_clauses_def
set_mset_filter true_cls_mset_def
proof
fix C
assume ‹C ∈ {a. a ∈# mset_set (simple_clss (atms_of_mm (init_clss S))) ∧
{#pNeg {#L ∈# x. ρ (atm_of L)#}.
x ∈# {#x ∈# mset_set (simple_clss (atms_of_mm (init_clss S))).
is_dominating (covering S) x ∧
atms_of x = atms_of_mm (init_clss S)#}#} +
init_clss S ⊨pm
a}›
then have simp_C: ‹C ∈ simple_clss (atms_of_mm (init_clss S))› and
ent_C: ‹(λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm (init_clss S)). is_dominating (covering S) x ∧
atms_of x = atms_of_mm (init_clss S)} ∪
set_mset (init_clss S) ⊨p C›
by (auto simp: simple_clss_finite)
have tot_I2: ‹total_over_m I
((λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm (init_clss S)).
is_dominating (covering S) x ∧
atms_of x = atms_of_mm (init_clss S)} ∪
set_mset (init_clss S) ∪
{C}) ⟷ total_over_m I (set_mset N)› for I
using simp_C NS[symmetric]
by (auto simp: total_over_m_def total_over_set_def
simple_clss_def atms_of_ms_def atms_of_def pNeg_def
dest!: multi_member_split)
have ‹I ⊨s (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm (init_clss S)). is_dominating (covering S) x ∧
atms_of x = atms_of_mm (init_clss S)}›
unfolding NS[symmetric]
total_over_m_alt_def true_clss_def
proof
fix D
assume ‹D ∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm N). is_dominating (covering S) x ∧
atms_of x = atms_of_mm N}›
then obtain x where
D: ‹D = pNeg {#L ∈# x. ρ (atm_of L)#}› and
x: ‹x ∈ simple_clss (atms_of_mm N)› and
dom: ‹is_dominating (covering S) x› and
tot_x: ‹atms_of x = atms_of_mm N›
by auto
then have ‹L ∈ atms_of x›
using cov L_in no_L
unfolding NS[symmetric]
by (auto simp: true_clss_def is_dominating_def model_is_dominated_def
covering_simple_clss_def atms_of_def pNeg_def image_image
total_over_m_alt_def atms_of_s_def
dest!: multi_member_split)
then have ‹Neg L ∈# x›
using no_L dom L unfolding atm_iff_pos_or_neg_lit
by (auto simp: is_dominating_def model_is_dominated_def insert_subset_eq_iff
dest!: multi_member_split)
then have ‹Pos L ∈# D›
using L
by (auto simp: pNeg_def image_image D image_iff
dest!: multi_member_split)
then show ‹I ⊨ D›
using L_I by (auto dest: multi_member_split)
qed
then show ‹I ⊨ C›
using total cons ent_C ent
unfolding true_clss_cls_def tot_I2
by auto
qed
then show I_S: ‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state S)›
using ent
by (auto simp: abs_state_def init_clss.simps)
qed
lemma exists_model_with_true_lit_still_model:
assumes
L_I: ‹Pos L ∈ I› and
L: ‹ρ L› and
L_in: ‹L ∈ atms_of_mm (init_clss S)› and
ent: ‹I ⊨m init_clss S› and
cons: ‹consistent_interp I› and
total: ‹total_over_m I (set_mset N)› and
cdcl: ‹cdcl_bnb S T› and
no_L_T: ‹¬(∃J∈# covering T. Pos L ∈# J)› and
cov: ‹covering_simple_clss N S› and
NS: ‹atms_of_mm N = atms_of_mm (init_clss S)›
shows ‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state T)›
proof -
have no_L: ‹¬(∃J∈# covering S. Pos L ∈# J)›
using cdcl no_L_T
by (cases) (auto elim!: rulesE improveE conflict_optE obacktrackE
simp: ocdcl⇩W_o.simps cdcl_bnb_bj.simps)
have I_S: ‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state S)›
by (rule exists_model_with_true_lit_entails_conflicting[OF assms(1-6) no_L assms(9) NS])
have I_T': ‹I ⊨m conflicting_clss (update_weight_information M' S)›
if T: ‹T ∼ update_weight_information M' S› for M'
unfolding conflicting_clss_def conflicting_clauses_def
set_mset_filter true_cls_mset_def
proof
let ?T = ‹update_weight_information M' S›
fix C
assume ‹C ∈ {a. a ∈# mset_set (simple_clss (atms_of_mm (init_clss ?T))) ∧
{#pNeg {#L ∈# x. ρ (atm_of L)#}.
x ∈# {#x ∈# mset_set (simple_clss (atms_of_mm (init_clss ?T))).
is_dominating (covering ?T) x ∧
atms_of x = atms_of_mm (init_clss ?T)#}#} +
init_clss ?T ⊨pm
a}›
then have simp_C: ‹C ∈ simple_clss (atms_of_mm (init_clss ?T))› and
ent_C: ‹(λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm (init_clss ?T)). is_dominating (covering ?T) x ∧
atms_of x = atms_of_mm (init_clss ?T)} ∪
set_mset (init_clss ?T) ⊨p C›
by (auto simp: simple_clss_finite)
have tot_I2: ‹total_over_m I
((λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm (init_clss ?T)).
is_dominating (covering ?T) x ∧
atms_of x = atms_of_mm (init_clss ?T)} ∪
set_mset (init_clss ?T) ∪
{C}) ⟷ total_over_m I (set_mset N)› for I
using simp_C NS[symmetric]
by (auto simp: total_over_m_def total_over_set_def
simple_clss_def atms_of_ms_def atms_of_def pNeg_def
dest!: multi_member_split)
have H: ‹atms_of_mm (init_clss (update_weight_information M' S)) = atms_of_mm N›
by (auto simp: NS)
have ‹I ⊨s (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm (init_clss ?T)). is_dominating (covering ?T) x ∧
atms_of x = atms_of_mm (init_clss ?T)}›
unfolding NS[symmetric] H
total_over_m_alt_def true_clss_def
proof
fix D
assume ‹D ∈ (λx. pNeg {#L ∈# x. ρ (atm_of L)#}) `
{x ∈ simple_clss (atms_of_mm N). is_dominating (covering ?T) x ∧
atms_of x = atms_of_mm N}›
then obtain x where
D: ‹D = pNeg {#L ∈# x. ρ (atm_of L)#}› and
x: ‹x ∈ simple_clss (atms_of_mm N)› and
dom: ‹is_dominating (covering ?T) x› and
tot_x: ‹atms_of x = atms_of_mm N›
by auto
then have ‹L ∈ atms_of x›
using cov L_in no_L
unfolding NS[symmetric]
by (auto simp: true_clss_def is_dominating_def model_is_dominated_def
covering_simple_clss_def atms_of_def pNeg_def image_image
total_over_m_alt_def atms_of_s_def
dest!: multi_member_split)
then have ‹Neg L ∈# x›
using no_L_T dom L T unfolding atm_iff_pos_or_neg_lit
by (auto simp: is_dominating_def model_is_dominated_def insert_subset_eq_iff
dest!: multi_member_split)
then have ‹Pos L ∈# D›
using L
by (auto simp: pNeg_def image_image D image_iff
dest!: multi_member_split)
then show ‹I ⊨ D›
using L_I by (auto dest: multi_member_split)
qed
then show ‹I ⊨ C›
using total cons ent_C ent
unfolding true_clss_cls_def tot_I2
by auto
qed
show ?thesis
using cdcl
proof (cases)
case cdcl_conflict
then show ?thesis using I_S by (auto elim!: conflictE)
next
case cdcl_propagate
then show ?thesis using I_S by (auto elim!: rulesE)
next
case cdcl_improve
show ?thesis
using I_S cdcl_improve I_T'
by (auto simp: abs_state_def init_clss.simps
elim!: improveE)
next
case cdcl_conflict_opt
then show ?thesis using I_S by (auto elim!: conflict_optE)
next
case cdcl_other'
then show ?thesis using I_S by (auto elim!: rulesE obacktrackE simp: ocdcl⇩W_o.simps cdcl_bnb_bj.simps)
qed
qed
lemma rtranclp_exists_model_with_true_lit_still_model:
assumes
L_I: ‹Pos L ∈ I› and
L: ‹ρ L› and
L_in: ‹L ∈ atms_of_mm (init_clss S)› and
ent: ‹I ⊨m init_clss S› and
cons: ‹consistent_interp I› and
total: ‹total_over_m I (set_mset N)› and
cdcl: ‹cdcl_bnb⇧*⇧* S T› and
cov: ‹covering_simple_clss N S› and
‹N = init_clss S›
shows ‹I ⊨m CDCL_W_Abstract_State.init_clss (abs_state T) ∨ (∃J∈# covering T. Pos L ∈# J)›
using cdcl assms
apply (induction rule: rtranclp_induct)
subgoal using exists_model_with_true_lit_entails_conflicting[of L I S N]
by auto
subgoal for T U
apply (rule disjCI)
apply (rule exists_model_with_true_lit_still_model[OF L_I L _ _ cons total, of T U])
by (auto dest: rtranclp_cdcl_bnb_no_more_init_clss
intro: rtranclp_cdcl_bnb_covering_simple_clss cdcl_bnb_covering_simple_clss)
done
lemma is_dominating_nil[simp]: ‹¬is_dominating {#} x›
by (auto simp: is_dominating_def)
lemma atms_of_conflicting_clss_init_state:
‹atms_of_mm (conflicting_clss (init_state N)) ⊆ atms_of_mm N›
by (auto simp: conflicting_clss_def conflicting_clauses_def
atms_of_ms_def simple_clss_finite
dest!: simple_clssE)
lemma no_step_cdcl_bnb_stgy_empty_conflict2:
assumes
n_s: ‹no_step cdcl_bnb S› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
stgy_inv: ‹cdcl_bnb_stgy_inv S›
shows ‹conflicting S = Some {#}›
by (rule no_step_cdcl_bnb_stgy_empty_conflict[OF can_always_improve assms])
theorem cdclcm_correctness:
assumes
full: ‹full cdcl_bnb_stgy (init_state N) T› and
dist: ‹distinct_mset_mset N›
shows
‹Pos L ∈ I ⟹ ρ L ⟹ L ∈ atms_of_mm N ⟹ total_over_m I (set_mset N) ⟹ consistent_interp I ⟹ I ⊨m N ⟹
∃J ∈# covering T. Pos L ∈# J›
proof -
let ?S = ‹init_state N›
have ns: ‹no_step cdcl_bnb_stgy T› and
st: ‹cdcl_bnb_stgy⇧*⇧* ?S T› and
st': ‹cdcl_bnb⇧*⇧* ?S T›
using full unfolding full_def by (auto intro: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
have ns': ‹no_step cdcl_bnb T›
by (meson cdcl_bnb.cases cdcl_bnb_stgy.simps no_confl_prop_impr.elims(3) ns)
have ‹distinct_mset C› if ‹C ∈# N› for C
using dist that by (auto simp: distinct_mset_set_def dest: multi_member_split)
then have dist: ‹distinct_mset_mset (N)›
by (auto simp: distinct_mset_set_def)
then have [simp]: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv ([], N, {#}, None)›
unfolding init_state.simps[symmetric]
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def)
have [iff]: ‹cdcl_bnb_struct_invs ?S›
using atms_of_conflicting_clss_init_state[of N]
by (auto simp: cdcl_bnb_struct_invs_def)
have stgy_inv: ‹cdcl_bnb_stgy_inv ?S›
by (auto simp: cdcl_bnb_stgy_inv_def conflict_is_false_with_level_def)
have ent: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (abs_state ?S)›
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def)
have all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state (init_state N))›
unfolding CDCL_W_Abstract_State.init_state.simps abs_state_def
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def dist
cdcl⇩W_restart_mset.no_strange_atm_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def distinct_mset_mset_conflicting_clss
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def)
have cdcl: ‹cdcl_bnb⇧*⇧* ?S T›
using st rtranclp_cdcl_bnb_stgy_cdcl_bnb unfolding full_def by blast
have cov: ‹covering_simple_clss N ?S›
by (auto simp: covering_simple_clss_def)
have struct_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
have stgy_T: ‹cdcl_bnb_stgy_inv T›
using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
have confl: ‹conflicting T = Some {#}›
using no_step_cdcl_bnb_stgy_empty_conflict2[OF ns' struct_T stgy_T] .
have tot_I: ‹total_over_m I (set_mset (clauses T + conflicting_clss T)) ⟷
total_over_m I (set_mset (init_clss T + conflicting_clss T))› for I
using struct_T atms_of_conflicting_clss[of T]
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def satisfiable_def
cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: clauses_def satisfiable_def total_over_m_alt_def
abs_state_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.clauses_def)
have ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
using full_cdcl_bnb_stgy_unsat[OF _ full all_struct _ stgy_inv]
by (auto simp: can_always_improve)
have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init
(abs_state T)›
using rtranclp_cdcl_bnb_cdcl⇩W_learned_clauses_entailed_by_init[OF st' ent all_struct] .
then have ‹init_clss T + conflicting_clss T ⊨pm {#}›
using struct_T confl
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
cdcl⇩W_restart_mset.no_strange_atm_def tot_I
cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
by (auto simp: clauses_def abs_state_def cdcl⇩W_restart_mset_state
cdcl⇩W_restart_mset.clauses_def
satisfiable_def dest: true_clss_clss_left_right)
then have unsat: ‹unsatisfiable (set_mset (init_clss T + conflicting_clss T))›
by (auto simp: clauses_def true_clss_cls_def
satisfiable_def)
assume
L_I: ‹Pos L ∈ I› and
L: ‹ρ L› and
L_N: ‹L ∈ atms_of_mm N› and
tot_I: ‹total_over_m I (set_mset N)› and
cons: ‹consistent_interp I› and
I_N: ‹I ⊨m N›
show ‹Multiset.Bex (covering T) ((∈#) (Pos L))›
using rtranclp_exists_model_with_true_lit_still_model[OF L_I L _ _ _ _ cdcl, of N] L_N
I_N tot_I cons cov unsat
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
qed
end
text ‹Now we instantiate the previous with \<^term>‹λ_. True›: This means that we aim at making
all variables that appears at least ones true.›
global_interpretation cover_all_vars: covering_models ‹λ_. True›
.
context conflict_driven_clause_learning⇩W_covering_models
begin
interpretation cover_all_vars: conflict_driven_clause_learning⇩W_covering_models where
ρ = ‹λ_::'v. True› 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
by standard
lemma
‹cover_all_vars.model_is_dominated M M' ⟷
filter_mset (λL. is_pos L) M ⊆# filter_mset (λL. is_pos L) M'›
unfolding cover_all_vars.model_is_dominated_def
by auto
lemma
‹cover_all_vars.conflicting_clauses N ℳ =
{# C ∈# (mset_set (simple_clss (atms_of_mm N))).
(pNeg `
{a. a ∈# mset_set (simple_clss (atms_of_mm N)) ∧
(∃M∈#ℳ. ∃J. a ⊆# J ∧ cover_all_vars.model_is_dominated J M) ∧
atms_of a = atms_of_mm N} ∪
set_mset N) ⊨p C#}›
unfolding cover_all_vars.conflicting_clauses_def
cover_all_vars.is_dominating_def
by auto
theorem cdclcm_correctness_all_vars:
assumes
full: ‹full cover_all_vars.cdcl_bnb_stgy (init_state N) T› and
dist: ‹distinct_mset_mset N›
shows
‹Pos L ∈ I ⟹ L ∈ atms_of_mm N ⟹ total_over_m I (set_mset N) ⟹ consistent_interp I ⟹ I ⊨m N ⟹
∃J ∈# covering T. Pos L ∈# J›
using cover_all_vars.cdclcm_correctness[OF assms]
by blast
end
end