theory DPLL_W_Optimal_Model
imports
CDCL_W_Optimal_Model
CDCL.DPLL_W
begin
lemma [simp]: ‹backtrack_split M1 = (M', L # M) ⟹ is_decided L›
by (metis backtrack_split_snd_hd_decided list.sel(1) list.simps(3) snd_conv)
lemma funpow_tl_append_skip_ge:
‹n ≥ length M' ⟹ ((tl ^^ n) (M' @ M)) = (tl ^^ (n - length M')) M›
apply (induction n arbitrary: M')
subgoal by auto
subgoal for n M'
by (cases M')
(auto simp del: funpow.simps(2) simp: funpow_Suc_right)
done
text ‹The following version is more suited than @{thm backtrack_split_some_is_decided_then_snd_has_hd}
for direct use.›
lemma backtrack_split_some_is_decided_then_snd_has_hd':
‹l∈set M ⟹ is_decided l ⟹ ∃M' L' M''. backtrack_split M = (M'', L' # M')›
by (metis backtrack_snd_empty_not_decided list.exhaust prod.collapse)
lemma total_over_m_entailed_or_conflict:
shows ‹total_over_m M N ⟹ M ⊨s N ∨ (∃C ∈ N. M ⊨s CNot C)›
by (metis Set.set_insert total_not_true_cls_true_clss_CNot total_over_m_empty total_over_m_insert true_clss_def)
text ‹The locales on DPLL should eventually be moved to the DPLL theory, but currently it is only a discount
version (in particular, we cheat and don't use \<^text>‹S ∼ T› in the transition system below, even if it
would be cleaner to do as as we de for CDCL).
›
locale dpll_ops =
fixes
trail :: ‹'st ⇒ 'v dpll⇩W_ann_lits› and
clauses :: ‹'st ⇒ 'v clauses› and
tl_trail :: ‹'st ⇒ 'st› and
cons_trail :: ‹'v dpll⇩W_ann_lit ⇒ 'st ⇒ 'st› and
state_eq :: ‹'st ⇒ 'st ⇒ bool› (infix "∼" 50) and
state :: ‹'st ⇒ 'v dpll⇩W_ann_lits × 'v clauses × 'b›
begin
definition additional_info :: ‹'st ⇒ 'b› where
‹additional_info S = (λ(M, N, w). w) (state S)›
definition reduce_trail_to :: ‹'v dpll⇩W_ann_lits ⇒ 'st ⇒ 'st› where
‹reduce_trail_to M S = (tl_trail ^^ (length (trail S) - length M)) S›
end
locale bnb_ops =
fixes
trail :: ‹'st ⇒ 'v dpll⇩W_ann_lits› and
clauses :: ‹'st ⇒ 'v clauses› and
tl_trail :: ‹'st ⇒ 'st› and
cons_trail :: ‹'v dpll⇩W_ann_lit ⇒ 'st ⇒ 'st› and
state_eq :: ‹'st ⇒ 'st ⇒ bool› (infix "∼" 50) and
state :: ‹'st ⇒ 'v dpll⇩W_ann_lits × 'v clauses × 'a × 'b› and
weight :: ‹'st ⇒ 'a› and
update_weight_information :: "'v dpll⇩W_ann_lits ⇒ 'st ⇒ 'st" and
is_improving_int :: "'v dpll⇩W_ann_lits ⇒ 'v dpll⇩W_ann_lits ⇒ 'v clauses ⇒ 'a ⇒ bool" and
conflicting_clauses :: "'v clauses ⇒ 'a ⇒ 'v clauses"
begin
interpretation dpll: dpll_ops where
trail = trail and
clauses = clauses and
tl_trail = tl_trail and
cons_trail = cons_trail and
state_eq = state_eq and
state = state
.
definition conflicting_clss :: ‹'st ⇒ 'v literal multiset multiset› where
‹conflicting_clss S = conflicting_clauses (clauses S) (weight S)›
definition abs_state where
‹abs_state S = (trail S, clauses S + conflicting_clss S)›
abbreviation is_improving where
‹is_improving M M' S ≡ is_improving_int M M' (clauses S) (weight S)›
definition state' :: ‹'st ⇒ 'v dpll⇩W_ann_lits × 'v clauses × 'a × 'v clauses› where
‹state' S = (trail S, clauses S, weight S, conflicting_clss S)›
definition additional_info :: ‹'st ⇒ 'b› where
‹additional_info S = (λ(M, N, _, w). w) (state S)›
end
locale dpll⇩W_state =
dpll_ops trail clauses
tl_trail cons_trail state_eq state
for
trail :: ‹'st ⇒ 'v dpll⇩W_ann_lits› and
clauses :: ‹'st ⇒ 'v clauses› and
tl_trail :: ‹'st ⇒ 'st› and
cons_trail :: ‹'v dpll⇩W_ann_lit ⇒ 'st ⇒ 'st› and
state_eq :: ‹'st ⇒ 'st ⇒ bool› (infix "∼" 50) and
state :: ‹'st ⇒ 'v dpll⇩W_ann_lits × 'v clauses × 'b› +
assumes
state_eq_ref[simp, intro]: ‹S ∼ S› and
state_eq_sym: ‹S ∼ T ⟷ T ∼ S› and
state_eq_trans: ‹S ∼ T ⟹ T ∼ U' ⟹ S ∼ U'› and
state_eq_state: ‹S ∼ T ⟹ state S = state T› and
cons_trail:
"⋀S'. state st = (M, S') ⟹
state (cons_trail L st) = (L # M, S')" and
tl_trail:
"⋀S'. state st = (M, S') ⟹ state (tl_trail st) = (tl M, S')" and
state:
‹state S = (trail S, clauses S, additional_info S)›
begin
lemma [simp]:
‹clauses (cons_trail uu S) = clauses S›
‹trail (cons_trail uu S) = uu # trail S›
‹trail (tl_trail S) = tl (trail S)›
‹clauses (tl_trail S) = clauses (S)›
‹additional_info (cons_trail L S) = additional_info S›
‹additional_info (tl_trail S) = additional_info S›
using
cons_trail[of S]
tl_trail[of S]
by (auto simp: state)
lemma state_simp[simp]:
‹T ∼ S ⟹ trail T = trail S›
‹T ∼ S ⟹ clauses T = clauses S›
by (auto dest!: state_eq_state simp: state)
lemma state_tl_trail: ‹state (tl_trail S) = (tl (trail S), clauses S, additional_info S)›
by (auto simp: state)
lemma state_tl_trail_comp_pow: ‹state ((tl_trail ^^ n) S) = ((tl ^^ n) (trail S), clauses S, additional_info S)›
apply (induction n)
using state apply fastforce
apply (auto simp: state_tl_trail state)[]
done
lemma reduce_trail_to_simps[simp]:
‹backtrack_split (trail S) = (M', L # M) ⟹ trail (reduce_trail_to M S) = M›
‹clauses (reduce_trail_to M S) = clauses S›
‹additional_info (reduce_trail_to M S) = additional_info S›
using state_tl_trail_comp_pow[of ‹Suc (length M')› S] backtrack_split_list_eq[of ‹trail S›, symmetric]
unfolding reduce_trail_to_def
apply (auto simp: state funpow_tl_append_skip_ge)
using state state_tl_trail_comp_pow apply auto
done
inductive dpll_backtrack :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll_backtrack S T›
if
‹D ∈# clauses S› and
‹trail S ⊨as CNot D› and
‹backtrack_split (trail S) = (M', L # M)› and
‹T ∼cons_trail (Propagated (-lit_of L) ()) (reduce_trail_to M S)›
inductive dpll_propagate :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll_propagate S T›
if
‹add_mset L D ∈# clauses S› and
‹trail S ⊨as CNot D› and
‹undefined_lit (trail S) L›
‹T ∼ cons_trail (Propagated L ()) S›
inductive dpll_decide :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll_decide S T›
if
‹undefined_lit (trail S) L›
‹T ∼ cons_trail (Decided L) S›
‹atm_of L ∈ atms_of_mm (clauses S)›
inductive dpll :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll S T› if ‹dpll_decide S T› |
‹dpll S T› if ‹dpll_propagate S T› |
‹dpll S T› if ‹dpll_backtrack S T›
lemma dpll_is_dpll⇩W:
‹dpll S T ⟹ dpll⇩W (trail S, clauses S) (trail T, clauses T)›
apply (induction rule: dpll.induct)
subgoal for S T
apply (auto simp: dpll.simps dpll⇩W.simps dpll_decide.simps dpll_backtrack.simps dpll_propagate.simps
dest!: multi_member_split[of _ ‹clauses S›])
done
subgoal for S T
unfolding dpll.simps dpll⇩W.simps dpll_decide.simps dpll_backtrack.simps dpll_propagate.simps
by auto
subgoal for S T
unfolding dpll⇩W.simps dpll_decide.simps dpll_backtrack.simps dpll_propagate.simps
by (auto simp: state)
done
end
locale bnb =
bnb_ops trail clauses
tl_trail cons_trail state_eq state weight update_weight_information is_improving_int conflicting_clauses
for
weight :: ‹'st ⇒ 'a› and
update_weight_information :: "'v dpll⇩W_ann_lits ⇒ 'st ⇒ 'st" and
is_improving_int :: "'v dpll⇩W_ann_lits ⇒ 'v dpll⇩W_ann_lits ⇒ 'v clauses ⇒ 'a ⇒ bool" and
trail :: ‹'st ⇒ 'v dpll⇩W_ann_lits› and
clauses :: ‹'st ⇒ 'v clauses› and
tl_trail :: ‹'st ⇒ 'st› and
cons_trail :: ‹'v dpll⇩W_ann_lit ⇒ 'st ⇒ 'st› and
state_eq :: ‹'st ⇒ 'st ⇒ bool› (infix "∼" 50) and
conflicting_clauses :: "'v clauses ⇒ 'a ⇒ 'v clauses"and
state :: ‹'st ⇒ 'v dpll⇩W_ann_lits × 'v clauses × 'a × 'b› +
assumes
state_eq_ref[simp, intro]: ‹S ∼ S› and
state_eq_sym: ‹S ∼ T ⟷ T ∼ S› and
state_eq_trans: ‹S ∼ T ⟹ T ∼ U' ⟹ S ∼ U'› and
state_eq_state: ‹S ∼ T ⟹ state S = state T› and
cons_trail:
"⋀S'. state st = (M, S') ⟹
state (cons_trail L st) = (L # M, S')" and
tl_trail:
"⋀S'. state st = (M, S') ⟹ state (tl_trail st) = (tl M, S')" and
update_weight_information:
‹state S = (M, N, w, oth) ⟹
∃w'. state (update_weight_information M' S) = (M, N, w', oth)› and
conflicting_clss_update_weight_information_mono:
‹dpll⇩W_all_inv (abs_state S) ⟹ is_improving M M' S ⟹
conflicting_clss S ⊆# conflicting_clss (update_weight_information M' S)› and
conflicting_clss_update_weight_information_in:
‹is_improving M M' S ⟹ negate_ann_lits M' ∈# conflicting_clss (update_weight_information M' S)› and
atms_of_conflicting_clss:
‹atms_of_mm (conflicting_clss S) ⊆ atms_of_mm (clauses S)› and
state:
‹state S = (trail S, clauses S, weight S, additional_info S)›
begin
lemma [simp]: ‹DPLL_W.clauses (abs_state S) = clauses S + conflicting_clss S›
‹DPLL_W.trail (abs_state S) = trail S›
by (auto simp: abs_state_def)
lemma [simp]: ‹trail (update_weight_information M' S) = trail S›
using update_weight_information[of S]
by (auto simp: state)
lemma [simp]:
‹clauses (update_weight_information M' S) = clauses S›
‹weight (cons_trail uu S) = weight S›
‹clauses (cons_trail uu S) = clauses S›
‹conflicting_clss (cons_trail uu S) = conflicting_clss S›
‹trail (cons_trail uu S) = uu # trail S›
‹trail (tl_trail S) = tl (trail S)›
‹clauses (tl_trail S) = clauses (S)›
‹weight (tl_trail S) = weight (S)›
‹conflicting_clss (tl_trail S) = conflicting_clss (S)›
‹additional_info (cons_trail L S) = additional_info S›
‹additional_info (tl_trail S) = additional_info S›
‹additional_info (update_weight_information M' S) = additional_info S›
using update_weight_information[of S]
cons_trail[of S]
tl_trail[of S]
by (auto simp: state conflicting_clss_def)
lemma state_simp[simp]:
‹T ∼ S ⟹ trail T = trail S›
‹T ∼ S ⟹ clauses T = clauses S›
‹T ∼ S ⟹ weight T = weight S›
‹T ∼ S ⟹ conflicting_clss T = conflicting_clss S›
by (auto dest!: state_eq_state simp: state conflicting_clss_def)
interpretation dpll: dpll_ops trail clauses tl_trail cons_trail state_eq state
.
interpretation dpll: dpll⇩W_state trail clauses tl_trail cons_trail state_eq state
apply standard
apply (auto dest: state_eq_sym[THEN iffD1] intro: state_eq_trans dest: state_eq_state)
apply (auto simp: state cons_trail dpll.additional_info_def)
done
lemma [simp]:
‹conflicting_clss (dpll.reduce_trail_to M S) = conflicting_clss S›
‹weight (dpll.reduce_trail_to M S) = weight S›
using dpll.reduce_trail_to_simps(2-)[of M S] state[of S]
unfolding dpll.additional_info_def
apply (auto simp: )
by (smt conflicting_clss_def dpll.reduce_trail_to_simps(2) dpll.state dpll_ops.additional_info_def
old.prod.inject state)+
inductive backtrack_opt :: ‹'st ⇒ 'st ⇒ bool› where
backtrack_opt: "backtrack_split (trail S) = (M', L # M) ⟹ is_decided L ⟹ D ∈# conflicting_clss S
⟹ trail S ⊨as CNot D
⟹ T ∼cons_trail (Propagated (-lit_of L) ()) (dpll.reduce_trail_to M S)
⟹ backtrack_opt S T"
text ‹
In the definition below the \<^term>‹state' T = (Propagated L () # trail
S, clauses S, weight S, conflicting_clss S)› are not necessary, but
avoids to change the DPLL formalisation with proper locales, as we
did for CDCL.
The DPLL calculus looks slightly more general than the CDCL calculus
because we can take any conflicting clause from \<^term>‹conflicting_clss S›.
However, this does not make a difference for the trail, as we backtrack
to the last decision independantly of the conflict.
›
inductive dpll⇩W_core :: "'st ⇒ 'st ⇒ bool" for S T where
propagate: "dpll.dpll_propagate S T ⟹ dpll⇩W_core S T" |
decided: "dpll.dpll_decide S T ⟹ dpll⇩W_core S T " |
backtrack: "dpll.dpll_backtrack S T ⟹ dpll⇩W_core S T" |
backtrack_opt: ‹backtrack_opt S T ⟹ dpll⇩W_core S T›
inductive_cases dpll⇩W_coreE: ‹dpll⇩W_core S T›
inductive dpll⇩W_bound :: "'st ⇒ 'st ⇒ bool" where
update_info:
‹is_improving M M' S ⟹ T ∼ (update_weight_information M' S)
⟹ dpll⇩W_bound S T›
inductive dpll⇩W_bnb :: ‹'st ⇒ 'st ⇒ bool› where
dpll:
‹dpll⇩W_bnb S T›
if ‹dpll⇩W_core S T› |
bnb:
‹dpll⇩W_bnb S T›
if ‹dpll⇩W_bound S T›
inductive_cases dpll⇩W_bnbE: ‹dpll⇩W_bnb S T›
lemma dpll⇩W_core_is_dpll⇩W:
‹dpll⇩W_core S T ⟹ dpll⇩W (abs_state S) (abs_state T)›
supply abs_state_def[simp] state'_def[simp]
apply (induction rule: dpll⇩W_core.induct)
subgoal
by (auto simp: dpll⇩W.simps dpll.dpll_propagate.simps)
subgoal
by (auto simp: dpll⇩W.simps dpll.dpll_decide.simps)
subgoal
by (auto simp: dpll⇩W.simps dpll.dpll_backtrack.simps)
subgoal
by (auto simp: dpll⇩W.simps backtrack_opt.simps)
done
lemma dpll⇩W_core_abs_state_all_inv:
‹dpll⇩W_core S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ dpll⇩W_all_inv (abs_state T)›
by (auto dest!: dpll⇩W_core_is_dpll⇩W intro: dpll⇩W_all_inv)
lemma dpll⇩W_core_same_weight:
‹dpll⇩W_core S T ⟹ weight S = weight T›
supply abs_state_def[simp] state'_def[simp]
apply (induction rule: dpll⇩W_core.induct)
subgoal
by (auto simp: dpll⇩W.simps dpll.dpll_propagate.simps)
subgoal
by (auto simp: dpll⇩W.simps dpll.dpll_decide.simps)
subgoal
by (auto simp: dpll⇩W.simps dpll.dpll_backtrack.simps)
subgoal
by (auto simp: dpll⇩W.simps backtrack_opt.simps)
done
lemma dpll⇩W_bound_trail:
‹dpll⇩W_bound S T ⟹ trail S = trail T› and
dpll⇩W_bound_clauses:
‹dpll⇩W_bound S T ⟹ clauses S = clauses T› and
dpll⇩W_bound_conflicting_clss:
‹dpll⇩W_bound S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ conflicting_clss S ⊆# conflicting_clss T›
subgoal
by (induction rule: dpll⇩W_bound.induct)
(auto simp: dpll⇩W_all_inv_def state dest!: conflicting_clss_update_weight_information_mono)
subgoal
by (induction rule: dpll⇩W_bound.induct)
(auto simp: dpll⇩W_all_inv_def state dest!: conflicting_clss_update_weight_information_mono)
subgoal
by (induction rule: dpll⇩W_bound.induct)
(auto simp: state conflicting_clss_def
dest!: conflicting_clss_update_weight_information_mono)
done
lemma dpll⇩W_bound_abs_state_all_inv:
‹dpll⇩W_bound S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ dpll⇩W_all_inv (abs_state T)›
using dpll⇩W_bound_conflicting_clss[of S T] dpll⇩W_bound_clauses[of S T]
atms_of_conflicting_clss[of T] atms_of_conflicting_clss[of S]
apply (auto simp: dpll⇩W_all_inv_def dpll⇩W_bound_trail lits_of_def image_image
intro: all_decomposition_implies_mono[OF set_mset_mono] dest: dpll⇩W_bound_conflicting_clss)
by (blast intro: all_decomposition_implies_mono)
lemma dpll⇩W_bnb_abs_state_all_inv:
‹dpll⇩W_bnb S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ dpll⇩W_all_inv (abs_state T)›
by (auto elim!: dpll⇩W_bnb.cases intro: dpll⇩W_bound_abs_state_all_inv dpll⇩W_core_abs_state_all_inv)
lemma rtranclp_dpll⇩W_bnb_abs_state_all_inv:
‹dpll⇩W_bnb⇧*⇧* S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ dpll⇩W_all_inv (abs_state T)›
by (induction rule: rtranclp_induct)
(auto simp: dpll⇩W_bnb_abs_state_all_inv)
lemma dpll⇩W_core_clauses:
‹dpll⇩W_core S T ⟹ clauses S = clauses T›
supply abs_state_def[simp] state'_def[simp]
apply (induction rule: dpll⇩W_core.induct)
subgoal
by (auto simp: dpll⇩W.simps dpll.dpll_propagate.simps)
subgoal
by (auto simp: dpll⇩W.simps dpll.dpll_decide.simps)
subgoal
by (auto simp: dpll⇩W.simps dpll.dpll_backtrack.simps)
subgoal
by (auto simp: dpll⇩W.simps backtrack_opt.simps)
done
lemma dpll⇩W_bnb_clauses:
‹dpll⇩W_bnb S T ⟹ clauses S = clauses T›
by (auto elim!: dpll⇩W_bnbE simp: dpll⇩W_bound_clauses dpll⇩W_core_clauses)
lemma rtranclp_dpll⇩W_bnb_clauses:
‹dpll⇩W_bnb⇧*⇧* S T ⟹ clauses S = clauses T›
by (induction rule: rtranclp_induct)
(auto simp: dpll⇩W_bnb_clauses)
lemma atms_of_clauses_conflicting_clss[simp]:
‹atms_of_mm (clauses S) ∪ atms_of_mm (conflicting_clss S) = atms_of_mm (clauses S)›
using atms_of_conflicting_clss[of S] by blast
lemma wf_dpll⇩W_bnb_bnb:
assumes improve: ‹⋀S T. dpll⇩W_bound S T ⟹ clauses S = N ⟹ (ν (weight T), ν (weight S)) ∈ R› and
wf_R: ‹wf R›
shows ‹wf {(T, S). dpll⇩W_all_inv (abs_state S) ∧ dpll⇩W_bnb S T ∧
clauses S = N}›
(is ‹wf ?A›)
proof -
let ?R = ‹{(T, S). (ν (weight T), ν (weight S)) ∈ R}›
have ‹wf {(T, S). dpll⇩W_all_inv S ∧ dpll⇩W S T}›
by (rule wf_dpll⇩W)
from wf_if_measure_f[OF this, of abs_state]
have wf: ‹wf {(T, S). dpll⇩W_all_inv (abs_state S) ∧
dpll⇩W (abs_state S) (abs_state T) ∧ weight S = weight T}›
(is ‹wf ?CDCL›)
by (rule wf_subset) auto
have ‹wf (?R ∪ ?CDCL)›
apply (rule wf_union_compatible)
subgoal by (rule wf_if_measure_f[OF wf_R, of ‹λx. ν (weight x)›])
subgoal by (rule wf)
subgoal by (auto simp: dpll⇩W_core_same_weight)
done
moreover have ‹?A ⊆ ?R ∪ ?CDCL›
by (auto elim!: dpll⇩W_bnbE dest: dpll⇩W_core_abs_state_all_inv dpll⇩W_core_is_dpll⇩W
simp: dpll⇩W_core_same_weight improve)
ultimately show ?thesis
by (rule wf_subset)
qed
lemma [simp]:
‹weight ((tl_trail ^^ n) S) = weight S›
‹trail ((tl_trail ^^ n) S) = (tl ^^ n) (trail S)›
‹clauses ((tl_trail ^^ n) S) = clauses S›
‹conflicting_clss ((tl_trail ^^ n) S) = conflicting_clss S›
using dpll.state_tl_trail_comp_pow[of n S]
apply (auto simp: state conflicting_clss_def)
apply (metis (mono_tags, lifting) Pair_inject dpll.state state)+
done
lemma dpll⇩W_core_Ex_propagate:
‹add_mset L C ∈# clauses S ⟹ trail S ⊨as CNot C ⟹ undefined_lit (trail S) L ⟹
Ex (dpll⇩W_core S)› and
dpll⇩W_core_Ex_decide:
"undefined_lit (trail S) L ⟹ atm_of L ∈ atms_of_mm (clauses S) ⟹
Ex (dpll⇩W_core S)" and
dpll⇩W_core_Ex_backtrack: "backtrack_split (trail S) = (M', L' # M) ⟹ is_decided L' ⟹ D ∈# clauses S ⟹
trail S ⊨as CNot D ⟹ Ex (dpll⇩W_core S)" and
dpll⇩W_core_Ex_backtrack_opt: "backtrack_split (trail S) = (M', L' # M) ⟹ is_decided L' ⟹ D ∈# conflicting_clss S
⟹ trail S ⊨as CNot D ⟹
Ex (dpll⇩W_core S)"
subgoal
by (rule exI[of _ ‹cons_trail (Propagated L ()) S›])
(fastforce simp: dpll⇩W_core.simps state_eq_ref dpll.dpll_propagate.simps)
subgoal
by (rule exI[of _ ‹cons_trail (Decided L) S›])
(auto simp: dpll⇩W_core.simps state'_def dpll.dpll_decide.simps dpll.dpll_backtrack.simps
backtrack_opt.simps dpll.dpll_propagate.simps)
subgoal
using backtrack_split_list_eq[of ‹trail S›, symmetric] apply -
apply (rule exI[of _ ‹cons_trail (Propagated (-lit_of L') ()) (dpll.reduce_trail_to M S)›])
apply (auto simp: dpll⇩W_core.simps state'_def funpow_tl_append_skip_ge
dpll.dpll_decide.simps dpll.dpll_backtrack.simps backtrack_opt.simps
dpll.dpll_propagate.simps)
done
subgoal
using backtrack_split_list_eq[of ‹trail S›, symmetric] apply -
apply (rule exI[of _ ‹cons_trail (Propagated (-lit_of L') ()) (dpll.reduce_trail_to M S)›])
apply (auto simp: dpll⇩W_core.simps state'_def funpow_tl_append_skip_ge
dpll.dpll_decide.simps dpll.dpll_backtrack.simps backtrack_opt.simps
dpll.dpll_propagate.simps)
done
done
text ‹
Unlike the CDCL case, we do not need assumptions on improve. The reason behind it is that
we do not need any strategy on propagation and decisions.
›
lemma no_step_dpll_bnb_dpll⇩W:
assumes
ns: ‹no_step dpll⇩W_bnb S› and
struct_invs: ‹dpll⇩W_all_inv (abs_state S)›
shows ‹no_step dpll⇩W (abs_state S)›
proof -
have no_decide: ‹atm_of L ∈ atms_of_mm (clauses S) ⟹
defined_lit (trail S) L› for L
using spec[OF ns, of ‹cons_trail _ S›]
apply (fastforce simp: dpll⇩W_bnb.simps total_over_m_def total_over_set_def
dpll⇩W_core.simps state'_def
dpll.dpll_decide.simps dpll.dpll_backtrack.simps backtrack_opt.simps
dpll.dpll_propagate.simps)
done
have [intro]: ‹is_decided L ⟹
backtrack_split (trail S) = (M', L # M) ⟹
trail S ⊨as CNot D ⟹ D ∈# clauses S ⟹ False› for M' L M D
using dpll⇩W_core_Ex_backtrack[of S M' L M D] ns
by (auto simp: dpll⇩W_bnb.simps)
have [intro]: ‹is_decided L ⟹
backtrack_split (trail S) = (M', L # M) ⟹
trail S ⊨as CNot D ⟹ D ∈# conflicting_clss S ⟹ False› for M' L M D
using dpll⇩W_core_Ex_backtrack_opt[of S M' L M D] ns
by (auto simp: dpll⇩W_bnb.simps)
have tot: ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))›
using no_decide
by (force simp: total_over_m_def total_over_set_def state'_def
Decided_Propagated_in_iff_in_lits_of_l)
have [simp]: ‹add_mset L C ∈# clauses S ⟹ defined_lit (trail S) L› for L C
using no_decide
by (auto dest!: multi_member_split)
have [simp]: ‹add_mset L C ∈# conflicting_clss S ⟹ defined_lit (trail S) L› for L C
using no_decide atms_of_conflicting_clss[of S]
by (auto dest!: multi_member_split)
show ?thesis
by (auto simp: dpll⇩W.simps no_decide)
qed
context
assumes can_always_improve:
‹⋀S. trail S ⊨asm clauses S ⟹ (∀C ∈# conflicting_clss S. ¬ trail S ⊨as CNot C) ⟹
dpll⇩W_all_inv (abs_state S) ⟹
total_over_m (lits_of_l (trail S)) (set_mset (clauses S)) ⟹ Ex (dpll⇩W_bound S)›
begin
lemma no_step_dpll⇩W_bnb_conflict:
assumes
ns: ‹no_step dpll⇩W_bnb S› and
invs: ‹dpll⇩W_all_inv (abs_state S)›
shows ‹∃C ∈# clauses S + conflicting_clss S. trail S ⊨as CNot C› (is ?A) and
‹count_decided (trail S) = 0› and
‹unsatisfiable (set_mset (clauses S + conflicting_clss S))›
proof (rule ccontr)
have no_decide: ‹atm_of L ∈ atms_of_mm (clauses S) ⟹ defined_lit (trail S) L› for L
using spec[OF ns, of ‹cons_trail _ S›]
apply (fastforce simp: dpll⇩W_bnb.simps total_over_m_def total_over_set_def
dpll⇩W_core.simps state'_def
dpll.dpll_decide.simps dpll.dpll_backtrack.simps backtrack_opt.simps
dpll.dpll_propagate.simps)
done
have tot: ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))›
using no_decide
by (force simp: total_over_m_def total_over_set_def state'_def
Decided_Propagated_in_iff_in_lits_of_l)
have dec0: ‹count_decided (trail S) = 0› if ent: ‹?A›
proof -
obtain C where
‹C ∈# clauses S + conflicting_clss S› and
‹trail S ⊨as CNot C›
using ent tot ns invs
by (auto simp: dpll⇩W_bnb.simps)
then show ‹count_decided (trail S) = 0›
using ns dpll⇩W_core_Ex_backtrack[of S _ _ _ C] dpll⇩W_core_Ex_backtrack_opt[of S _ _ _ C]
unfolding count_decided_0_iff
apply clarify
apply (frule backtrack_split_some_is_decided_then_snd_has_hd'[of _ ‹trail S›], assumption)
apply (auto simp: dpll⇩W_bnb.simps count_decided_0_iff)
apply (metis backtrack_split_snd_hd_decided list.sel(1) list.simps(3) snd_conv)+
done
qed
show A: False if ‹¬?A›
proof -
have ‹trail S ⊨a C› if ‹C ∈# clauses S + conflicting_clss S› for C
proof -
have ‹¬ trail S ⊨as CNot C›
using ‹¬?A› that by (auto dest!: multi_member_split)
then show ‹?thesis›
using tot that
total_not_true_cls_true_clss_CNot[of ‹lits_of_l (trail S)› C]
apply (auto simp: true_annots_def simp del: true_clss_def_iff_negation_in_model dest!: multi_member_split )
using true_annot_def apply blast
using true_annot_def apply blast
by (metis Decided_Propagated_in_iff_in_lits_of_l atms_of_clauses_conflicting_clss atms_of_ms_union
in_m_in_literals no_decide set_mset_union that true_annot_def true_cls_add_mset)
qed
then have ‹trail S ⊨asm clauses S + conflicting_clss S›
by (auto simp: true_annots_def dest!: multi_member_split )
then show ?thesis
using can_always_improve[of S] ‹¬?A› tot invs ns by (auto simp: dpll⇩W_bnb.simps)
qed
then show ‹count_decided (trail S) = 0›
using dec0 by blast
moreover have ?A
using A by blast
ultimately show ‹unsatisfiable (set_mset (clauses S + conflicting_clss S))›
using only_propagated_vars_unsat[of ‹trail S› _ ‹set_mset (clauses S + conflicting_clss S)›] invs
unfolding dpll⇩W_all_inv_def count_decided_0_iff
by auto
qed
end
inductive dpll⇩W_core_stgy :: "'st ⇒ 'st ⇒ bool" for S T where
propagate: "dpll.dpll_propagate S T ⟹ dpll⇩W_core_stgy S T" |
decided: "dpll.dpll_decide S T ⟹ no_step dpll.dpll_propagate S ⟹ dpll⇩W_core_stgy S T " |
backtrack: "dpll.dpll_backtrack S T ⟹ dpll⇩W_core_stgy S T" |
backtrack_opt: ‹backtrack_opt S T ⟹ dpll⇩W_core_stgy S T›
lemma dpll⇩W_core_stgy_dpll⇩W_core: ‹dpll⇩W_core_stgy S T ⟹ dpll⇩W_core S T›
by (induction rule: dpll⇩W_core_stgy.induct)
(auto intro: dpll⇩W_core.intros)
lemma rtranclp_dpll⇩W_core_stgy_dpll⇩W_core: ‹dpll⇩W_core_stgy⇧*⇧* S T ⟹ dpll⇩W_core⇧*⇧* S T›
by (induction rule: rtranclp_induct)
(auto dest: dpll⇩W_core_stgy_dpll⇩W_core)
lemma no_step_stgy_iff: ‹no_step dpll⇩W_core_stgy S ⟷ no_step dpll⇩W_core S›
by (auto simp: dpll⇩W_core_stgy.simps dpll⇩W_core.simps)
lemma full_dpll⇩W_core_stgy_dpll⇩W_core: ‹full dpll⇩W_core_stgy S T ⟹ full dpll⇩W_core S T›
unfolding full_def by (simp add: no_step_stgy_iff rtranclp_dpll⇩W_core_stgy_dpll⇩W_core)
lemma dpll⇩W_core_stgy_clauses:
‹dpll⇩W_core_stgy S T ⟹ clauses T = clauses S›
by (induction rule: dpll⇩W_core_stgy.induct)
(auto simp: dpll.dpll_propagate.simps dpll.dpll_decide.simps dpll.dpll_backtrack.simps
backtrack_opt.simps)
lemma rtranclp_dpll⇩W_core_stgy_clauses:
‹dpll⇩W_core_stgy⇧*⇧* S T ⟹ clauses T = clauses S›
by (induction rule: rtranclp_induct)
(auto dest: dpll⇩W_core_stgy_clauses)
end
locale dpll⇩W_state_optimal_weight =
dpll⇩W_state trail clauses
tl_trail cons_trail state_eq state +
ocdcl_weight ρ
for
trail :: ‹'st ⇒ 'v dpll⇩W_ann_lits› and
clauses :: ‹'st ⇒ 'v clauses› and
tl_trail :: ‹'st ⇒ 'st› and
cons_trail :: ‹'v dpll⇩W_ann_lit ⇒ 'st ⇒ 'st› and
state_eq :: ‹'st ⇒ 'st ⇒ bool› (infix "∼" 50) and
state :: ‹'st ⇒ 'v dpll⇩W_ann_lits × 'v clauses × 'v clause option × 'b› and
ρ :: ‹'v clause ⇒ 'a :: {linorder}› +
fixes
update_additional_info :: ‹'v clause option × 'b ⇒ 'st ⇒ 'st›
assumes
update_additional_info:
‹state S = (M, N, K) ⟹ state (update_additional_info K' S) = (M, N, K')›
begin
definition update_weight_information :: ‹('v literal, 'v literal, unit) annotated_lits ⇒ 'st ⇒ 'st› where
‹update_weight_information M S =
update_additional_info (Some (lit_of `# mset M), snd (additional_info S)) S›
lemma [simp]:
‹trail (update_weight_information M' S) = trail S›
‹clauses (update_weight_information M' S) = clauses S›
‹clauses (update_additional_info c S) = clauses S›
‹additional_info (update_additional_info (w, oth) S) = (w, oth)›
using update_additional_info[of S] unfolding update_weight_information_def
by (auto simp: state)
lemma state_update_weight_information: ‹state S = (M, N, w, oth) ⟹
∃w'. state (update_weight_information M' S) = (M, N, w', oth)›
apply (auto simp: state)
apply (auto simp: update_weight_information_def)
done
definition weight where
‹weight S = fst (additional_info S)›
lemma [simp]: ‹(weight (update_weight_information M' S)) = Some (lit_of `# mset M')›
unfolding weight_def by (auto simp: update_weight_information_def)
text ‹
We test here a slightly different decision. In the CDCL version, we renamed \<^term>‹additional_info›
from the BNB version to avoid collisions. Here instead of renaming, we add the prefix
\<^text>‹bnb.› to every name.
›
sublocale bnb: bnb_ops where
trail = trail and
clauses = clauses and
tl_trail = tl_trail and
cons_trail = cons_trail and
state_eq = state_eq and
state = state and
weight = weight and
conflicting_clauses = conflicting_clauses and
is_improving_int = is_improving_int and
update_weight_information = update_weight_information
by unfold_locales
lemma atms_of_mm_conflicting_clss_incl_init_clauses:
‹atms_of_mm (bnb.conflicting_clss S) ⊆ atms_of_mm (clauses S)›
using conflicting_clss_incl_init_clauses[of ‹clauses S› ‹weight S›]
unfolding bnb.conflicting_clss_def
by auto
lemma is_improving_conflicting_clss_update_weight_information: ‹bnb.is_improving M M' S ⟹
bnb.conflicting_clss S ⊆# bnb.conflicting_clss (update_weight_information M' S)›
using is_improving_conflicting_clss_update_weight_information[of M M' ‹clauses S› ‹weight S›]
unfolding bnb.conflicting_clss_def
by (auto simp: update_weight_information_def weight_def)
lemma conflicting_clss_update_weight_information_in2:
assumes ‹bnb.is_improving M M' S›
shows ‹negate_ann_lits M' ∈# bnb.conflicting_clss (update_weight_information M' S)›
using conflicting_clss_update_weight_information_in2[of M M' ‹clauses S› ‹weight S›] assms
unfolding bnb.conflicting_clss_def
unfolding bnb.conflicting_clss_def
by (auto simp: update_weight_information_def weight_def)
lemma state_additional_info':
‹state S = (trail S, clauses S, weight S, bnb.additional_info S)›
unfolding additional_info_def by (cases ‹state S›; auto simp: state weight_def bnb.additional_info_def)
sublocale bnb: bnb where
trail = trail and
clauses = clauses and
tl_trail = tl_trail and
cons_trail = cons_trail and
state_eq = state_eq and
state = state and
weight = weight and
conflicting_clauses = conflicting_clauses and
is_improving_int = is_improving_int and
update_weight_information = update_weight_information
apply unfold_locales
subgoal by auto
subgoal by (rule state_eq_sym)
subgoal by (rule state_eq_trans)
subgoal by (auto dest!: state_eq_state)
subgoal by (rule cons_trail)
subgoal by (rule tl_trail)
subgoal by (rule state_update_weight_information)
subgoal by (rule is_improving_conflicting_clss_update_weight_information)
subgoal by (rule conflicting_clss_update_weight_information_in2; assumption)
subgoal by (rule atms_of_mm_conflicting_clss_incl_init_clauses)
subgoal by (rule state_additional_info')
done
lemma improve_model_still_model:
assumes
‹bnb.dpll⇩W_bound S T› and
all_struct: ‹dpll⇩W_all_inv (bnb.abs_state S)› and
ent: ‹set_mset I ⊨sm clauses S› ‹set_mset I ⊨sm bnb.conflicting_clss S› and
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (clauses S)› and
le: ‹Found (ρ I) < ρ' (weight T)›
shows
‹set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm bnb.conflicting_clss T›
using assms(1)
proof (cases rule: bnb.dpll⇩W_bound.cases)
case (update_info M M') note imp = this(1) and T = this(2)
have atm_trail: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (clauses S)› and
dist2: ‹distinct_mset (lit_of `# mset (trail S))› and
taut2: ‹¬ tautology (lit_of `# mset (trail S))›
using all_struct unfolding dpll⇩W_all_inv_def by (auto simp: lits_of_def atms_of_def
dest: no_dup_distinct no_dup_not_tautology)
have tot2: ‹total_over_m (set_mset I) (set_mset (clauses S))›
using tot[symmetric]
by (auto simp: total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit)
have atm_trail: ‹atms_of (lit_of `# mset M') ⊆ atms_of_mm (clauses S)› and
dist2: ‹distinct_mset (lit_of `# mset M')› and
taut2: ‹¬ tautology (lit_of `# mset M')›
using imp by (auto simp: lits_of_def atms_of_def is_improving_int_def
simple_clss_def)
have tot2: ‹total_over_m (set_mset I) (set_mset (clauses S))›
using tot[symmetric]
by (auto simp: total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit)
have
‹set_mset I ⊨m conflicting_clauses (clauses S) (weight (update_weight_information M' S))›
using entails_conflicting_clauses_if_le[of I ‹clauses S› M' M ‹weight S›]
using T dist cons tot le imp by auto
then have ‹set_mset I ⊨m bnb.conflicting_clss (update_weight_information M' S)›
by (auto simp: update_weight_information_def bnb.conflicting_clss_def)
then show ?thesis
using ent T by (auto simp: bnb.conflicting_clss_def state)
qed
lemma cdcl_bnb_still_model:
assumes
‹bnb.dpll⇩W_bnb S T› and
all_struct: ‹dpll⇩W_all_inv (bnb.abs_state S)› and
ent: ‹set_mset I ⊨sm clauses S› ‹set_mset I ⊨sm bnb.conflicting_clss S› and
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (clauses S)›
shows
‹(set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm bnb.conflicting_clss T) ∨ Found (ρ I) ≥ ρ' (weight T)›
using assms
proof (induction rule: bnb.dpll⇩W_bnb.induct)
case (dpll S T)
then show ?case using ent by (auto elim!: bnb.dpll⇩W_coreE simp: bnb.state'_def
dpll_decide.simps dpll_backtrack.simps bnb.backtrack_opt.simps
dpll_propagate.simps)
next
case (bnb S T)
then show ?case
using improve_model_still_model[of S T I] using assms(2-) by auto
qed
lemma cdcl_bnb_larger_still_larger:
assumes
‹bnb.dpll⇩W_bnb S T›
shows ‹ρ' (weight S) ≥ ρ' (weight T)›
using assms apply (cases rule: bnb.dpll⇩W_bnb.cases)
by (auto simp: bnb.dpll⇩W_bound.simps is_improving_int_def bnb.dpll⇩W_core_same_weight)
lemma rtranclp_cdcl_bnb_still_model:
assumes
st: ‹bnb.dpll⇩W_bnb⇧*⇧* S T› and
all_struct: ‹dpll⇩W_all_inv (bnb.abs_state S)› and
ent: ‹(set_mset I ⊨sm clauses S ∧ set_mset I ⊨sm bnb.conflicting_clss S) ∨ Found (ρ I) ≥ ρ' (weight S)› and
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (clauses S)›
shows
‹(set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm bnb.conflicting_clss T) ∨ Found (ρ I) ≥ ρ' (weight T)›
using st
proof (induction rule: rtranclp_induct)
case base
then show ?case
using ent by auto
next
case (step T U) note star = this(1) and st = this(2) and IH = this(3)
have 1: ‹dpll⇩W_all_inv (bnb.abs_state T)›
using bnb.rtranclp_dpll⇩W_bnb_abs_state_all_inv[OF star all_struct] .
have 3: ‹atms_of I = atms_of_mm (clauses T)›
using bnb.rtranclp_dpll⇩W_bnb_clauses[OF star] tot by auto
show ?case
using cdcl_bnb_still_model[OF st 1 _ _ dist cons 3] IH
cdcl_bnb_larger_still_larger[OF st]
by auto
qed
lemma simple_clss_entailed_by_too_heavy_in_conflicting:
‹C ∈# mset_set (simple_clss (atms_of_mm (clauses S))) ⟹
too_heavy_clauses (clauses S) (weight S) ⊨pm
(C) ⟹ C ∈# bnb.conflicting_clss S›
by (auto simp: conflicting_clauses_def bnb.conflicting_clss_def)
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: ‹(∀C ∈# bnb.conflicting_clss S. ¬ trail S ⊨as CNot C)› and
all_struct: ‹dpll⇩W_all_inv (bnb.abs_state S)›
shows ‹Ex (bnb.dpll⇩W_bound S)›
proof -
have H: ‹(lit_of `# mset (trail S)) ∈# mset_set (simple_clss (atms_of_mm (clauses S)))›
‹(lit_of `# mset (trail S)) ∈ simple_clss (atms_of_mm (clauses S))›
‹no_dup (trail S)›
apply (subst finite_set_mset_mset_set[OF simple_clss_finite])
using all_struct by (auto simp: simple_clss_def
dpll⇩W_all_inv_def atms_of_def lits_of_def image_image clauses_def
dest: no_dup_not_tautology no_dup_distinct)
moreover have ‹trail S ⊨as CNot (pNeg (lit_of `# mset (trail S)))›
by (auto simp: pNeg_def true_annots_true_cls_def_iff_negation_in_model lits_of_def)
ultimately have le: ‹Found (ρ (lit_of `# mset (trail S))) < ρ' (weight S)›
using n_s total not_entailed_too_heavy_clauses_ge[of ‹lit_of `# mset (trail S)› ‹clauses S› ‹weight S›]
simple_clss_entailed_by_too_heavy_in_conflicting[of ‹pNeg (lit_of `# mset (trail S))› S]
by (cases ‹¬ too_heavy_clauses (clauses S) (weight S) ⊨pm
pNeg (lit_of `# mset (trail S))›)
(auto simp: lits_of_def
conflicting_clauses_def clauses_def negate_ann_lits_pNeg_lit_of image_iff
simple_clss_finite subset_iff
dest: bspec[of _ _ ‹(lit_of `# mset (trail S))›] dest: total_over_m_atms_incl
true_clss_cls_in too_heavy_clauses_contains_itself
dest!: multi_member_split)
have tr: ‹trail S ⊨asm clauses S›
using ent by (auto simp: clauses_def)
have tot': ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))›
using total all_struct by (auto simp: total_over_m_def total_over_set_def)
have M': ‹ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))›
if ‹total_over_m (lits_of_l M') (set_mset (clauses S))› and
incl: ‹mset (trail S) ⊆# mset M'› and
‹lit_of `# mset M' ∈ simple_clss (atms_of_mm (clauses S))›
for M'
proof -
have [simp]: ‹lits_of_l M' = set_mset (lit_of `# mset M')›
by (auto simp: lits_of_def)
obtain A where A: ‹mset M' = A + mset (trail S)›
using incl by (auto simp: mset_subset_eq_exists_conv)
have M': ‹lits_of_l M' = lit_of ` set_mset A ∪ lits_of_l (trail S)›
unfolding lits_of_def
by (metis A image_Un set_mset_mset set_mset_union)
have ‹mset M' = mset (trail S)›
using that tot' total unfolding A total_over_m_alt_def
apply (case_tac A)
apply (auto simp: A simple_clss_def distinct_mset_add M' image_Un
tautology_union mset_inter_empty_set_mset atms_of_def atms_of_s_def
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set image_image
tautology_add_mset)
by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
lits_of_def subsetCE)
then show ?thesis
using total by auto
qed
have ‹bnb.is_improving (trail S) (trail S) S›
if ‹Found (ρ (lit_of `# mset (trail S))) < ρ' (weight S)›
using that total H tr tot' M' unfolding is_improving_int_def lits_of_def
by fast
then show ?thesis
using bnb.dpll⇩W_bound.intros[of ‹trail S› _ S ‹update_weight_information (trail S) S›] total H le
by fast
qed
lemma no_step_dpll⇩W_bnb_conflict:
assumes
ns: ‹no_step bnb.dpll⇩W_bnb S› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state S)›
shows ‹∃C ∈# clauses S + bnb.conflicting_clss S. trail S ⊨as CNot C› (is ?A) and
‹count_decided (trail S) = 0› and
‹unsatisfiable (set_mset (clauses S + bnb.conflicting_clss S))›
apply (rule bnb.no_step_dpll⇩W_bnb_conflict[OF _ assms])
subgoal using can_always_improve by blast
apply (rule bnb.no_step_dpll⇩W_bnb_conflict[OF _ assms])
subgoal using can_always_improve by blast
apply (rule bnb.no_step_dpll⇩W_bnb_conflict[OF _ assms])
subgoal using can_always_improve by blast
done
lemma full_cdcl_bnb_stgy_larger_or_equal_weight:
assumes
st: ‹full bnb.dpll⇩W_bnb S T› and
all_struct: ‹dpll⇩W_all_inv (bnb.abs_state S)› and
ent: ‹(set_mset I ⊨sm clauses S ∧ set_mset I ⊨sm bnb.conflicting_clss S) ∨ Found (ρ I) ≥ ρ' (weight S)› and
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (clauses S)›
shows
‹Found (ρ I) ≥ ρ' (weight T)› and
‹unsatisfiable (set_mset (clauses T + bnb.conflicting_clss T))›
proof -
have ns: ‹no_step bnb.dpll⇩W_bnb T› and
st: ‹bnb.dpll⇩W_bnb⇧*⇧* S T›
using st unfolding full_def by (auto intro: )
have struct_T: ‹dpll⇩W_all_inv (bnb.abs_state T)›
using bnb.rtranclp_dpll⇩W_bnb_abs_state_all_inv[OF st all_struct] .
have atms_eq: ‹atms_of I ∪ atms_of_mm (bnb.conflicting_clss T) = atms_of_mm (clauses T)›
using atms_of_mm_conflicting_clss_incl_init_clauses[of T]
bnb.rtranclp_dpll⇩W_bnb_clauses[OF st] tot
by auto
show ‹unsatisfiable (set_mset (clauses T + bnb.conflicting_clss T))›
using no_step_dpll⇩W_bnb_conflict[of T] ns struct_T
by fast
then have ‹¬set_mset I ⊨sm clauses T + bnb.conflicting_clss T›
using dist cons by auto
then have ‹False› if ‹Found (ρ I) < ρ' (weight T)›
using ent that rtranclp_cdcl_bnb_still_model[OF st assms(2-)]
bnb.rtranclp_dpll⇩W_bnb_clauses[OF st] by auto
then show ‹Found (ρ I) ≥ ρ' (weight T)›
by force
qed
end
end