theory CDCL_W_Partial_Encoding
imports CDCL_W_Optimal_Model
begin
lemma consistent_interp_unionI:
‹consistent_interp A ⟹ consistent_interp B ⟹ (⋀a. a ∈ A ⟹ -a ∉ B) ⟹ (⋀a. a ∈ B ⟹ -a ∉ A) ⟹
consistent_interp (A ∪ B)›
by (auto simp: consistent_interp_def)
lemma consistent_interp_poss: ‹consistent_interp (Pos ` A)› and
consistent_interp_negs: ‹consistent_interp (Neg ` A)›
by (auto simp: consistent_interp_def)
lemma Neg_in_lits_of_l_definedD:
‹Neg A ∈ lits_of_l M ⟹ defined_lit M (Pos A)›
by (simp add: Decided_Propagated_in_iff_in_lits_of_l)
subsection ‹Encoding of partial SAT into total SAT›
text ‹As a way to make sure we don't reuse theorems names:›
interpretation test: conflict_driven_clause_learning⇩W_optimal_weight where
state_eq = ‹(=)› and
state = id and
trail = ‹λ(M, N, U, D, W). M› and
init_clss = ‹λ(M, N, U, D, W). N› and
learned_clss = ‹λ(M, N, U, D, W). U› and
conflicting = ‹λ(M, N, U, D, W). D› and
cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
init_state = ‹λN. ([], N, {#}, None, None, ())› and
ρ = ‹λ_. 0› and
update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)›
by unfold_locales (auto simp: state⇩W_ops.additional_info_def)
text ‹
We here formalise the encoding from a formula to another formula from which we will use to derive the
optimal partial model.
While the proofs are still inspired by Dominic Zimmer's upcoming bachelor thesis, we now use the dual
rail encoding, which is more elegant that the solution found by Christoph to solve the problem.
The intended meaning is the following:
▪ \<^term>‹Σ› is the set of all variables
▪ \<^term>‹ΔΣ› is the set of all variables with a (possibly non-zero) weight: These are the variable that needs
to be replaced during encoding, but it does not matter if the weight 0.
›
locale optimal_encoding_opt_ops =
fixes Σ ΔΣ :: ‹'v set› and
new_vars :: ‹'v ⇒ 'v × 'v›
begin
abbreviation replacement_pos :: ‹'v ⇒ 'v› ("(_)⇧↦⇧1" 100) where
‹replacement_pos A ≡ fst (new_vars A)›
abbreviation replacement_neg :: ‹'v ⇒ 'v› ("(_)⇧↦⇧0" 100) where
‹replacement_neg A ≡ snd (new_vars A)›
fun encode_lit where
‹encode_lit (Pos A) = (if A ∈ ΔΣ then Pos (replacement_pos A) else Pos A)› |
‹encode_lit (Neg A) = (if A ∈ ΔΣ then Pos (replacement_neg A) else Neg A)›
lemma encode_lit_alt_def:
‹encode_lit A = (if atm_of A ∈ ΔΣ
then Pos (if is_pos A then replacement_pos (atm_of A) else replacement_neg (atm_of A))
else A)›
by (cases A) auto
definition encode_clause :: ‹'v clause ⇒ 'v clause› where
‹encode_clause C = encode_lit `# C›
lemma encode_clause_simp[simp]:
‹encode_clause {#} = {#}›
‹encode_clause (add_mset A C) = add_mset (encode_lit A) (encode_clause C)›
‹encode_clause (C + D) = encode_clause C + encode_clause D›
by (auto simp: encode_clause_def)
definition encode_clauses :: ‹'v clauses ⇒ 'v clauses› where
‹encode_clauses C = encode_clause `# C›
lemma encode_clauses_simp[simp]:
‹encode_clauses {#} = {#}›
‹encode_clauses (add_mset A C) = add_mset (encode_clause A) (encode_clauses C)›
‹encode_clauses (C + D) = encode_clauses C + encode_clauses D›
by (auto simp: encode_clauses_def)
definition additional_constraint :: ‹'v ⇒ 'v clauses› where
‹additional_constraint A =
{#{#Neg (A⇧↦⇧1), Neg (A⇧↦⇧0)#}#}›
definition additional_constraints :: ‹'v clauses› where
‹additional_constraints = ⋃#(additional_constraint `# (mset_set ΔΣ))›
definition penc :: ‹'v clauses ⇒ 'v clauses› where
‹penc N = encode_clauses N + additional_constraints›
lemma size_encode_clauses[simp]: ‹size (encode_clauses N) = size N›
by (auto simp: encode_clauses_def)
lemma size_penc:
‹size (penc N) = size N + card ΔΣ›
by (auto simp: penc_def additional_constraints_def
additional_constraint_def size_Union_mset_image_mset)
lemma atms_of_mm_additional_constraints: ‹finite ΔΣ ⟹
atms_of_mm additional_constraints = replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
by (auto simp: additional_constraints_def additional_constraint_def atms_of_ms_def)
lemma atms_of_mm_encode_clause_subset:
‹atms_of_mm (encode_clauses N) ⊆ (atms_of_mm N - ΔΣ) ∪ replacement_pos ` {A ∈ ΔΣ. A ∈ atms_of_mm N}
∪ replacement_neg ` {A ∈ ΔΣ. A ∈ atms_of_mm N}›
by (auto simp: encode_clauses_def encode_lit_alt_def atms_of_ms_def atms_of_def
encode_clause_def split: if_splits
dest!: multi_member_split[of _ N])
text ‹In every meaningful application of the theorem below, we have ‹ΔΣ ⊆ atms_of_mm N›.›
lemma atms_of_mm_penc_subset: ‹finite ΔΣ ⟹
atms_of_mm (penc N) ⊆ atms_of_mm N ∪ replacement_pos ` ΔΣ
∪ replacement_neg ` ΔΣ ∪ ΔΣ›
using atms_of_mm_encode_clause_subset[of N]
by (auto simp: penc_def atms_of_mm_additional_constraints)
lemma atms_of_mm_encode_clause_subset2: ‹finite ΔΣ ⟹ ΔΣ ⊆ atms_of_mm N ⟹
atms_of_mm N ⊆ atms_of_mm (encode_clauses N) ∪ ΔΣ›
by (auto simp: encode_clauses_def encode_lit_alt_def atms_of_ms_def atms_of_def
encode_clause_def split: if_splits
dest!: multi_member_split[of _ N])
lemma atms_of_mm_penc_subset2: ‹finite ΔΣ ⟹ ΔΣ ⊆ atms_of_mm N ⟹
atms_of_mm (penc N) = (atms_of_mm N - ΔΣ) ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
using atms_of_mm_encode_clause_subset[of N] atms_of_mm_encode_clause_subset2[of N]
by (auto simp: penc_def atms_of_mm_additional_constraints)
theorem card_atms_of_mm_penc:
assumes ‹finite ΔΣ› and ‹ΔΣ ⊆ atms_of_mm N›
shows ‹card (atms_of_mm (penc N)) ≤ card (atms_of_mm N - ΔΣ) + 2 * card ΔΣ› (is ‹?A ≤ ?B›)
proof -
have ‹?A = card
((atms_of_mm N - ΔΣ) ∪ replacement_pos ` ΔΣ ∪
replacement_neg ` ΔΣ)› (is ‹_ = card (?W ∪ ?X ∪ ?Y)›)
using arg_cong[OF atms_of_mm_penc_subset2[of N], of card] assms card_Un_le
by auto
also have ‹... ≤ card (?W ∪ ?X) + card ?Y›
using card_Un_le[of ‹?W ∪ ?X› ?Y] by auto
also have ‹... ≤ card ?W + card ?X + card ?Y›
using card_Un_le[of ‹?W› ?X] by auto
also have ‹... ≤ card (atms_of_mm N - ΔΣ) + 2 * card ΔΣ›
using card_mono[of ‹atms_of_mm N› ‹ΔΣ›] assms
card_image_le[of ΔΣ replacement_pos] card_image_le[of ΔΣ replacement_neg]
by auto
finally show ?thesis .
qed
definition postp :: ‹'v partial_interp ⇒ 'v partial_interp› where
‹postp I =
{A ∈ I. atm_of A ∉ ΔΣ ∧ atm_of A ∈ Σ} ∪ Pos ` {A. A ∈ ΔΣ ∧ Pos (replacement_pos A) ∈ I}
∪ Neg ` {A. A ∈ ΔΣ ∧ Pos (replacement_neg A) ∈ I ∧ Pos (replacement_pos A) ∉ I}›
lemma preprocess_clss_model_additional_variables2:
assumes
‹atm_of A ∈ Σ - ΔΣ›
shows
‹A ∈ postp I ⟷ A ∈ I› (is ?A)
proof -
show ?A
using assms
by (auto simp: postp_def)
qed
lemma encode_clause_iff:
assumes
‹⋀A. A ∈ ΔΣ ⟹ Pos A ∈ I ⟷ Pos (replacement_pos A) ∈ I›
‹⋀A. A ∈ ΔΣ ⟹ Neg A ∈ I ⟷ Pos (replacement_neg A) ∈ I›
shows ‹I ⊨ encode_clause C ⟷ I ⊨ C›
using assms
apply (induction C)
subgoal by auto
subgoal for A C
by (cases A)
(auto simp: encode_clause_def encode_lit_alt_def split: if_splits)
done
lemma encode_clauses_iff:
assumes
‹⋀A. A ∈ ΔΣ ⟹ Pos A ∈ I ⟷ Pos (replacement_pos A) ∈ I›
‹⋀A. A ∈ ΔΣ ⟹ Neg A ∈ I ⟷ Pos (replacement_neg A) ∈ I›
shows ‹I ⊨m encode_clauses C ⟷ I ⊨m C›
using encode_clause_iff[OF assms]
by (auto simp: encode_clauses_def true_cls_mset_def)
definition Σ⇩a⇩d⇩d where
‹Σ⇩a⇩d⇩d = replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
definition upostp :: ‹'v partial_interp ⇒ 'v partial_interp› where
‹upostp I =
Neg ` {A ∈ Σ. A ∉ ΔΣ ∧ Pos A ∉ I ∧ Neg A ∉ I}
∪ {A ∈ I. atm_of A ∈ Σ ∧ atm_of A ∉ ΔΣ}
∪ Pos ` replacement_pos ` {A ∈ ΔΣ. Pos A ∈ I}
∪ Neg ` replacement_pos ` {A ∈ ΔΣ. Pos A ∉ I}
∪ Pos ` replacement_neg ` {A ∈ ΔΣ. Neg A ∈ I}
∪ Neg ` replacement_neg ` {A ∈ ΔΣ. Neg A ∉ I}›
lemma atm_of_upostp_subset:
‹atm_of ` (upostp I) ⊆
(atm_of ` I - ΔΣ) ∪ replacement_pos ` ΔΣ ∪
replacement_neg ` ΔΣ ∪ Σ›
by (auto simp: upostp_def image_Un)
end
locale optimal_encoding_opt = conflict_driven_clause_learning⇩W_optimal_weight
state_eq
state
trail init_clss learned_clss conflicting
cons_trail tl_trail add_learned_cls remove_cls
update_conflicting
init_state ρ
update_additional_info +
optimal_encoding_opt_ops Σ ΔΣ new_vars
for
state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) and
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'v clause option × '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
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
‹conflicting S = None› and
‹undefined_lit (trail S) L› and
‹atm_of L ∈ atms_of_mm (init_clss S)› and
‹T ∼ cons_trail (Decided L) S› and
‹atm_of L ∈ Σ - ΔΣ› |
odecide_replacement_pos: ‹odecide S T›
if
‹conflicting S = None› and
‹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
‹conflicting S = None› and
‹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›
definition no_new_lonely_clause :: ‹'v clause ⇒ bool› where
‹no_new_lonely_clause C ⟷
(∀L ∈ ΔΣ. L ∈ atms_of C ⟶
Neg (replacement_pos L) ∈# C ∨ Neg (replacement_neg L) ∈# C ∨ C ∈# additional_constraint L)›
definition lonely_weighted_lit_decided where
‹lonely_weighted_lit_decided S ⟷
(∀L ∈ ΔΣ. Decided (Pos L) ∉ set (trail S) ∧ Decided (Neg L) ∉ set (trail S))›
end
locale optimal_encoding_ops = optimal_encoding_opt_ops
Σ ΔΣ
new_vars +
ocdcl_weight ρ
for
Σ ΔΣ :: ‹'v set› and
new_vars :: ‹'v ⇒ 'v × 'v› and
ρ :: ‹'v clause ⇒ 'a :: {linorder}› +
assumes
finite_Σ:
‹finite ΔΣ› and
ΔΣ_Σ:
‹ΔΣ ⊆ Σ› and
new_vars_pos:
‹A ∈ ΔΣ ⟹ replacement_pos A ∉ Σ› and
new_vars_neg:
‹A ∈ ΔΣ ⟹ replacement_neg A ∉ Σ› and
new_vars_dist:
‹inj_on replacement_pos ΔΣ›
‹inj_on replacement_neg ΔΣ›
‹replacement_pos ` ΔΣ ∩ replacement_neg ` ΔΣ = {}› and
Σ_no_weight:
‹atm_of C ∈ Σ - ΔΣ ⟹ ρ (add_mset C M) = ρ M›
begin
lemma new_vars_dist2:
‹A ∈ ΔΣ ⟹ B ∈ ΔΣ ⟹ A ≠ B ⟹ replacement_pos A ≠ replacement_pos B›
‹A ∈ ΔΣ ⟹ B ∈ ΔΣ ⟹ A ≠ B ⟹ replacement_neg A ≠ replacement_neg B›
‹A ∈ ΔΣ ⟹ B ∈ ΔΣ ⟹ replacement_neg A ≠ replacement_pos B›
using new_vars_dist unfolding inj_on_def apply blast
using new_vars_dist unfolding inj_on_def apply blast
using new_vars_dist unfolding inj_on_def apply blast
done
lemma consistent_interp_postp:
‹consistent_interp I ⟹ consistent_interp (postp I)›
by (auto simp: consistent_interp_def postp_def uminus_lit_swap)
text ‹The reverse of the previous theorem does not hold due to the filtering on the variables of
\<^term>‹ΔΣ›. One example of version that holds:›
lemma
assumes ‹A ∈ ΔΣ›
shows ‹consistent_interp (postp {Pos A , Neg A})› and
‹¬consistent_interp {Pos A, Neg A}›
using assms ΔΣ_Σ
by (auto simp: consistent_interp_def postp_def uminus_lit_swap)
text ‹Some more restricted version of the reverse hold, like:›
lemma consistent_interp_postp_iff:
‹atm_of ` I ⊆ Σ - ΔΣ ⟹ consistent_interp I ⟷ consistent_interp (postp I)›
by (auto simp: consistent_interp_def postp_def uminus_lit_swap)
lemma new_vars_different_iff[simp]:
‹A ≠ x⇧↦⇧1›
‹A ≠ x⇧↦⇧0›
‹x⇧↦⇧1 ≠ A›
‹x⇧↦⇧0 ≠ A›
‹A⇧↦⇧0 ≠ x⇧↦⇧1›
‹A⇧↦⇧1 ≠ x⇧↦⇧0›
‹A⇧↦⇧0 = x⇧↦⇧0 ⟷ A = x›
‹A⇧↦⇧1 = x⇧↦⇧1 ⟷ A = x›
‹(A⇧↦⇧1) ∉ Σ›
‹(A⇧↦⇧0) ∉ Σ›
‹(A⇧↦⇧1) ∉ ΔΣ›
‹(A⇧↦⇧0) ∉ ΔΣ›if ‹A ∈ ΔΣ› ‹x ∈ ΔΣ› for A x
using ΔΣ_Σ new_vars_pos[of x] new_vars_pos[of A] new_vars_neg[of x] new_vars_neg[of A]
new_vars_neg new_vars_dist2[of A x] new_vars_dist2[of x A] that
by (cases ‹A = x›; fastforce simp: comp_def; fail)+
lemma consistent_interp_upostp:
‹consistent_interp I ⟹ consistent_interp (upostp I)›
using ΔΣ_Σ
by (auto simp: consistent_interp_def upostp_def uminus_lit_swap)
lemma atm_of_upostp_subset2:
‹atm_of ` I ⊆ Σ ⟹ replacement_pos ` ΔΣ ∪
replacement_neg ` ΔΣ ∪ (Σ - ΔΣ) ⊆ atm_of ` (upostp I)›
apply (auto simp: upostp_def image_Un image_image)
apply (metis (mono_tags, lifting) imageI literal.sel(1) mem_Collect_eq)
apply (metis (mono_tags, lifting) imageI literal.sel(2) mem_Collect_eq)
done
lemma ΔΣ_notin_upost[simp]:
‹y ∈ ΔΣ ⟹ Neg y ∉ upostp I›
‹y ∈ ΔΣ ⟹ Pos y ∉ upostp I›
using ΔΣ_Σ by (auto simp: upostp_def)
lemma penc_ent_upostp:
assumes Σ: ‹atms_of_mm N = Σ› and
sat: ‹I ⊨sm N› and
cons: ‹consistent_interp I› and
atm: ‹atm_of ` I ⊆ atms_of_mm N›
shows ‹upostp I ⊨m penc N›
proof -
have [iff]: ‹Pos (A⇧↦⇧0) ∉ I› ‹Pos (A⇧↦⇧1) ∉ I›
‹Neg (A⇧↦⇧0) ∉ I› ‹Neg (A⇧↦⇧1) ∉ I› if ‹A ∈ ΔΣ› for A
using atm new_vars_neg[of A] new_vars_pos[of A] that
unfolding Σ by force+
have enc: ‹upostp I ⊨m encode_clauses N›
unfolding true_cls_mset_def
proof
fix C
assume ‹C ∈# encode_clauses N›
then obtain C' where
‹C' ∈# N› and
‹C = encode_clause C'›
by (auto simp: encode_clauses_def)
then obtain A where
‹A ∈# C'› and
‹A ∈ I›
using sat
by (auto simp: true_cls_def
dest!: multi_member_split[of _ N])
moreover have ‹atm_of A ∈ Σ - ΔΣ ∨ atm_of A ∈ ΔΣ›
using atm ‹A ∈ I› unfolding Σ by blast
ultimately have ‹encode_lit A ∈ upostp I›
by (auto simp: encode_lit_alt_def upostp_def)
then show ‹upostp I ⊨ C›
using ‹A ∈# C'›
unfolding ‹C = encode_clause C'›
by (auto simp: encode_clause_def dest: multi_member_split)
qed
have [iff]: ‹Pos (y⇧↦⇧1) ∉ upostp I ⟷ Neg (y⇧↦⇧1) ∈ upostp I›
‹Pos (y⇧↦⇧0) ∉ upostp I ⟷ Neg (y⇧↦⇧0) ∈ upostp I›
if ‹y ∈ ΔΣ› for y
using that
by (cases ‹Pos y ∈ I›; auto simp: upostp_def image_image; fail)+
have H:
‹Neg (y⇧↦⇧0) ∉ upostp I ⟹ Neg (y⇧↦⇧1) ∈ upostp I›
if ‹y ∈ ΔΣ› for y
using that cons ΔΣ_Σ unfolding upostp_def consistent_interp_def
by (cases ‹Pos y ∈ I›) (auto simp: image_image)
have [dest]: ‹Neg A ∈ upostp I ⟹ Pos A ∉ upostp I›
‹Pos A ∈ upostp I ⟹ Neg A ∉ upostp I› for A
using consistent_interp_upostp[OF cons]
by (auto simp: consistent_interp_def)
have add: ‹upostp I ⊨m additional_constraints›
using finite_Σ H
by (auto simp: additional_constraints_def true_cls_mset_def additional_constraint_def)
show ‹upostp I ⊨m penc N›
using enc add unfolding penc_def by auto
qed
lemma penc_ent_postp:
assumes Σ: ‹atms_of_mm N = Σ› and
sat: ‹I ⊨sm penc N› and
cons: ‹consistent_interp I›
shows ‹postp I ⊨m N›
proof -
have enc: ‹I ⊨m encode_clauses N› and ‹I ⊨m additional_constraints›
using sat unfolding penc_def
by auto
have [dest]: ‹Pos (x2⇧↦⇧0) ∈ I ⟹ Neg (x2⇧↦⇧1) ∈ I› if ‹x2 ∈ ΔΣ› for x2
using ‹I ⊨m additional_constraints› that cons
multi_member_split[of x2 ‹mset_set ΔΣ›] finite_Σ
unfolding additional_constraints_def additional_constraint_def
consistent_interp_def
by (auto simp: true_cls_mset_def)
have [dest]: ‹Pos (x2⇧↦⇧0) ∈ I ⟹ Pos (x2⇧↦⇧1) ∉ I› if ‹x2 ∈ ΔΣ› for x2
using that cons
unfolding consistent_interp_def
by auto
show ‹postp I ⊨m N›
unfolding true_cls_mset_def
proof
fix C
assume ‹C ∈# N›
then have ‹I ⊨ encode_clause C›
using enc by (auto dest!: multi_member_split)
then show ‹postp I ⊨ C›
unfolding true_cls_def
using cons finite_Σ sat
preprocess_clss_model_additional_variables2[of _ I]
Σ ‹C ∈# N› in_m_in_literals
apply (auto simp: encode_clause_def postp_def encode_lit_alt_def
split: if_splits
dest!: multi_member_split[of _ C])
using image_iff apply fastforce
apply (case_tac xa; auto)
apply auto
done
qed
qed
lemma satisfiable_penc_satisfiable:
assumes Σ: ‹atms_of_mm N = Σ› and
sat: ‹satisfiable (set_mset (penc N))›
shows ‹satisfiable (set_mset N)›
using assms apply (subst (asm) satisfiable_def)
apply clarify
subgoal for I
using penc_ent_postp[OF Σ, of I] consistent_interp_postp[of I]
by auto
done
lemma satisfiable_penc:
assumes Σ: ‹atms_of_mm N = Σ› and
sat: ‹satisfiable (set_mset N)›
shows ‹satisfiable (set_mset (penc N))›
using assms
apply (subst (asm) satisfiable_def_min)
apply clarify
subgoal for I
using penc_ent_upostp[of N I] consistent_interp_upostp[of I]
by auto
done
lemma satisfiable_penc_iff:
assumes Σ: ‹atms_of_mm N = Σ›
shows ‹satisfiable (set_mset (penc N)) ⟷ satisfiable (set_mset N)›
using assms satisfiable_penc satisfiable_penc_satisfiable by blast
abbreviation ρ⇩e_filter :: ‹'v literal multiset ⇒ 'v literal multiset› where
‹ρ⇩e_filter M ≡ {#L ∈# poss (mset_set ΔΣ). Pos (atm_of L⇧↦⇧1) ∈# M#} +
{#L ∈# negs (mset_set ΔΣ). Pos (atm_of L⇧↦⇧0) ∈# M#}›
lemma finite_upostp: ‹finite I ⟹ finite Σ ⟹ finite (upostp I)›
using finite_Σ ΔΣ_Σ
by (auto simp: upostp_def)
declare finite_Σ[simp]
lemma encode_lit_eq_iff:
‹atm_of x ∈ Σ ⟹ atm_of y ∈ Σ ⟹ encode_lit x = encode_lit y ⟷ x = y›
by (cases x; cases y) (auto simp: encode_lit_alt_def atm_of_eq_atm_of)
lemma distinct_mset_encode_clause_iff:
‹atms_of N ⊆ Σ ⟹ distinct_mset (encode_clause N) ⟷ distinct_mset N›
by (induction N)
(auto simp: encode_clause_def encode_lit_eq_iff
dest!: multi_member_split)
lemma distinct_mset_encodes_clause_iff:
‹atms_of_mm N ⊆ Σ ⟹ distinct_mset_mset (encode_clauses N) ⟷ distinct_mset_mset N›
by (induction N)
(auto simp: encode_clauses_def distinct_mset_encode_clause_iff)
lemma distinct_additional_constraints[simp]:
‹distinct_mset_mset additional_constraints›
by (auto simp: additional_constraints_def additional_constraint_def
distinct_mset_set_def)
lemma distinct_mset_penc:
‹atms_of_mm N ⊆ Σ ⟹ distinct_mset_mset (penc N) ⟷ distinct_mset_mset N›
by (auto simp: penc_def
distinct_mset_encodes_clause_iff)
lemma finite_postp: ‹finite I ⟹ finite (postp I)›
by (auto simp: postp_def)
lemma total_entails_iff_no_conflict:
assumes ‹atms_of_mm N ⊆ atm_of ` I› and ‹consistent_interp I›
shows ‹I ⊨sm N ⟷ (∀C ∈# N. ¬I ⊨s CNot C)›
apply rule
subgoal
using assms by (auto dest!: multi_member_split
simp: consistent_CNot_not)
subgoal
by (smt assms(1) atms_of_atms_of_ms_mono atms_of_ms_CNot_atms_of
atms_of_ms_insert atms_of_ms_mono atms_of_s_def empty_iff
subset_iff sup.orderE total_not_true_cls_true_clss_CNot
total_over_m_alt_def true_clss_def)
done
definition ρ⇩e :: ‹'v literal multiset ⇒ 'a :: {linorder}› where
‹ρ⇩e M = ρ (ρ⇩e_filter M)›
lemma Σ_no_weight_ρ⇩e: ‹atm_of C ∈ Σ - ΔΣ ⟹ ρ⇩e (add_mset C M) = ρ⇩e M›
using Σ_no_weight[of C ‹ρ⇩e_filter M›]
apply (auto simp: ρ⇩e_def finite_Σ image_mset_mset_set inj_on_Neg inj_on_Pos)
by (smt Collect_cong image_iff literal.sel(1) literal.sel(2) new_vars_neg new_vars_pos)
lemma ρ_cancel_notin_ΔΣ:
‹(⋀x. x ∈# M ⟹ atm_of x ∈ Σ - ΔΣ) ⟹ ρ (M + M') = ρ M'›
by (induction M) (auto simp: Σ_no_weight)
lemma ρ_mono2:
‹consistent_interp (set_mset M') ⟹ distinct_mset M' ⟹
(⋀A. A ∈# M ⟹ atm_of A ∈ Σ) ⟹ (⋀A. A ∈# M' ⟹ atm_of A ∈ Σ) ⟹
{#A ∈# M. atm_of A ∈ ΔΣ#} ⊆# {#A ∈# M'. atm_of A ∈ ΔΣ#} ⟹ ρ M ≤ ρ M'›
apply (subst (2) multiset_partition[of _ ‹λA. atm_of A ∉ ΔΣ›])
apply (subst multiset_partition[of _ ‹λA. atm_of A ∉ ΔΣ›])
apply (subst ρ_cancel_notin_ΔΣ)
subgoal by auto
apply (subst ρ_cancel_notin_ΔΣ)
subgoal by auto
by (auto intro!: ρ_mono intro: consistent_interp_subset intro!: distinct_mset_mono[of _ M'])
lemma ρ⇩e_mono: ‹distinct_mset B ⟹ A ⊆# B ⟹ ρ⇩e A ≤ ρ⇩e B›
unfolding ρ⇩e_def
apply (rule ρ_mono)
subgoal
by (subst distinct_mset_add)
(auto simp: distinct_image_mset_inj distinct_mset_filter distinct_mset_mset_set inj_on_Pos
mset_inter_empty_set_mset image_mset_mset_set inj_on_Neg)
subgoal
by (rule subset_mset.add_mono; rule filter_mset_mono_subset) auto
done
lemma ρ⇩e_upostp_ρ:
assumes [simp]: ‹finite Σ› and
‹finite I› and
cons: ‹consistent_interp I› and
I_Σ: ‹atm_of ` I ⊆ Σ›
shows ‹ρ⇩e (mset_set (upostp I)) = ρ (mset_set I)› (is ‹?A = ?B›)
proof -
have [simp]: ‹finite I›
using assms by auto
have [simp]: ‹mset_set
{x ∈ I.
atm_of x ∈ Σ ∧
atm_of x ∉ replacement_pos ` ΔΣ ∧
atm_of x ∉ replacement_neg ` ΔΣ} = mset_set I›
using I_Σ by auto
have [simp]: ‹finite {A ∈ ΔΣ. P A}› for P
by (rule finite_subset[of _ ΔΣ])
(use ΔΣ_Σ finite_Σ in auto)
have [dest]: ‹xa ∈ ΔΣ ⟹ Pos (xa⇧↦⇧1) ∈ upostp I ⟹ Pos (xa⇧↦⇧0) ∈ upostp I ⟹ False› for xa
using cons unfolding penc_def
by (auto simp: additional_constraint_def additional_constraints_def
true_cls_mset_def consistent_interp_def upostp_def)
have ‹?A ≤ ?B›
using assms ΔΣ_Σ apply -
unfolding ρ⇩e_def filter_filter_mset
apply (rule ρ_mono2)
subgoal using cons by auto
subgoal using distinct_mset_mset_set by auto
subgoal by auto
subgoal by auto
apply (rule filter_mset_mono_subset)
subgoal
by (subst distinct_subseteq_iff[symmetric])
(auto simp: upostp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)
subgoal for x
by (cases ‹x ∈ I›; cases x) (auto simp: upostp_def)
done
moreover have ‹?B ≤ ?A›
using assms ΔΣ_Σ apply -
unfolding ρ⇩e_def filter_filter_mset
apply (rule ρ_mono2)
subgoal using cons by (auto intro:
intro: consistent_interp_subset[of _ ‹Pos ` ΔΣ›]
intro: consistent_interp_subset[of _ ‹Neg ` ΔΣ›]
intro!: consistent_interp_unionI
simp: consistent_interp_upostp finite_upostp consistent_interp_poss
consistent_interp_negs)
subgoal by (auto
simp: distinct_mset_mset_set distinct_mset_add image_mset_mset_set inj_on_Pos inj_on_Neg
mset_inter_empty_set_mset)
subgoal by auto
subgoal by auto
apply (auto simp: image_mset_mset_set inj_on_Neg inj_on_Pos)
apply (subst distinct_subseteq_iff[symmetric])
apply (auto simp: distinct_mset_mset_set distinct_mset_add image_mset_mset_set inj_on_Pos inj_on_Neg
mset_inter_empty_set_mset finite_upostp)
apply (metis image_eqI literal.exhaust_sel)
apply (auto simp: upostp_def image_image)
apply (metis (mono_tags, lifting) imageI literal.collapse(1) literal.collapse(2) mem_Collect_eq)
apply (metis (mono_tags, lifting) imageI literal.collapse(1) literal.collapse(2) mem_Collect_eq)
apply (metis (mono_tags, lifting) imageI literal.collapse(1) literal.collapse(2) mem_Collect_eq)
done
ultimately show ?thesis
by simp
qed
end
locale optimal_encoding = optimal_encoding_opt
state_eq
state
trail init_clss learned_clss conflicting
cons_trail tl_trail add_learned_cls remove_cls
update_conflicting
init_state
update_additional_info
Σ ΔΣ
ρ
new_vars +
optimal_encoding_ops
Σ ΔΣ
new_vars ρ
for
state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) and
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'v clause option × '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 clause ⇒ 'a :: {linorder}› and
update_additional_info :: ‹'v clause option × 'b ⇒ 'st ⇒ 'st› and
Σ ΔΣ :: ‹'v set› and
new_vars :: ‹'v ⇒ 'v × 'v›
begin
interpretation enc_weight_opt: conflict_driven_clause_learning⇩W_optimal_weight where
state_eq = state_eq and
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state and
ρ = ρ⇩e and
update_additional_info = update_additional_info
apply unfold_locales
subgoal by (rule ρ⇩e_mono)
subgoal using update_additional_info by fast
subgoal using weight_init_state by fast
done
theorem full_encoding_OCDCL_correctness:
assumes
st: ‹full enc_weight_opt.cdcl_bnb_stgy (init_state (penc N)) T› and
dist: ‹distinct_mset_mset N› and
atms: ‹atms_of_mm N = Σ›
shows
‹weight T = None ⟹ unsatisfiable (set_mset N)› and
‹weight T ≠ None ⟹ postp (set_mset (the (weight T))) ⊨sm N›
‹weight T ≠ None ⟹ distinct_mset I ⟹ consistent_interp (set_mset I) ⟹
atms_of I ⊆ atms_of_mm N ⟹ set_mset I ⊨sm N ⟹
ρ I ≥ ρ (mset_set (postp (set_mset (the (weight T)))))›
‹weight T ≠ None ⟹ ρ⇩e (the (enc_weight_opt.weight T)) =
ρ (mset_set (postp (set_mset (the (enc_weight_opt.weight T)))))›
proof -
let ?N = ‹penc N›
have ‹distinct_mset_mset (penc N)›
by (subst distinct_mset_penc)
(use dist atms in auto)
then have
unsat: ‹weight T = None ⟹ unsatisfiable (set_mset ?N)› and
model: ‹weight T ≠ None ⟹ consistent_interp (set_mset (the (weight T))) ∧
atms_of (the (weight T)) ⊆ atms_of_mm ?N ∧ set_mset (the (weight T)) ⊨sm ?N ∧
distinct_mset (the (weight T))› and
opt: ‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm ?N ⟹
set_mset I ⊨sm ?N ⟹ Found (ρ⇩e I) ≥ enc_weight_opt.ρ' (weight T)›
for I
using enc_weight_opt.full_cdcl_bnb_stgy_no_conflicting_clause_from_init_state[of
‹penc N› T, OF st]
by fast+
show ‹unsatisfiable (set_mset N)› if ‹weight T = None›
using unsat[OF that] satisfiable_penc[OF atms] by blast
let ?K = ‹postp (set_mset (the (weight T)))›
show ‹?K ⊨sm N› if ‹weight T ≠ None›
using penc_ent_postp[OF atms, of ‹set_mset (the (weight T))›] model[OF that]
by auto
assume Some: ‹weight T ≠ None›
have Some': ‹enc_weight_opt.weight T ≠ None›
using Some by auto
have cons_K: ‹consistent_interp ?K›
using model Some by (auto simp: consistent_interp_postp)
define J where ‹J = the (weight T)›
then have [simp]: ‹weight T = Some J› ‹enc_weight_opt.weight T = Some J›
using Some by auto
have ‹set_mset J ⊨sm additional_constraints›
using model by (auto simp: penc_def)
then have H: ‹x ∈ ΔΣ ⟹ Neg (replacement_pos x) ∈# J ∨ Neg (replacement_neg x) ∈# J› and
[dest]: ‹Pos (xa⇧↦⇧1) ∈# J ⟹ Pos (xa⇧↦⇧0) ∈# J ⟹ xa ∈ ΔΣ ⟹ False› for x xa
using model
apply (auto simp: additional_constraints_def additional_constraint_def true_clss_def
consistent_interp_def)
by (metis uminus_Pos)
have cons_f: ‹consistent_interp (set_mset (ρ⇩e_filter (the (weight T))))›
using model
by (auto simp: postp_def ρ⇩e_def Σ⇩a⇩d⇩d_def conj_disj_distribR
consistent_interp_poss
consistent_interp_negs
mset_set_Union intro!: consistent_interp_unionI
intro: consistent_interp_subset distinct_mset_mset_set
consistent_interp_subset[of _ ‹Pos ` ΔΣ›]
consistent_interp_subset[of _ ‹Neg ` ΔΣ›])
have dist_f: ‹distinct_mset ((ρ⇩e_filter (the (weight T))))›
using model
by (auto simp: postp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)
have ‹enc_weight_opt.ρ' (weight T) ≤ Found (ρ (mset_set ?K))›
using Some'
apply auto
unfolding ρ⇩e_def
apply (rule ρ_mono2)
subgoal
using model Some' by (auto simp: finite_postp consistent_interp_postp)
subgoal by (auto simp: distinct_mset_mset_set)
subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
subgoal
apply (subst distinct_subseteq_iff[symmetric])
using dist model[OF Some] H
by (force simp: filter_filter_mset consistent_interp_def postp_def
image_mset_mset_set inj_on_Neg inj_on_Pos finite_postp
distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set
intro: distinct_mset_mono[of _ ‹the (enc_weight_opt.weight T)›])+
done
moreover {
have ‹ρ (mset_set ?K) ≤ ρ⇩e (the (weight T))›
unfolding ρ⇩e_def
apply (rule ρ_mono2)
subgoal by (rule cons_f)
subgoal by (rule dist_f)
subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
subgoal
by (subst distinct_subseteq_iff[symmetric])
(auto simp: postp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)
done
then have ‹Found (ρ (mset_set ?K)) ≤ enc_weight_opt.ρ' (weight T)›
using Some by auto
} note le =this
ultimately show ‹ρ⇩e (the (weight T)) = (ρ (mset_set ?K))›
using Some' by auto
show ‹ρ I ≥ ρ (mset_set ?K)›
if dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
atm: ‹atms_of I ⊆ atms_of_mm N› and
I_N: ‹set_mset I ⊨sm N›
proof -
let ?I = ‹mset_set (upostp (set_mset I))›
have [simp]: ‹finite (upostp (set_mset I))›
by (rule finite_upostp)
(use atms in auto)
then have I: ‹set_mset ?I = upostp (set_mset I)›
by auto
have ‹set_mset ?I ⊨m ?N›
unfolding I
by (rule penc_ent_upostp[OF atms I_N cons])
(use atm in ‹auto dest: multi_member_split›)
moreover have ‹distinct_mset ?I›
by (rule distinct_mset_mset_set)
moreover {
have A: ‹atms_of (mset_set (upostp (set_mset I))) = atm_of ` (upostp (set_mset I))›
‹atm_of ` set_mset I = atms_of I›
by (auto simp: atms_of_def)
have ‹atms_of ?I = atms_of_mm ?N›
apply (subst atms_of_mm_penc_subset2[OF finite_Σ])
subgoal using ΔΣ_Σ atms by auto
subgoal
using atm_of_upostp_subset[of ‹set_mset I›] atm_of_upostp_subset2[of ‹set_mset I›] atm
unfolding atms A
by (auto simp: upostp_def)
done
}
moreover have cons': ‹consistent_interp (set_mset ?I)›
using cons unfolding I by (rule consistent_interp_upostp)
ultimately have ‹Found (ρ⇩e ?I) ≥ enc_weight_opt.ρ' (weight T)›
using opt[of ?I] by auto
moreover {
have ‹ρ⇩e ?I = ρ (mset_set (set_mset I))›
by (rule ρ⇩e_upostp_ρ)
(use ΔΣ_Σ atms atm cons in ‹auto dest: multi_member_split›)
then have ‹ρ⇩e ?I = ρ I›
by (subst (asm) distinct_mset_set_mset_ident)
(use atms dist in auto)
}
ultimately have ‹Found (ρ I) ≥ enc_weight_opt.ρ' (weight T)›
using Some'
by auto
moreover {
have ‹ρ⇩e (mset_set ?K) ≤ ρ⇩e (mset_set (set_mset (the (weight T))))›
unfolding ρ⇩e_def
apply (rule ρ_mono2)
subgoal using cons_f by auto
subgoal using dist_f by auto
subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
subgoal
by (subst distinct_subseteq_iff[symmetric])
(auto simp: postp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)
done
then have ‹Found (ρ⇩e (mset_set ?K)) ≤ enc_weight_opt.ρ' (weight T)›
apply (subst (asm) distinct_mset_set_mset_ident)
apply (use atms dist model[OF Some] in auto; fail)[]
using Some' by auto
}
moreover have ‹ρ⇩e (mset_set ?K) ≤ ρ (mset_set ?K)›
unfolding ρ⇩e_def
apply (rule ρ_mono2)
subgoal
using model Some' by (auto simp: finite_postp consistent_interp_postp)
subgoal by (auto simp: distinct_mset_mset_set)
subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
subgoal using atms dist model[OF Some] atms ΔΣ_Σ by (auto simp: postp_def)
subgoal
by (subst distinct_subseteq_iff[symmetric])
(auto simp: postp_def simp: image_mset_mset_set inj_on_Neg inj_on_Pos
distinct_mset_add mset_inter_empty_set_mset distinct_mset_mset_set)
done
ultimately show ?thesis
using Some' le by auto
qed
qed
inductive ocdcl⇩W_o_r :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
decide: "odecide S S' ⟹ ocdcl⇩W_o_r S S'" |
bj: "enc_weight_opt.cdcl_bnb_bj S S' ⟹ ocdcl⇩W_o_r S S'"
inductive cdcl_bnb_r :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
cdcl_conflict: "conflict S S' ⟹ cdcl_bnb_r S S'" |
cdcl_propagate: "propagate S S' ⟹ cdcl_bnb_r S S'" |
cdcl_improve: "enc_weight_opt.improvep S S' ⟹ cdcl_bnb_r S S'" |
cdcl_conflict_opt: "enc_weight_opt.conflict_opt S S' ⟹ cdcl_bnb_r S S'" |
cdcl_o': "ocdcl⇩W_o_r S S' ⟹ cdcl_bnb_r S S'"
inductive cdcl_bnb_r_stgy :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
cdcl_bnb_r_conflict: "conflict S S' ⟹ cdcl_bnb_r_stgy S S'" |
cdcl_bnb_r_propagate: "propagate S S' ⟹ cdcl_bnb_r_stgy S S'" |
cdcl_bnb_r_improve: "enc_weight_opt.improvep S S' ⟹ cdcl_bnb_r_stgy S S'" |
cdcl_bnb_r_conflict_opt: "enc_weight_opt.conflict_opt S S' ⟹ cdcl_bnb_r_stgy S S'" |
cdcl_bnb_r_other': "ocdcl⇩W_o_r S S' ⟹ no_confl_prop_impr S ⟹ cdcl_bnb_r_stgy S S'"
lemma ocdcl⇩W_o_r_cases[consumes 1, case_names odecode obacktrack skip resolve]:
assumes
‹ocdcl⇩W_o_r S T›
‹odecide S T ⟹ P T›
‹enc_weight_opt.obacktrack S T ⟹ P T›
‹skip S T ⟹ P T›
‹resolve S T ⟹ P T›
shows ‹P T›
using assms by (auto simp: ocdcl⇩W_o_r.simps enc_weight_opt.cdcl_bnb_bj.simps)
context
fixes S :: 'st
assumes S_Σ: ‹atms_of_mm (init_clss S) = (Σ - ΔΣ) ∪ replacement_pos ` ΔΣ
∪ replacement_neg ` ΔΣ›
begin
lemma odecide_decide:
‹odecide S T ⟹ decide S T›
apply (elim odecideE)
subgoal for L
by (rule decide.intros[of S ‹L›]) auto
subgoal for L
by (rule decide.intros[of S ‹Pos (L⇧↦⇧1)›]) (use S_Σ ΔΣ_Σ in auto)
subgoal for L
by (rule decide.intros[of S ‹Pos (L⇧↦⇧0)›]) (use S_Σ ΔΣ_Σ in auto)
done
lemma ocdcl⇩W_o_r_ocdcl⇩W_o:
‹ocdcl⇩W_o_r S T ⟹ enc_weight_opt.ocdcl⇩W_o S T›
using S_Σ by (auto simp: ocdcl⇩W_o_r.simps enc_weight_opt.ocdcl⇩W_o.simps
dest: odecide_decide)
lemma cdcl_bnb_r_cdcl_bnb:
‹cdcl_bnb_r S T ⟹ enc_weight_opt.cdcl_bnb S T›
using S_Σ by (auto simp: cdcl_bnb_r.simps enc_weight_opt.cdcl_bnb.simps
dest: ocdcl⇩W_o_r_ocdcl⇩W_o)
lemma cdcl_bnb_r_stgy_cdcl_bnb_stgy:
‹cdcl_bnb_r_stgy S T ⟹ enc_weight_opt.cdcl_bnb_stgy S T›
using S_Σ by (auto simp: cdcl_bnb_r_stgy.simps enc_weight_opt.cdcl_bnb_stgy.simps
dest: ocdcl⇩W_o_r_ocdcl⇩W_o)
end
context
fixes S :: 'st
assumes S_Σ: ‹atms_of_mm (init_clss S) = (Σ - ΔΣ) ∪ replacement_pos ` ΔΣ
∪ replacement_neg ` ΔΣ›
begin
lemma rtranclp_cdcl_bnb_r_cdcl_bnb:
‹cdcl_bnb_r⇧*⇧* S T ⟹ enc_weight_opt.cdcl_bnb⇧*⇧* S T›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for T U
using S_Σ enc_weight_opt.rtranclp_cdcl_bnb_no_more_init_clss[of S T]
by(auto dest: cdcl_bnb_r_cdcl_bnb)
done
lemma rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_stgy:
‹cdcl_bnb_r_stgy⇧*⇧* S T ⟹ enc_weight_opt.cdcl_bnb_stgy⇧*⇧* S T›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for T U
using S_Σ
enc_weight_opt.rtranclp_cdcl_bnb_no_more_init_clss[of S T,
OF enc_weight_opt.rtranclp_cdcl_bnb_stgy_cdcl_bnb]
by (auto dest: cdcl_bnb_r_stgy_cdcl_bnb_stgy)
done
lemma rtranclp_cdcl_bnb_r_all_struct_inv:
‹cdcl_bnb_r⇧*⇧* S T ⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S) ⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state T)›
using rtranclp_cdcl_bnb_r_cdcl_bnb[of T]
enc_weight_opt.rtranclp_cdcl_bnb_stgy_all_struct_inv by blast
lemma rtranclp_cdcl_bnb_r_stgy_all_struct_inv:
‹cdcl_bnb_r_stgy⇧*⇧* S T ⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S) ⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state T)›
using rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_stgy[of T]
enc_weight_opt.rtranclp_cdcl_bnb_stgy_all_struct_inv[of S T]
enc_weight_opt.rtranclp_cdcl_bnb_stgy_cdcl_bnb[of S T]
by auto
end
lemma no_step_cdcl_bnb_r_stgy_no_step_cdcl_bnb_stgy:
assumes
N: ‹init_clss S = penc N› and
Σ: ‹atms_of_mm N = Σ› and
n_d: ‹no_dup (trail S)› and
tr_alien: ‹atm_of ` lits_of_l (trail S) ⊆ Σ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
shows
‹no_step cdcl_bnb_r_stgy S ⟷ no_step enc_weight_opt.cdcl_bnb_stgy S› (is ‹?A ⟷ ?B›)
proof
assume ?B
then show ‹?A›
using N cdcl_bnb_r_stgy_cdcl_bnb_stgy[of S] atms_of_mm_encode_clause_subset[of N]
atms_of_mm_encode_clause_subset2[of N] finite_Σ ΔΣ_Σ
atms_of_mm_penc_subset2[of N]
by (auto simp: Σ)
next
assume ?A
then have
nsd: ‹no_step odecide S› and
nsp: ‹no_step propagate S› and
nsc: ‹no_step conflict S› and
nsi: ‹no_step enc_weight_opt.improvep S› and
nsco: ‹no_step enc_weight_opt.conflict_opt S›
by (auto simp: cdcl_bnb_r_stgy.simps ocdcl⇩W_o_r.simps)
have
nsi': ‹⋀M'. conflicting S = None ⟹ ¬enc_weight_opt.is_improving (trail S) M' S› and
nsco': ‹conflicting S = None ⟹ negate_ann_lits (trail S) ∉# enc_weight_opt.conflicting_clss S›
using nsi nsco unfolding enc_weight_opt.improvep.simps enc_weight_opt.conflict_opt.simps
by auto
have N_Σ: ‹atms_of_mm (penc N) =
(Σ - ΔΣ) ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ›
using N Σ cdcl_bnb_r_stgy_cdcl_bnb_stgy[of S] atms_of_mm_encode_clause_subset[of N]
atms_of_mm_encode_clause_subset2[of N] finite_Σ ΔΣ_Σ
atms_of_mm_penc_subset2[of N]
by auto
have False if dec: ‹decide S T› for T
proof -
obtain L where
[simp]: ‹conflicting S = None› and
undef: ‹undefined_lit (trail S) L› and
L: ‹atm_of L ∈ atms_of_mm (init_clss S)› and
T: ‹T ∼ cons_trail (Decided L) S›
using dec unfolding decide.simps
by auto
have 1: ‹atm_of L ∉ Σ - ΔΣ›
using nsd L undef by (fastforce simp: odecide.simps N Σ)
have 2: False if L: ‹atm_of L ∈ replacement_pos ` ΔΣ ∪
replacement_neg ` ΔΣ›
proof -
obtain A where
‹A ∈ ΔΣ› and
‹atm_of L = replacement_pos A ∨ atm_of L = replacement_neg A› and
‹A ∈ Σ›
using L ΔΣ_Σ by auto
then show False
using nsd L undef T N_Σ
using odecide.intros(2-)[of S ‹A›]
unfolding N Σ
by (cases L) (auto 6 5 simp: defined_lit_Neg_Pos_iff Σ)
qed
have defined_replacement_pos: ‹defined_lit (trail S) (Pos (replacement_pos L))›
if ‹L ∈ ΔΣ› for L
using nsd that ΔΣ_Σ odecide.intros(2-)[of S ‹L›] by (auto simp: N Σ N_Σ)
have defined_all: ‹defined_lit (trail S) L›
if ‹atm_of L ∈ Σ - ΔΣ› for L
using nsd that ΔΣ_Σ odecide.intros(1)[of S ‹L›] by (force simp: N Σ N_Σ)
have defined_replacement_neg: ‹defined_lit (trail S) (Pos (replacement_neg L))›
if ‹L ∈ ΔΣ› for L
using nsd that ΔΣ_Σ odecide.intros(2-)[of S ‹L›] by (force simp: N Σ N_Σ)
have [simp]: ‹{A ∈ ΔΣ. A ∈ Σ} = ΔΣ›
using ΔΣ_Σ by auto
have atms_tr': ‹Σ - ΔΣ ∪ replacement_pos ` ΔΣ ∪ replacement_neg ` ΔΣ ⊆
atm_of ` (lits_of_l (trail S))›
using N Σ cdcl_bnb_r_stgy_cdcl_bnb_stgy[of S] atms_of_mm_encode_clause_subset[of N]
atms_of_mm_encode_clause_subset2[of N] finite_Σ ΔΣ_Σ
defined_replacement_pos defined_replacement_neg defined_all
unfolding N Σ N_Σ
apply (auto simp: Decided_Propagated_in_iff_in_lits_of_l)
apply (metis image_eqI literal.sel(1) literal.sel(2) uminus_Pos)
apply (metis image_eqI literal.sel(1) literal.sel(2))
apply (metis image_eqI literal.sel(1) literal.sel(2))
done
then have atms_tr: ‹atms_of_mm (encode_clauses N) ⊆ atm_of ` (lits_of_l (trail S))›
using N atms_of_mm_encode_clause_subset[of N]
atms_of_mm_encode_clause_subset2[of N, OF finite_Σ] ΔΣ_Σ
unfolding N Σ N_Σ ‹{A ∈ ΔΣ. A ∈ Σ} = ΔΣ›
by (meson order_trans)
show False
by (metis L N N_Σ atm_lit_of_set_lits_of_l
atms_tr' defined_lit_map subsetCE undef)
qed
then show ?B
using ‹?A›
by (auto simp: cdcl_bnb_r_stgy.simps enc_weight_opt.cdcl_bnb_stgy.simps
ocdcl⇩W_o_r.simps enc_weight_opt.ocdcl⇩W_o.simps)
qed
lemma cdcl_bnb_r_stgy_init_clss:
‹cdcl_bnb_r_stgy S T ⟹ init_clss S = init_clss T›
by (auto simp: cdcl_bnb_r_stgy.simps ocdcl⇩W_o_r.simps enc_weight_opt.cdcl_bnb_bj.simps
elim: conflictE propagateE enc_weight_opt.improveE enc_weight_opt.conflict_optE
odecideE skipE resolveE enc_weight_opt.obacktrackE)
lemma rtranclp_cdcl_bnb_r_stgy_init_clss:
‹cdcl_bnb_r_stgy⇧*⇧* S T ⟹ init_clss S = init_clss T›
by (induction rule: rtranclp_induct)(auto simp: dest: cdcl_bnb_r_stgy_init_clss)
lemma [simp]:
‹enc_weight_opt.abs_state (init_state N) = abs_state (init_state N)›
by (auto simp: enc_weight_opt.abs_state_def abs_state_def)
corollary
assumes
Σ: ‹atms_of_mm N = Σ› and dist: ‹distinct_mset_mset N› and
‹full cdcl_bnb_r_stgy (init_state (penc N)) T›
shows
‹full enc_weight_opt.cdcl_bnb_stgy (init_state (penc N)) T›
proof -
have [simp]: ‹atms_of_mm (CDCL_W_Abstract_State.init_clss (enc_weight_opt.abs_state T)) =
atms_of_mm (init_clss T)›
by (auto simp: enc_weight_opt.abs_state_def init_clss.simps)
let ?S = ‹init_state (penc N)›
have
st: ‹cdcl_bnb_r_stgy⇧*⇧* ?S T› and
ns: ‹no_step cdcl_bnb_r_stgy T›
using assms unfolding full_def by metis+
have st': ‹enc_weight_opt.cdcl_bnb_stgy⇧*⇧* ?S T›
by (rule rtranclp_cdcl_bnb_r_stgy_cdcl_bnb_stgy[OF _ st])
(use atms_of_mm_penc_subset2[of N] finite_Σ ΔΣ_Σ Σ in auto)
have [simp]:
‹CDCL_W_Abstract_State.init_clss (abs_state (init_state (penc N))) =
(penc N)›
by (auto simp: abs_state_def init_clss.simps)
have [iff]: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state ?S)›
using dist distinct_mset_penc[of N]
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def Σ
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def)
have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state T)›
using enc_weight_opt.rtranclp_cdcl_bnb_stgy_all_struct_inv[of ?S T]
enc_weight_opt.rtranclp_cdcl_bnb_stgy_cdcl_bnb[OF st']
by auto
then have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (enc_weight_opt.abs_state T)› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (enc_weight_opt.abs_state T)›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have [simp]: ‹init_clss T = penc N›
using rtranclp_cdcl_bnb_r_stgy_init_clss[OF st] by auto
have ‹no_step enc_weight_opt.cdcl_bnb_stgy T›
by (rule no_step_cdcl_bnb_r_stgy_no_step_cdcl_bnb_stgy[THEN iffD1, of _ N, OF _ _ _ _ ns])
(use alien atms_of_mm_penc_subset2[of N] finite_Σ ΔΣ_Σ lev
in ‹auto simp: cdcl⇩W_restart_mset.no_strange_atm_def Σ
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def›)
then show ‹full enc_weight_opt.cdcl_bnb_stgy (init_state (penc N)) T›
using st' unfolding full_def
by auto
qed
lemma propagation_one_lit_of_same_lvl:
assumes
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
‹no_smaller_propa S› and
‹Propagated L E ∈ set (trail S)› and
rea: ‹reasons_in_clauses S› and
nempty: ‹E - {#L#} ≠ {#}›
shows
‹∃L' ∈# E - {#L#}. get_level (trail S) L = get_level (trail S) L'›
proof (rule ccontr)
assume H: ‹¬?thesis›
have ns: ‹⋀M K M' D L.
trail S = M' @ Decided K # M ⟹
D + {#L#} ∈# clauses S ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D› and
n_d: ‹no_dup (trail S)›
using assms unfolding no_smaller_propa_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
obtain M1 M2 where M2: ‹trail S = M2 @ Propagated L E # M1›
using assms by (auto dest!: split_list)
have ‹⋀L mark a b.
a @ Propagated L mark # b = trail S ⟹
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› and
‹set (get_all_mark_of_propagated (trail S)) ⊆ set_mset (clauses S)›
using assms unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
reasons_in_clauses_def
by auto
from this(1)[OF M2[symmetric]] this(2)
have ‹M1 ⊨as CNot (remove1_mset L E)› and ‹L ∈# E› and ‹E ∈# clauses S›
by (auto simp: M2)
then have lev_le:
‹L' ∈# E - {#L#} ⟹ get_level (trail S) L > get_level (trail S) L'› and
‹trail S ⊨as CNot (remove1_mset L E)› for L'
using H n_d defined_lit_no_dupD(1)[of M1 _ M2]
count_decided_ge_get_level[of M1 L']
by (auto simp: M2 get_level_append_if get_level_cons_if
Decided_Propagated_in_iff_in_lits_of_l atm_of_eq_atm_of
true_annots_append_l
dest!: multi_member_split)
define i where ‹i = get_level (trail S) L - 1›
have ‹i < local.backtrack_lvl S› and ‹get_level (trail S) L ≥ 1›
‹get_level (trail S) L > i› and
i2: ‹get_level (trail S) L = Suc i›
using lev_le nempty count_decided_ge_get_level[of ‹trail S› L] i_def
by (cases ‹E - {#L#}›; force)+
from backtrack_ex_decomp[OF n_d this(1)] obtain M3 M4 K where
decomp: ‹(Decided K # M3, M4) ∈ set (get_all_ann_decomposition (trail S))› and
lev_K: ‹get_level (trail S) K = Suc i›
by blast
then obtain M5 where
tr: ‹trail S = (M5 @ M4) @ Decided K # M3›
by auto
define M4' where ‹M4' = M5 @ M4›
have ‹undefined_lit M3 L›
using n_d ‹get_level (trail S) L > i› lev_K
count_decided_ge_get_level[of M3 L] unfolding tr M4'_def[symmetric]
by (auto simp: get_level_append_if get_level_cons_if
atm_of_eq_atm_of
split: if_splits dest: defined_lit_no_dupD)
moreover have ‹M3 ⊨as CNot (remove1_mset L E)›
using ‹trail S ⊨as CNot (remove1_mset L E)› lev_K n_d
unfolding true_annots_def true_annot_def
apply clarsimp
subgoal for L'
using lev_le[of ‹-L'›] lev_le[of ‹L'›] lev_K
unfolding i2
unfolding tr M4'_def[symmetric]
by (auto simp: get_level_append_if get_level_cons_if
atm_of_eq_atm_of if_distrib if_distribR Decided_Propagated_in_iff_in_lits_of_l
split: if_splits dest: defined_lit_no_dupD
dest!: multi_member_split)
done
ultimately show False
using ns[OF tr, of ‹remove1_mset L E› L] ‹E ∈# clauses S› ‹L ∈# E›
by auto
qed
lemma simple_backtrack_obacktrack:
‹simple_backtrack S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (enc_weight_opt.abs_state S) ⟹
enc_weight_opt.obacktrack S T›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
apply (auto simp: simple_backtrack.simps
enc_weight_opt.obacktrack.simps)
apply (rule_tac x=L in exI)
apply (rule_tac x=D in exI)
apply auto
apply (rule_tac x=K in exI)
apply (rule_tac x=M1 in exI)
apply auto
apply (rule_tac x=D in exI)
apply (auto simp:)
done
end
interpretation test_real: optimal_encoding_opt where
state_eq = ‹(=)› and
state = id and
trail = ‹λ(M, N, U, D, W). M› and
init_clss = ‹λ(M, N, U, D, W). N› and
learned_clss = ‹λ(M, N, U, D, W). U› and
conflicting = ‹λ(M, N, U, D, W). D› and
cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
init_state = ‹λN. ([], N, {#}, None, None, ())› and
ρ = ‹λ_. (0::real)› and
update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)› and
Σ = ‹{1..(100::nat)}› and
ΔΣ = ‹{1..(50::nat)}› and
new_vars = ‹λn. (200 + 2*n, 200 + 2*n+1)›
by unfold_locales
lemma mult3_inj:
‹2 * A = Suc (2 * Aa) ⟷ False› for A Aa::nat
by presburger+
interpretation test_real: optimal_encoding where
state_eq = ‹(=)› and
state = id and
trail = ‹λ(M, N, U, D, W). M› and
init_clss = ‹λ(M, N, U, D, W). N› and
learned_clss = ‹λ(M, N, U, D, W). U› and
conflicting = ‹λ(M, N, U, D, W). D› and
cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
init_state = ‹λN. ([], N, {#}, None, None, ())› and
ρ = ‹λ_. (0::real)› and
update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)› and
Σ = ‹{1..(100::nat)}› and
ΔΣ = ‹{1..(50::nat)}› and
new_vars = ‹λn. (200 + 2*n, 200 + 2*n+1)›
by unfold_locales (auto simp: inj_on_def mult3_inj)
interpretation test_nat: optimal_encoding_opt where
state_eq = ‹(=)› and
state = id and
trail = ‹λ(M, N, U, D, W). M› and
init_clss = ‹λ(M, N, U, D, W). N› and
learned_clss = ‹λ(M, N, U, D, W). U› and
conflicting = ‹λ(M, N, U, D, W). D› and
cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
init_state = ‹λN. ([], N, {#}, None, None, ())› and
ρ = ‹λ_. (0::nat)› and
update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)› and
Σ = ‹{1..(100::nat)}› and
ΔΣ = ‹{1..(50::nat)}› and
new_vars = ‹λn. (200 + 2*n, 200 + 2*n+1)›
by unfold_locales
interpretation test_nat: optimal_encoding where
state_eq = ‹(=)› and
state = id and
trail = ‹λ(M, N, U, D, W). M› and
init_clss = ‹λ(M, N, U, D, W). N› and
learned_clss = ‹λ(M, N, U, D, W). U› and
conflicting = ‹λ(M, N, U, D, W). D› and
cons_trail = ‹λK (M, N, U, D, W). (K # M, N, U, D, W)› and
tl_trail = ‹λ(M, N, U, D, W). (tl M, N, U, D, W)› and
add_learned_cls = ‹λC (M, N, U, D, W). (M, N, add_mset C U, D, W)› and
remove_cls = ‹λC (M, N, U, D, W). (M, removeAll_mset C N, removeAll_mset C U, D, W)› and
update_conflicting = ‹λC (M, N, U, _, W). (M, N, U, C, W)› and
init_state = ‹λN. ([], N, {#}, None, None, ())› and
ρ = ‹λ_. (0::nat)› and
update_additional_info = ‹λW (M, N, U, D, _, _). (M, N, U, D, W)› and
Σ = ‹{1..(100::nat)}› and
ΔΣ = ‹{1..(50::nat)}› and
new_vars = ‹λn. (200 + 2*n, 200 + 2*n+1)›
by unfold_locales (auto simp: inj_on_def mult3_inj)
end