theory DPLL_W_Partial_Encoding
imports
DPLL_W_Optimal_Model
CDCL_W_Partial_Encoding
begin
context optimal_encoding_ops
begin
text ‹
We use the following list to generate an upper bound of the derived
trails by ODPLL: using lists makes it possible to use recursion. Using
\<^text>‹inductive_set› does not work, because it is not possible to
recurse on the arguments of a predicate.
The idea is similar to an earlier definition of \<^term>‹simple_clss›,
although in that case, we went for recursion over the set of literals
directly, via a choice in the recursive call.
›
definition list_new_vars :: ‹'v list› where
‹list_new_vars = (SOME v. set v = ΔΣ ∧ distinct v)›
lemma
set_list_new_vars: ‹set list_new_vars = ΔΣ› and
distinct_list_new_vars: ‹distinct list_new_vars› and
length_list_new_vars: ‹length list_new_vars = card ΔΣ›
using someI[of ‹λv. set v = ΔΣ ∧ distinct v›]
unfolding list_new_vars_def[symmetric]
using finite_Σ finite_distinct_list apply blast
using someI[of ‹λv. set v = ΔΣ ∧ distinct v›]
unfolding list_new_vars_def[symmetric]
using finite_Σ finite_distinct_list apply blast
using someI[of ‹λv. set v = ΔΣ ∧ distinct v›]
unfolding list_new_vars_def[symmetric]
by (metis distinct_card finite_Σ finite_distinct_list)
fun all_sound_trails where
‹all_sound_trails [] = simple_clss (Σ - ΔΣ)› |
‹all_sound_trails (L # M) =
all_sound_trails M ∪ add_mset (Pos (replacement_pos L)) ` all_sound_trails M
∪ add_mset (Pos (replacement_neg L)) ` all_sound_trails M›
lemma all_sound_trails_atms:
‹set xs ⊆ ΔΣ ⟹
C ∈ all_sound_trails xs ⟹
atms_of C ⊆ Σ - ΔΣ ∪ replacement_pos ` set xs ∪ replacement_neg ` set xs›
apply (induction xs arbitrary: C)
subgoal by (auto simp: simple_clss_def)
subgoal for x xs C
apply (auto simp: tautology_add_mset)
apply blast+
done
done
lemma all_sound_trails_distinct_mset:
‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹
C ∈ all_sound_trails xs ⟹
distinct_mset C›
using all_sound_trails_atms[of xs C]
apply (induction xs arbitrary: C)
subgoal by (auto simp: simple_clss_def)
subgoal for x xs C
apply clarsimp
apply (auto simp: tautology_add_mset)
apply (simp add: all_sound_trails_atms; fail)+
apply (frule all_sound_trails_atms, assumption)
apply (auto dest!: multi_member_split simp: subsetD)
apply (simp add: all_sound_trails_atms; fail)+
apply (frule all_sound_trails_atms, assumption)
apply (auto dest!: multi_member_split simp: subsetD)
apply (simp add: all_sound_trails_atms; fail)+
done
done
lemma all_sound_trails_tautology:
‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹
C ∈ all_sound_trails xs ⟹
¬tautology C›
using all_sound_trails_atms[of xs C]
apply (induction xs arbitrary: C)
subgoal by (auto simp: simple_clss_def)
subgoal for x xs C
apply clarsimp
apply (auto simp: tautology_add_mset)
apply (simp add: all_sound_trails_atms; fail)+
apply (frule all_sound_trails_atms, assumption)
apply (auto dest!: multi_member_split simp: subsetD)
apply (simp add: all_sound_trails_atms; fail)+
apply (frule all_sound_trails_atms, assumption)
apply (auto dest!: multi_member_split simp: subsetD)
done
done
lemma all_sound_trails_simple_clss:
‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹
all_sound_trails xs ⊆ simple_clss (Σ - ΔΣ ∪ replacement_pos ` set xs ∪ replacement_neg ` set xs)›
using all_sound_trails_tautology[of xs]
all_sound_trails_distinct_mset[of xs]
all_sound_trails_atms[of xs]
by (fastforce simp: simple_clss_def)
lemma in_all_sound_trails_inD:
‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹ a ∈ ΔΣ ⟹
add_mset (Pos (a⇧↦⇧0)) xa ∈ all_sound_trails xs ⟹ a ∈ set xs›
using all_sound_trails_simple_clss[of xs]
apply (auto simp: simple_clss_def)
apply (rotate_tac 3)
apply (frule set_mp, assumption)
apply auto
done
lemma in_all_sound_trails_inD':
‹set xs ⊆ ΔΣ ⟹ distinct xs ⟹ a ∈ ΔΣ ⟹
add_mset (Pos (a⇧↦⇧1)) xa ∈ all_sound_trails xs ⟹ a ∈ set xs›
using all_sound_trails_simple_clss[of xs]
apply (auto simp: simple_clss_def)
apply (rotate_tac 3)
apply (frule set_mp, assumption)
apply auto
done
context
assumes [simp]: ‹finite Σ›
begin
lemma all_sound_trails_finite[simp]:
‹finite (all_sound_trails xs)›
by (induction xs)
(auto intro!: simple_clss_finite finite_Σ)
lemma card_all_sound_trails:
assumes ‹set xs ⊆ ΔΣ› and ‹distinct xs›
shows ‹card (all_sound_trails xs) = card (simple_clss (Σ - ΔΣ)) * 3 ^ (length xs)›
using assms
apply (induction xs)
apply auto
apply (subst card_Un_disjoint)
apply (auto simp: add_mset_eq_add_mset dest: in_all_sound_trails_inD)
apply (subst card_Un_disjoint)
apply (auto simp: add_mset_eq_add_mset dest: in_all_sound_trails_inD')
apply (subst card_image)
apply (auto simp: inj_on_def)
apply (subst card_image)
apply (auto simp: inj_on_def)
done
end
lemma simple_clss_all_sound_trails: ‹simple_clss (Σ - ΔΣ) ⊆ all_sound_trails ys›
apply (induction ys)
apply auto
done
lemma all_sound_trails_decomp_in:
assumes
‹C ⊆ ΔΣ› ‹C' ⊆ ΔΣ› ‹C ∩ C' = {}› ‹C ∪ C' ⊆ set xs›
‹D ∈ simple_clss (Σ - ΔΣ)›
shows
‹(Pos o replacement_pos) `# mset_set C + (Pos o replacement_neg) `# mset_set C' + D ∈ all_sound_trails xs›
using assms
apply (induction xs arbitrary: C C' D)
subgoal
using simple_clss_all_sound_trails[of ‹[]›]
by auto
subgoal premises p for a xs C C' D
apply (cases ‹a ∈# mset_set C›)
subgoal
using p(1)[of ‹C - {a}› C' D] p(2-)
finite_subset[OF p(3)]
apply -
apply (subgoal_tac ‹finite C ∧ C - {a} ⊆ ΔΣ ∧ C' ⊆ ΔΣ ∧ (C - {a}) ∩ C' = {} ∧ C - {a} ∪ C' ⊆ set xs›)
defer
apply (auto simp: disjoint_iff_not_equal finite_subset)[]
apply (auto dest!: multi_member_split)
by (simp add: mset_set.remove)
apply (cases ‹a ∈# mset_set C'›)
subgoal
using p(1)[of C ‹C' - {a}› D] p(2-)
finite_subset[OF p(3)]
apply -
apply (subgoal_tac ‹finite C ∧ C ⊆ ΔΣ ∧ C'- {a} ⊆ ΔΣ ∧ (C) ∩ (C'- {a}) = {} ∧ C ∪ C'- {a} ⊆ set xs ∧
C ⊆ set xs ∧ C' - {a} ⊆ set xs›)
defer
apply (auto simp: disjoint_iff_not_equal finite_subset)[]
apply (auto dest!: multi_member_split)
by (simp add: mset_set.remove)
subgoal
using p(1)[of C C' D] p(2-)
finite_subset[OF p(3)]
apply -
apply (subgoal_tac ‹finite C ∧ C ⊆ ΔΣ ∧ C' ⊆ ΔΣ ∧ (C) ∩ (C') = {} ∧ C ∪ C' ⊆ set xs ∧
C ⊆ set xs ∧ C' ⊆ set xs›)
defer
apply (auto simp: disjoint_iff_not_equal finite_subset)[]
by (auto dest!: multi_member_split)
done
done
lemma (in -)image_union_subset_decomp:
‹f ` (C) ⊆ A ∪ B ⟷ (∃A' B'. f ` A' ⊆ A ∧ f ` B' ⊆ B ∧ C = A' ∪ B' ∧ A' ∩ B' = {})›
apply (rule iffI)
apply (rule exI[of _ ‹{x ∈ C. f x ∈ A}›])
apply (rule exI[of _ ‹{x ∈ C. f x ∈ B ∧ f x ∉ A}›])
apply auto
done
lemma in_all_sound_trails:
assumes
‹⋀L. L ∈ ΔΣ ⟹ Neg (replacement_pos L) ∉# C›
‹⋀L. L ∈ ΔΣ ⟹ Neg (replacement_neg L) ∉# C›
‹⋀L. L ∈ ΔΣ ⟹ Pos (replacement_pos L) ∈# C ⟹ Pos (replacement_neg L) ∉# C›
‹C ∈ simple_clss (Σ - ΔΣ ∪ replacement_pos ` set xs ∪ replacement_neg ` set xs)› and
xs: ‹set xs ⊆ ΔΣ›
shows
‹C ∈ all_sound_trails xs›
proof -
have
atms: ‹atms_of C ⊆ (Σ - ΔΣ ∪ replacement_pos ` set xs ∪ replacement_neg ` set xs)› and
taut: ‹¬tautology C› and
dist: ‹distinct_mset C›
using assms unfolding simple_clss_def
by blast+
obtain A' B' A'a B'' where
A'a: ‹atm_of ` A'a ⊆ Σ - ΔΣ› and
B'': ‹atm_of ` B'' ⊆ replacement_pos ` set xs› and
‹A' = A'a ∪ B''› and
B': ‹atm_of ` B' ⊆ replacement_neg ` set xs› and
C: ‹set_mset C = A'a ∪ B'' ∪ B'› and
inter:
‹B'' ∩ B' = {}›
‹A'a ∩ B' = {}›
‹A'a ∩ B'' = {}›
using atms unfolding atms_of_def
apply (subst (asm)image_union_subset_decomp)
apply (subst (asm)image_union_subset_decomp)
by (auto simp: Int_Un_distrib2)
have H: ‹f ` A ⊆ B ⟹ x ∈ A ⟹ f x ∈ B› for x A B f
by auto
have [simp]: ‹finite A'a› ‹finite B''› ‹finite B'›
by (metis C finite_Un finite_set_mset)+
obtain CB'' CB' where
CB: ‹CB' ⊆ set xs› ‹CB'' ⊆ set xs› and
decomp:
‹atm_of ` B'' = replacement_pos ` CB''›
‹atm_of ` B' = replacement_neg ` CB'›
using B' B'' by (auto simp: subset_image_iff)
have C: ‹C =mset_set B'' + mset_set B' + mset_set A'a›
using inter
apply (subst distinct_set_mset_eq_iff[symmetric, OF dist])
apply (auto simp: C distinct_mset_mset_set simp flip: mset_set_Union)
apply (subst mset_set_Union[symmetric])
using inter
apply auto
apply (auto simp: distinct_mset_mset_set)
done
have B'': ‹B'' = (Pos) ` (atm_of ` B'')›
using assms(1-3) B'' xs A'a B'' unfolding C
apply (auto simp: )
apply (frule H, assumption)
apply (case_tac x)
apply auto
apply (rule_tac x = ‹replacement_pos A› in imageI)
apply (auto simp add: rev_image_eqI)
apply (frule H, assumption)
apply (case_tac xb)
apply auto
done
have B': ‹B' = (Pos) ` (atm_of ` B')›
using assms(1-3) B' xs A'a B' unfolding C
apply (auto simp: )
apply (frule H, assumption)
apply (case_tac x)
apply auto
apply (rule_tac x = ‹replacement_neg A› in imageI)
apply (auto simp add: rev_image_eqI)
apply (frule H, assumption)
apply (case_tac xb)
apply auto
done
have simple: ‹mset_set A'a ∈ simple_clss (Σ - ΔΣ)›
using assms A'a
by (auto simp: simple_clss_def C atms_of_def image_Un tautology_decomp distinct_mset_mset_set)
have [simp]: ‹finite (Pos ` replacement_pos ` CB'')› ‹finite (Pos ` replacement_neg ` CB')›
using B'' ‹finite B''› decomp ‹finite B'› B' apply auto
by (meson CB(1) finite_Σ finite_imageI finite_subset xs)
show ?thesis
unfolding C
apply (subst B'', subst B')
unfolding decomp image_image
apply (subst image_mset_mset_set[symmetric])
subgoal
using decomp xs B' B'' inter CB
by (auto simp: C inj_on_def subset_iff)
apply (subst image_mset_mset_set[symmetric])
subgoal
using decomp xs B' B'' inter CB
by (auto simp: C inj_on_def subset_iff)
apply (rule all_sound_trails_decomp_in[unfolded comp_def])
using decomp xs B' B'' inter CB assms(3) simple
unfolding C
apply (auto simp: image_image)
subgoal for x
apply (subgoal_tac ‹x ∈ ΔΣ›)
using assms(3)[of x]
apply auto
by (metis (mono_tags, lifting) B' ‹finite (Pos ` replacement_neg ` CB')› ‹finite B''› decomp(2)
finite_set_mset_mset_set image_iff)
done
qed
end
locale dpll_optimal_encoding_opt =
dpll⇩W_state_optimal_weight trail clauses
tl_trail cons_trail state_eq state ρ update_additional_info +
optimal_encoding_opt_ops Σ ΔΣ new_vars
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
update_additional_info :: ‹'v clause option × 'b ⇒ 'st ⇒ 'st› and
Σ ΔΣ :: ‹'v set› and
ρ :: ‹'v clause ⇒ 'a :: {linorder}› and
new_vars :: ‹'v ⇒ 'v × 'v›
begin
end
locale dpll_optimal_encoding =
dpll_optimal_encoding_opt trail clauses
tl_trail cons_trail state_eq state
update_additional_info Σ ΔΣ ρ new_vars +
optimal_encoding_ops
Σ ΔΣ
new_vars ρ
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
update_additional_info :: ‹'v clause option × 'b ⇒ 'st ⇒ 'st› and
Σ ΔΣ :: ‹'v set› and
ρ :: ‹'v clause ⇒ 'a :: {linorder}› and
new_vars :: ‹'v ⇒ 'v × 'v›
begin
inductive odecide :: ‹'st ⇒ 'st ⇒ bool› where
odecide_noweight: ‹odecide S T›
if
‹undefined_lit (trail S) L› and
‹atm_of L ∈ atms_of_mm (clauses S)› and
‹T ∼ cons_trail (Decided L) S› and
‹atm_of L ∈ Σ - ΔΣ› |
odecide_replacement_pos: ‹odecide S T›
if
‹undefined_lit (trail S) (Pos (replacement_pos L))› and
‹T ∼ cons_trail (Decided (Pos (replacement_pos L))) S› and
‹L ∈ ΔΣ› |
odecide_replacement_neg: ‹odecide S T›
if
‹undefined_lit (trail S) (Pos (replacement_neg L))› and
‹T ∼ cons_trail (Decided (Pos (replacement_neg L))) S› and
‹L ∈ ΔΣ›
inductive_cases odecideE: ‹odecide S T›
inductive dpll_conflict :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll_conflict S S›
if ‹C ∈# clauses S› and
‹trail S ⊨as CNot C›
inductive odpll⇩W_core_stgy :: "'st ⇒ 'st ⇒ bool" for S T where
propagate: "dpll_propagate S T ⟹ odpll⇩W_core_stgy S T" |
decided: "odecide S T ⟹ no_step dpll_propagate S ⟹ odpll⇩W_core_stgy S T " |
backtrack: "dpll_backtrack S T ⟹ odpll⇩W_core_stgy S T" |
backtrack_opt: ‹bnb.backtrack_opt S T ⟹ odpll⇩W_core_stgy S T›
lemma odpll⇩W_core_stgy_clauses:
‹odpll⇩W_core_stgy S T ⟹ clauses T = clauses S›
by (induction rule: odpll⇩W_core_stgy.induct)
(auto simp: dpll_propagate.simps odecide.simps dpll_backtrack.simps
bnb.backtrack_opt.simps)
lemma rtranclp_odpll⇩W_core_stgy_clauses:
‹odpll⇩W_core_stgy⇧*⇧* S T ⟹ clauses T = clauses S›
by (induction rule: rtranclp_induct)
(auto dest: odpll⇩W_core_stgy_clauses)
inductive odpll⇩W_bnb_stgy :: ‹'st ⇒ 'st ⇒ bool› for S T :: 'st where
dpll:
‹odpll⇩W_bnb_stgy S T›
if ‹odpll⇩W_core_stgy S T› |
bnb:
‹odpll⇩W_bnb_stgy S T›
if ‹bnb.dpll⇩W_bound S T›
lemma odpll⇩W_bnb_stgy_clauses:
‹odpll⇩W_bnb_stgy S T ⟹ clauses T = clauses S›
by (induction rule: odpll⇩W_bnb_stgy.induct)
(auto simp: bnb.dpll⇩W_bound.simps dest: odpll⇩W_core_stgy_clauses)
lemma rtranclp_odpll⇩W_bnb_stgy_clauses:
‹odpll⇩W_bnb_stgy⇧*⇧* S T ⟹ clauses T = clauses S›
by (induction rule: rtranclp_induct)
(auto dest: odpll⇩W_bnb_stgy_clauses)
lemma odecide_dpll_decide_iff:
assumes ‹clauses S = penc N› ‹atms_of_mm N = Σ›
shows ‹odecide S T ⟹ dpll_decide S T›
‹dpll_decide S T ⟹ Ex(odecide S)›
using assms atms_of_mm_penc_subset2[of N] ΔΣ_Σ
unfolding odecide.simps dpll_decide.simps
apply (auto simp: odecide.simps dpll_decide.simps)
apply (metis defined_lit_Pos_atm_iff state_eq_ref)+
done
lemma
assumes ‹clauses S = penc N› ‹atms_of_mm N = Σ›
shows
odpll⇩W_core_stgy_dpll⇩W_core_stgy: ‹odpll⇩W_core_stgy S T ⟹ bnb.dpll⇩W_core_stgy S T›
using odecide_dpll_decide_iff[OF assms]
by (auto simp: odpll⇩W_core_stgy.simps bnb.dpll⇩W_core_stgy.simps)
lemma
assumes ‹clauses S = penc N› ‹atms_of_mm N = Σ›
shows
odpll⇩W_bnb_stgy_dpll⇩W_bnb_stgy: ‹odpll⇩W_bnb_stgy S T ⟹ bnb.dpll⇩W_bnb S T›
using odecide_dpll_decide_iff[OF assms]
by (auto simp: odpll⇩W_bnb_stgy.simps bnb.dpll⇩W_bnb.simps dest: odpll⇩W_core_stgy_dpll⇩W_core_stgy[OF assms]
bnb.dpll⇩W_core_stgy_dpll⇩W_core)
lemma
assumes ‹clauses S = penc N› and [simp]: ‹atms_of_mm N = Σ›
shows
rtranclp_odpll⇩W_bnb_stgy_dpll⇩W_bnb_stgy: ‹odpll⇩W_bnb_stgy⇧*⇧* S T ⟹ bnb.dpll⇩W_bnb⇧*⇧* S T›
using assms(1) apply -
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for T U
using odpll⇩W_bnb_stgy_dpll⇩W_bnb_stgy[of T N U] rtranclp_odpll⇩W_bnb_stgy_clauses[of S T]
by auto
done
lemma no_step_odpll⇩W_core_stgy_no_step_dpll⇩W_core_stgy:
assumes ‹clauses S = penc N› and [simp]:‹atms_of_mm N = Σ›
shows
‹no_step odpll⇩W_core_stgy S ⟷ no_step bnb.dpll⇩W_core_stgy S›
using odecide_dpll_decide_iff[of S, OF assms]
by (auto simp: odpll⇩W_core_stgy.simps bnb.dpll⇩W_core_stgy.simps)
lemma no_step_odpll⇩W_bnb_stgy_no_step_dpll⇩W_bnb:
assumes ‹clauses S = penc N› and [simp]:‹atms_of_mm N = Σ›
shows
‹no_step odpll⇩W_bnb_stgy S ⟷ no_step bnb.dpll⇩W_bnb S›
using no_step_odpll⇩W_core_stgy_no_step_dpll⇩W_core_stgy[of S, OF assms] bnb.no_step_stgy_iff
by (auto simp: odpll⇩W_bnb_stgy.simps bnb.dpll⇩W_bnb.simps dest: odpll⇩W_core_stgy_dpll⇩W_core_stgy[OF assms]
bnb.dpll⇩W_core_stgy_dpll⇩W_core)
lemma full_odpll⇩W_core_stgy_full_dpll⇩W_core_stgy:
assumes ‹clauses S = penc N› and [simp]:‹atms_of_mm N = Σ›
shows
‹full odpll⇩W_bnb_stgy S T ⟹ full bnb.dpll⇩W_bnb S T›
using no_step_odpll⇩W_bnb_stgy_no_step_dpll⇩W_bnb[of T, OF _ assms(2)]
rtranclp_odpll⇩W_bnb_stgy_clauses[of S T, symmetric, unfolded assms]
rtranclp_odpll⇩W_bnb_stgy_dpll⇩W_bnb_stgy[of S N T, OF assms]
by (auto simp: full_def)
lemma decided_cons_eq_append_decide_cons:
"Decided L # Ms = M' @ Decided K # M ⟷
(L = K ∧ Ms = M ∧ M' = []) ∨
(hd M' = Decided L ∧ Ms = tl M' @ Decided K # M ∧ M' ≠ [])"
by (cases M')
auto
lemma no_step_dpll_backtrack_iff:
‹no_step dpll_backtrack S ⟷ (count_decided (trail S) = 0 ∨ (∀C ∈# clauses S. ¬trail S ⊨as CNot C))›
using backtrack_snd_empty_not_decided[of ‹trail S›] backtrack_split_list_eq[of ‹trail S›, symmetric]
apply (cases ‹backtrack_split (trail S)›; cases ‹snd(backtrack_split (trail S))›)
by (auto simp: dpll_backtrack.simps count_decided_0_iff)
lemma no_step_dpll_conflict:
‹no_step dpll_conflict S ⟷ (∀C ∈# clauses S. ¬trail S ⊨as CNot C)›
by (auto simp: dpll_conflict.simps)
definition no_smaller_propa :: ‹'st ⇒ bool› where
"no_smaller_propa (S ::'st) ⟷
(∀M K M' D L. trail S = M' @ Decided K # M ⟶ add_mset L D ∈# clauses S ⟶ undefined_lit M L ⟶ ¬M ⊨as CNot D)"
lemma [simp]: ‹T ∼ S ⟹ no_smaller_propa T = no_smaller_propa S›
by (auto simp: no_smaller_propa_def)
lemma no_smaller_propa_cons_trail[simp]:
‹no_smaller_propa (cons_trail (Propagated L C) S) ⟷ no_smaller_propa S›
‹no_smaller_propa (update_weight_information M' S) ⟷ no_smaller_propa S›
by (force simp: no_smaller_propa_def cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons)+
lemma no_smaller_propa_cons_trail_decided[simp]:
‹no_smaller_propa S ⟹ no_smaller_propa (cons_trail (Decided L) S) ⟷ (∀L C. add_mset L C ∈# clauses S ⟶ undefined_lit (trail S)L ⟶ ¬trail S ⊨as CNot C)›
by (auto simp: no_smaller_propa_def cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons
decided_cons_eq_append_decide_cons)
lemma no_step_dpll_propagate_iff:
‹no_step dpll_propagate S ⟷ (∀L C. add_mset L C ∈# clauses S ⟶ undefined_lit (trail S)L ⟶ ¬trail S ⊨as CNot C)›
by (auto simp: dpll_propagate.simps)
lemma count_decided_0_no_smaller_propa: ‹count_decided (trail S) = 0 ⟹ no_smaller_propa S›
by (auto simp: no_smaller_propa_def)
lemma no_smaller_propa_backtrack_split:
‹no_smaller_propa S ⟹
backtrack_split (trail S) = (M', L # M) ⟹
no_smaller_propa (reduce_trail_to M S)›
using backtrack_split_list_eq[of ‹trail S›, symmetric]
by (auto simp: no_smaller_propa_def)
lemma odpll⇩W_core_stgy_no_smaller_propa:
‹odpll⇩W_core_stgy S T ⟹ no_smaller_propa S ⟹ no_smaller_propa T›
using no_step_dpll_backtrack_iff[of S] apply -
by (induction rule: odpll⇩W_core_stgy.induct)
(auto 5 5 simp: cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons count_decided_0_no_smaller_propa
dpll_propagate.simps dpll_decide.simps odecide.simps decided_cons_eq_append_decide_cons
bnb.backtrack_opt.simps dpll_backtrack.simps no_step_dpll_conflict no_smaller_propa_backtrack_split)
lemma odpll⇩W_bound_stgy_no_smaller_propa: ‹bnb.dpll⇩W_bound S T ⟹ no_smaller_propa S ⟹ no_smaller_propa T›
by (auto simp: cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons count_decided_0_no_smaller_propa
dpll_propagate.simps dpll_decide.simps odecide.simps decided_cons_eq_append_decide_cons bnb.dpll⇩W_bound.simps
bnb.backtrack_opt.simps dpll_backtrack.simps no_step_dpll_conflict no_smaller_propa_backtrack_split)
lemma odpll⇩W_bnb_stgy_no_smaller_propa:
‹odpll⇩W_bnb_stgy S T ⟹ no_smaller_propa S ⟹ no_smaller_propa T›
by (induction rule: odpll⇩W_bnb_stgy.induct)
(auto simp: odpll⇩W_core_stgy_no_smaller_propa odpll⇩W_bound_stgy_no_smaller_propa)
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 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 isabelle_should_do_that_automatically: ‹Suc (a - Suc 0) = a ⟷ a ≥ 1›
by auto
lemma distinct_count_list_if: ‹distinct xs ⟹ count_list xs x = (if x ∈ set xs then 1 else 0)›
by (induction xs) auto
abbreviation (input) cut_and_complete_trail :: ‹'st ⇒ _› where
‹cut_and_complete_trail S ≡ trail S›
inductive odpll⇩W_core_stgy_count :: "'st × _ ⇒ 'st × _ ⇒ bool" where
propagate: "dpll_propagate S T ⟹ odpll⇩W_core_stgy_count (S, C) (T, C)" |
decided: "odecide S T ⟹ no_step dpll_propagate S ⟹ odpll⇩W_core_stgy_count (S, C) (T, C) " |
backtrack: "dpll_backtrack S T ⟹ odpll⇩W_core_stgy_count (S, C) (T, add_mset (cut_and_complete_trail S) C)" |
backtrack_opt: ‹bnb.backtrack_opt S T ⟹ odpll⇩W_core_stgy_count (S, C) (T, add_mset (cut_and_complete_trail S) C)›
inductive odpll⇩W_bnb_stgy_count :: ‹'st × _ ⇒ 'st × _ ⇒ bool› where
dpll:
‹odpll⇩W_bnb_stgy_count S T›
if ‹odpll⇩W_core_stgy_count S T› |
bnb:
‹odpll⇩W_bnb_stgy_count (S, C) (T, C)›
if ‹bnb.dpll⇩W_bound S T›
lemma odpll⇩W_core_stgy_countD:
‹odpll⇩W_core_stgy_count S T ⟹ odpll⇩W_core_stgy (fst S) (fst T)›
‹odpll⇩W_core_stgy_count S T ⟹ snd S ⊆# snd T›
by (induction rule: odpll⇩W_core_stgy_count.induct; auto intro: odpll⇩W_core_stgy.intros)+
lemma odpll⇩W_bnb_stgy_countD:
‹odpll⇩W_bnb_stgy_count S T ⟹ odpll⇩W_bnb_stgy (fst S) (fst T)›
‹odpll⇩W_bnb_stgy_count S T ⟹ snd S ⊆# snd T›
by (induction rule: odpll⇩W_bnb_stgy_count.induct; auto dest: odpll⇩W_core_stgy_countD intro: odpll⇩W_bnb_stgy.intros)+
lemma rtranclp_odpll⇩W_bnb_stgy_countD:
‹odpll⇩W_bnb_stgy_count⇧*⇧* S T ⟹ odpll⇩W_bnb_stgy⇧*⇧* (fst S) (fst T)›
‹odpll⇩W_bnb_stgy_count⇧*⇧* S T ⟹ snd S ⊆# snd T›
by (induction rule: rtranclp_induct; auto dest: odpll⇩W_bnb_stgy_countD)+
lemmas odpll⇩W_core_stgy_count_induct = odpll⇩W_core_stgy_count.induct[of ‹(S, n)› ‹(T, m)› for S n T m, split_format(complete), OF dpll_optimal_encoding_axioms,
consumes 1]
definition conflict_clauses_are_entailed :: ‹'st × _ ⇒ bool› where
‹conflict_clauses_are_entailed =
(λ(S, Cs). ∀C ∈# Cs. (∃M' K M M''. trail S = M' @ Propagated K () # M ∧ C = M'' @ Decided (-K) # M))›
definition conflict_clauses_are_entailed2 :: ‹'st × ('v literal, 'v literal, unit) annotated_lits multiset ⇒ bool› where
‹conflict_clauses_are_entailed2 =
(λ(S, Cs). ∀C ∈# Cs. ∀C' ∈# remove1_mset C Cs. (∃L. Decided L ∈ set C ∧ Propagated (-L) () ∈ set C') ∨
(∃L. Propagated (L) () ∈ set C ∧ Decided (-L) ∈ set C'))›
lemma propagated_cons_eq_append_propagated_cons:
‹Propagated L () # M = M' @ Propagated K () # Ma ⟷
(M' = [] ∧ K = L ∧ M = Ma) ∨
(M' ≠ [] ∧ hd M' = Propagated L () ∧ M = tl M' @ Propagated K () # Ma)›
by (cases M')
auto
lemma odpll⇩W_core_stgy_count_conflict_clauses_are_entailed:
assumes
‹odpll⇩W_core_stgy_count S T› and
‹conflict_clauses_are_entailed S›
shows
‹conflict_clauses_are_entailed T›
using assms
apply (induction rule: odpll⇩W_core_stgy_count.induct)
subgoal
apply (auto simp: dpll_propagate.simps conflict_clauses_are_entailed_def
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons)
by (metis append_Cons)
subgoal for S T
apply (auto simp: odecide.simps conflict_clauses_are_entailed_def
dest!: multi_member_split intro: exI[of _ ‹Decided _ # _›])
by (metis append_Cons)+
subgoal for S T C
using backtrack_split_list_eq[of ‹trail S›, symmetric]
backtrack_split_snd_hd_decided[of ‹trail S›]
apply (auto simp: dpll_backtrack.simps conflict_clauses_are_entailed_def
propagated_cons_eq_append_propagated_cons is_decided_def append_eq_append_conv2
eq_commute[of _ ‹Propagated _ () # _›] conj_disj_distribR ex_disj_distrib
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons dpll⇩W_all_inv_def
dest!: multi_member_split
simp del: backtrack_split_list_eq
)
apply (case_tac us)
by force+
subgoal for S T C
using backtrack_split_list_eq[of ‹trail S›, symmetric]
backtrack_split_snd_hd_decided[of ‹trail S›]
apply (auto simp: bnb.backtrack_opt.simps conflict_clauses_are_entailed_def
propagated_cons_eq_append_propagated_cons is_decided_def append_eq_append_conv2
eq_commute[of _ ‹Propagated _ () # _›] conj_disj_distribR ex_disj_distrib
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons
dpll⇩W_all_inv_def
dest!: multi_member_split
simp del: backtrack_split_list_eq
)
apply (case_tac us)
by force+
done
lemma odpll⇩W_bnb_stgy_count_conflict_clauses_are_entailed:
assumes
‹odpll⇩W_bnb_stgy_count S T› and
‹conflict_clauses_are_entailed S›
shows
‹conflict_clauses_are_entailed T›
using assms odpll⇩W_core_stgy_count_conflict_clauses_are_entailed[of S T]
apply (auto simp: odpll⇩W_bnb_stgy_count.simps)
apply (auto simp: conflict_clauses_are_entailed_def
bnb.dpll⇩W_bound.simps)
done
lemma odpll⇩W_core_stgy_count_no_dup_clss:
assumes
‹odpll⇩W_core_stgy_count S T› and
‹∀C ∈# snd S. no_dup C› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state (fst S))›
shows
‹∀C ∈# snd T. no_dup C›
using assms
by (induction rule: odpll⇩W_core_stgy_count.induct)
(auto simp: dpll⇩W_all_inv_def)
lemma odpll⇩W_bnb_stgy_count_no_dup_clss:
assumes
‹odpll⇩W_bnb_stgy_count S T› and
‹∀C ∈# snd S. no_dup C› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state (fst S))›
shows
‹∀C ∈# snd T. no_dup C›
using assms
by (induction rule: odpll⇩W_bnb_stgy_count.induct)
(auto simp: dpll⇩W_all_inv_def
bnb.dpll⇩W_bound.simps dest!: odpll⇩W_core_stgy_count_no_dup_clss)
lemma backtrack_split_conflict_clauses_are_entailed_itself:
assumes
‹backtrack_split (trail S) = (M', L # M)› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state S)›
shows ‹¬ conflict_clauses_are_entailed
(S, add_mset (trail S) C)› (is ‹¬ ?A›)
proof
assume ?A
then obtain M' K Ma where
tr: ‹trail S = M' @ Propagated K () # Ma› and
‹add_mset (- K) (lit_of `# mset Ma) ⊆#
add_mset (lit_of L) (lit_of `# mset M)›
by (clarsimp simp: conflict_clauses_are_entailed_def)
then have ‹-K ∈# add_mset (lit_of L) (lit_of `# mset M)›
by (meson member_add_mset mset_subset_eqD)
then have ‹-K ∈# lit_of `# mset (trail S)›
using backtrack_split_list_eq[of ‹trail S›, symmetric] assms(1)
by auto
moreover have ‹K ∈# lit_of `# mset (trail S)›
by (auto simp: tr)
ultimately show False using invs unfolding dpll⇩W_all_inv_def
by (auto simp add: no_dup_cannot_not_lit_and_uminus uminus_lit_swap)
qed
lemma odpll⇩W_core_stgy_count_distinct_mset:
assumes
‹odpll⇩W_core_stgy_count S T› and
‹conflict_clauses_are_entailed S› and
‹distinct_mset (snd S)› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state (fst S))›
shows
‹distinct_mset (snd T)›
using assms(1,2,3,4) odpll⇩W_core_stgy_count_conflict_clauses_are_entailed[OF assms(1,2)]
apply (induction rule: odpll⇩W_core_stgy_count.induct)
subgoal
by (auto simp: dpll_propagate.simps conflict_clauses_are_entailed_def
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons)
subgoal
by (auto simp:)
subgoal for S T C
by (clarsimp simp: dpll_backtrack.simps backtrack_split_conflict_clauses_are_entailed_itself
dest!: multi_member_split)
subgoal for S T C
by (clarsimp simp: bnb.backtrack_opt.simps backtrack_split_conflict_clauses_are_entailed_itself
dest!: multi_member_split)
done
lemma odpll⇩W_bnb_stgy_count_distinct_mset:
assumes
‹odpll⇩W_bnb_stgy_count S T› and
‹conflict_clauses_are_entailed S› and
‹distinct_mset (snd S)› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state (fst S))›
shows
‹distinct_mset (snd T)›
using assms odpll⇩W_core_stgy_count_distinct_mset[OF _ assms(2-), of T]
by (auto simp: odpll⇩W_bnb_stgy_count.simps)
lemma odpll⇩W_core_stgy_count_conflict_clauses_are_entailed2:
assumes
‹odpll⇩W_core_stgy_count S T› and
‹conflict_clauses_are_entailed S› and
‹conflict_clauses_are_entailed2 S› and
‹distinct_mset (snd S)› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state (fst S))›
shows
‹conflict_clauses_are_entailed2 T›
using assms
proof (induction rule: odpll⇩W_core_stgy_count.induct)
case (propagate S T C)
then show ?case
by (auto simp: dpll_propagate.simps conflict_clauses_are_entailed2_def)
next
case (decided S T C)
then show ?case
by (auto simp: dpll_decide.simps conflict_clauses_are_entailed2_def)
next
case (backtrack S T C) note bt = this(1) and ent = this(2) and ent2 = this(3) and dist = this(4)
and invs = this(5)
let ?M = ‹(cut_and_complete_trail S)›
have ‹conflict_clauses_are_entailed (T, add_mset ?M C)› and
dist': ‹distinct_mset (add_mset ?M C)›
using odpll⇩W_core_stgy_count_conflict_clauses_are_entailed[OF _ ent, of ‹(T, add_mset ?M C)›]
odpll⇩W_core_stgy_count_distinct_mset[OF _ ent dist invs, of ‹(T, add_mset ?M C)›]
bt by (auto dest!: odpll⇩W_core_stgy_count.intros(3)[of S T C])
obtain M1 K M2 where
spl: ‹backtrack_split (trail S) = (M2, Decided K # M1)›
using bt backtrack_split_snd_hd_decided[of ‹trail S›]
by (cases ‹hd (snd (backtrack_split (trail S)))›) (auto simp: dpll_backtrack.simps)
have has_dec: ‹∃l∈set (trail S). is_decided l›
using bt apply (auto simp: dpll_backtrack.simps)
using bt count_decided_0_iff no_step_dpll_backtrack_iff by blast
let ?P = ‹λCa C'.
(∃L. Decided L ∈ set Ca ∧ Propagated (- L) () ∈ set C') ∨
(∃L. Propagated L () ∈ set Ca ∧ Decided (- L) ∈ set C')›
have ‹∀C'∈#remove1_mset ?M C. ?P ?M C'›
proof
fix C'
assume ‹C'∈#remove1_mset ?M C›
then have ‹C' ∈# C› and ‹C' ≠ ?M›
using dist' by auto
then obtain M' L M M'' where
‹trail S = M' @ Propagated L () # M› and
‹C' = M'' @ Decided (- L) # M›
using ent unfolding conflict_clauses_are_entailed_def
by auto
then show ‹?P ?M C'›
using backtrack_split_some_is_decided_then_snd_has_hd[of ‹trail S›, OF has_dec]
spl backtrack_split_list_eq[of ‹trail S›, symmetric]
by (clarsimp simp: conj_disj_distribR ex_disj_distrib decided_cons_eq_append_decide_cons
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons propagated_cons_eq_append_propagated_cons
append_eq_append_conv2)
qed
moreover have H: ‹?case ⟷ (∀Ca∈#add_mset ?M C.
∀C'∈#remove1_mset Ca C. ?P Ca C')›
unfolding conflict_clauses_are_entailed2_def prod.case
apply (intro conjI iffI impI ballI)
subgoal for Ca C'
by (auto dest: multi_member_split dest: in_diffD)
subgoal for Ca C'
using dist'
by (auto 5 3 dest!: multi_member_split[of Ca] dest: in_diffD)
done
moreover have ‹(∀Ca∈#C. ∀C'∈#remove1_mset Ca C. ?P Ca C')›
using ent2 unfolding conflict_clauses_are_entailed2_def
by auto
ultimately show ?case
unfolding H
by auto
next
case (backtrack_opt S T C) note bt = this(1) and ent = this(2) and ent2 = this(3) and dist = this(4)
and invs = this(5)
let ?M = ‹(cut_and_complete_trail S)›
have ‹conflict_clauses_are_entailed (T, add_mset ?M C)› and
dist': ‹distinct_mset (add_mset ?M C)›
using odpll⇩W_core_stgy_count_conflict_clauses_are_entailed[OF _ ent, of ‹(T, add_mset ?M C)›]
odpll⇩W_core_stgy_count_distinct_mset[OF _ ent dist invs, of ‹(T, add_mset ?M C)›]
bt by (auto dest!: odpll⇩W_core_stgy_count.intros(4)[of S T C])
obtain M1 K M2 where
spl: ‹backtrack_split (trail S) = (M2, Decided K # M1)›
using bt backtrack_split_snd_hd_decided[of ‹trail S›]
by (cases ‹hd (snd (backtrack_split (trail S)))›) (auto simp: bnb.backtrack_opt.simps)
have has_dec: ‹∃l∈set (trail S). is_decided l›
using bt apply (auto simp: bnb.backtrack_opt.simps)
by (metis annotated_lit.disc(1) backtrack_split_list_eq in_set_conv_decomp snd_conv spl)
let ?P = ‹λCa C'.
(∃L. Decided L ∈ set Ca ∧ Propagated (- L) () ∈ set C') ∨
(∃L. Propagated L () ∈ set Ca ∧ Decided (- L) ∈ set C')›
have ‹∀C'∈#remove1_mset ?M C. ?P ?M C'›
proof
fix C'
assume ‹C'∈#remove1_mset ?M C›
then have ‹C' ∈# C› and ‹C' ≠ ?M›
using dist' by auto
then obtain M' L M M'' where
‹trail S = M' @ Propagated L () # M› and
‹C' = M'' @ Decided (- L) # M›
using ent unfolding conflict_clauses_are_entailed_def
by auto
then show ‹?P ?M C'›
using backtrack_split_some_is_decided_then_snd_has_hd[of ‹trail S›, OF has_dec]
spl backtrack_split_list_eq[of ‹trail S›, symmetric]
by (clarsimp simp: conj_disj_distribR ex_disj_distrib decided_cons_eq_append_decide_cons
cdcl⇩W_restart_mset.propagated_cons_eq_append_decide_cons propagated_cons_eq_append_propagated_cons
append_eq_append_conv2)
qed
moreover have H: ‹?case ⟷ (∀Ca∈#add_mset ?M C.
∀C'∈#remove1_mset Ca C. ?P Ca C')›
unfolding conflict_clauses_are_entailed2_def prod.case
apply (intro conjI iffI impI ballI)
subgoal for Ca C'
by (auto dest: multi_member_split dest: in_diffD)
subgoal for Ca C'
using dist'
by (auto 5 3 dest!: multi_member_split[of Ca] dest: in_diffD)
done
moreover have ‹(∀Ca∈#C. ∀C'∈#remove1_mset Ca C. ?P Ca C')›
using ent2 unfolding conflict_clauses_are_entailed2_def
by auto
ultimately show ?case
unfolding H
by auto
qed
lemma odpll⇩W_bnb_stgy_count_conflict_clauses_are_entailed2:
assumes
‹odpll⇩W_bnb_stgy_count S T› and
‹conflict_clauses_are_entailed S› and
‹conflict_clauses_are_entailed2 S› and
‹distinct_mset (snd S)› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state (fst S))›
shows
‹conflict_clauses_are_entailed2 T›
using assms odpll⇩W_core_stgy_count_conflict_clauses_are_entailed2[of S T]
apply (auto simp: odpll⇩W_bnb_stgy_count.simps)
apply (auto simp: conflict_clauses_are_entailed2_def
bnb.dpll⇩W_bound.simps)
done
definition no_complement_set_lit :: ‹'v dpll⇩W_ann_lits ⇒ bool› where
‹no_complement_set_lit M ⟷
(∀L ∈ ΔΣ. Decided (Pos (replacement_pos L)) ∈ set M ⟶ Decided (Pos (replacement_neg L)) ∉ set M) ∧
(∀L ∈ ΔΣ. Decided (Neg (replacement_pos L)) ∉ set M) ∧
(∀L ∈ ΔΣ. Decided (Neg (replacement_neg L)) ∉ set M) ∧
atm_of ` lits_of_l M ⊆ Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
definition no_complement_set_lit_st :: ‹'st × 'v dpll⇩W_ann_lits multiset ⇒ bool› where
‹no_complement_set_lit_st = (λ(S, Cs). (∀C∈#Cs. no_complement_set_lit C) ∧ no_complement_set_lit (trail S))›
lemma backtrack_no_complement_set_lit: ‹no_complement_set_lit (trail S) ⟹
backtrack_split (trail S) = (M', L # M) ⟹
no_complement_set_lit (Propagated (- lit_of L) () # M)›
using backtrack_split_list_eq[of ‹trail S›, symmetric]
by (auto simp: no_complement_set_lit_def)
lemma odpll⇩W_core_stgy_count_no_complement_set_lit_st:
assumes
‹odpll⇩W_core_stgy_count S T› and
‹conflict_clauses_are_entailed S› and
‹conflict_clauses_are_entailed2 S› and
‹distinct_mset (snd S)› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state (fst S))› and
‹no_complement_set_lit_st S› and
atms: ‹clauses (fst S) = penc N› ‹atms_of_mm N = Σ› and
‹no_smaller_propa (fst S)›
shows
‹no_complement_set_lit_st T›
using assms
proof (induction rule: odpll⇩W_core_stgy_count.induct)
case (propagate S T C)
then show ?case
using atms_of_mm_penc_subset2[of N] ΔΣ_Σ
apply (auto simp: dpll_propagate.simps no_complement_set_lit_st_def no_complement_set_lit_def
dpll⇩W_all_inv_def dest!: multi_member_split)
apply blast
apply blast
apply auto
done
next
case (decided S T C)
have H1: False if ‹Decided (Pos (L⇧↦⇧0)) ∈ set (trail S)›
‹undefined_lit (trail S) (Pos (L⇧↦⇧1))› ‹L ∈ ΔΣ› for L
proof -
have ‹{#Neg (L⇧↦⇧0), Neg (L⇧↦⇧1)#} ∈# clauses S›
using decided that
by (fastforce simp: penc_def additional_constraints_def additional_constraint_def)
then show False
using decided(2) that
apply (auto 7 4 simp: dpll_propagate.simps add_mset_eq_add_mset all_conj_distrib
imp_conjR imp_conjL remove1_mset_empty_iff defined_lit_Neg_Pos_iff lits_of_def
dest!: multi_member_split dest: in_lits_of_l_defined_litD)
apply (metis (full_types) image_iff lit_of.simps(1))
apply auto
apply (metis (full_types) image_iff lit_of.simps(1))
done
qed
have H2: False if ‹Decided (Pos (L⇧↦⇧1)) ∈ set (trail S)›
‹undefined_lit (trail S) (Pos (L⇧↦⇧0))› ‹L ∈ ΔΣ› for L
proof -
have ‹{#Neg (L⇧↦⇧0), Neg (L⇧↦⇧1)#} ∈# clauses S›
using decided that
by (fastforce simp: penc_def additional_constraints_def additional_constraint_def)
then show False
using decided(2) that
apply (auto 7 4 simp: dpll_propagate.simps add_mset_eq_add_mset all_conj_distrib
imp_conjR imp_conjL remove1_mset_empty_iff defined_lit_Neg_Pos_iff lits_of_def
dest!: multi_member_split dest: in_lits_of_l_defined_litD)
apply (metis (full_types) image_iff lit_of.simps(1))
apply auto
apply (metis (full_types) image_iff lit_of.simps(1))
done
qed
have ‹?case ⟷ no_complement_set_lit (trail T)›
using decided(1,7) unfolding no_complement_set_lit_st_def
by (auto simp: odecide.simps)
moreover have ‹no_complement_set_lit (trail T)›
proof -
have H: ‹L ∈ ΔΣ ⟹
Decided (Pos (L⇧↦⇧1)) ∈ set (trail S) ⟹
Decided (Pos (L⇧↦⇧0)) ∈ set (trail S) ⟹ False›
‹L ∈ ΔΣ ⟹ Decided (Neg (L⇧↦⇧1)) ∈ set (trail S) ⟹ False›
‹L ∈ ΔΣ ⟹ Decided (Neg (L⇧↦⇧0)) ∈ set (trail S) ⟹ False›
‹atm_of ` lits_of_l (trail S) ⊆ Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
for L
using decided(7) unfolding no_complement_set_lit_st_def no_complement_set_lit_def
by blast+
have ‹L ∈ ΔΣ ⟹
Decided (Pos (L⇧↦⇧1)) ∈ set (trail T) ⟹
Decided (Pos (L⇧↦⇧0)) ∈ set (trail T) ⟹ False› for L
using decided(1) H(1)[of L] H1[of L] H2[of L]
by (auto simp: odecide.simps no_complement_set_lit_def)
moreover have ‹L ∈ ΔΣ ⟹ Decided (Neg (L⇧↦⇧1)) ∈ set (trail T) ⟹ False› for L
using decided(1) H(2)[of L]
by (auto simp: odecide.simps no_complement_set_lit_def)
moreover have ‹L ∈ ΔΣ ⟹ Decided (Neg (L⇧↦⇧0)) ∈ set (trail T) ⟹ False› for L
using decided(1) H(3)[of L]
by (auto simp: odecide.simps no_complement_set_lit_def)
moreover have ‹atm_of ` lits_of_l (trail T) ⊆ Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
using decided(1) H(4)
by (auto 5 3 simp: odecide.simps no_complement_set_lit_def lits_of_def image_image)
ultimately show ?thesis
by (auto simp: no_complement_set_lit_def)
qed
ultimately show ?case
by fast
next
case (backtrack S T C) note bt = this(1) and ent = this(2) and ent2 = this(3) and dist = this(4)
and invs = this(6)
show ?case
using bt invs
by (auto simp: dpll_backtrack.simps no_complement_set_lit_st_def
backtrack_no_complement_set_lit)
next
case (backtrack_opt S T C) note bt = this(1) and ent = this(2) and ent2 = this(3) and dist = this(4)
and invs = this(6)
show ?case
using bt invs
by (auto simp: bnb.backtrack_opt.simps no_complement_set_lit_st_def
backtrack_no_complement_set_lit)
qed
lemma odpll⇩W_bnb_stgy_count_no_complement_set_lit_st:
assumes
‹odpll⇩W_bnb_stgy_count S T› and
‹conflict_clauses_are_entailed S› and
‹conflict_clauses_are_entailed2 S› and
‹distinct_mset (snd S)› and
invs: ‹dpll⇩W_all_inv (bnb.abs_state (fst S))› and
‹no_complement_set_lit_st S› and
atms: ‹clauses (fst S) = penc N› ‹atms_of_mm N = Σ› and
‹no_smaller_propa (fst S)›
shows
‹no_complement_set_lit_st T›
using odpll⇩W_core_stgy_count_no_complement_set_lit_st[of S T, OF _ assms(2-)] assms(1,6)
by (auto simp: odpll⇩W_bnb_stgy_count.simps no_complement_set_lit_st_def
bnb.dpll⇩W_bound.simps)
definition stgy_invs :: ‹'v clauses ⇒ 'st × _ ⇒ bool› where
‹stgy_invs N S ⟷
no_smaller_propa (fst S) ∧
conflict_clauses_are_entailed S ∧
conflict_clauses_are_entailed2 S ∧
distinct_mset (snd S) ∧
(∀C ∈# snd S. no_dup C) ∧
dpll⇩W_all_inv (bnb.abs_state (fst S)) ∧
no_complement_set_lit_st S ∧
clauses (fst S) = penc N ∧
atms_of_mm N = Σ
›
lemma odpll⇩W_bnb_stgy_count_stgy_invs:
assumes
‹odpll⇩W_bnb_stgy_count S T› and
‹stgy_invs N S›
shows ‹stgy_invs N T›
using odpll⇩W_bnb_stgy_count_conflict_clauses_are_entailed2[of S T]
odpll⇩W_bnb_stgy_count_conflict_clauses_are_entailed[of S T]
odpll⇩W_bnb_stgy_no_smaller_propa[of ‹fst S› ‹fst T›]
odpll⇩W_bnb_stgy_countD[of S T]
odpll⇩W_bnb_stgy_clauses[of ‹fst S› ‹fst T›]
odpll⇩W_core_stgy_count_distinct_mset[of S T]
odpll⇩W_bnb_stgy_count_no_dup_clss[of S T]
odpll⇩W_bnb_stgy_count_distinct_mset[of S T]
assms
odpll⇩W_bnb_stgy_dpll⇩W_bnb_stgy[of ‹fst S› N ‹fst T›]
odpll⇩W_bnb_stgy_count_no_complement_set_lit_st[of S T]
using local.bnb.dpll⇩W_bnb_abs_state_all_inv
unfolding stgy_invs_def
by auto
lemma stgy_invs_size_le:
assumes ‹stgy_invs N S›
shows ‹size (snd S) ≤ 3 ^ (card Σ)›
proof -
have ‹no_smaller_propa (fst S)› and
‹conflict_clauses_are_entailed S› and
ent2: ‹conflict_clauses_are_entailed2 S› and
dist: ‹distinct_mset (snd S)› and
n_d: ‹(∀C ∈# snd S. no_dup C)› and
‹dpll⇩W_all_inv (bnb.abs_state (fst S))› and
nc: ‹no_complement_set_lit_st S› and
Σ: ‹atms_of_mm N = Σ›
using assms unfolding stgy_invs_def by fast+
let ?f = ‹(filter_mset is_decided o mset)›
have ‹distinct_mset (?f `# (snd S))›
apply (subst distinct_image_mset_inj)
subgoal
using ent2 n_d
apply (auto simp: conflict_clauses_are_entailed2_def
inj_on_def add_mset_eq_add_mset dest!: multi_member_split split_list)
using n_d apply auto
apply (metis defined_lit_def multiset_partition set_mset_mset union_iff union_single_eq_member)+
done
subgoal
using dist by auto
done
have H: ‹lit_of `# ?f C ∈ all_sound_trails list_new_vars› if ‹C ∈# (snd S)› for C
proof -
have nc: ‹no_complement_set_lit C› and n_d: ‹no_dup C›
using nc that n_d unfolding no_complement_set_lit_st_def
by (auto dest!: multi_member_split)
have taut: ‹¬tautology (lit_of `# mset C)›
using n_d no_dup_not_tautology by blast
have taut: ‹¬tautology (lit_of `# ?f C)›
apply (rule not_tautology_mono[OF _ taut])
by (simp add: image_mset_subseteq_mono)
have dist: ‹distinct_mset (lit_of `# mset C)›
using n_d no_dup_distinct by blast
have dist: ‹distinct_mset (lit_of `# ?f C)›
apply (rule distinct_mset_mono[OF _ dist])
by (simp add: image_mset_subseteq_mono)
show ?thesis
apply (rule in_all_sound_trails)
subgoal
using nc unfolding no_complement_set_lit_def
by (auto dest!: multi_member_split simp: is_decided_def)
subgoal
using nc unfolding no_complement_set_lit_def
by (auto dest!: multi_member_split simp: is_decided_def)
subgoal
using nc unfolding no_complement_set_lit_def
by (auto dest!: multi_member_split simp: is_decided_def)
subgoal
using nc n_d taut dist unfolding no_complement_set_lit_def set_list_new_vars
by (auto dest!: multi_member_split simp: set_list_new_vars
is_decided_def simple_clss_def atms_of_def lits_of_def
image_image dest!: split_list)
subgoal
by (auto simp: set_list_new_vars)
done
qed
then have incl: ‹set_mset ((image_mset lit_of o ?f) `# (snd S)) ⊆ all_sound_trails list_new_vars›
by auto
have K: ‹xs ≠ [] ⟹ ∃y ys. xs = y # ys› for xs
by (cases xs) auto
have K2: ‹Decided La # zsb = us @ Propagated (L) () # zsa ⟷
(us ≠ [] ∧ hd us = Decided La ∧ zsb = tl us @ Propagated (L) () # zsa)› for La zsb us L zsa
apply (cases us)
apply auto
done
have inj: ‹inj_on ((`#) lit_of ∘ (filter_mset is_decided ∘ mset))
(set_mset (snd S))›
unfolding inj_on_def
proof (intro ballI impI, rule ccontr)
fix x y
assume x: ‹x ∈# snd S› and
y: ‹y ∈# snd S› and
eq: ‹((`#) lit_of ∘ (filter_mset is_decided ∘ mset)) x =
((`#) lit_of ∘ (filter_mset is_decided ∘ mset)) y› and
neq: ‹x ≠ y›
consider
L where ‹Decided L ∈ set x› ‹Propagated (- L) () ∈ set y› |
L where ‹Decided L ∈ set y› ‹Propagated (- L) () ∈ set x›
using ent2 n_d x y unfolding conflict_clauses_are_entailed2_def
by (auto dest!: multi_member_split simp: add_mset_eq_add_mset neq)
then show False
proof cases
case 1
show False
using eq 1(1) multi_member_split[of ‹Decided L› ‹mset x›]
apply auto
by (smt "1"(2) lit_of.simps(2) msed_map_invR multiset_partition n_d
no_dup_cannot_not_lit_and_uminus set_mset_mset union_mset_add_mset_left union_single_eq_member y)
next
case 2
show False
using eq 2 multi_member_split[of ‹Decided L› ‹mset y›]
apply auto
by (smt lit_of.simps(2) msed_map_invR multiset_partition n_d
no_dup_cannot_not_lit_and_uminus set_mset_mset union_mset_add_mset_left union_single_eq_member x)
qed
qed
have [simp]: ‹finite Σ›
unfolding Σ[symmetric]
by auto
have [simp]: ‹Σ ∪ ΔΣ = Σ›
using ΔΣ_Σ by blast
have ‹size (snd S) = size (((image_mset lit_of o ?f) `# (snd S)))›
by auto
also have ‹... = card (set_mset ((image_mset lit_of o ?f) `# (snd S)))›
supply [[goals_limit=1]]
apply (subst distinct_mset_size_eq_card)
apply (subst distinct_image_mset_inj[OF inj])
using dist by auto
also have ‹... ≤ card (all_sound_trails list_new_vars)›
by (rule card_mono[OF _ incl]) simp
also have ‹... ≤ card (simple_clss (Σ - ΔΣ)) * 3 ^ card ΔΣ›
using card_all_sound_trails[of list_new_vars]
by (auto simp: set_list_new_vars distinct_list_new_vars
length_list_new_vars)
also have ‹... ≤ 3 ^ card (Σ - ΔΣ) * 3 ^ card ΔΣ›
using simple_clss_card[of ‹Σ - ΔΣ›]
unfolding set_list_new_vars distinct_list_new_vars
length_list_new_vars
by (auto simp: set_list_new_vars distinct_list_new_vars
length_list_new_vars)
also have ‹... = (3 :: nat) ^ (card Σ)›
unfolding comm_semiring_1_class.semiring_normalization_rules(26)
by (subst card_Un_disjoint[symmetric])
auto
finally show ‹size (snd S) ≤ 3 ^ card Σ›
.
qed
lemma rtranclp_odpll⇩W_bnb_stgy_count_stgy_invs: ‹odpll⇩W_bnb_stgy_count⇧*⇧* S T ⟹ stgy_invs N S ⟹ stgy_invs N T›
apply (induction rule: rtranclp_induct)
apply (auto dest!: odpll⇩W_bnb_stgy_count_stgy_invs)
done
theorem
assumes ‹clauses S = penc N› ‹atms_of_mm N = Σ› and
‹odpll⇩W_bnb_stgy_count⇧*⇧* (S, {#}) (T, D)› and
tr: ‹trail S = []›
shows ‹size D ≤ 3 ^ (card Σ)›
proof -
have i: ‹stgy_invs N (S, {#})›
using tr unfolding no_smaller_propa_def
stgy_invs_def conflict_clauses_are_entailed_def
conflict_clauses_are_entailed2_def assms(1,2)
no_complement_set_lit_st_def no_complement_set_lit_def
dpll⇩W_all_inv_def
by (auto simp: assms(1))
show ?thesis
using rtranclp_odpll⇩W_bnb_stgy_count_stgy_invs[OF assms(3) i]
stgy_invs_size_le[of N ‹(T, D)›]
by auto
qed
end
end