theory CDCL_NOT
imports Partial_Annotated_Clausal_Logic List_More Wellfounded_More Partial_Clausal_Logic
begin
section ‹NOT's CDCL›
declare set_mset_minus_replicate_mset[simp]
subsection ‹Auxiliary Lemmas and Measure›
lemma no_dup_cannot_not_lit_and_uminus:
"no_dup M ⟹ - lit_of xa = lit_of x ⟹ x ∈ set M ⟹ xa ∉ set M"
by (metis atm_of_uminus distinct_map inj_on_eq_iff uminus_not_id')
lemma true_clss_single_iff_incl:
"I ⊨s single ` B ⟷ B ⊆ I"
unfolding true_clss_def by auto
lemma atms_of_ms_single_atm_of[simp]:
"atms_of_ms {{#lit_of L#} |L. P L} = atm_of ` {lit_of L |L. P L}"
unfolding atms_of_ms_def by auto
lemma atms_of_uminus_lit_atm_of_lit_of:
"atms_of {#- lit_of x. x ∈# A#} = atm_of ` (lit_of ` (set_mset A))"
unfolding atms_of_def by (auto simp add: Fun.image_comp)
lemma atms_of_ms_single_image_atm_of_lit_of:
"atms_of_ms ((λx. {#lit_of x#}) ` A) = atm_of ` (lit_of ` A)"
unfolding atms_of_ms_def by auto
text ‹This measure can also be seen as the increasing lexicographic order: it is an order on bounded
sequences, when each element is bounded. The proof involves a measure like the one defined here
(the same?).›
definition μ⇩C :: "nat ⇒ nat ⇒ nat list ⇒ nat" where
"μ⇩C s b M ≡ (∑i=0..<length M. M!i * b^ (s +i - length M))"
lemma μ⇩C_nil[simp]:
"μ⇩C s b [] = 0"
unfolding μ⇩C_def by auto
lemma μ⇩C_single[simp]:
"μ⇩C s b [L] = L * b ^ (s - Suc 0)"
unfolding μ⇩C_def by auto
lemma set_sum_atLeastLessThan_add:
"(∑i=k..<k+(b::nat). f i) = (∑i=0..<b. f (k+ i))"
by (induction b) auto
lemma set_sum_atLeastLessThan_Suc:
"(∑i=1..<Suc j. f i) = (∑i=0..<j. f (Suc i))"
using set_sum_atLeastLessThan_add[of _ 1 j] by force
lemma μ⇩C_cons:
"μ⇩C s b (L # M) = L * b ^ (s - 1 - length M) + μ⇩C s b M"
proof -
have "μ⇩C s b (L # M) = (∑i=0..<length (L#M). (L#M)!i * b^ (s +i - length (L#M)))"
unfolding μ⇩C_def by blast
also have "… = (∑i=0..<1. (L#M)!i * b^ (s +i - length (L#M)))
+ (∑i=1..<length (L#M). (L#M)!i * b^ (s +i - length (L#M)))"
by (rule setsum_add_nat_ivl[symmetric]) simp_all
finally have "μ⇩C s b (L # M)= L * b ^ (s - 1 - length M)
+ (∑i=1..<length (L#M). (L#M)!i * b^ (s +i - length (L#M)))"
by auto
moreover {
have "(∑i=1..<length (L#M). (L#M)!i * b^ (s +i - length (L#M))) =
(∑i=0..<length (M). (L#M)!(Suc i) * b^ (s + (Suc i) - length (L#M)))"
unfolding length_Cons set_sum_atLeastLessThan_Suc by blast
also have "… = (∑i=0..<length (M). M!i * b^ (s + i - length M))"
by auto
finally have "(∑i=1..<length (L#M). (L#M)!i * b^ (s +i - length (L#M))) = μ⇩C s b M"
unfolding μ⇩C_def .
}
ultimately show ?thesis by presburger
qed
lemma μ⇩C_append:
assumes "s ≥ length (M@M')"
shows "μ⇩C s b (M@M') = μ⇩C (s - length M') b M + μ⇩C s b M'"
proof -
have "μ⇩C s b (M@M') = (∑i=0..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M')))"
unfolding μ⇩C_def by blast
moreover then have "… = (∑i=0..< length M. (M@M')!i * b^ (s +i - length (M@M')))
+ (∑i=length M..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M')))"
by (auto intro!: setsum_add_nat_ivl[symmetric])
moreover
have "∀i∈{0..< length M}. (M@M')!i * b^ (s +i - length (M@M')) = M ! i * b ^ (s - length M'
+ i - length M)"
using ‹s ≥ length (M@M')› by (auto simp add: nth_append ac_simps)
then have "μ⇩C (s - length M') b M = (∑i=0..< length M. (M@M')!i * b^ (s +i - length (M@M')))"
unfolding μ⇩C_def by auto
ultimately have "μ⇩C s b (M@M')= μ⇩C (s - length M') b M
+ (∑i=length M..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M')))"
by auto
moreover {
have "(∑i=length M..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M'))) =
(∑i=0..<length M'. M'!i * b^ (s + i - length M'))"
unfolding length_append set_sum_atLeastLessThan_add by auto
then have "(∑i=length M..<length (M@M'). (M@M')!i * b^ (s +i - length (M@M'))) = μ⇩C s b M'"
unfolding μ⇩C_def .
}
ultimately show ?thesis by presburger
qed
lemma μ⇩C_cons_non_empty_inf:
assumes M_ge_1: "∀i∈set M. i ≥ 1" and M: "M ≠ []"
shows "μ⇩C s b M ≥ b ^ (s - length M)"
using assms by (cases M) (auto simp: mult_eq_if μ⇩C_cons)
text ‹Duplicate of "~~/src/HOL/ex/NatSum.thy" (but generalized to @{term "k≥0"})›
lemma sum_of_powers: "0 ≤ k ⟹ (k - 1) * (∑i=0..<n. k^i) = k^n - (1::nat)"
apply (cases "k = 0")
apply (cases n; simp)
by (induct n) (auto simp: Nat.nat_distrib)
text ‹In the degenerated cases, we only have the large inequality holds. In the other cases, the
following strict inequality holds:›
lemma μ⇩C_bounded_non_degenerated:
fixes b ::nat
assumes
"b > 0" and
"M ≠ []" and
M_le: "∀i < length M. M!i < b" and
"s ≥ length M"
shows "μ⇩C s b M < b^s"
proof -
consider (b1) "b= 1" | (b) "b>1" using ‹b>0› by (cases b) auto
then show ?thesis
proof cases
case b1
then have "∀i < length M. M!i = 0" using M_le by auto
then have "μ⇩C s b M = 0" unfolding μ⇩C_def by auto
then show ?thesis using ‹b > 0› by auto
next
case b
have "∀ i ∈ {0..<length M}. M!i * b^ (s +i - length M) ≤ (b-1) * b^ (s +i - length M)"
using M_le ‹b > 1› by auto
then have "μ⇩C s b M ≤ (∑i=0..<length M. (b-1) * b^ (s +i - length M))"
using ‹M≠[]› ‹b>0› unfolding μ⇩C_def by (auto intro: setsum_mono)
also
have "∀ i ∈ {0..<length M}. (b-1) * b^ (s +i - length M) = (b-1) * b^ i * b^(s - length M)"
by (metis Nat.add_diff_assoc2 add.commute assms(4) mult.assoc power_add)
then have "(∑i=0..<length M. (b-1) * b^ (s +i - length M))
= (∑i=0..<length M. (b-1)* b^ i * b^(s - length M))"
by (auto simp add: ac_simps)
also have "… = (∑i=0..<length M. b^ i) * b^(s - length M) * (b-1)"
by (simp add: setsum_left_distrib setsum_right_distrib ac_simps)
finally have "μ⇩C s b M ≤ (∑i=0..<length M. b^ i) * (b-1) * b^(s - length M)"
by (simp add: ac_simps)
also
have "(∑i=0..<length M. b^ i)* (b-1) = b ^ (length M) - 1"
using sum_of_powers[of b "length M"] ‹b>1›
by (auto simp add: ac_simps)
finally have "μ⇩C s b M ≤ (b ^ (length M) - 1) * b ^ (s - length M)"
by auto
also have "… < b ^ (length M) * b ^ (s - length M)"
using ‹b>1› by auto
also have "… = b ^ s"
by (metis assms(4) le_add_diff_inverse power_add)
finally show ?thesis unfolding μ⇩C_def by (auto simp add: ac_simps)
qed
qed
text ‹In the degenerate case @{term "b=0"}, the list @{term M} is empty (since the list cannot
contain any element).›
lemma μ⇩C_bounded:
fixes b ::nat
assumes
M_le: "∀i < length M. M!i < b" and
"s ≥ length M"
"b > 0"
shows "μ⇩C s b M < b ^ s"
proof -
consider (M0) "M = []" | (M) "b > 0" and "M ≠ []"
using M_le by (cases b, cases M) auto
then show ?thesis
proof cases
case M0
then show ?thesis using M_le ‹b > 0› by auto
next
case M
show ?thesis using μ⇩C_bounded_non_degenerated[OF M assms(1,2)] by arith
qed
qed
text ‹When @{term "b=(0::nat)"}, we cannot show that the measure is empty, since @{term "0^0 =
(1::nat)"}.›
lemma μ⇩C_base_0:
assumes "length M ≤ s"
shows "μ⇩C s 0 M ≤ M!0"
proof -
{
assume "s = length M"
moreover {
fix n
have "(∑i=0..<n. M ! i * (0::nat) ^ i) ≤ M ! 0"
apply (induction n rule: nat_induct)
by simp (rename_tac n, case_tac n, auto)
}
ultimately have ?thesis unfolding μ⇩C_def by auto
}
moreover
{
assume "length M < s"
then have "μ⇩C s 0 M = 0" unfolding μ⇩C_def by auto}
ultimately show ?thesis using assms unfolding μ⇩C_def by linarith
qed
subsection ‹Initial definitions›
subsubsection ‹The state›
text ‹We define here an abstraction over operation on the state we are manipulating.›
locale dpll_state =
fixes
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒'st" and
add_cls⇩N⇩O⇩T :: "'v clause ⇒ 'st ⇒ 'st" and
remove_cls⇩N⇩O⇩T :: "'v clause ⇒ 'st ⇒ 'st"
assumes
trail_prepend_trail[simp]:
"⋀st L. undefined_lit (trail st) (lit_of L) ⟹ trail (prepend_trail L st) = L # trail st"
and
tl_trail[simp]: "trail (tl_trail S) = tl (trail S)" and
trail_add_cls⇩N⇩O⇩T[simp]: "⋀st C. no_dup (trail st) ⟹ trail (add_cls⇩N⇩O⇩T C st) = trail st" and
trail_remove_cls⇩N⇩O⇩T[simp]: "⋀st C. trail (remove_cls⇩N⇩O⇩T C st) = trail st" and
clauses_prepend_trail[simp]:
"⋀st L. undefined_lit (trail st) (lit_of L) ⟹ clauses (prepend_trail L st) = clauses st"
and
clauses_tl_trail[simp]: "⋀st. clauses (tl_trail st) = clauses st" and
clauses_add_cls⇩N⇩O⇩T[simp]:
"⋀st C. no_dup (trail st) ⟹ clauses (add_cls⇩N⇩O⇩T C st) = {#C#} + clauses st" and
clauses_remove_cls⇩N⇩O⇩T[simp]: "⋀st C. clauses (remove_cls⇩N⇩O⇩T C st) = remove_mset C (clauses st)"
begin
function reduce_trail_to⇩N⇩O⇩T :: "'a list ⇒ 'st ⇒ 'st" where
"reduce_trail_to⇩N⇩O⇩T F S =
(if length (trail S) = length F ∨ trail S = [] then S else reduce_trail_to⇩N⇩O⇩T F (tl_trail S))"
by fast+
termination by (relation "measure (λ(_, S). length (trail S))") auto
declare reduce_trail_to⇩N⇩O⇩T.simps[simp del]
lemma
shows
reduce_trail_to⇩N⇩O⇩T_nil[simp]: "trail S = [] ⟹ reduce_trail_to⇩N⇩O⇩T F S = S" and
reduce_trail_to⇩N⇩O⇩T_eq_length[simp]: "length (trail S) = length F ⟹ reduce_trail_to⇩N⇩O⇩T F S = S"
by (auto simp: reduce_trail_to⇩N⇩O⇩T.simps)
lemma reduce_trail_to⇩N⇩O⇩T_length_ne[simp]:
"length (trail S) ≠ length F ⟹ trail S ≠ [] ⟹
reduce_trail_to⇩N⇩O⇩T F S = reduce_trail_to⇩N⇩O⇩T F (tl_trail S)"
by (auto simp: reduce_trail_to⇩N⇩O⇩T.simps)
lemma trail_reduce_trail_to⇩N⇩O⇩T_length_le:
assumes "length F > length (trail S)"
shows "trail (reduce_trail_to⇩N⇩O⇩T F S) = []"
using assms by (induction F S rule: reduce_trail_to⇩N⇩O⇩T.induct)
(simp add: less_imp_diff_less reduce_trail_to⇩N⇩O⇩T.simps)
lemma trail_reduce_trail_to⇩N⇩O⇩T_nil[simp]:
"trail (reduce_trail_to⇩N⇩O⇩T [] S) = []"
by (induction "[]" S rule: reduce_trail_to⇩N⇩O⇩T.induct)
(simp add: less_imp_diff_less reduce_trail_to⇩N⇩O⇩T.simps)
lemma clauses_reduce_trail_to⇩N⇩O⇩T_nil:
"clauses (reduce_trail_to⇩N⇩O⇩T [] S) = clauses S"
by (induction "[]" S rule: reduce_trail_to⇩N⇩O⇩T.induct)
(simp add: less_imp_diff_less reduce_trail_to⇩N⇩O⇩T.simps)
lemma trail_reduce_trail_to⇩N⇩O⇩T_drop:
"trail (reduce_trail_to⇩N⇩O⇩T F S) =
(if length (trail S) ≥ length F
then drop (length (trail S) - length F) (trail S)
else [])"
apply (induction F S rule: reduce_trail_to⇩N⇩O⇩T.induct)
apply (rename_tac F S, case_tac "trail S")
apply auto[]
apply (rename_tac list, case_tac "Suc (length list) > length F")
prefer 2 apply simp
apply (subgoal_tac "Suc (length list) - length F = Suc (length list - length F)")
apply simp
apply simp
done
lemma reduce_trail_to⇩N⇩O⇩T_skip_beginning:
assumes "trail S = F' @ F"
shows "trail (reduce_trail_to⇩N⇩O⇩T F S) = F"
using assms by (auto simp: trail_reduce_trail_to⇩N⇩O⇩T_drop)
lemma reduce_trail_to⇩N⇩O⇩T_clauses[simp]:
"clauses (reduce_trail_to⇩N⇩O⇩T F S) = clauses S"
by (induction F S rule: reduce_trail_to⇩N⇩O⇩T.induct)
(simp add: less_imp_diff_less reduce_trail_to⇩N⇩O⇩T.simps)
abbreviation trail_weight where
"trail_weight S ≡ map ((λl. 1 + length l) o snd) (get_all_decided_decomposition (trail S))"
definition state_eq⇩N⇩O⇩T :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) where
"S ∼ T ⟷ trail S = trail T ∧ clauses S = clauses T"
lemma state_eq⇩N⇩O⇩T_ref[simp]:
"S ∼ S"
unfolding state_eq⇩N⇩O⇩T_def by auto
lemma state_eq⇩N⇩O⇩T_sym:
"S ∼ T ⟷ T ∼ S"
unfolding state_eq⇩N⇩O⇩T_def by auto
lemma state_eq⇩N⇩O⇩T_trans:
"S ∼ T ⟹ T ∼ U ⟹ S ∼ U"
unfolding state_eq⇩N⇩O⇩T_def by auto
lemma
shows
state_eq⇩N⇩O⇩T_trail: "S ∼ T ⟹ trail S = trail T" and
state_eq⇩N⇩O⇩T_clauses: "S ∼ T ⟹ clauses S = clauses T"
unfolding state_eq⇩N⇩O⇩T_def by auto
lemmas state_simp⇩N⇩O⇩T[simp]= state_eq⇩N⇩O⇩T_trail state_eq⇩N⇩O⇩T_clauses
lemma trail_eq_reduce_trail_to⇩N⇩O⇩T_eq:
"trail S = trail T ⟹ trail (reduce_trail_to⇩N⇩O⇩T F S) = trail (reduce_trail_to⇩N⇩O⇩T F T)"
apply (induction F S arbitrary: T rule: reduce_trail_to⇩N⇩O⇩T.induct)
by (metis tl_trail reduce_trail_to⇩N⇩O⇩T_eq_length reduce_trail_to⇩N⇩O⇩T_length_ne reduce_trail_to⇩N⇩O⇩T_nil)
lemma reduce_trail_to⇩N⇩O⇩T_state_eq⇩N⇩O⇩T_compatible:
assumes ST: "S ∼ T"
shows "reduce_trail_to⇩N⇩O⇩T F S ∼ reduce_trail_to⇩N⇩O⇩T F T"
proof -
have "clauses (reduce_trail_to⇩N⇩O⇩T F S) = clauses (reduce_trail_to⇩N⇩O⇩T F T)"
using ST by auto
moreover have "trail (reduce_trail_to⇩N⇩O⇩T F S) = trail (reduce_trail_to⇩N⇩O⇩T F T)"
using trail_eq_reduce_trail_to⇩N⇩O⇩T_eq[of S T F] ST by auto
ultimately show ?thesis by (auto simp del: state_simp⇩N⇩O⇩T simp: state_eq⇩N⇩O⇩T_def)
qed
lemma trail_reduce_trail_to⇩N⇩O⇩T_add_cls⇩N⇩O⇩T[simp]:
"no_dup (trail S) ⟹
trail (reduce_trail_to⇩N⇩O⇩T F (add_cls⇩N⇩O⇩T C S)) = trail (reduce_trail_to⇩N⇩O⇩T F S)"
by (rule trail_eq_reduce_trail_to⇩N⇩O⇩T_eq) simp
lemma reduce_trail_to⇩N⇩O⇩T_trail_tl_trail_decomp[simp]:
"trail S = F' @ Decided K () # F ⟹
trail (reduce_trail_to⇩N⇩O⇩T F (tl_trail S)) = F"
apply (rule reduce_trail_to⇩N⇩O⇩T_skip_beginning[of _ "tl (F' @ Decided K () # [])"])
by (cases F') (auto simp add:tl_append reduce_trail_to⇩N⇩O⇩T_skip_beginning)
end
subsubsection ‹Definition of the operation›
locale propagate_ops =
dpll_state trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_cond :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool"
begin
inductive propagate⇩N⇩O⇩T :: "'st ⇒ 'st ⇒ bool" where
propagate⇩N⇩O⇩T[intro]: "C + {#L#} ∈# clauses S ⟹ trail S ⊨as CNot C
⟹ undefined_lit (trail S) L
⟹ propagate_cond (Propagated L ()) S
⟹ T ∼ prepend_trail (Propagated L ()) S
⟹ propagate⇩N⇩O⇩T S T"
inductive_cases propagate⇩N⇩O⇩TE[elim]: "propagate⇩N⇩O⇩T S T"
end
locale decide_ops =
dpll_state trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st"
begin
inductive decide⇩N⇩O⇩T :: "'st ⇒ 'st ⇒ bool" where
decide⇩N⇩O⇩T[intro]: "undefined_lit (trail S) L ⟹ atm_of L ∈ atms_of_msu (clauses S)
⟹ T ∼ prepend_trail (Decided L ()) S
⟹ decide⇩N⇩O⇩T S T"
inductive_cases decide⇩N⇩O⇩TE[elim]: "decide⇩N⇩O⇩T S S'"
end
locale backjumping_ops =
dpll_state trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" +
fixes
backjump_conds :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool"
begin
inductive backjump where
"trail S = F' @ Decided K ()# F
⟹ T ∼ prepend_trail (Propagated L ()) (reduce_trail_to⇩N⇩O⇩T F S)
⟹ C ∈# clauses S
⟹ trail S ⊨as CNot C
⟹ undefined_lit F L
⟹ atm_of L ∈ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S))
⟹ clauses S ⊨pm C' + {#L#}
⟹ F ⊨as CNot C'
⟹ backjump_conds C C' L S T
⟹ backjump S T"
inductive_cases backjumpE: "backjump S T"
end
subsection ‹DPLL with backjumping›
locale dpll_with_backjumping_ops =
dpll_state trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T +
propagate_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T propagate_conds +
decide_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T +
backjumping_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T backjump_conds
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
inv :: "'st ⇒ bool" and
backjump_conds :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool" +
assumes
bj_can_jump:
"⋀S C F' K F L.
inv S ⟹
no_dup (trail S) ⟹
trail S = F' @ Decided K () # F ⟹
C ∈# clauses S ⟹
trail S ⊨as CNot C ⟹
undefined_lit F L ⟹
atm_of L ∈ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (F' @ Decided K () # F)) ⟹
clauses S ⊨pm C' + {#L#} ⟹
F ⊨as CNot C' ⟹
¬no_step backjump S"
begin
text ‹We cannot add a like condition @{term "atms_of C' ⊆ atms_of_ms N"} because to ensure that we
can backjump even if the last decision variable has disappeared.
The part of the condition @{term "atm_of L ∈ atm_of ` (lits_of (F' @ Decided K () # F))"} is
important, otherwise you are not sure that you can backtrack.›
subsubsection‹Definition›
text ‹We define dpll with backjumping:›
inductive dpll_bj :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
bj_decide⇩N⇩O⇩T: "decide⇩N⇩O⇩T S S' ⟹ dpll_bj S S'" |
bj_propagate⇩N⇩O⇩T: "propagate⇩N⇩O⇩T S S' ⟹ dpll_bj S S'" |
bj_backjump: "backjump S S' ⟹ dpll_bj S S'"
lemmas dpll_bj_induct = dpll_bj.induct[split_format(complete)]
thm dpll_bj_induct[OF dpll_with_backjumping_ops_axioms]
lemma dpll_bj_all_induct[consumes 2, case_names decide⇩N⇩O⇩T propagate⇩N⇩O⇩T backjump]:
fixes S T :: "'st"
assumes
"dpll_bj S T" and
"inv S"
"⋀L T. undefined_lit (trail S) L ⟹ atm_of L ∈ atms_of_msu (clauses S)
⟹ T ∼ prepend_trail (Decided L ()) S
⟹ P S T" and
"⋀C L T. C + {#L#} ∈# clauses S ⟹ trail S ⊨as CNot C ⟹ undefined_lit (trail S) L
⟹ T ∼ prepend_trail (Propagated L ()) S
⟹ P S T" and
"⋀C F' K F L C' T. C ∈# clauses S ⟹ F' @ Decided K () # F ⊨as CNot C
⟹ trail S = F' @ Decided K () # F
⟹ undefined_lit F L
⟹ atm_of L ∈ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (F' @ Decided K () # F))
⟹ clauses S ⊨pm C' + {#L#}
⟹ F ⊨as CNot C'
⟹ T ∼ prepend_trail (Propagated L ()) (reduce_trail_to⇩N⇩O⇩T F S)
⟹ P S T"
shows "P S T"
apply (induct T rule: dpll_bj_induct[OF local.dpll_with_backjumping_ops_axioms])
apply (rule assms(1))
using assms(3) apply blast
apply (elim propagate⇩N⇩O⇩TE) using assms(4) apply blast
apply (elim backjumpE) using assms(5) ‹inv S› by simp
subsubsection ‹Basic properties›
paragraph ‹First, some better suited induction principle›
lemma dpll_bj_clauses:
assumes "dpll_bj S T" and "inv S"
shows "clauses S = clauses T"
using assms by (induction rule: dpll_bj_all_induct) auto
paragraph ‹No duplicates in the trail›
lemma dpll_bj_no_dup:
assumes "dpll_bj S T" and "inv S"
and "no_dup (trail S)"
shows "no_dup (trail T)"
using assms by (induction rule: dpll_bj_all_induct)
(auto simp add: defined_lit_map reduce_trail_to⇩N⇩O⇩T_skip_beginning)
paragraph ‹Valuations›
lemma dpll_bj_sat_iff:
assumes "dpll_bj S T" and "inv S"
shows "I ⊨sm clauses S ⟷ I ⊨sm clauses T"
using assms by (induction rule: dpll_bj_all_induct) auto
paragraph ‹Clauses›
lemma dpll_bj_atms_of_ms_clauses_inv:
assumes
"dpll_bj S T" and
"inv S"
shows "atms_of_msu (clauses S) = atms_of_msu (clauses T)"
using assms by (induction rule: dpll_bj_all_induct) auto
lemma dpll_bj_atms_in_trail:
assumes
"dpll_bj S T" and
"inv S" and
"atm_of ` (lits_of (trail S)) ⊆ atms_of_msu (clauses S)"
shows "atm_of ` (lits_of (trail T)) ⊆ atms_of_msu (clauses S)"
using assms by (induction rule: dpll_bj_all_induct)
(auto simp: in_plus_implies_atm_of_on_atms_of_ms reduce_trail_to⇩N⇩O⇩T_skip_beginning)
lemma dpll_bj_atms_in_trail_in_set:
assumes "dpll_bj S T"and
"inv S" and
"atms_of_msu (clauses S) ⊆ A" and
"atm_of ` (lits_of (trail S)) ⊆ A"
shows "atm_of ` (lits_of (trail T)) ⊆ A"
using assms by (induction rule: dpll_bj_all_induct)
(auto simp: in_plus_implies_atm_of_on_atms_of_ms)
lemma dpll_bj_all_decomposition_implies_inv:
assumes
"dpll_bj S T" and
inv: "inv S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows "all_decomposition_implies_m (clauses T) (get_all_decided_decomposition (trail T))"
using assms(1,2)
proof (induction rule:dpll_bj_all_induct)
case decide⇩N⇩O⇩T
then show ?case using decomp by auto
next
case (propagate⇩N⇩O⇩T C L T) note propa = this(1) and undef = this(3) and T = this(4)
let ?M' = "trail (prepend_trail (Propagated L ()) S)"
let ?N = "clauses S"
obtain a y l where ay: "get_all_decided_decomposition ?M' = (a, y) # l"
by (cases "get_all_decided_decomposition ?M'") fastforce+
then have M': "?M' = y @ a" using get_all_decided_decomposition_decomp[of ?M'] by auto
have M: "get_all_decided_decomposition (trail S) = (a, tl y) # l"
using ay undef by (cases " get_all_decided_decomposition (trail S)") auto
have y⇩0: "y = (Propagated L ()) # (tl y)"
using ay undef by (auto simp add: M)
from arg_cong[OF this, of set] have y[simp]: "set y = insert (Propagated L ()) (set (tl y))"
by simp
have tr_S: "trail S = tl y @ a"
using arg_cong[OF M', of tl] y⇩0 M get_all_decided_decomposition_decomp by force
have a_Un_N_M: "unmark a ∪ set_mset ?N ⊨ps unmark (tl y)"
using decomp ay unfolding all_decomposition_implies_def by (simp add: M)+
moreover have "unmark a ∪ set_mset ?N ⊨p {#L#}" (is "?I ⊨p _")
proof (rule true_clss_cls_plus_CNot)
show "?I ⊨p C + {#L#}"
using propa propagate⇩N⇩O⇩T.prems by (auto dest!: true_clss_clss_in_imp_true_clss_cls)
next
have "(λm. {#lit_of m#}) ` set ?M' ⊨ps CNot C"
using ‹trail S ⊨as CNot C› undef by (auto simp add: true_annots_true_clss_clss)
have a1: "(λm. {#lit_of m#}) ` set a ∪ (λm. {#lit_of m#}) ` set (tl y) ⊨ps CNot C"
using propagate⇩N⇩O⇩T.hyps(2) tr_S true_annots_true_clss_clss
by (force simp add: image_Un sup_commute)
have a2: "set_mset (clauses S)∪ unmark a
⊨ps unmark (tl y)"
using calculation by (auto simp add: sup_commute)
show "(λm. {#lit_of m#}) ` set a ∪ set_mset (clauses S)⊨ps CNot C"
proof -
have "set_mset (clauses S) ∪ (λm. {#lit_of m#}) ` set a ⊨ps
(λm. {#lit_of m#}) ` set a ∪ (λm. {#lit_of m#}) ` set (tl y)"
using a2 true_clss_clss_def by blast
then show "(λm. {#lit_of m#}) ` set a ∪ set_mset (clauses S)⊨ps CNot C"
using a1 unfolding sup_commute by (meson true_clss_clss_left_right
true_clss_clss_union_and true_clss_clss_union_l_r )
qed
qed
ultimately have "unmark a ∪ set_mset ?N ⊨ps unmark ?M'"
unfolding M' by (auto simp add: all_in_true_clss_clss image_Un)
then show ?case
using decomp T M undef unfolding ay all_decomposition_implies_def by (auto simp add: ay)
next
case (backjump C F' K F L D T) note confl = this(2) and tr = this(3) and undef = this(4)
and L = this(5) and N_C = this(6) and vars_D = this(5) and T = this(8)
have decomp: "all_decomposition_implies_m (clauses S) (get_all_decided_decomposition F)"
using decomp unfolding tr all_decomposition_implies_def
by (metis (no_types, lifting) get_all_decided_decomposition.simps(1)
get_all_decided_decomposition_never_empty hd_Cons_tl insert_iff list.sel(3) list.set(2)
tl_get_all_decided_decomposition_skip_some)
moreover have "unmark (fst (hd (get_all_decided_decomposition F)))
∪ set_mset (clauses S)
⊨ps unmark (snd (hd (get_all_decided_decomposition F)))"
by (metis all_decomposition_implies_cons_single decomp get_all_decided_decomposition_never_empty
hd_Cons_tl)
moreover
have vars_of_D: "atms_of D ⊆ atm_of ` lits_of F"
using ‹F ⊨as CNot D› unfolding atms_of_def
by (meson image_subsetI mem_set_mset_iff true_annots_CNot_all_atms_defined)
obtain a b li where F: "get_all_decided_decomposition F = (a, b) # li"
by (cases "get_all_decided_decomposition F") auto
have "F = b @ a"
using get_all_decided_decomposition_decomp[of F a b] F by auto
have a_N_b:"unmark a ∪ set_mset (clauses S) ⊨ps unmark b"
using decomp unfolding all_decomposition_implies_def by (auto simp add: F)
have F_D:"unmark F ⊨ps CNot D"
using ‹F ⊨as CNot D› by (simp add: true_annots_true_clss_clss)
then have "unmark a ∪ unmark b ⊨ps CNot D"
unfolding ‹F = b @ a› by (simp add: image_Un sup.commute)
have a_N_CNot_D: "unmark a ∪ set_mset (clauses S)
⊨ps CNot D ∪ unmark b"
apply (rule true_clss_clss_left_right)
using a_N_b F_D unfolding ‹F = b @ a› by (auto simp add: image_Un ac_simps)
have a_N_D_L: "unmark a ∪ set_mset (clauses S) ⊨p D+{#L#}"
by (simp add: N_C)
have "unmark a ∪ set_mset (clauses S) ⊨p {#L#}"
using a_N_D_L a_N_CNot_D by (blast intro: true_clss_cls_plus_CNot)
then show ?case
using decomp T tr undef unfolding all_decomposition_implies_def by (auto simp add: F)
qed
subsubsection ‹Termination›
paragraph ‹Using a proper measure›
lemma length_get_all_decided_decomposition_append_Decided:
"length (get_all_decided_decomposition (F' @ Decided K () # F)) =
length (get_all_decided_decomposition F')
+ length (get_all_decided_decomposition (Decided K () # F))
- 1"
by (induction F' rule: ann_literal_list_induct) auto
lemma take_length_get_all_decided_decomposition_decided_sandwich:
"take (length (get_all_decided_decomposition F))
(map (f o snd) (rev (get_all_decided_decomposition (F' @ Decided K () # F))))
=
map (f o snd) (rev (get_all_decided_decomposition F))
"
proof (induction F' rule: ann_literal_list_induct)
case nil
then show ?case by auto
next
case (decided K)
then show ?case by (simp add: length_get_all_decided_decomposition_append_Decided)
next
case (proped L m F') note IH = this(1)
obtain a b l where F': "get_all_decided_decomposition (F' @ Decided K () # F) = (a, b) # l"
by (cases "get_all_decided_decomposition (F' @ Decided K () # F)") auto
have "length (get_all_decided_decomposition F) - length l = 0"
using length_get_all_decided_decomposition_append_Decided[of F' K F]
unfolding F' by (cases "get_all_decided_decomposition F'") auto
then show ?case
using IH by (simp add: F')
qed
lemma length_get_all_decided_decomposition_length:
"length (get_all_decided_decomposition M) ≤ 1 + length M"
by (induction M rule: ann_literal_list_induct) auto
lemma length_in_get_all_decided_decomposition_bounded:
assumes i:"i ∈ set (trail_weight S)"
shows "i ≤ Suc (length (trail S))"
proof -
obtain a b where
"(a, b) ∈ set (get_all_decided_decomposition (trail S))" and
ib: "i = Suc (length b)"
using i by auto
then obtain c where "trail S = c @ b @ a"
using get_all_decided_decomposition_exists_prepend' by metis
from arg_cong[OF this, of length] show ?thesis using i ib by auto
qed
paragraph ‹Well-foundedness›
text ‹The bounds are the following:
▪ @{term "1+card (atms_of_ms A)"}: @{term "card (atms_of_ms A)"} is an upper bound on the length of
the list. As @{term get_all_decided_decomposition} appends an possibly empty couple at the end,
adding one is needed.
▪ @{term "2+card (atms_of_ms A)"}: @{term "card (atms_of_ms A)"} is an upper bound on the number of
elements, where adding one is necessary for the same reason as for the bound on the list, and one
is needed to have a strict bound.
›
abbreviation unassigned_lit :: "'b literal multiset set ⇒ 'a list ⇒ nat" where
"unassigned_lit N M ≡ card (atms_of_ms N) - length M"
lemma dpll_bj_trail_mes_increasing_prop:
fixes M :: "('v, unit, unit) ann_literals " and N :: "'v clauses"
assumes
"dpll_bj S T" and
"inv S" and
NA: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
MA: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
finite: "finite A"
shows "μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)
> μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)"
using assms(1,2)
proof (induction rule: dpll_bj_all_induct)
case (propagate⇩N⇩O⇩T C L) note CLN = this(1) and MC =this(2) and undef_L = this(3) and T = this(4)
have incl: "atm_of ` lits_of (Propagated L () # trail S) ⊆ atms_of_ms A"
using propagate⇩N⇩O⇩T.hyps propagate_ops.propagate⇩N⇩O⇩T dpll_bj_atms_in_trail_in_set bj_propagate⇩N⇩O⇩T
NA MA CLN by (auto simp: in_plus_implies_atm_of_on_atms_of_ms)
have no_dup: "no_dup (Propagated L () # trail S)"
using defined_lit_map n_d undef_L by auto
obtain a b l where M: "get_all_decided_decomposition (trail S) = (a, b) # l"
by (cases "get_all_decided_decomposition (trail S)") auto
have b_le_M: "length b ≤ length (trail S)"
using get_all_decided_decomposition_decomp[of "trail S"] by (simp add: M)
have "finite (atms_of_ms A)" using finite by simp
then have "length (Propagated L () # trail S) ≤ card (atms_of_ms A)"
using incl finite unfolding no_dup_length_eq_card_atm_of_lits_of[OF no_dup]
by (simp add: card_mono)
then have latm: "unassigned_lit A b = Suc (unassigned_lit A (Propagated L d # b))"
using b_le_M by auto
then show ?case using T undef_L by (auto simp: latm M μ⇩C_cons)
next
case (decide⇩N⇩O⇩T L) note undef_L = this(1) and MC = this(2) and T = this(3)
have incl: "atm_of ` lits_of (Decided L () # (trail S)) ⊆ atms_of_ms A"
using dpll_bj_atms_in_trail_in_set bj_decide⇩N⇩O⇩T decide⇩N⇩O⇩T.decide⇩N⇩O⇩T[OF decide⇩N⇩O⇩T.hyps] NA MA MC
by auto
have no_dup: "no_dup (Decided L () # (trail S))"
using defined_lit_map n_d undef_L by auto
obtain a b l where M: "get_all_decided_decomposition (trail S) = (a, b) # l"
by (cases "get_all_decided_decomposition (trail S)") auto
then have "length (Decided L () # (trail S)) ≤ card (atms_of_ms A)"
using incl finite unfolding no_dup_length_eq_card_atm_of_lits_of[OF no_dup]
by (simp add: card_mono)
then have latm: "unassigned_lit A (trail S) = Suc (unassigned_lit A (Decided L lv # (trail S)))"
by force
show ?case using T undef_L by (simp add: latm μ⇩C_cons)
next
case (backjump C F' K F L C' T) note undef_L = this(4) and MC =this(1) and tr_S = this(3) and
L = this(5) and T = this(8)
have incl: "atm_of ` lits_of (Propagated L () # F) ⊆ atms_of_ms A"
using dpll_bj_atms_in_trail_in_set NA MA tr_S L by auto
have no_dup: "no_dup (Propagated L () # F)"
using defined_lit_map n_d undef_L tr_S by auto
obtain a b l where M: "get_all_decided_decomposition (trail S) = (a, b) # l"
by (cases "get_all_decided_decomposition (trail S)") auto
have b_le_M: "length b ≤ length (trail S)"
using get_all_decided_decomposition_decomp[of "trail S"] by (simp add: M)
have fin_atms_A: "finite (atms_of_ms A)" using finite by simp
then have F_le_A: "length (Propagated L () # F) ≤ card (atms_of_ms A)"
using incl finite unfolding no_dup_length_eq_card_atm_of_lits_of[OF no_dup]
by (simp add: card_mono)
have tr_S_le_A: "length (trail S) ≤ (card (atms_of_ms A))"
using n_d MA by (metis fin_atms_A card_mono no_dup_length_eq_card_atm_of_lits_of)
obtain a b l where F: "get_all_decided_decomposition F = (a, b) # l"
by (cases "get_all_decided_decomposition F") auto
then have "F = b @ a"
using get_all_decided_decomposition_decomp[of "Propagated L () # F" a
"Propagated L () # b"] by simp
then have latm: "unassigned_lit A b = Suc (unassigned_lit A (Propagated L () # b))"
using F_le_A by simp
obtain rem where
rem:"map (λa. Suc (length (snd a))) (rev (get_all_decided_decomposition (F' @ Decided K () # F)))
= map (λa. Suc (length (snd a))) (rev (get_all_decided_decomposition F)) @ rem"
using take_length_get_all_decided_decomposition_decided_sandwich[of F "λa. Suc (length a)" F' K]
unfolding o_def by (metis append_take_drop_id)
then have rem: "map (λa. Suc (length (snd a)))
(get_all_decided_decomposition (F' @ Decided K () # F))
= rev rem @ map (λa. Suc (length (snd a))) ((get_all_decided_decomposition F))"
by (simp add: rev_map[symmetric] rev_swap)
have "length (rev rem @ map (λa. Suc (length (snd a))) (get_all_decided_decomposition F))
≤ Suc (card (atms_of_ms A))"
using arg_cong[OF rem, of length] tr_S_le_A
length_get_all_decided_decomposition_length[of "F' @ Decided K () # F"] tr_S by auto
moreover
{ fix i :: nat and xs :: "'a list"
have "i < length xs ⟹ length xs - Suc i < length xs"
by auto
then have H: "i<length xs ⟹ rev xs ! i ∈ set xs"
using rev_nth[of i xs] unfolding in_set_conv_nth by (force simp add: in_set_conv_nth)
} note H = this
have "∀i<length rem. rev rem ! i < card (atms_of_ms A) + 2"
using tr_S_le_A length_in_get_all_decided_decomposition_bounded[of _ S] unfolding tr_S
by (force simp add: o_def rem dest!: H intro: length_get_all_decided_decomposition_length)
ultimately show ?case
using μ⇩C_bounded[of "rev rem" "card (atms_of_ms A)+2" "unassigned_lit A l"] T undef_L
by (simp add: rem μ⇩C_append μ⇩C_cons F tr_S)
qed
lemma dpll_bj_trail_mes_decreasing_prop:
assumes dpll: "dpll_bj S T" and inv: "inv S" and
N_A: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
M_A: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
nd: "no_dup (trail S)" and
fin_A: "finite A"
shows "(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
- μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)
< (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
- μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)"
proof -
let ?b = "2+card (atms_of_ms A)"
let ?s = "1+card (atms_of_ms A)"
let ?μ = "μ⇩C ?s ?b"
have M'_A: "atm_of ` lits_of (trail T) ⊆ atms_of_ms A"
by (meson M_A N_A dpll dpll_bj_atms_in_trail_in_set inv)
have nd': "no_dup (trail T)"
using ‹dpll_bj S T› dpll_bj_no_dup nd inv by blast
{ fix i :: nat and xs :: "'a list"
have "i < length xs ⟹ length xs - Suc i < length xs"
by auto
then have H: "i<length xs ⟹ xs ! i ∈ set xs"
using rev_nth[of i xs] unfolding in_set_conv_nth by (force simp add: in_set_conv_nth)
} note H = this
have l_M_A: "length (trail S) ≤ card (atms_of_ms A)"
by (simp add: fin_A M_A card_mono no_dup_length_eq_card_atm_of_lits_of nd)
have l_M'_A: "length (trail T) ≤ card (atms_of_ms A)"
by (simp add: fin_A M'_A card_mono no_dup_length_eq_card_atm_of_lits_of nd')
have l_trail_weight_M: "length (trail_weight T) ≤ 1+card (atms_of_ms A)"
using l_M'_A length_get_all_decided_decomposition_length[of "trail T"] by auto
have bounded_M: "∀i<length (trail_weight T). (trail_weight T)! i < card (atms_of_ms A) + 2"
using length_in_get_all_decided_decomposition_bounded[of _ T] l_M'_A
by (metis (no_types, lifting) Nat.le_trans One_nat_def Suc_1 add.right_neutral add_Suc_right
le_imp_less_Suc less_eq_Suc_le nth_mem)
from dpll_bj_trail_mes_increasing_prop[OF dpll inv N_A M_A nd fin_A]
have "μ⇩C ?s ?b (trail_weight S) < μ⇩C ?s ?b (trail_weight T)" by simp
moreover from μ⇩C_bounded[OF bounded_M l_trail_weight_M]
have "μ⇩C ?s ?b (trail_weight T) ≤ ?b ^ ?s" by auto
ultimately show ?thesis by linarith
qed
lemma wf_dpll_bj:
assumes fin: "finite A"
shows "wf {(T, S). dpll_bj S T
∧ atms_of_msu (clauses S) ⊆ atms_of_ms A ∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A
∧ no_dup (trail S) ∧ inv S}"
(is "wf ?A")
proof (rule wf_bounded_measure[of _
"λ_. (2 + card (atms_of_ms A))^(1 + card (atms_of_ms A))"
"λS. μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)"])
fix a b :: "'st"
let ?b = "2+card (atms_of_ms A)"
let ?s = "1+card (atms_of_ms A)"
let ?μ = "μ⇩C ?s ?b"
assume ab: "(b, a) ∈ {(T, S). dpll_bj S T
∧ atms_of_msu (clauses S) ⊆ atms_of_ms A ∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A
∧ no_dup (trail S) ∧ inv S}"
have fin_A: "finite (atms_of_ms A)"
using fin by auto
have
dpll_bj: "dpll_bj a b" and
N_A: "atms_of_msu (clauses a) ⊆ atms_of_ms A" and
M_A: "atm_of ` lits_of (trail a) ⊆ atms_of_ms A" and
nd: "no_dup (trail a)" and
inv: "inv a"
using ab by auto
have M'_A: "atm_of ` lits_of (trail b) ⊆ atms_of_ms A"
by (meson M_A N_A ‹dpll_bj a b› dpll_bj_atms_in_trail_in_set inv)
have nd': "no_dup (trail b)"
using ‹dpll_bj a b› dpll_bj_no_dup nd inv by blast
{ fix i :: nat and xs :: "'a list"
have "i < length xs ⟹ length xs - Suc i < length xs"
by auto
then have H: "i<length xs ⟹ xs ! i ∈ set xs"
using rev_nth[of i xs] unfolding in_set_conv_nth by (force simp add: in_set_conv_nth)
} note H = this
have l_M_A: "length (trail a) ≤ card (atms_of_ms A)"
by (simp add: fin_A M_A card_mono no_dup_length_eq_card_atm_of_lits_of nd)
have l_M'_A: "length (trail b) ≤ card (atms_of_ms A)"
by (simp add: fin_A M'_A card_mono no_dup_length_eq_card_atm_of_lits_of nd')
have l_trail_weight_M: "length (trail_weight b) ≤ 1+card (atms_of_ms A)"
using l_M'_A length_get_all_decided_decomposition_length[of "trail b"] by auto
have bounded_M: "∀i<length (trail_weight b). (trail_weight b)! i < card (atms_of_ms A) + 2"
using length_in_get_all_decided_decomposition_bounded[of _ b] l_M'_A
by (metis (no_types, lifting) Nat.le_trans One_nat_def Suc_1 add.right_neutral add_Suc_right
le_imp_less_Suc less_eq_Suc_le nth_mem)
from dpll_bj_trail_mes_increasing_prop[OF dpll_bj inv N_A M_A nd fin]
have "μ⇩C ?s ?b (trail_weight a) < μ⇩C ?s ?b (trail_weight b)" by simp
moreover from μ⇩C_bounded[OF bounded_M l_trail_weight_M]
have "μ⇩C ?s ?b (trail_weight b) ≤ ?b ^ ?s" by auto
ultimately show "?b ^ ?s ≤ ?b ^ ?s ∧
μ⇩C ?s ?b (trail_weight b) ≤ ?b ^ ?s ∧
μ⇩C ?s ?b (trail_weight a) < μ⇩C ?s ?b (trail_weight b)"
by blast
qed
subsubsection ‹Normal Forms›
text ‹
We prove that given a normal form of DPLL, with some invariants, the either @{term N} is
satisfiable and the built valuation @{term M} is a model; or @{term N} is unsatisfiable.
Idea of the proof: We have to prove tat @{term "satisfiable N"}, @{term "¬M⊨as N"}
and there is no remaining step is incompatible.
▸ The @{term decide} rules tells us that every variable in @{term N} has a value.
▸ @{term "¬M⊨as N"} tells us that there is conflict.
▸ There is at least one decision in the trail (otherwise, @{term M} is a model of @{term N}).
▸ Now if we build the clause with all the decision literals of the trail, we can apply the
@{term backjump} rule.
The assumption are saying that we have a finite upper bound @{term A} for the literals, that we
cannot do any step @{term "no_step dpll_bj S"}›
theorem dpll_backjump_final_state:
fixes A :: "'v literal multiset set" and S T :: "'st"
assumes
"atms_of_msu (clauses S) ⊆ atms_of_ms A" and
"atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
"no_dup (trail S)" and
"finite A" and
inv: "inv S" and
n_s: "no_step dpll_bj S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows "unsatisfiable (set_mset (clauses S))
∨ (trail S ⊨asm clauses S ∧ satisfiable (set_mset (clauses S)))"
proof -
let ?N = "set_mset (clauses S)"
let ?M = "trail S"
consider
(sat) "satisfiable ?N" and "?M ⊨as ?N"
| (sat') "satisfiable ?N" and "¬ ?M ⊨as ?N"
| (unsat) "unsatisfiable ?N"
by auto
then show ?thesis
proof cases
case sat' note sat = this(1) and M = this(2)
obtain C where "C ∈ ?N" and "¬?M ⊨a C" using M unfolding true_annots_def by auto
obtain I :: "'v literal set" where
"I ⊨s ?N" and
cons: "consistent_interp I" and
tot: "total_over_m I ?N" and
atm_I_N: "atm_of `I ⊆ atms_of_ms ?N"
using sat unfolding satisfiable_def_min by auto
let ?I = "I ∪ {P| P. P ∈ lits_of ?M ∧ atm_of P ∉ atm_of ` I}"
let ?O = "{{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}"
have cons_I': "consistent_interp ?I"
using cons using ‹no_dup ?M› unfolding consistent_interp_def
by (auto simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set lits_of_def
dest!: no_dup_cannot_not_lit_and_uminus)
have tot_I': "total_over_m ?I (?N ∪ unmark ?M)"
using tot atms_of_s_def unfolding total_over_m_def total_over_set_def
by fastforce
have "{P |P. P ∈ lits_of ?M ∧ atm_of P ∉ atm_of ` I} ⊨s ?O"
using ‹I⊨s ?N› atm_I_N by (auto simp add: atm_of_eq_atm_of true_clss_def lits_of_def)
then have I'_N: "?I ⊨s ?N ∪ ?O"
using ‹I⊨s ?N› true_clss_union_increase by force
have tot': "total_over_m ?I (?N∪?O)"
using atm_I_N tot unfolding total_over_m_def total_over_set_def
by (force simp: image_iff lits_of_def dest!: is_decided_ex_Decided)
have atms_N_M: "atms_of_ms ?N ⊆ atm_of ` lits_of ?M"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain l :: 'v where
l_N: "l ∈ atms_of_ms ?N" and
l_M: "l ∉ atm_of ` lits_of ?M"
by auto
have "undefined_lit ?M (Pos l)"
using l_M by (metis Decided_Propagated_in_iff_in_lits_of
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set literal.sel(1))
from bj_decide⇩N⇩O⇩T[OF decide⇩N⇩O⇩T[OF this]] show False
using l_N n_s by (metis literal.sel(1) state_eq⇩N⇩O⇩T_ref)
qed
have "?M ⊨as CNot C"
by (metis ‹C ∈ set_mset (clauses S)› ‹¬ trail S ⊨a C› all_variables_defined_not_imply_cnot
atms_N_M atms_of_atms_of_ms_mono atms_of_ms_CNot_atms_of atms_of_ms_CNot_atms_of_ms
subset_eq)
have "∃l ∈ set ?M. is_decided l"
proof (rule ccontr)
let ?O = "{{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}"
have θ[iff]: "⋀I. total_over_m I (?N ∪ ?O ∪ unmark ?M)
⟷ total_over_m I (?N ∪unmark ?M)"
unfolding total_over_set_def total_over_m_def atms_of_ms_def by auto
assume "¬ ?thesis"
then have [simp]:"{{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M}
= {{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}"
by auto
then have "?N ∪ ?O ⊨ps unmark ?M"
using all_decomposition_implies_propagated_lits_are_implied[OF decomp] by auto
then have "?I ⊨s unmark ?M"
using cons_I' I'_N tot_I' ‹?I ⊨s ?N ∪ ?O› unfolding θ true_clss_clss_def by blast
then have "lits_of ?M ⊆ ?I"
unfolding true_clss_def lits_of_def by auto
then have "?M ⊨as ?N"
using I'_N ‹C ∈ ?N› ‹¬ ?M ⊨a C› cons_I' atms_N_M
by (meson ‹trail S ⊨as CNot C› consistent_CNot_not rev_subsetD sup_ge1 true_annot_def
true_annots_def true_cls_mono_set_mset_l true_clss_def)
then show False using M by fast
qed
from List.split_list_first_propE[OF this] obtain K :: "'v literal" and
F F' :: "('v, unit, unit) ann_literal list" where
M_K: "?M = F' @ Decided K () # F" and
nm: "∀f∈set F'. ¬is_decided f"
unfolding is_decided_def by (metis (full_types) old.unit.exhaust)
let ?K = "Decided K ()::('v, unit, unit) ann_literal"
have "?K ∈ set ?M"
unfolding M_K by auto
let ?C = "image_mset lit_of {#L∈#mset ?M. is_decided L ∧ L≠?K#} :: 'v literal multiset"
let ?C' = "set_mset (image_mset (λL::'v literal. {#L#}) (?C+{#lit_of ?K#}))"
have "?N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M} ⊨ps unmark ?M"
using all_decomposition_implies_propagated_lits_are_implied[OF decomp] .
moreover have C': "?C' = {{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M}"
unfolding M_K apply standard
apply force
using IntI by auto
ultimately have N_C_M: "?N ∪ ?C' ⊨ps unmark ?M"
by auto
have N_M_False: "?N ∪ (λL. {#lit_of L#}) ` (set ?M) ⊨ps {{#}}"
using M ‹?M ⊨as CNot C› ‹C∈?N› unfolding true_clss_clss_def true_annots_def Ball_def
true_annot_def by (metis consistent_CNot_not sup.orderE sup_commute true_clss_def
true_clss_singleton_lit_of_implies_incl true_clss_union true_clss_union_increase)
have "undefined_lit F K" using ‹no_dup ?M› unfolding M_K by (simp add: defined_lit_map)
moreover
have "?N ∪ ?C' ⊨ps {{#}}"
proof -
have A: "?N ∪ ?C' ∪ unmark ?M =
?N ∪ unmark ?M"
unfolding M_K by auto
show ?thesis
using true_clss_clss_left_right[OF N_C_M, of "{{#}}"] N_M_False unfolding A by auto
qed
have "?N ⊨p image_mset uminus ?C + {#-K#}"
unfolding true_clss_cls_def true_clss_clss_def total_over_m_def
proof (intro allI impI)
fix I
assume
tot: "total_over_set I (atms_of_ms (?N ∪ {image_mset uminus ?C+ {#- K#}}))" and
cons: "consistent_interp I" and
"I ⊨s ?N"
have "(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)"
using cons tot unfolding consistent_interp_def by (cases K) auto
have tot': "total_over_set I
(atm_of ` lit_of ` (set ?M ∩ {L. is_decided L ∧ L ≠ Decided K ()}))"
using tot by (auto simp add: atms_of_uminus_lit_atm_of_lit_of)
{ fix x :: "('v, unit, unit) ann_literal"
assume
a3: "lit_of x ∉ I" and
a1: "x ∈ set ?M" and
a4: "is_decided x" and
a5: "x ≠ Decided K ()"
then have "Pos (atm_of (lit_of x)) ∈ I ∨ Neg (atm_of (lit_of x)) ∈ I"
using a5 a4 tot' a1 unfolding total_over_set_def atms_of_s_def by blast
moreover have f6: "Neg (atm_of (lit_of x)) = - Pos (atm_of (lit_of x))"
by simp
ultimately have "- lit_of x ∈ I"
using f6 a3 by (metis (no_types) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
literal.sel(1))
} note H = this
have "¬I ⊨s ?C'"
using ‹?N ∪ ?C' ⊨ps {{#}}› tot cons ‹I ⊨s ?N›
unfolding true_clss_clss_def total_over_m_def
by (simp add: atms_of_uminus_lit_atm_of_lit_of atms_of_ms_single_image_atm_of_lit_of)
then show "I ⊨ image_mset uminus ?C + {#- K#}"
unfolding true_clss_def true_cls_def Bex_mset_def
using ‹(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)›
by (auto dest!: H)
qed
moreover have "F ⊨as CNot (image_mset uminus ?C)"
using nm unfolding true_annots_def CNot_def M_K by (auto simp add: lits_of_def)
ultimately have False
using bj_can_jump[of S F' K F C "-K"
"image_mset uminus (image_mset lit_of {# L :# mset ?M. is_decided L ∧ L ≠ Decided K ()#})"]
‹C∈?N› n_s ‹?M ⊨as CNot C› bj_backjump inv ‹no_dup (trail S)› unfolding M_K by auto
then show ?thesis by fast
qed auto
qed
end
locale dpll_with_backjumping =
dpll_with_backjumping_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv backjump_conds
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
inv :: "'st ⇒ bool" and
backjump_conds :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool"
+
assumes dpll_bj_inv:"⋀S T. dpll_bj S T ⟹ inv S ⟹ inv T"
begin
lemma rtranclp_dpll_bj_inv:
assumes "dpll_bj⇧*⇧* S T" and "inv S"
shows "inv T"
using assms by (induction rule: rtranclp_induct)
(auto simp add: dpll_bj_no_dup intro: dpll_bj_inv)
lemma rtranclp_dpll_bj_no_dup:
assumes "dpll_bj⇧*⇧* S T" and "inv S"
and "no_dup (trail S)"
shows "no_dup (trail T)"
using assms by (induction rule: rtranclp_induct)
(auto simp add: dpll_bj_no_dup dest: rtranclp_dpll_bj_inv dpll_bj_inv)
lemma rtranclp_dpll_bj_atms_of_ms_clauses_inv:
assumes
"dpll_bj⇧*⇧* S T" and "inv S"
shows "atms_of_msu (clauses S) = atms_of_msu (clauses T)"
using assms by (induction rule: rtranclp_induct)
(auto dest: rtranclp_dpll_bj_inv dpll_bj_atms_of_ms_clauses_inv)
lemma rtranclp_dpll_bj_atms_in_trail:
assumes
"dpll_bj⇧*⇧* S T" and
"inv S" and
"atm_of ` (lits_of (trail S)) ⊆ atms_of_msu (clauses S)"
shows "atm_of ` (lits_of (trail T)) ⊆ atms_of_msu (clauses T)"
using assms apply (induction rule: rtranclp_induct)
using dpll_bj_atms_in_trail dpll_bj_atms_of_ms_clauses_inv rtranclp_dpll_bj_inv by auto
lemma rtranclp_dpll_bj_sat_iff:
assumes "dpll_bj⇧*⇧* S T" and "inv S"
shows "I ⊨sm clauses S ⟷ I ⊨sm clauses T"
using assms by (induction rule: rtranclp_induct)
(auto dest!: dpll_bj_sat_iff simp: rtranclp_dpll_bj_inv)
lemma rtranclp_dpll_bj_atms_in_trail_in_set:
assumes
"dpll_bj⇧*⇧* S T" and
"inv S"
"atms_of_msu (clauses S) ⊆ A" and
"atm_of ` (lits_of (trail S)) ⊆ A"
shows "atm_of ` (lits_of (trail T)) ⊆ A"
using assms
by (induction rule: rtranclp_induct)
(auto dest: rtranclp_dpll_bj_inv
simp add: dpll_bj_atms_in_trail_in_set rtranclp_dpll_bj_atms_of_ms_clauses_inv
rtranclp_dpll_bj_inv)
lemma rtranclp_dpll_bj_all_decomposition_implies_inv:
assumes
"dpll_bj⇧*⇧* S T" and
"inv S"
"all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows "all_decomposition_implies_m (clauses T) (get_all_decided_decomposition (trail T))"
using assms by (induction rule: rtranclp_induct)
(auto intro: dpll_bj_all_decomposition_implies_inv simp: rtranclp_dpll_bj_inv)
lemma rtranclp_dpll_bj_inv_incl_dpll_bj_inv_trancl:
"{(T, S). dpll_bj⇧+⇧+ S T
∧ atms_of_msu (clauses S) ⊆ atms_of_ms A ∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A
∧ no_dup (trail S) ∧ inv S}
⊆ {(T, S). dpll_bj S T ∧ atms_of_msu (clauses S) ⊆ atms_of_ms A
∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A ∧ no_dup (trail S) ∧ inv S}⇧+"
(is "?A ⊆ ?B⇧+")
proof standard
fix x
assume x_A: "x ∈ ?A"
obtain S T::"'st" where
x[simp]: "x = (T, S)" by (cases x) auto
have
"dpll_bj⇧+⇧+ S T" and
"atms_of_msu (clauses S) ⊆ atms_of_ms A" and
"atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
"no_dup (trail S)" and
"inv S"
using x_A by auto
then show "x ∈ ?B⇧+" unfolding x
proof (induction rule: tranclp_induct)
case base
then show ?case by auto
next
case (step T U) note step = this(1) and ST = this(2) and IH = this(3)[OF this(4-7)]
and N_A = this(4) and M_A = this(5) and nd = this(6) and inv = this(7)
have [simp]: "atms_of_msu (clauses S) = atms_of_msu (clauses T)"
using step rtranclp_dpll_bj_atms_of_ms_clauses_inv tranclp_into_rtranclp inv by fastforce
have "no_dup (trail T)"
using local.step nd rtranclp_dpll_bj_no_dup tranclp_into_rtranclp inv by fastforce
moreover have "atm_of ` (lits_of (trail T)) ⊆ atms_of_ms A"
by (metis inv M_A N_A local.step rtranclp_dpll_bj_atms_in_trail_in_set
tranclp_into_rtranclp)
moreover have "inv T"
using inv local.step rtranclp_dpll_bj_inv tranclp_into_rtranclp by fastforce
ultimately have "(U, T) ∈ ?B" using ST N_A M_A inv by auto
then show ?case using IH by (rule trancl_into_trancl2)
qed
qed
lemma wf_tranclp_dpll_bj:
assumes fin: "finite A"
shows "wf {(T, S). dpll_bj⇧+⇧+ S T
∧ atms_of_msu (clauses S) ⊆ atms_of_ms A ∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A
∧ no_dup (trail S) ∧ inv S}"
using wf_trancl[OF wf_dpll_bj[OF fin]] rtranclp_dpll_bj_inv_incl_dpll_bj_inv_trancl
by (rule wf_subset)
lemma dpll_bj_sat_ext_iff:
"dpll_bj S T ⟹ inv S ⟹ I⊨sextm clauses S ⟷ I⊨sextm clauses T"
by (simp add: dpll_bj_clauses)
lemma rtranclp_dpll_bj_sat_ext_iff:
"dpll_bj⇧*⇧* S T ⟹ inv S ⟹ I⊨sextm clauses S ⟷ I⊨sextm clauses T"
by (induction rule: rtranclp_induct) (simp_all add: rtranclp_dpll_bj_inv dpll_bj_sat_ext_iff)
theorem full_dpll_backjump_final_state:
fixes A :: "'v literal multiset set" and S T :: "'st"
assumes
full: "full dpll_bj S T" and
atms_S: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atms_trail: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
"finite A" and
inv: "inv S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows "unsatisfiable (set_mset (clauses S))
∨ (trail T ⊨asm clauses S ∧ satisfiable (set_mset (clauses S)))"
proof -
have st: "dpll_bj⇧*⇧* S T" and "no_step dpll_bj T"
using full unfolding full_def by fast+
moreover have "atms_of_msu (clauses T) ⊆ atms_of_ms A"
using atms_S inv rtranclp_dpll_bj_atms_of_ms_clauses_inv st by blast
moreover have "atm_of ` lits_of (trail T) ⊆ atms_of_ms A"
using atms_S atms_trail inv rtranclp_dpll_bj_atms_in_trail_in_set st by auto
moreover have "no_dup (trail T)"
using n_d inv rtranclp_dpll_bj_no_dup st by blast
moreover have inv: "inv T"
using inv rtranclp_dpll_bj_inv st by blast
moreover
have decomp: "all_decomposition_implies_m (clauses T) (get_all_decided_decomposition (trail T))"
using ‹inv S› decomp rtranclp_dpll_bj_all_decomposition_implies_inv st by blast
ultimately have "unsatisfiable (set_mset (clauses T))
∨ (trail T ⊨asm clauses T ∧ satisfiable (set_mset (clauses T)))"
using ‹finite A› dpll_backjump_final_state by force
then show ?thesis
by (meson ‹inv S› rtranclp_dpll_bj_sat_iff satisfiable_carac st true_annots_true_cls)
qed
corollary full_dpll_backjump_final_state_from_init_state:
fixes A :: "'v literal multiset set" and S T :: "'st"
assumes
full: "full dpll_bj S T" and
"trail S = []" and
"clauses S = N" and
"inv S"
shows "unsatisfiable (set_mset N) ∨ (trail T ⊨asm N ∧ satisfiable (set_mset N))"
using assms full_dpll_backjump_final_state[of S T "set_mset N"] by auto
lemma tranclp_dpll_bj_trail_mes_decreasing_prop:
assumes dpll: "dpll_bj⇧+⇧+ S T" and inv: "inv S" and
N_A: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
M_A: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
fin_A: "finite A"
shows "(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
- μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)
< (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
- μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)"
using dpll
proof (induction)
case base
then show ?case
using N_A M_A n_d dpll_bj_trail_mes_decreasing_prop fin_A inv by blast
next
case (step T U) note st = this(1) and dpll = this(2) and IH = this(3)
have " atms_of_msu (clauses S) = atms_of_msu (clauses T)"
using rtranclp_dpll_bj_atms_of_ms_clauses_inv by (metis dpll_bj_clauses dpll_bj_inv inv st
tranclpD)
then have N_A': "atms_of_msu (clauses T) ⊆ atms_of_ms A"
using N_A by auto
moreover have M_A': "atm_of ` lits_of (trail T) ⊆ atms_of_ms A"
by (meson M_A N_A inv rtranclp_dpll_bj_atms_in_trail_in_set st dpll
tranclp.r_into_trancl tranclp_into_rtranclp tranclp_trans)
moreover have nd: "no_dup (trail T)"
by (metis inv n_d rtranclp_dpll_bj_no_dup st tranclp_into_rtranclp)
moreover have "inv T"
by (meson dpll dpll_bj_inv inv rtranclp_dpll_bj_inv st tranclp_into_rtranclp)
ultimately show ?case
using IH dpll_bj_trail_mes_decreasing_prop[of T U A] dpll fin_A by linarith
qed
end
subsection ‹CDCL›
subsubsection ‹Learn and Forget›
locale learn_ops =
dpll_state trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" +
fixes
learn_cond :: "'v clause ⇒ 'st ⇒ bool"
begin
inductive learn :: "'st ⇒ 'st ⇒ bool" where
"clauses S ⊨pm C ⟹ atms_of C ⊆ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S))
⟹ learn_cond C S
⟹ T ∼ add_cls⇩N⇩O⇩T C S
⟹ learn S T"
inductive_cases learn⇩N⇩O⇩TE: "learn S T"
lemma learn_μ⇩C_stable:
assumes "learn S T" and "no_dup (trail S)"
shows "μ⇩C A B (trail_weight S) = μ⇩C A B (trail_weight T)"
using assms by (auto elim: learn⇩N⇩O⇩TE)
end
locale forget_ops =
dpll_state trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" +
fixes
forget_cond :: "'v clause ⇒ 'st ⇒ bool"
begin
inductive forget⇩N⇩O⇩T :: "'st ⇒ 'st ⇒ bool" where
forget⇩N⇩O⇩T:"clauses S - replicate_mset (count (clauses S) C) C ⊨pm C
⟹ forget_cond C S
⟹ C ∈# clauses S
⟹ T ∼ remove_cls⇩N⇩O⇩T C S
⟹ forget⇩N⇩O⇩T S T"
inductive_cases forget⇩N⇩O⇩TE: "forget⇩N⇩O⇩T S T"
lemma forget_μ⇩C_stable:
assumes "forget⇩N⇩O⇩T S T"
shows "μ⇩C A B (trail_weight S) = μ⇩C A B (trail_weight T)"
using assms by (auto elim!: forget⇩N⇩O⇩TE)
end
locale learn_and_forget⇩N⇩O⇩T =
learn_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T learn_cond +
forget_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T forget_cond
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
learn_cond forget_cond :: "'v clause ⇒ 'st ⇒ bool"
begin
inductive learn_and_forget⇩N⇩O⇩T :: "'st ⇒ 'st ⇒ bool"
where
lf_learn: "learn S T ⟹ learn_and_forget⇩N⇩O⇩T S T" |
lf_forget: "forget⇩N⇩O⇩T S T ⟹ learn_and_forget⇩N⇩O⇩T S T"
end
subsubsection ‹Definition of CDCL›
locale conflict_driven_clause_learning_ops =
dpll_with_backjumping_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv backjump_conds +
learn_and_forget⇩N⇩O⇩T trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T learn_cond
forget_cond
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒'st ⇒ bool" and
inv :: "'st ⇒ bool" and
backjump_conds :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool" and
learn_cond forget_cond :: "'v clause ⇒ 'st ⇒ bool"
begin
inductive cdcl⇩N⇩O⇩T :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
c_dpll_bj: "dpll_bj S S' ⟹ cdcl⇩N⇩O⇩T S S'" |
c_learn: "learn S S' ⟹ cdcl⇩N⇩O⇩T S S'" |
c_forget⇩N⇩O⇩T: "forget⇩N⇩O⇩T S S' ⟹ cdcl⇩N⇩O⇩T S S'"
lemma cdcl⇩N⇩O⇩T_all_induct[consumes 1, case_names dpll_bj learn forget⇩N⇩O⇩T]:
fixes S T :: "'st"
assumes "cdcl⇩N⇩O⇩T S T" and
dpll: "⋀T. dpll_bj S T ⟹ P S T" and
learning:
"⋀C T. clauses S ⊨pm C ⟹
atms_of C ⊆ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S)) ⟹
T ∼ add_cls⇩N⇩O⇩T C S ⟹
P S T" and
forgetting: "⋀C T. clauses S - replicate_mset (count (clauses S) C) C ⊨pm C ⟹
C ∈# clauses S ⟹
T ∼ remove_cls⇩N⇩O⇩T C S ⟹
P S T"
shows "P S T"
using assms(1) by (induction rule: cdcl⇩N⇩O⇩T.induct)
(auto intro: assms(2, 3, 4) elim!: learn⇩N⇩O⇩TE forget⇩N⇩O⇩TE)+
lemma cdcl⇩N⇩O⇩T_no_dup:
assumes
"cdcl⇩N⇩O⇩T S T" and
"inv S" and
"no_dup (trail S)"
shows "no_dup (trail T)"
using assms by (induction rule: cdcl⇩N⇩O⇩T_all_induct) (auto intro: dpll_bj_no_dup)
paragraph ‹Consistency of the trail›
lemma cdcl⇩N⇩O⇩T_consistent:
assumes
"cdcl⇩N⇩O⇩T S T" and
"inv S" and
"no_dup (trail S)"
shows "consistent_interp (lits_of (trail T))"
using cdcl⇩N⇩O⇩T_no_dup[OF assms] distinctconsistent_interp by fast
text ‹The subtle problem here is that tautologies can be removed, meaning that some variable can
disappear of the problem. It is also possible that some variable of the trail are not in the
clauses anymore.›
lemma cdcl⇩N⇩O⇩T_atms_of_ms_clauses_decreasing:
assumes "cdcl⇩N⇩O⇩T S T"and "inv S" and "no_dup (trail S)"
shows "atms_of_msu (clauses T) ⊆ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S))"
using assms by (induction rule: cdcl⇩N⇩O⇩T_all_induct)
(auto dest!: dpll_bj_atms_of_ms_clauses_inv set_mp simp add: atms_of_ms_def Union_eq)
lemma cdcl⇩N⇩O⇩T_atms_in_trail:
assumes "cdcl⇩N⇩O⇩T S T"and "inv S" and "no_dup (trail S)"
and "atm_of ` (lits_of (trail S)) ⊆ atms_of_msu (clauses S)"
shows "atm_of ` (lits_of (trail T)) ⊆ atms_of_msu (clauses S)"
using assms by (induction rule: cdcl⇩N⇩O⇩T_all_induct) (auto simp add: dpll_bj_atms_in_trail)
lemma cdcl⇩N⇩O⇩T_atms_in_trail_in_set:
assumes
"cdcl⇩N⇩O⇩T S T" and "inv S" and "no_dup (trail S)" and
"atms_of_msu (clauses S) ⊆ A" and
"atm_of ` (lits_of (trail S)) ⊆ A"
shows "atm_of ` (lits_of (trail T)) ⊆ A"
using assms
by (induction rule: cdcl⇩N⇩O⇩T_all_induct)
(simp_all add: dpll_bj_atms_in_trail_in_set dpll_bj_atms_of_ms_clauses_inv)
lemma cdcl⇩N⇩O⇩T_all_decomposition_implies:
assumes "cdcl⇩N⇩O⇩T S T" and "inv S" and n_d[simp]: "no_dup (trail S)" and
"all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows
"all_decomposition_implies_m (clauses T) (get_all_decided_decomposition (trail T))"
using assms(1,2,4)
proof (induction rule: cdcl⇩N⇩O⇩T_all_induct)
case dpll_bj
then show ?case
using dpll_bj_all_decomposition_implies_inv n_d by blast
next
case learn
then show ?case by (auto simp add: all_decomposition_implies_def)
next
case (forget⇩N⇩O⇩T C T) note cls_C = this(1) and C = this(2) and T = this(3) and iniv = this(4) and
decomp = this(5)
show ?case
unfolding all_decomposition_implies_def Ball_def
proof (intro allI, clarify)
fix a b
assume "(a, b) ∈ set (get_all_decided_decomposition (trail T))"
then have "unmark a ∪ set_mset (clauses S) ⊨ps unmark b"
using decomp T by (auto simp add: all_decomposition_implies_def)
moreover
have "C ∈ set_mset (clauses S)"
by (simp add: C)
then have "set_mset (clauses T) ⊨ps set_mset (clauses S)"
by (metis (no_types) T clauses_remove_cls⇩N⇩O⇩T cls_C insert_Diff order_refl
set_mset_minus_replicate_mset(1) state_eq⇩N⇩O⇩T_clauses true_clss_clss_def
true_clss_clss_insert)
ultimately show "unmark a ∪ set_mset (clauses T)
⊨ps unmark b"
using true_clss_clss_generalise_true_clss_clss by blast
qed
qed
paragraph ‹Extension of models›
lemma cdcl⇩N⇩O⇩T_bj_sat_ext_iff:
assumes "cdcl⇩N⇩O⇩T S T"and "inv S" and n_d: "no_dup (trail S)"
shows "I⊨sextm clauses S ⟷ I⊨sextm clauses T"
using assms
proof (induction rule:cdcl⇩N⇩O⇩T_all_induct)
case dpll_bj
then show ?case by (simp add: dpll_bj_clauses)
next
case (learn C T) note T = this(3)
{ fix J
assume
"I ⊨sextm clauses S" and
"I ⊆ J" and
tot: "total_over_m J (set_mset ({#C#} + (clauses S)))" and
cons: "consistent_interp J"
then have "J ⊨sm clauses S" unfolding true_clss_ext_def by auto
moreover
with ‹clauses S⊨pm C› have "J ⊨ C"
using tot cons unfolding true_clss_cls_def by auto
ultimately have "J ⊨sm {#C#} + clauses S" by auto
}
then have H: "I ⊨sextm (clauses S) ⟹ I ⊨sext insert C (set_mset (clauses S))"
unfolding true_clss_ext_def by auto
show ?case
apply standard
using T n_d apply (auto simp add: H)[]
using T n_d apply simp
by (metis Diff_insert_absorb insert_subset subsetI subset_antisym
true_clss_ext_decrease_right_remove_r)
next
case (forget⇩N⇩O⇩T C T) note cls_C = this(1) and T = this(3)
{ fix J
assume
"I ⊨sext set_mset (clauses S) - {C}" and
"I ⊆ J" and
tot: "total_over_m J (set_mset (clauses S))" and
cons: "consistent_interp J"
then have "J ⊨s set_mset (clauses S) - {C}"
unfolding true_clss_ext_def by (meson Diff_subset total_over_m_subset)
moreover
with cls_C have "J ⊨ C"
using tot cons unfolding true_clss_cls_def
by (metis Un_commute forget⇩N⇩O⇩T.hyps(2) insert_Diff insert_is_Un mem_set_mset_iff order_refl
set_mset_minus_replicate_mset(1))
ultimately have "J ⊨sm (clauses S)" by (metis insert_Diff_single true_clss_insert)
}
then have H: "I ⊨sext set_mset (clauses S) - {C} ⟹ I ⊨sextm (clauses S)"
unfolding true_clss_ext_def by blast
show ?case using T by (auto simp: true_clss_ext_decrease_right_remove_r H)
qed
end ― ‹end of ‹conflict_driven_clause_learning_ops››
subsection ‹CDCL with invariant›
locale conflict_driven_clause_learning =
conflict_driven_clause_learning_ops +
assumes cdcl⇩N⇩O⇩T_inv: "⋀S T. cdcl⇩N⇩O⇩T S T ⟹ inv S ⟹ inv T"
begin
sublocale dpll_with_backjumping
apply unfold_locales
using cdcl⇩N⇩O⇩T.simps cdcl⇩N⇩O⇩T_inv by auto
lemma rtranclp_cdcl⇩N⇩O⇩T_inv:
"cdcl⇩N⇩O⇩T⇧*⇧* S T ⟹ inv S ⟹ inv T"
by (induction rule: rtranclp_induct) (auto simp add: cdcl⇩N⇩O⇩T_inv)
lemma rtranclp_cdcl⇩N⇩O⇩T_no_dup:
assumes "cdcl⇩N⇩O⇩T⇧*⇧* S T" and "inv S"
and "no_dup (trail S)"
shows "no_dup (trail T)"
using assms by (induction rule: rtranclp_induct) (auto intro: cdcl⇩N⇩O⇩T_no_dup rtranclp_cdcl⇩N⇩O⇩T_inv)
lemma rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound:
assumes
cdcl: "cdcl⇩N⇩O⇩T⇧*⇧* S T" and
inv: "inv S" and
n_d: "no_dup (trail S)" and
atms_clauses_S: "atms_of_msu (clauses S) ⊆ A" and
atms_trail_S: "atm_of `(lits_of (trail S)) ⊆ A"
shows "atm_of `(lits_of (trail T)) ⊆ A ∧ atms_of_msu (clauses T) ⊆ A"
using cdcl
proof (induction rule: rtranclp_induct)
case base
then show ?case using atms_clauses_S atms_trail_S by simp
next
case (step T U) note st = this(1) and cdcl⇩N⇩O⇩T = this(2) and IH = this(3)
have "inv T" using inv st rtranclp_cdcl⇩N⇩O⇩T_inv by blast
have "no_dup (trail T)"
using rtranclp_cdcl⇩N⇩O⇩T_no_dup[of S T] st cdcl⇩N⇩O⇩T inv n_d by blast
then have "atms_of_msu (clauses U) ⊆ A"
using cdcl⇩N⇩O⇩T_atms_of_ms_clauses_decreasing[OF cdcl⇩N⇩O⇩T] IH n_d ‹inv T› by auto
moreover
have "atm_of `(lits_of (trail U)) ⊆ A"
using cdcl⇩N⇩O⇩T_atms_in_trail_in_set[OF cdcl⇩N⇩O⇩T, of A] ‹no_dup (trail T)›
by (meson atms_trail_S atms_clauses_S IH ‹inv T› cdcl⇩N⇩O⇩T )
ultimately show ?case by fast
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_all_decomposition_implies:
assumes "cdcl⇩N⇩O⇩T⇧*⇧* S T" and "inv S" and "no_dup (trail S)" and
"all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows
"all_decomposition_implies_m (clauses T) (get_all_decided_decomposition (trail T))"
using assms by (induction)
(auto intro: rtranclp_cdcl⇩N⇩O⇩T_inv cdcl⇩N⇩O⇩T_all_decomposition_implies rtranclp_cdcl⇩N⇩O⇩T_no_dup)
lemma rtranclp_cdcl⇩N⇩O⇩T_bj_sat_ext_iff:
assumes "cdcl⇩N⇩O⇩T⇧*⇧* S T"and "inv S" and "no_dup (trail S)"
shows "I⊨sextm clauses S ⟷ I⊨sextm clauses T"
using assms apply (induction rule: rtranclp_induct)
using cdcl⇩N⇩O⇩T_bj_sat_ext_iff by (auto intro: rtranclp_cdcl⇩N⇩O⇩T_inv rtranclp_cdcl⇩N⇩O⇩T_no_dup)
definition cdcl⇩N⇩O⇩T_NOT_all_inv where
"cdcl⇩N⇩O⇩T_NOT_all_inv A S ⟷ (finite A ∧ inv S ∧ atms_of_msu (clauses S) ⊆ atms_of_ms A
∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A ∧ no_dup (trail S))"
lemma cdcl⇩N⇩O⇩T_NOT_all_inv:
assumes "cdcl⇩N⇩O⇩T⇧*⇧* S T" and "cdcl⇩N⇩O⇩T_NOT_all_inv A S"
shows "cdcl⇩N⇩O⇩T_NOT_all_inv A T"
using assms unfolding cdcl⇩N⇩O⇩T_NOT_all_inv_def
by (simp add: rtranclp_cdcl⇩N⇩O⇩T_inv rtranclp_cdcl⇩N⇩O⇩T_no_dup rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound)
abbreviation learn_or_forget where
"learn_or_forget S T ≡ (λS T. learn S T ∨ forget⇩N⇩O⇩T S T) S T"
lemma rtranclp_learn_or_forget_cdcl⇩N⇩O⇩T:
"learn_or_forget⇧*⇧* S T ⟹ cdcl⇩N⇩O⇩T⇧*⇧* S T"
using rtranclp_mono[of learn_or_forget cdcl⇩N⇩O⇩T] cdcl⇩N⇩O⇩T.c_learn cdcl⇩N⇩O⇩T.c_forget⇩N⇩O⇩T by blast
lemma learn_or_forget_dpll_μ⇩C:
assumes
l_f: "learn_or_forget⇧*⇧* S T" and
dpll: "dpll_bj T U" and
inv: "cdcl⇩N⇩O⇩T_NOT_all_inv A S"
shows "(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
- μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight U)
< (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
- μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight S)"
(is "?μ U < ?μ S")
proof -
have "?μ S = ?μ T"
using l_f
proof (induction)
case base
then show ?case by simp
next
case (step T U)
moreover then have "no_dup (trail T)"
using rtranclp_cdcl⇩N⇩O⇩T_no_dup[of S T] cdcl⇩N⇩O⇩T_NOT_all_inv_def inv
rtranclp_learn_or_forget_cdcl⇩N⇩O⇩T by auto
ultimately show ?case
using forget_μ⇩C_stable learn_μ⇩C_stable inv unfolding cdcl⇩N⇩O⇩T_NOT_all_inv_def by presburger
qed
moreover have "cdcl⇩N⇩O⇩T_NOT_all_inv A T"
using rtranclp_learn_or_forget_cdcl⇩N⇩O⇩T cdcl⇩N⇩O⇩T_NOT_all_inv l_f inv by blast
ultimately show ?thesis
using dpll_bj_trail_mes_decreasing_prop[of T U A, OF dpll] finite
unfolding cdcl⇩N⇩O⇩T_NOT_all_inv_def by linarith
qed
lemma infinite_cdcl⇩N⇩O⇩T_exists_learn_and_forget_infinite_chain:
assumes
"⋀i. cdcl⇩N⇩O⇩T (f i) (f(Suc i))" and
inv: "cdcl⇩N⇩O⇩T_NOT_all_inv A (f 0)"
shows "∃j. ∀i≥j. learn_or_forget (f i) (f (Suc i))"
using assms
proof (induction "(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
- μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight (f 0))"
arbitrary: f
rule: nat_less_induct_case)
case (Suc n) note IH = this(1) and μ = this(2) and cdcl⇩N⇩O⇩T = this(3) and inv = this(4)
consider
(dpll_end) "∃j. ∀i≥j. learn_or_forget (f i) (f (Suc i))"
| (dpll_more) "¬(∃j. ∀i≥j. learn_or_forget (f i) (f (Suc i)))"
by blast
then show ?case
proof cases
case dpll_end
then show ?thesis by auto
next
case dpll_more
then have j: "∃i. ¬ learn (f i) (f (Suc i)) ∧ ¬forget⇩N⇩O⇩T (f i) (f (Suc i))"
by blast
obtain i where
"¬learn (f i) (f (Suc i)) ∧ ¬forget⇩N⇩O⇩T (f i) (f (Suc i))" and
"∀k<i. learn_or_forget (f k) (f (Suc k))"
proof -
obtain i⇩0 where "¬ learn (f i⇩0) (f (Suc i⇩0)) ∧ ¬forget⇩N⇩O⇩T (f i⇩0) (f (Suc i⇩0))"
using j by auto
then have "{i. i≤i⇩0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬forget⇩N⇩O⇩T (f i) (f (Suc i))} ≠ {}"
by auto
let ?I = "{i. i≤i⇩0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬forget⇩N⇩O⇩T (f i) (f (Suc i))}"
let ?i = "Min ?I"
have "finite ?I"
by auto
have "¬ learn (f ?i) (f (Suc ?i)) ∧ ¬forget⇩N⇩O⇩T (f ?i) (f (Suc ?i))"
using Min_in[OF ‹finite ?I› ‹?I ≠ {}›] by auto
moreover have "∀k<?i. learn_or_forget (f k) (f (Suc k))"
using Min.coboundedI[of "{i. i ≤ i⇩0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬ forget⇩N⇩O⇩T (f i)
(f (Suc i))}", simplified]
by (meson ‹¬ learn (f i⇩0) (f (Suc i⇩0)) ∧ ¬ forget⇩N⇩O⇩T (f i⇩0) (f (Suc i⇩0))› less_imp_le
dual_order.trans not_le)
ultimately show ?thesis using that by blast
qed
def g ≡ "λn. f (n + Suc i)"
have "dpll_bj (f i) (g 0)"
using ‹¬ learn (f i) (f (Suc i)) ∧ ¬ forget⇩N⇩O⇩T (f i) (f (Suc i))› cdcl⇩N⇩O⇩T cdcl⇩N⇩O⇩T.cases
g_def by auto
{
fix j
assume "j ≤ i"
then have "learn_or_forget⇧*⇧* (f 0) (f j)"
apply (induction j)
apply simp
by (metis (no_types, lifting) Suc_leD Suc_le_lessD rtranclp.simps
‹∀k<i. learn (f k) (f (Suc k)) ∨ forget⇩N⇩O⇩T (f k) (f (Suc k))›)
}
then have "learn_or_forget⇧*⇧* (f 0) (f i)" by blast
then have "(2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight (g 0))
< (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight (f 0))"
using learn_or_forget_dpll_μ⇩C[of "f 0" "f i" "g 0" A] inv ‹dpll_bj (f i) (g 0)›
unfolding cdcl⇩N⇩O⇩T_NOT_all_inv_def by linarith
moreover have cdcl⇩N⇩O⇩T_i: "cdcl⇩N⇩O⇩T⇧*⇧* (f 0) (g 0)"
using rtranclp_learn_or_forget_cdcl⇩N⇩O⇩T[of "f 0" "f i"] ‹learn_or_forget⇧*⇧* (f 0) (f i)›
cdcl⇩N⇩O⇩T[of i] unfolding g_def by auto
moreover have "⋀i. cdcl⇩N⇩O⇩T (g i) (g (Suc i))"
using cdcl⇩N⇩O⇩T g_def by auto
moreover have "cdcl⇩N⇩O⇩T_NOT_all_inv A (g 0)"
using inv cdcl⇩N⇩O⇩T_i rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound g_def cdcl⇩N⇩O⇩T_NOT_all_inv by auto
ultimately obtain j where j: "⋀i. i≥j ⟹ learn_or_forget (g i) (g (Suc i))"
using IH unfolding μ[symmetric] by presburger
show ?thesis
proof
{
fix k
assume "k ≥ j + Suc i"
then have "learn_or_forget (f k) (f (Suc k))"
using j[of "k-Suc i"] unfolding g_def by auto
}
then show "∀k≥j+Suc i. learn_or_forget (f k) (f (Suc k))"
by auto
qed
qed
next
case 0 note H = this(1) and cdcl⇩N⇩O⇩T = this(2) and inv = this(3)
show ?case
proof (rule ccontr)
assume "¬ ?case"
then have j: "∃i. ¬ learn (f i) (f (Suc i)) ∧ ¬forget⇩N⇩O⇩T (f i) (f (Suc i))"
by blast
obtain i where
"¬learn (f i) (f (Suc i)) ∧ ¬forget⇩N⇩O⇩T (f i) (f (Suc i))" and
"∀k<i. learn_or_forget (f k) (f (Suc k))"
proof -
obtain i⇩0 where "¬ learn (f i⇩0) (f (Suc i⇩0)) ∧ ¬forget⇩N⇩O⇩T (f i⇩0) (f (Suc i⇩0))"
using j by auto
then have "{i. i≤i⇩0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬forget⇩N⇩O⇩T (f i) (f (Suc i))} ≠ {}"
by auto
let ?I = "{i. i≤i⇩0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬forget⇩N⇩O⇩T (f i) (f (Suc i))}"
let ?i = "Min ?I"
have "finite ?I"
by auto
have "¬ learn (f ?i) (f (Suc ?i)) ∧ ¬forget⇩N⇩O⇩T (f ?i) (f (Suc ?i))"
using Min_in[OF ‹finite ?I› ‹?I ≠ {}›] by auto
moreover have "∀k<?i. learn_or_forget (f k) (f (Suc k))"
using Min.coboundedI[of "{i. i ≤ i⇩0 ∧ ¬ learn (f i) (f (Suc i)) ∧ ¬ forget⇩N⇩O⇩T (f i)
(f (Suc i))}", simplified]
by (meson ‹¬ learn (f i⇩0) (f (Suc i⇩0)) ∧ ¬ forget⇩N⇩O⇩T (f i⇩0) (f (Suc i⇩0))› less_imp_le
dual_order.trans not_le)
ultimately show ?thesis using that by blast
qed
have "dpll_bj (f i) (f (Suc i))"
using ‹¬ learn (f i) (f (Suc i)) ∧ ¬ forget⇩N⇩O⇩T (f i) (f (Suc i))› cdcl⇩N⇩O⇩T cdcl⇩N⇩O⇩T.cases
by blast
{
fix j
assume "j ≤ i"
then have "learn_or_forget⇧*⇧* (f 0) (f j)"
apply (induction j)
apply simp
by (metis (no_types, lifting) Suc_leD Suc_le_lessD rtranclp.simps
‹∀k<i. learn (f k) (f (Suc k)) ∨ forget⇩N⇩O⇩T (f k) (f (Suc k))›)
}
then have "learn_or_forget⇧*⇧* (f 0) (f i)" by blast
then show False
using learn_or_forget_dpll_μ⇩C[of "f 0" "f i" "f (Suc i)" A] inv 0
‹dpll_bj (f i) (f (Suc i))› unfolding cdcl⇩N⇩O⇩T_NOT_all_inv_def by linarith
qed
qed
lemma wf_cdcl⇩N⇩O⇩T_no_learn_and_forget_infinite_chain:
assumes
no_infinite_lf: "⋀f j. ¬ (∀i≥j. learn_or_forget (f i) (f (Suc i)))"
shows "wf {(T, S). cdcl⇩N⇩O⇩T S T ∧ cdcl⇩N⇩O⇩T_NOT_all_inv A S}" (is "wf {(T, S). cdcl⇩N⇩O⇩T S T
∧ ?inv S}")
unfolding wf_iff_no_infinite_down_chain
proof (rule ccontr)
assume "¬ ¬ (∃f. ∀i. (f (Suc i), f i) ∈ {(T, S). cdcl⇩N⇩O⇩T S T ∧ ?inv S})"
then obtain f where
"∀i. cdcl⇩N⇩O⇩T (f i) (f (Suc i)) ∧ ?inv (f i)"
by fast
then have "∃j. ∀i≥j. learn_or_forget (f i) (f (Suc i))"
using infinite_cdcl⇩N⇩O⇩T_exists_learn_and_forget_infinite_chain[of f] by meson
then show False using no_infinite_lf by blast
qed
lemma inv_and_tranclp_cdcl_⇩N⇩O⇩T_tranclp_cdcl⇩N⇩O⇩T_and_inv:
"cdcl⇩N⇩O⇩T⇧+⇧+ S T ∧ cdcl⇩N⇩O⇩T_NOT_all_inv A S ⟷ (λS T. cdcl⇩N⇩O⇩T S T ∧ cdcl⇩N⇩O⇩T_NOT_all_inv A S)⇧+⇧+ S T"
(is "?A ∧ ?I ⟷ ?B")
proof
assume "?A ∧ ?I"
then have ?A and ?I by blast+
then show ?B
apply induction
apply (simp add: tranclp.r_into_trancl)
by (metis (no_types, lifting) cdcl⇩N⇩O⇩T_NOT_all_inv tranclp.simps tranclp_into_rtranclp)
next
assume ?B
then have "?A" by induction auto
moreover have ?I using ‹?B› tranclpD by fastforce
ultimately show "?A ∧ ?I" by blast
qed
lemma wf_tranclp_cdcl⇩N⇩O⇩T_no_learn_and_forget_infinite_chain:
assumes
no_infinite_lf: "⋀f j. ¬ (∀i≥j. learn_or_forget (f i) (f (Suc i)))"
shows "wf {(T, S). cdcl⇩N⇩O⇩T⇧+⇧+ S T ∧ cdcl⇩N⇩O⇩T_NOT_all_inv A S}"
using wf_trancl[OF wf_cdcl⇩N⇩O⇩T_no_learn_and_forget_infinite_chain[OF no_infinite_lf]]
apply (rule wf_subset)
by (auto simp: trancl_set_tranclp inv_and_tranclp_cdcl_⇩N⇩O⇩T_tranclp_cdcl⇩N⇩O⇩T_and_inv)
lemma cdcl⇩N⇩O⇩T_final_state:
assumes
n_s: "no_step cdcl⇩N⇩O⇩T S" and
inv: "cdcl⇩N⇩O⇩T_NOT_all_inv A S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows "unsatisfiable (set_mset (clauses S))
∨ (trail S ⊨asm clauses S ∧ satisfiable (set_mset (clauses S)))"
proof -
have n_s': "no_step dpll_bj S"
using n_s by (auto simp: cdcl⇩N⇩O⇩T.simps)
show ?thesis
apply (rule dpll_backjump_final_state[of S A])
using inv decomp n_s' unfolding cdcl⇩N⇩O⇩T_NOT_all_inv_def by auto
qed
lemma full_cdcl⇩N⇩O⇩T_final_state:
assumes
full: "full cdcl⇩N⇩O⇩T S T" and
inv: "cdcl⇩N⇩O⇩T_NOT_all_inv A S" and
n_d: "no_dup (trail S)" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows "unsatisfiable (set_mset (clauses T))
∨ (trail T ⊨asm clauses T ∧ satisfiable (set_mset (clauses T)))"
proof -
have st: "cdcl⇩N⇩O⇩T⇧*⇧* S T" and n_s: "no_step cdcl⇩N⇩O⇩T T"
using full unfolding full_def by blast+
have n_s': "cdcl⇩N⇩O⇩T_NOT_all_inv A T"
using cdcl⇩N⇩O⇩T_NOT_all_inv inv st by blast
moreover have "all_decomposition_implies_m (clauses T) (get_all_decided_decomposition (trail T))"
using cdcl⇩N⇩O⇩T_NOT_all_inv_def decomp inv rtranclp_cdcl⇩N⇩O⇩T_all_decomposition_implies st by auto
ultimately show ?thesis
using cdcl⇩N⇩O⇩T_final_state n_s by blast
qed
end ― ‹end of ‹conflict_driven_clause_learning››
subsection ‹Termination›
subsubsection ‹Restricting learn and forget›
locale conflict_driven_clause_learning_learning_before_backjump_only_distinct_learnt =
conflict_driven_clause_learning trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv backjump_conds
"λC S. distinct_mset C ∧ ¬tautology C ∧ learn_restrictions C S ∧
(∃F K d F' C' L. trail S = F' @ Decided K () # F ∧ C = C' + {#L#} ∧ F ⊨as CNot C'
∧ C' + {#L#} ∉# clauses S)"
"λC S. ¬(∃F' F K d L. trail S = F' @ Decided K () # F ∧ F ⊨as CNot (C - {#L#}))
∧ forget_restrictions C S"
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
inv :: "'st ⇒ bool" and
backjump_conds :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool" and
learn_restrictions forget_restrictions :: "'v clause ⇒ 'st ⇒ bool"
begin
lemma cdcl⇩N⇩O⇩T_learn_all_induct[consumes 1, case_names dpll_bj learn forget⇩N⇩O⇩T]:
fixes S T :: "'st"
assumes "cdcl⇩N⇩O⇩T S T" and
dpll: "⋀T. dpll_bj S T ⟹ P S T" and
learning:
"⋀C F K F' C' L T. clauses S ⊨pm C
⟹ atms_of C ⊆ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S))
⟹ distinct_mset C ⟹ ¬ tautology C ⟹ learn_restrictions C S
⟹ trail S = F' @ Decided K () # F ⟹ C = C' + {#L#} ⟹ F ⊨as CNot C'
⟹ C' + {#L#} ∉# clauses S ⟹ T ∼ add_cls⇩N⇩O⇩T C S
⟹ P S T" and
forgetting: "⋀C T. clauses S - replicate_mset (count (clauses S) C) C ⊨pm C
⟹ C ∈# clauses S
⟹ ¬(∃F' F K L. trail S = F' @ Decided K () # F ∧ F ⊨as CNot (C - {#L#}))
⟹ T ∼ remove_cls⇩N⇩O⇩T C S
⟹ forget_restrictions C S ⟹ P S T"
shows "P S T"
using assms(1)
apply (induction rule: cdcl⇩N⇩O⇩T.induct)
apply (auto dest: assms(2) simp add: learn_ops_axioms)[]
apply (auto elim!: learn_ops.learn.cases[OF learn_ops_axioms] dest: assms(3))[]
apply (auto elim!: forget_ops.forget⇩N⇩O⇩T.cases[OF forget_ops_axioms] dest!: assms(4))
done
lemma rtranclp_cdcl⇩N⇩O⇩T_inv:
"cdcl⇩N⇩O⇩T⇧*⇧* S T ⟹ inv S ⟹ inv T"
apply (induction rule: rtranclp_induct)
apply simp
using cdcl⇩N⇩O⇩T_inv unfolding conflict_driven_clause_learning_def
conflict_driven_clause_learning_axioms_def by blast
lemma learn_always_simple_clauses:
assumes
learn: "learn S T" and
n_d: "no_dup (trail S)"
shows "set_mset (clauses T - clauses S)
⊆ simple_clss (atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S))"
proof
fix C assume C: "C ∈ set_mset (clauses T - clauses S)"
have "distinct_mset C" "¬tautology C" using learn C n_d by (elim learn⇩N⇩O⇩TE; auto)+
then have "C ∈ simple_clss (atms_of C)"
using distinct_mset_not_tautology_implies_in_simple_clss by blast
moreover have "atms_of C ⊆ atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S)"
using learn C n_d by (elim learn⇩N⇩O⇩TE) (auto simp: atms_of_ms_def atms_of_def image_Un
true_annots_CNot_all_atms_defined)
moreover have "finite (atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S))"
by auto
ultimately show "C ∈ simple_clss (atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S))"
using simple_clss_mono by (metis (no_types) insert_subset mk_disjoint_insert)
qed
definition "conflicting_bj_clss S ≡
{C+{#L#}|C L. C+{#L#} ∈# clauses S ∧ distinct_mset (C+{#L#}) ∧ ¬tautology (C+{#L#})
∧ (∃F' K F. trail S = F' @ Decided K () # F ∧ F ⊨as CNot C)}"
lemma conflicting_bj_clss_remove_cls⇩N⇩O⇩T[simp]:
"conflicting_bj_clss (remove_cls⇩N⇩O⇩T C S) = conflicting_bj_clss S - {C}"
unfolding conflicting_bj_clss_def by fastforce
lemma conflicting_bj_clss_add_cls⇩N⇩O⇩T_state_eq:
"T ∼ add_cls⇩N⇩O⇩T C' S ⟹ no_dup (trail S) ⟹ conflicting_bj_clss T
= conflicting_bj_clss S
∪ (if ∃C L. C' = C +{#L#} ∧ distinct_mset (C+{#L#}) ∧ ¬tautology (C+{#L#})
∧ (∃F' K d F. trail S = F' @ Decided K () # F ∧ F ⊨as CNot C)
then {C'} else {})"
unfolding conflicting_bj_clss_def by auto metis+
lemma conflicting_bj_clss_add_cls⇩N⇩O⇩T:
" no_dup (trail S) ⟹
conflicting_bj_clss (add_cls⇩N⇩O⇩T C' S)
= conflicting_bj_clss S
∪ (if ∃C L. C' = C +{#L#}∧ distinct_mset (C+{#L#}) ∧ ¬tautology (C+{#L#})
∧ (∃F' K d F. trail S = F' @ Decided K () # F ∧ F ⊨as CNot C)
then {C'} else {})"
using conflicting_bj_clss_add_cls⇩N⇩O⇩T_state_eq by auto
lemma conflicting_bj_clss_incl_clauses:
"conflicting_bj_clss S ⊆ set_mset (clauses S)"
unfolding conflicting_bj_clss_def by auto
lemma finite_conflicting_bj_clss[simp]:
"finite (conflicting_bj_clss S)"
using conflicting_bj_clss_incl_clauses[of S] rev_finite_subset by blast
lemma learn_conflicting_increasing:
"no_dup (trail S) ⟹ learn S T ⟹ conflicting_bj_clss S ⊆ conflicting_bj_clss T"
apply (elim learn⇩N⇩O⇩TE)
by (subst conflicting_bj_clss_add_cls⇩N⇩O⇩T_state_eq[of T]) auto
abbreviation "conflicting_bj_clss_yet b S ≡
3 ^ b - card (conflicting_bj_clss S)"
abbreviation μ⇩L :: "nat ⇒ 'st ⇒ nat × nat" where
"μ⇩L b S ≡ (conflicting_bj_clss_yet b S, card (set_mset (clauses S)))"
lemma do_not_forget_before_backtrack_rule_clause_learned_clause_untouched:
assumes "forget⇩N⇩O⇩T S T"
shows "conflicting_bj_clss S = conflicting_bj_clss T"
using assms apply induction
unfolding conflicting_bj_clss_def
by (metis (no_types, lifting) Diff_insert_absorb Set.set_insert clauses_remove_cls⇩N⇩O⇩T
diff_union_cancelR insert_iff mem_set_mset_iff order_refl set_mset_minus_replicate_mset(1)
state_eq⇩N⇩O⇩T_clauses state_eq⇩N⇩O⇩T_trail trail_remove_cls⇩N⇩O⇩T)
lemma forget_μ⇩L_decrease:
assumes forget⇩N⇩O⇩T: "forget⇩N⇩O⇩T S T"
shows "(μ⇩L b T, μ⇩L b S) ∈ less_than <*lex*> less_than"
proof -
have "card (set_mset (clauses T)) < card (set_mset (clauses S))"
using forget⇩N⇩O⇩T apply induction
by (metis card_Diff1_less clauses_remove_cls⇩N⇩O⇩T finite_set_mset mem_set_mset_iff order_refl
set_mset_minus_replicate_mset(1) state_eq⇩N⇩O⇩T_clauses)
then show ?thesis
unfolding do_not_forget_before_backtrack_rule_clause_learned_clause_untouched[OF forget⇩N⇩O⇩T]
by auto
qed
lemma set_condition_or_split:
"{a. (a = b ∨ Q a) ∧ S a} = (if S b then {b} else {}) ∪ {a. Q a ∧ S a}"
by auto
lemma set_insert_neq:
"A ≠ insert a A ⟷ a ∉ A"
by auto
lemma learn_μ⇩L_decrease:
assumes learnST: "learn S T" and n_d: "no_dup (trail S)" and
A: "atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S) ⊆ A" and
fin_A: "finite A"
shows "(μ⇩L (card A) T, μ⇩L (card A) S) ∈ less_than <*lex*> less_than"
proof -
have [simp]: "(atms_of_msu (clauses T) ∪ atm_of ` lits_of (trail T))
= (atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S))"
using learnST n_d by (elim learn⇩N⇩O⇩TE) auto
then have "card (atms_of_msu (clauses T) ∪ atm_of ` lits_of (trail T))
= card (atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S))"
by (auto intro!: card_mono)
then have 3: "(3::nat) ^ card (atms_of_msu (clauses T) ∪ atm_of ` lits_of (trail T))
= 3 ^ card (atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S))"
by (auto intro: power_mono)
moreover have "conflicting_bj_clss S ⊆ conflicting_bj_clss T"
using learnST n_d by (simp add: learn_conflicting_increasing)
moreover have "conflicting_bj_clss S ≠ conflicting_bj_clss T"
using learnST
proof (elim learn⇩N⇩O⇩TE, goal_cases)
case (1 C) note clss_S = this(1) and atms_C = this(2) and inv = this(3) and T = this(4)
then obtain F K F' C' L where
tr_S: "trail S = F' @ Decided K () # F" and
C: "C = C' + {#L#}" and
F: "F ⊨as CNot C'" and
C_S:"C' + {#L#} ∉# clauses S"
by blast
moreover have "distinct_mset C" "¬ tautology C" using inv by blast+
ultimately have "C' + {#L#} ∈ conflicting_bj_clss T"
using T n_d unfolding conflicting_bj_clss_def by fastforce
moreover have "C' + {#L#} ∉ conflicting_bj_clss S"
using C_S unfolding conflicting_bj_clss_def by auto
ultimately show ?case by blast
qed
moreover have fin_T: "finite (conflicting_bj_clss T)"
using learnST by induction (auto simp add: conflicting_bj_clss_add_cls⇩N⇩O⇩T )
ultimately have "card (conflicting_bj_clss T) ≥ card (conflicting_bj_clss S)"
using card_mono by blast
moreover
have fin': "finite (atms_of_msu (clauses T) ∪ atm_of ` lits_of (trail T))"
by auto
have 1:"atms_of_ms (conflicting_bj_clss T) ⊆ atms_of_msu (clauses T)"
unfolding conflicting_bj_clss_def atms_of_ms_def by auto
have 2: "⋀x. x∈ conflicting_bj_clss T ⟹ ¬ tautology x ∧ distinct_mset x"
unfolding conflicting_bj_clss_def by auto
have T: "conflicting_bj_clss T
⊆ simple_clss (atms_of_msu (clauses T) ∪ atm_of ` lits_of (trail T))"
by standard (meson "1" "2" fin' ‹finite (conflicting_bj_clss T)› simple_clss_mono
distinct_mset_set_def simplified_in_simple_clss subsetCE sup.coboundedI1)
moreover
then have #: "3 ^ card (atms_of_msu (clauses T) ∪ atm_of ` lits_of (trail T))
≥ card (conflicting_bj_clss T)"
by (meson Nat.le_trans simple_clss_card simple_clss_finite card_mono fin')
have "atms_of_msu (clauses T) ∪ atm_of ` lits_of (trail T) ⊆ A"
using learn⇩N⇩O⇩TE[OF learnST] A by simp
then have "3 ^ (card A) ≥ card (conflicting_bj_clss T)"
using # fin_A by (meson simple_clss_card simple_clss_finite
simple_clss_mono calculation(2) card_mono dual_order.trans)
ultimately show ?thesis
using psubset_card_mono[OF fin_T ]
unfolding less_than_iff lex_prod_def by clarify
(meson ‹conflicting_bj_clss S ≠ conflicting_bj_clss T›
‹conflicting_bj_clss S ⊆ conflicting_bj_clss T›
diff_less_mono2 le_less_trans not_le psubsetI)
qed
text ‹We have to assume the following:
▪ @{term "inv S"}: the invariant holds in the inital state.
▪ @{term A} is a (finite @{term "finite A"}) superset of the literals in the trail
@{term "atm_of ` lits_of (trail S) ⊆ atms_of_ms A"}
and in the clauses @{term "atms_of_msu (clauses S) ⊆ atms_of_ms A"}. This can the the set of all
the literals in the starting set of clauses.
▪ @{term "no_dup (trail S)"}: no duplicate in the trail. This is invariant along the path.›
definition μ⇩C⇩D⇩C⇩L where
"μ⇩C⇩D⇩C⇩L A T ≡ ((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))
- μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T),
conflicting_bj_clss_yet (card (atms_of_ms A)) T, card (set_mset (clauses T)))"
lemma cdcl⇩N⇩O⇩T_decreasing_measure:
assumes
"cdcl⇩N⇩O⇩T S T" and
inv: "inv S" and
atm_clss: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atm_lits: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
fin_A: "finite A"
shows "(μ⇩C⇩D⇩C⇩L A T, μ⇩C⇩D⇩C⇩L A S)
∈ less_than <*lex*> (less_than <*lex*> less_than)"
using assms(1)
proof induction
case (c_dpll_bj T)
from dpll_bj_trail_mes_decreasing_prop[OF this(1) inv atm_clss atm_lits n_d fin_A]
show ?case unfolding μ⇩C⇩D⇩C⇩L_def
by (meson in_lex_prod less_than_iff)
next
case (c_learn T) note learn = this(1)
then have S: "trail S = trail T"
using inv atm_clss atm_lits n_d fin_A
by (elim learn⇩N⇩O⇩TE) auto
show ?case
using learn_μ⇩L_decrease[OF learn _ ] atm_clss atm_lits fin_A n_d unfolding S μ⇩C⇩D⇩C⇩L_def by auto
next
case (c_forget⇩N⇩O⇩T T) note forget⇩N⇩O⇩T = this(1)
have "trail S = trail T" using forget⇩N⇩O⇩T by induction auto
then show ?case
using forget_μ⇩L_decrease[OF forget⇩N⇩O⇩T] unfolding μ⇩C⇩D⇩C⇩L_def by auto
qed
lemma wf_cdcl⇩N⇩O⇩T_restricted_learning:
assumes "finite A"
shows "wf {(T, S).
(atms_of_msu (clauses S) ⊆ atms_of_ms A ∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A
∧ no_dup (trail S)
∧ inv S)
∧ cdcl⇩N⇩O⇩T S T }"
by (rule wf_wf_if_measure'[of "less_than <*lex*> (less_than <*lex*> less_than)"])
(auto intro: cdcl⇩N⇩O⇩T_decreasing_measure[OF _ _ _ _ _ assms])
definition μ⇩C' :: "'v literal multiset set ⇒ 'st ⇒ nat" where
"μ⇩C' A T ≡ μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)"
definition μ⇩C⇩D⇩C⇩L' :: "'v literal multiset set ⇒ 'st ⇒ nat" where
"μ⇩C⇩D⇩C⇩L' A T ≡
((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μ⇩C' A T) * (1+ 3^card (atms_of_ms A)) * 2
+ conflicting_bj_clss_yet (card (atms_of_ms A)) T * 2
+ card (set_mset (clauses T))"
lemma cdcl⇩N⇩O⇩T_decreasing_measure':
assumes
"cdcl⇩N⇩O⇩T S T" and
inv: "inv S" and
atms_clss: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atms_trail: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
fin_A: "finite A"
shows "μ⇩C⇩D⇩C⇩L' A T < μ⇩C⇩D⇩C⇩L' A S"
using assms(1)
proof (induction rule: cdcl⇩N⇩O⇩T_learn_all_induct)
case (dpll_bj T)
then have "(2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μ⇩C' A T
< (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μ⇩C' A S"
using dpll_bj_trail_mes_decreasing_prop fin_A inv n_d atms_clss atms_trail
unfolding μ⇩C'_def by blast
then have XX: "((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μ⇩C' A T) + 1
≤ (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μ⇩C' A S"
by auto
from mult_le_mono1[OF this, of "(1 + 3 ^ card (atms_of_ms A))"]
have "((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A T) *
(1 + 3 ^ card (atms_of_ms A)) + (1 + 3 ^ card (atms_of_ms A))
≤ ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A S)
* (1 + 3 ^ card (atms_of_ms A))"
unfolding Nat.add_mult_distrib
by presburger
moreover
have cl_T_S: "clauses T = clauses S"
using dpll_bj.hyps inv dpll_bj_clauses by auto
have "conflicting_bj_clss_yet (card (atms_of_ms A)) S < 1+ 3 ^ card (atms_of_ms A)"
by simp
ultimately have "((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A T)
* (1 + 3 ^ card (atms_of_ms A)) + conflicting_bj_clss_yet (card (atms_of_ms A)) T
< ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A S) *(1 + 3 ^ card (atms_of_ms A))"
by linarith
then have "((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A T)
* (1 + 3 ^ card (atms_of_ms A))
+ conflicting_bj_clss_yet (card (atms_of_ms A)) T
< ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A S)
* (1 + 3 ^ card (atms_of_ms A))
+ conflicting_bj_clss_yet (card (atms_of_ms A)) S"
by linarith
then have "((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A T)
* (1 + 3 ^ card (atms_of_ms A)) * 2
+ conflicting_bj_clss_yet (card (atms_of_ms A)) T * 2
< ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A S)
* (1 + 3 ^ card (atms_of_ms A)) * 2
+ conflicting_bj_clss_yet (card (atms_of_ms A)) S * 2"
by linarith
then show ?case unfolding μ⇩C⇩D⇩C⇩L'_def cl_T_S by presburger
next
case (learn C F' K F C' L T) note clss_S_C = this(1) and atms_C = this(2) and dist = this(3)
and tauto = this(4) and learn_restr = this(5) and tr_S = this(6) and C' = this(7) and
F_C = this(8) and C_new = this(9) and T =this(10)
have "insert C (conflicting_bj_clss S) ⊆ simple_clss (atms_of_ms A)"
proof -
have "C ∈ simple_clss (atms_of_ms A)"
by (metis (no_types, hide_lams) Un_subset_iff atms_of_ms_finite simple_clss_mono
contra_subsetD dist distinct_mset_not_tautology_implies_in_simple_clss
dual_order.trans fin_A atms_C atms_clss atms_trail tauto)
moreover have "conflicting_bj_clss S ⊆ simple_clss (atms_of_ms A)"
unfolding conflicting_bj_clss_def
proof
fix x :: "'v literal multiset"
assume "x ∈ {C + {#L#} |C L. C + {#L#} ∈# clauses S
∧ distinct_mset (C + {#L#}) ∧ ¬ tautology (C + {#L#})
∧ (∃F' K F. trail S = F' @ Decided K () # F ∧ F ⊨as CNot C)}"
then have "∃m l. x = m + {#l#} ∧ m + {#l#} ∈# clauses S
∧ distinct_mset (m + {#l#}) ∧ ¬ tautology (m + {#l#})
∧ (∃ms l msa. trail S = ms @ Decided l () # msa ∧ msa ⊨as CNot m)"
by blast
then show "x ∈ simple_clss (atms_of_ms A)"
by (meson atms_clss atms_of_atms_of_ms_mono atms_of_ms_finite simple_clss_mono
distinct_mset_not_tautology_implies_in_simple_clss fin_A finite_subset
mem_set_mset_iff set_rev_mp)
qed
ultimately show ?thesis
by auto
qed
then have "card (insert C (conflicting_bj_clss S)) ≤ 3 ^ (card (atms_of_ms A))"
by (meson Nat.le_trans atms_of_ms_finite simple_clss_card simple_clss_finite
card_mono fin_A)
moreover have [simp]: "card (insert C (conflicting_bj_clss S))
= Suc (card ((conflicting_bj_clss S)))"
by (metis (no_types) C' C_new card_insert_if conflicting_bj_clss_incl_clauses contra_subsetD
finite_conflicting_bj_clss mem_set_mset_iff)
moreover have [simp]: "conflicting_bj_clss (add_cls⇩N⇩O⇩T C S) = conflicting_bj_clss S ∪ {C}"
using dist tauto F_C n_d by (subst conflicting_bj_clss_add_cls⇩N⇩O⇩T)
(force simp add: ac_simps C' tr_S)+
ultimately have [simp]: "conflicting_bj_clss_yet (card (atms_of_ms A)) S
= Suc (conflicting_bj_clss_yet (card (atms_of_ms A)) (add_cls⇩N⇩O⇩T C S))"
by simp
have 1: "clauses T = clauses (add_cls⇩N⇩O⇩T C S)" using T by auto
have 2: "conflicting_bj_clss_yet (card (atms_of_ms A)) T
= conflicting_bj_clss_yet (card (atms_of_ms A)) (add_cls⇩N⇩O⇩T C S)"
using T unfolding conflicting_bj_clss_def by auto
have 3: "μ⇩C' A T = μ⇩C' A (add_cls⇩N⇩O⇩T C S)"
using T unfolding μ⇩C'_def by auto
have "((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A (add_cls⇩N⇩O⇩T C S))
* (1 + 3 ^ card (atms_of_ms A)) * 2
= ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A S)
* (1 + 3 ^ card (atms_of_ms A)) * 2"
using n_d unfolding μ⇩C'_def by auto
moreover
have "conflicting_bj_clss_yet (card (atms_of_ms A)) (add_cls⇩N⇩O⇩T C S)
* 2
+ card (set_mset (clauses (add_cls⇩N⇩O⇩T C S)))
< conflicting_bj_clss_yet (card (atms_of_ms A)) S * 2
+ card (set_mset (clauses S))"
by (simp add: C' C_new n_d)
ultimately show ?case unfolding μ⇩C⇩D⇩C⇩L'_def 1 2 3 by presburger
next
case (forget⇩N⇩O⇩T C T) note T = this(4)
have [simp]: "μ⇩C' A (remove_cls⇩N⇩O⇩T C S) = μ⇩C' A S"
unfolding μ⇩C'_def by auto
have "forget⇩N⇩O⇩T S T"
apply (rule forget⇩N⇩O⇩T.intros) using forget⇩N⇩O⇩T by auto
then have "conflicting_bj_clss T = conflicting_bj_clss S"
using do_not_forget_before_backtrack_rule_clause_learned_clause_untouched by blast
moreover have "card (set_mset (clauses T)) < card (set_mset (clauses S))"
by (metis T card_Diff1_less clauses_remove_cls⇩N⇩O⇩T finite_set_mset forget⇩N⇩O⇩T.hyps(2)
mem_set_mset_iff order_refl set_mset_minus_replicate_mset(1) state_eq⇩N⇩O⇩T_clauses)
ultimately show ?case unfolding μ⇩C⇩D⇩C⇩L'_def
by (metis (no_types) T ‹μ⇩C' A (remove_cls⇩N⇩O⇩T C S) = μ⇩C' A S› add_le_cancel_left
μ⇩C'_def not_le state_eq⇩N⇩O⇩T_trail)
qed
lemma cdcl⇩N⇩O⇩T_clauses_bound:
assumes
"cdcl⇩N⇩O⇩T S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ A" and
"atm_of `(lits_of (trail S)) ⊆ A" and
n_d: "no_dup (trail S)" and
fin_A[simp]: "finite A"
shows "set_mset (clauses T) ⊆ set_mset (clauses S) ∪ simple_clss A"
using assms
proof (induction rule: cdcl⇩N⇩O⇩T_learn_all_induct)
case dpll_bj
then show ?case using dpll_bj_clauses by simp
next
case forget⇩N⇩O⇩T
then show ?case using clauses_remove_cls⇩N⇩O⇩T unfolding state_eq⇩N⇩O⇩T_def by auto
next
case (learn C F K d F' C' L) note atms_C = this(2) and dist = this(3) and tauto = this(4) and
T = this(10) and atms_clss_S = this(12) and atms_trail_S = this(13)
have "atms_of C ⊆ A"
using atms_C atms_clss_S atms_trail_S by auto
then have "simple_clss (atms_of C) ⊆ simple_clss A"
by (simp add: simple_clss_mono)
then have "C ∈ simple_clss A"
using finite dist tauto
by (auto dest: distinct_mset_not_tautology_implies_in_simple_clss)
then show ?case using T n_d by auto
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_clauses_bound:
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ A" and
"atm_of `(lits_of (trail S)) ⊆ A" and
n_d: "no_dup (trail S)" and
finite: "finite A"
shows "set_mset (clauses T) ⊆ set_mset (clauses S) ∪ simple_clss A"
using assms(1-5)
proof induction
case base
then show ?case by simp
next
case (step T U) note st = this(1) and cdcl⇩N⇩O⇩T = this(2) and IH = this(3)[OF this(4-7)] and
inv = this(4) and atms_clss_S = this(5) and atms_trail_S = this(6) and finite_cls_S = this(7)
have "inv T"
using rtranclp_cdcl⇩N⇩O⇩T_inv st inv by blast
moreover have "atms_of_msu (clauses T) ⊆ A" and "atm_of ` lits_of (trail T) ⊆ A"
using rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound[OF st] inv atms_clss_S atms_trail_S n_d by blast+
moreover have "no_dup (trail T)"
using rtranclp_cdcl⇩N⇩O⇩T_no_dup[OF st ‹inv S› n_d] by simp
ultimately have "set_mset (clauses U) ⊆ set_mset (clauses T) ∪ simple_clss A"
using cdcl⇩N⇩O⇩T finite n_d by (auto simp: cdcl⇩N⇩O⇩T_clauses_bound)
then show ?case using IH by auto
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_card_clauses_bound:
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ A" and
"atm_of `(lits_of (trail S)) ⊆ A" and
n_d: "no_dup (trail S)" and
finite: "finite A"
shows "card (set_mset (clauses T)) ≤ card (set_mset (clauses S)) + 3 ^ (card A)"
using rtranclp_cdcl⇩N⇩O⇩T_clauses_bound[OF assms] finite by (meson Nat.le_trans
simple_clss_card simple_clss_finite card_Un_le card_mono finite_UnI
finite_set_mset nat_add_left_cancel_le)
lemma rtranclp_cdcl⇩N⇩O⇩T_card_clauses_bound':
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ A" and
"atm_of `(lits_of (trail S)) ⊆ A" and
n_d: "no_dup (trail S)" and
finite: "finite A"
shows "card {C|C. C ∈# clauses T ∧ (tautology C ∨ ¬distinct_mset C)}
≤ card {C|C. C∈# clauses S ∧ (tautology C ∨ ¬distinct_mset C)} + 3 ^ (card A)"
(is "card ?T ≤ card ?S + _")
using rtranclp_cdcl⇩N⇩O⇩T_clauses_bound[OF assms] finite
proof -
have "?T ⊆ ?S ∪ simple_clss A"
using rtranclp_cdcl⇩N⇩O⇩T_clauses_bound[OF assms] by force
then have "card ?T ≤ card (?S ∪ simple_clss A)"
using finite by (simp add: assms(5) simple_clss_finite card_mono)
then show ?thesis
by (meson le_trans simple_clss_card card_Un_le local.finite nat_add_left_cancel_le)
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_card_simple_clauses_bound:
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ A" and
"atm_of `(lits_of (trail S)) ⊆ A" and
n_d: "no_dup (trail S)" and
finite: "finite A"
shows "card (set_mset (clauses T))
≤ card {C. C ∈# clauses S ∧ (tautology C ∨ ¬distinct_mset C)} + 3 ^ (card A)"
(is "card ?T ≤ card ?S + _")
using rtranclp_cdcl⇩N⇩O⇩T_clauses_bound[OF assms] finite
proof -
have "⋀x. x ∈# clauses T ⟹¬ tautology x ⟹ distinct_mset x ⟹ x ∈ simple_clss A"
using rtranclp_cdcl⇩N⇩O⇩T_clauses_bound[OF assms] by (metis (no_types, hide_lams) Un_iff assms(3)
atms_of_atms_of_ms_mono simple_clss_mono contra_subsetD
distinct_mset_not_tautology_implies_in_simple_clss local.finite mem_set_mset_iff
subset_trans)
then have "set_mset (clauses T) ⊆ ?S ∪ simple_clss A"
using rtranclp_cdcl⇩N⇩O⇩T_clauses_bound[OF assms] by auto
then have "card(set_mset (clauses T)) ≤ card (?S ∪ simple_clss A)"
using finite by (simp add: assms(5) simple_clss_finite card_mono)
then show ?thesis
by (meson le_trans simple_clss_card card_Un_le local.finite nat_add_left_cancel_le)
qed
definition μ⇩C⇩D⇩C⇩L'_bound :: "'v literal multiset set ⇒ 'st ⇒ nat" where
"μ⇩C⇩D⇩C⇩L'_bound A S =
((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))) * (1 + 3 ^ card (atms_of_ms A)) * 2
+ 2*3 ^ (card (atms_of_ms A))
+ card {C. C ∈# clauses S ∧ (tautology C ∨ ¬distinct_mset C)} + 3 ^ (card (atms_of_ms A))"
lemma μ⇩C⇩D⇩C⇩L'_bound_reduce_trail_to⇩N⇩O⇩T[simp]:
"μ⇩C⇩D⇩C⇩L'_bound A (reduce_trail_to⇩N⇩O⇩T M S) = μ⇩C⇩D⇩C⇩L'_bound A S"
unfolding μ⇩C⇩D⇩C⇩L'_bound_def by auto
lemma rtranclp_cdcl⇩N⇩O⇩T_μ⇩C⇩D⇩C⇩L'_bound_reduce_trail_to⇩N⇩O⇩T:
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ atms_of_ms A" and
"atm_of `(lits_of (trail S)) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
finite: "finite (atms_of_ms A)" and
U: "U ∼ reduce_trail_to⇩N⇩O⇩T M T"
shows "μ⇩C⇩D⇩C⇩L' A U ≤ μ⇩C⇩D⇩C⇩L'_bound A S"
proof -
have " ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A U)
≤ (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))"
by auto
then have "((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A U)
* (1 + 3 ^ card (atms_of_ms A)) * 2
≤ (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) * (1 + 3 ^ card (atms_of_ms A)) * 2"
using mult_le_mono1 by blast
moreover
have "conflicting_bj_clss_yet (card (atms_of_ms A)) T * 2 ≤ 2 * 3 ^ card (atms_of_ms A)"
by linarith
moreover have "card (set_mset (clauses U))
≤ card {C. C ∈# clauses S ∧ (tautology C ∨ ¬distinct_mset C)} + 3 ^ card (atms_of_ms A)"
using rtranclp_cdcl⇩N⇩O⇩T_card_simple_clauses_bound[OF assms(1-6)] U by auto
ultimately show ?thesis
unfolding μ⇩C⇩D⇩C⇩L'_def μ⇩C⇩D⇩C⇩L'_bound_def by linarith
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_μ⇩C⇩D⇩C⇩L'_bound:
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ atms_of_ms A" and
"atm_of `(lits_of (trail S)) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
finite: "finite (atms_of_ms A)"
shows "μ⇩C⇩D⇩C⇩L' A T ≤ μ⇩C⇩D⇩C⇩L'_bound A S"
proof -
have "μ⇩C⇩D⇩C⇩L' A (reduce_trail_to⇩N⇩O⇩T (trail T) T) = μ⇩C⇩D⇩C⇩L' A T"
unfolding μ⇩C⇩D⇩C⇩L'_def μ⇩C'_def conflicting_bj_clss_def by auto
then show ?thesis using rtranclp_cdcl⇩N⇩O⇩T_μ⇩C⇩D⇩C⇩L'_bound_reduce_trail_to⇩N⇩O⇩T[OF assms, of _ "trail T"]
state_eq⇩N⇩O⇩T_ref by fastforce
qed
lemma rtranclp_μ⇩C⇩D⇩C⇩L'_bound_decreasing:
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ atms_of_ms A" and
"atm_of `(lits_of (trail S)) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
finite[simp]: "finite (atms_of_ms A)"
shows "μ⇩C⇩D⇩C⇩L'_bound A T ≤ μ⇩C⇩D⇩C⇩L'_bound A S"
proof -
have "{C. C ∈# clauses T ∧ (tautology C ∨ ¬ distinct_mset C)}
⊆ {C. C ∈# clauses S ∧ (tautology C ∨ ¬ distinct_mset C)}" (is "?T ⊆ ?S")
proof (rule Set.subsetI)
fix C assume "C ∈ ?T"
then have C_T: "C ∈# clauses T" and t_d: "tautology C ∨ ¬ distinct_mset C"
by auto
then have "C ∉ simple_clss (atms_of_ms A)"
by (auto dest: simple_clssE)
then show "C ∈ ?S"
using C_T rtranclp_cdcl⇩N⇩O⇩T_clauses_bound[OF assms] t_d by force
qed
then have "card {C. C ∈# clauses T ∧ (tautology C ∨ ¬ distinct_mset C)} ≤
card {C. C ∈# clauses S ∧ (tautology C ∨ ¬ distinct_mset C)}"
by (simp add: card_mono)
then show ?thesis
unfolding μ⇩C⇩D⇩C⇩L'_bound_def by auto
qed
end ― ‹end of ‹conflict_driven_clause_learning_learning_before_backjump_only_distinct_learnt››
subsection ‹CDCL with restarts›
subsubsection‹Definition›
locale restart_ops =
fixes
cdcl⇩N⇩O⇩T :: "'st ⇒ 'st ⇒ bool" and
restart :: "'st ⇒ 'st ⇒ bool"
begin
inductive cdcl⇩N⇩O⇩T_raw_restart :: "'st ⇒ 'st ⇒ bool" where
"cdcl⇩N⇩O⇩T S T ⟹ cdcl⇩N⇩O⇩T_raw_restart S T" |
"restart S T ⟹ cdcl⇩N⇩O⇩T_raw_restart S T"
end
locale conflict_driven_clause_learning_with_restarts =
conflict_driven_clause_learning trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv backjump_conds learn_cond forget_cond
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
inv :: "'st ⇒ bool" and
backjump_conds :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool" and
learn_cond forget_cond :: "'v clause ⇒ 'st ⇒ bool"
begin
lemma cdcl⇩N⇩O⇩T_iff_cdcl⇩N⇩O⇩T_raw_restart_no_restarts:
"cdcl⇩N⇩O⇩T S T ⟷ restart_ops.cdcl⇩N⇩O⇩T_raw_restart cdcl⇩N⇩O⇩T (λ_ _. False) S T"
(is "?C S T ⟷ ?R S T")
proof
fix S T
assume "?C S T"
then show "?R S T" by (simp add: restart_ops.cdcl⇩N⇩O⇩T_raw_restart.intros(1))
next
fix S T
assume "?R S T"
then show "?C S T"
apply (cases rule: restart_ops.cdcl⇩N⇩O⇩T_raw_restart.cases)
using ‹?R S T› by fast+
qed
lemma cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_raw_restart:
"cdcl⇩N⇩O⇩T S T ⟹ restart_ops.cdcl⇩N⇩O⇩T_raw_restart cdcl⇩N⇩O⇩T restart S T"
by (simp add: restart_ops.cdcl⇩N⇩O⇩T_raw_restart.intros(1))
end
subsubsection ‹Increasing restarts›
text ‹To add restarts we needs some assumptions on the predicate (called @{term cdcl⇩N⇩O⇩T} here):
▪ a function @{term f} that is strictly monotonic. The first step is actually only used as a
restart to clean the state (e.g. to ensure that the trail is empty). Then we assume that
@{term "f n ≥ 1"} for @{term "n ≥ 1"}: it means that between two consecutive
restarts, at least one step will be done. This is necessary to avoid sequence. like: full --
restart -- full -- ...
▪ a measure @{term "μ"}: it should decrease under the assumptions @{term bound_inv}, whenever a
@{term cdcl⇩N⇩O⇩T} or a @{term restart} is done. A parameter is given to @{term μ}: for conflict-
driven clause learning, it is an upper-bound of the clauses. We are assuming that such a bound
can be found after a restart whenever the invariant holds.
▪ we also assume that the measure decrease after any @{term cdcl⇩N⇩O⇩T} step.
▪ an invariant on the states @{term cdcl⇩N⇩O⇩T_inv} that also holds after restarts.
▪ it is ∗‹not required› that the measure decrease with respect to restarts, but the measure has to
be bound by some function @{term μ_bound} taking the same parameter as @{term μ} and the initial
state of the considered @{term cdcl⇩N⇩O⇩T} chain.›
locale cdcl⇩N⇩O⇩T_increasing_restarts_ops =
restart_ops cdcl⇩N⇩O⇩T restart for
restart :: "'st ⇒ 'st ⇒ bool" and
cdcl⇩N⇩O⇩T :: "'st ⇒ 'st ⇒ bool" +
fixes
f :: "nat ⇒ nat" and
bound_inv :: "'bound ⇒ 'st ⇒ bool" and
μ :: "'bound ⇒ 'st ⇒ nat" and
cdcl⇩N⇩O⇩T_inv :: "'st ⇒ bool" and
μ_bound :: "'bound ⇒ 'st ⇒ nat"
assumes
f: "unbounded f" and
f_ge_1:"⋀n. n≥1 ⟹ f n ≠ 0" and
bound_inv: "⋀A S T. cdcl⇩N⇩O⇩T_inv S ⟹ bound_inv A S ⟹ cdcl⇩N⇩O⇩T S T ⟹ bound_inv A T" and
cdcl⇩N⇩O⇩T_measure: "⋀A S T. cdcl⇩N⇩O⇩T_inv S ⟹ bound_inv A S ⟹ cdcl⇩N⇩O⇩T S T ⟹ μ A T < μ A S" and
measure_bound2: "⋀A T U. cdcl⇩N⇩O⇩T_inv T ⟹ bound_inv A T ⟹ cdcl⇩N⇩O⇩T⇧*⇧* T U
⟹ μ A U ≤ μ_bound A T" and
measure_bound4: "⋀A T U. cdcl⇩N⇩O⇩T_inv T ⟹ bound_inv A T ⟹ cdcl⇩N⇩O⇩T⇧*⇧* T U
⟹ μ_bound A U ≤ μ_bound A T" and
cdcl⇩N⇩O⇩T_restart_inv: "⋀A U V. cdcl⇩N⇩O⇩T_inv U ⟹ restart U V ⟹ bound_inv A U ⟹ bound_inv A V"
and
exists_bound: "⋀R S. cdcl⇩N⇩O⇩T_inv R ⟹ restart R S ⟹ ∃A. bound_inv A S" and
cdcl⇩N⇩O⇩T_inv: "⋀S T. cdcl⇩N⇩O⇩T_inv S ⟹ cdcl⇩N⇩O⇩T S T ⟹ cdcl⇩N⇩O⇩T_inv T" and
cdcl⇩N⇩O⇩T_inv_restart: "⋀S T. cdcl⇩N⇩O⇩T_inv S ⟹ restart S T ⟹ cdcl⇩N⇩O⇩T_inv T"
begin
lemma cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv:
assumes
"(cdcl⇩N⇩O⇩T^^n) S T" and
"cdcl⇩N⇩O⇩T_inv S"
shows "cdcl⇩N⇩O⇩T_inv T"
using assms by (induction n arbitrary: T) (auto intro:bound_inv cdcl⇩N⇩O⇩T_inv)
lemma cdcl⇩N⇩O⇩T_bound_inv:
assumes
"(cdcl⇩N⇩O⇩T^^n) S T" and
"cdcl⇩N⇩O⇩T_inv S"
"bound_inv A S"
shows "bound_inv A T"
using assms by (induction n arbitrary: T) (auto intro:bound_inv cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv)
lemma rtranclp_cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv:
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"cdcl⇩N⇩O⇩T_inv S"
shows "cdcl⇩N⇩O⇩T_inv T"
using assms by induction (auto intro: cdcl⇩N⇩O⇩T_inv)
lemma rtranclp_cdcl⇩N⇩O⇩T_bound_inv:
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"bound_inv A S" and
"cdcl⇩N⇩O⇩T_inv S"
shows "bound_inv A T"
using assms by induction (auto intro:bound_inv rtranclp_cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv)
lemma cdcl⇩N⇩O⇩T_comp_n_le:
assumes
"(cdcl⇩N⇩O⇩T^^(Suc n)) S T" and
"bound_inv A S"
"cdcl⇩N⇩O⇩T_inv S"
shows "μ A T < μ A S - n"
using assms
proof (induction n arbitrary: T)
case 0
then show ?case using cdcl⇩N⇩O⇩T_measure by auto
next
case (Suc n) note IH =this(1)[OF _ this(3) this(4)] and S_T =this(2) and b_inv = this(3) and
c_inv = this(4)
obtain U :: 'st where S_U: "(cdcl⇩N⇩O⇩T^^(Suc n)) S U" and U_T: "cdcl⇩N⇩O⇩T U T" using S_T by auto
then have "μ A U < μ A S - n" using IH[of U] by simp
moreover
have "bound_inv A U"
using S_U b_inv cdcl⇩N⇩O⇩T_bound_inv c_inv by blast
then have "μ A T < μ A U" using cdcl⇩N⇩O⇩T_measure[OF _ _ U_T] S_U c_inv cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv by auto
ultimately show ?case by linarith
qed
lemma wf_cdcl⇩N⇩O⇩T:
"wf {(T, S). cdcl⇩N⇩O⇩T S T ∧ cdcl⇩N⇩O⇩T_inv S ∧ bound_inv A S}" (is "wf ?A")
apply (rule wfP_if_measure2[of _ _ "μ A"])
using cdcl⇩N⇩O⇩T_comp_n_le[of 0 _ _ A] by auto
lemma rtranclp_cdcl⇩N⇩O⇩T_measure:
assumes
"cdcl⇩N⇩O⇩T⇧*⇧* S T" and
"bound_inv A S" and
"cdcl⇩N⇩O⇩T_inv S"
shows "μ A T ≤ μ A S"
using assms
proof (induction rule: rtranclp_induct)
case base
then show ?case by auto
next
case (step T U) note IH =this(3)[OF this(4) this(5)] and st =this(1) and cdcl⇩N⇩O⇩T= this(2) and
b_inv = this(4) and c_inv = this(5)
have "bound_inv A T"
by (meson cdcl⇩N⇩O⇩T_bound_inv rtranclp_imp_relpowp st step.prems)
moreover have "cdcl⇩N⇩O⇩T_inv T"
using c_inv rtranclp_cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv st by blast
ultimately have "μ A U < μ A T" using cdcl⇩N⇩O⇩T_measure[OF _ _ cdcl⇩N⇩O⇩T] by auto
then show ?case using IH by linarith
qed
lemma cdcl⇩N⇩O⇩T_comp_bounded:
assumes
"bound_inv A S" and "cdcl⇩N⇩O⇩T_inv S" and "m ≥ 1+μ A S"
shows "¬(cdcl⇩N⇩O⇩T ^^ m) S T"
using assms cdcl⇩N⇩O⇩T_comp_n_le[of "m-1" S T A] by fastforce
text ‹
▪ @{term "m > f n"} ensures that at least one step has been done.›
inductive cdcl⇩N⇩O⇩T_restart where
restart_step: "(cdcl⇩N⇩O⇩T^^m) S T ⟹ m ≥ f n ⟹ restart T U
⟹ cdcl⇩N⇩O⇩T_restart (S, n) (U, Suc n)" |
restart_full: "full1 cdcl⇩N⇩O⇩T S T ⟹ cdcl⇩N⇩O⇩T_restart (S, n) (T, Suc n)"
lemmas cdcl⇩N⇩O⇩T_with_restart_induct = cdcl⇩N⇩O⇩T_restart.induct[split_format(complete),
OF cdcl⇩N⇩O⇩T_increasing_restarts_ops_axioms]
lemma cdcl⇩N⇩O⇩T_restart_cdcl⇩N⇩O⇩T_raw_restart:
"cdcl⇩N⇩O⇩T_restart S T ⟹ cdcl⇩N⇩O⇩T_raw_restart⇧*⇧* (fst S) (fst T)"
proof (induction rule: cdcl⇩N⇩O⇩T_restart.induct)
case (restart_step m S T n U)
then have "cdcl⇩N⇩O⇩T⇧*⇧* S T" by (meson relpowp_imp_rtranclp)
then have "cdcl⇩N⇩O⇩T_raw_restart⇧*⇧* S T" using cdcl⇩N⇩O⇩T_raw_restart.intros(1)
rtranclp_mono[of cdcl⇩N⇩O⇩T cdcl⇩N⇩O⇩T_raw_restart] by blast
moreover have "cdcl⇩N⇩O⇩T_raw_restart T U"
using ‹restart T U› cdcl⇩N⇩O⇩T_raw_restart.intros(2) by blast
ultimately show ?case by auto
next
case (restart_full S T)
then have "cdcl⇩N⇩O⇩T⇧*⇧* S T" unfolding full1_def by auto
then show ?case using cdcl⇩N⇩O⇩T_raw_restart.intros(1)
rtranclp_mono[of cdcl⇩N⇩O⇩T cdcl⇩N⇩O⇩T_raw_restart] by auto
qed
lemma cdcl⇩N⇩O⇩T_with_restart_bound_inv:
assumes
"cdcl⇩N⇩O⇩T_restart S T" and
"bound_inv A (fst S)" and
"cdcl⇩N⇩O⇩T_inv (fst S)"
shows "bound_inv A (fst T)"
using assms apply (induction rule: cdcl⇩N⇩O⇩T_restart.induct)
prefer 2 apply (metis rtranclp_unfold fstI full1_def rtranclp_cdcl⇩N⇩O⇩T_bound_inv)
by (metis cdcl⇩N⇩O⇩T_bound_inv cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv cdcl⇩N⇩O⇩T_restart_inv fst_conv)
lemma cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv:
assumes
"cdcl⇩N⇩O⇩T_restart S T" and
"cdcl⇩N⇩O⇩T_inv (fst S)"
shows "cdcl⇩N⇩O⇩T_inv (fst T)"
using assms apply induction
apply (metis cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv cdcl⇩N⇩O⇩T_inv_restart fst_conv)
apply (metis fstI full_def full_unfold rtranclp_cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv)
done
lemma rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv:
assumes
"cdcl⇩N⇩O⇩T_restart⇧*⇧* S T" and
"cdcl⇩N⇩O⇩T_inv (fst S)"
shows "cdcl⇩N⇩O⇩T_inv (fst T)"
using assms by induction (auto intro: cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv)
lemma rtranclp_cdcl⇩N⇩O⇩T_with_restart_bound_inv:
assumes
"cdcl⇩N⇩O⇩T_restart⇧*⇧* S T" and
"cdcl⇩N⇩O⇩T_inv (fst S)" and
"bound_inv A (fst S)"
shows "bound_inv A (fst T)"
using assms apply induction
apply (simp add: cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv cdcl⇩N⇩O⇩T_with_restart_bound_inv)
using cdcl⇩N⇩O⇩T_with_restart_bound_inv rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv by blast
lemma cdcl⇩N⇩O⇩T_with_restart_increasing_number:
"cdcl⇩N⇩O⇩T_restart S T ⟹ snd T = 1 + snd S"
by (induction rule: cdcl⇩N⇩O⇩T_restart.induct) auto
end
locale cdcl⇩N⇩O⇩T_increasing_restarts =
cdcl⇩N⇩O⇩T_increasing_restarts_ops restart cdcl⇩N⇩O⇩T f bound_inv μ cdcl⇩N⇩O⇩T_inv μ_bound
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
f :: "nat ⇒ nat" and
restart :: "'st ⇒ 'st ⇒ bool" and
bound_inv :: "'bound ⇒ 'st ⇒ bool" and
μ :: "'bound ⇒ 'st ⇒ nat" and
cdcl⇩N⇩O⇩T :: "'st ⇒ 'st ⇒ bool" and
cdcl⇩N⇩O⇩T_inv :: "'st ⇒ bool" and
μ_bound :: "'bound ⇒ 'st ⇒ nat" +
assumes
measure_bound: "⋀A T V n. cdcl⇩N⇩O⇩T_inv T ⟹ bound_inv A T
⟹ cdcl⇩N⇩O⇩T_restart (T, n) (V, Suc n) ⟹ μ A V ≤ μ_bound A T" and
cdcl⇩N⇩O⇩T_raw_restart_μ_bound:
"cdcl⇩N⇩O⇩T_restart (T, a) (V, b) ⟹ cdcl⇩N⇩O⇩T_inv T ⟹ bound_inv A T
⟹ μ_bound A V ≤ μ_bound A T"
begin
lemma rtranclp_cdcl⇩N⇩O⇩T_raw_restart_μ_bound:
"cdcl⇩N⇩O⇩T_restart⇧*⇧* (T, a) (V, b) ⟹ cdcl⇩N⇩O⇩T_inv T ⟹ bound_inv A T
⟹ μ_bound A V ≤ μ_bound A T"
apply (induction rule: rtranclp_induct2)
apply simp
by (metis cdcl⇩N⇩O⇩T_raw_restart_μ_bound dual_order.trans fst_conv
rtranclp_cdcl⇩N⇩O⇩T_with_restart_bound_inv rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv)
lemma cdcl⇩N⇩O⇩T_raw_restart_measure_bound:
"cdcl⇩N⇩O⇩T_restart (T, a) (V, b) ⟹ cdcl⇩N⇩O⇩T_inv T ⟹ bound_inv A T
⟹ μ A V ≤ μ_bound A T"
apply (cases rule: cdcl⇩N⇩O⇩T_restart.cases)
apply simp
using measure_bound relpowp_imp_rtranclp apply fastforce
by (metis full_def full_unfold measure_bound2 prod.inject)
lemma rtranclp_cdcl⇩N⇩O⇩T_raw_restart_measure_bound:
"cdcl⇩N⇩O⇩T_restart⇧*⇧* (T, a) (V, b) ⟹ cdcl⇩N⇩O⇩T_inv T ⟹ bound_inv A T
⟹ μ A V ≤ μ_bound A T"
apply (induction rule: rtranclp_induct2)
apply (simp add: measure_bound2)
by (metis dual_order.trans fst_conv measure_bound2 r_into_rtranclp rtranclp.rtrancl_refl
rtranclp_cdcl⇩N⇩O⇩T_with_restart_bound_inv rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv
rtranclp_cdcl⇩N⇩O⇩T_raw_restart_μ_bound)
lemma wf_cdcl⇩N⇩O⇩T_restart:
"wf {(T, S). cdcl⇩N⇩O⇩T_restart S T ∧ cdcl⇩N⇩O⇩T_inv (fst S)}" (is "wf ?A")
proof (rule ccontr)
assume "¬ ?thesis"
then obtain g where
g: "⋀i. cdcl⇩N⇩O⇩T_restart (g i) (g (Suc i))" and
cdcl⇩N⇩O⇩T_inv_g: "⋀i. cdcl⇩N⇩O⇩T_inv (fst (g i))"
unfolding wf_iff_no_infinite_down_chain by fast
have snd_g: "⋀i. snd (g i) = i + snd (g 0)"
apply (induct_tac i)
apply simp
by (metis Suc_eq_plus1_left add.commute add.left_commute
cdcl⇩N⇩O⇩T_with_restart_increasing_number g)
then have snd_g_0: "⋀i. i > 0 ⟹ snd (g i) = i + snd (g 0)"
by blast
have unbounded_f_g: "unbounded (λi. f (snd (g i)))"
using f unfolding bounded_def by (metis add.commute f less_or_eq_imp_le snd_g
not_bounded_nat_exists_larger not_le le_iff_add)
{ fix i
have H: "⋀T Ta m. (cdcl⇩N⇩O⇩T ^^ m) T Ta ⟹ no_step cdcl⇩N⇩O⇩T T ⟹ m = 0"
apply (case_tac m) by simp (meson relpowp_E2)
have "∃ T m. (cdcl⇩N⇩O⇩T ^^ m) (fst (g i)) T ∧ m ≥ f (snd (g i))"
using g[of i] apply (cases rule: cdcl⇩N⇩O⇩T_restart.cases)
apply auto[]
using g[of "Suc i"] f_ge_1 apply (cases rule: cdcl⇩N⇩O⇩T_restart.cases)
apply (auto simp add: full1_def full_def dest: H dest: tranclpD)
using H Suc_leI leD by blast
} note H = this
obtain A where "bound_inv A (fst (g 1))"
using g[of 0] cdcl⇩N⇩O⇩T_inv_g[of 0] apply (cases rule: cdcl⇩N⇩O⇩T_restart.cases)
apply (metis One_nat_def cdcl⇩N⇩O⇩T_inv exists_bound fst_conv relpowp_imp_rtranclp
rtranclp_induct)
using H[of 1] unfolding full1_def by (metis One_nat_def Suc_eq_plus1 diff_is_0_eq' diff_zero
f_ge_1 fst_conv le_add2 relpowp_E2 snd_conv)
let ?j = "μ_bound A (fst (g 1)) + 1"
obtain j where
j: "f (snd (g j)) > ?j" and "j > 1"
using unbounded_f_g not_bounded_nat_exists_larger by blast
{
fix i j
have cdcl⇩N⇩O⇩T_with_restart: "j ≥ i ⟹ cdcl⇩N⇩O⇩T_restart⇧*⇧* (g i) (g j)"
apply (induction j)
apply simp
by (metis g le_Suc_eq rtranclp.rtrancl_into_rtrancl rtranclp.rtrancl_refl)
} note cdcl⇩N⇩O⇩T_restart = this
have "cdcl⇩N⇩O⇩T_inv (fst (g (Suc 0)))"
by (simp add: cdcl⇩N⇩O⇩T_inv_g)
have "cdcl⇩N⇩O⇩T_restart⇧*⇧* (fst (g 1), snd (g 1)) (fst (g j), snd (g j))"
using ‹j> 1› by (simp add: cdcl⇩N⇩O⇩T_restart)
have "μ A (fst (g j)) ≤ μ_bound A (fst (g 1))"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_raw_restart_measure_bound)
using ‹cdcl⇩N⇩O⇩T_restart⇧*⇧* (fst (g 1), snd (g 1)) (fst (g j), snd (g j))› apply blast
apply (simp add: cdcl⇩N⇩O⇩T_inv_g)
using ‹bound_inv A (fst (g 1))› apply simp
done
then have "μ A (fst (g j)) ≤ ?j"
by auto
have inv: "bound_inv A (fst (g j))"
using ‹bound_inv A (fst (g 1))› ‹cdcl⇩N⇩O⇩T_inv (fst (g (Suc 0)))›
‹cdcl⇩N⇩O⇩T_restart⇧*⇧* (fst (g 1), snd (g 1)) (fst (g j), snd (g j))›
rtranclp_cdcl⇩N⇩O⇩T_with_restart_bound_inv by auto
obtain T m where
cdcl⇩N⇩O⇩T_m: "(cdcl⇩N⇩O⇩T ^^ m) (fst (g j)) T" and
f_m: "f (snd (g j)) ≤ m"
using H[of "j"] by blast
have "?j < m"
using f_m j Nat.le_trans by linarith
then show False
using ‹μ A (fst (g j)) ≤ μ_bound A (fst (g 1))›
cdcl⇩N⇩O⇩T_comp_bounded[OF inv cdcl⇩N⇩O⇩T_inv_g, of ] cdcl⇩N⇩O⇩T_inv_g cdcl⇩N⇩O⇩T_m
‹?j < m› by auto
qed
lemma cdcl⇩N⇩O⇩T_restart_steps_bigger_than_bound:
assumes
"cdcl⇩N⇩O⇩T_restart S T" and
"bound_inv A (fst S)" and
"cdcl⇩N⇩O⇩T_inv (fst S)" and
"f (snd S) > μ_bound A (fst S)"
shows "full1 cdcl⇩N⇩O⇩T (fst S) (fst T)"
using assms
proof (induction rule: cdcl⇩N⇩O⇩T_restart.induct)
case restart_full
then show ?case by auto
next
case (restart_step m S T n U) note st = this(1) and f = this(2) and bound_inv = this(4) and
cdcl⇩N⇩O⇩T_inv =this(5) and μ = this(6)
then obtain m' where m: "m = Suc m'" by (cases m) auto
have "μ A S - m' = 0"
using f bound_inv cdcl⇩N⇩O⇩T_inv μ m rtranclp_cdcl⇩N⇩O⇩T_raw_restart_measure_bound by fastforce
then have False using cdcl⇩N⇩O⇩T_comp_n_le[of m' S T A] restart_step unfolding m by simp
then show ?case by fast
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_with_inv_inv_rtranclp_cdcl⇩N⇩O⇩T:
assumes
inv: "cdcl⇩N⇩O⇩T_inv S" and
binv: "bound_inv A S"
shows "(λS T. cdcl⇩N⇩O⇩T S T ∧ cdcl⇩N⇩O⇩T_inv S ∧ bound_inv A S)⇧*⇧* S T ⟷ cdcl⇩N⇩O⇩T⇧*⇧* S T"
(is "?A⇧*⇧* S T ⟷ ?B⇧*⇧* S T")
apply (rule iffI)
using rtranclp_mono[of ?A ?B] apply blast
apply (induction rule: rtranclp_induct)
using inv binv apply simp
by (metis (mono_tags, lifting) binv inv rtranclp.simps rtranclp_cdcl⇩N⇩O⇩T_bound_inv
rtranclp_cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv)
lemma no_step_cdcl⇩N⇩O⇩T_restart_no_step_cdcl⇩N⇩O⇩T:
assumes
n_s: "no_step cdcl⇩N⇩O⇩T_restart S" and
inv: "cdcl⇩N⇩O⇩T_inv (fst S)" and
binv: "bound_inv A (fst S)"
shows "no_step cdcl⇩N⇩O⇩T (fst S)"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain T where T: "cdcl⇩N⇩O⇩T (fst S) T"
by blast
then obtain U where U: "full (λS T. cdcl⇩N⇩O⇩T S T ∧ cdcl⇩N⇩O⇩T_inv S ∧ bound_inv A S) T U"
using wf_exists_normal_form_full[OF wf_cdcl⇩N⇩O⇩T, of A T] by auto
moreover have inv_T: "cdcl⇩N⇩O⇩T_inv T"
using ‹cdcl⇩N⇩O⇩T (fst S) T› cdcl⇩N⇩O⇩T_inv inv by blast
moreover have b_inv_T: "bound_inv A T"
using ‹cdcl⇩N⇩O⇩T (fst S) T› binv bound_inv inv by blast
ultimately have "full cdcl⇩N⇩O⇩T T U"
using rtranclp_cdcl⇩N⇩O⇩T_with_inv_inv_rtranclp_cdcl⇩N⇩O⇩T rtranclp_cdcl⇩N⇩O⇩T_bound_inv
rtranclp_cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv unfolding full_def by blast
then have "full1 cdcl⇩N⇩O⇩T (fst S) U"
using T full_fullI by metis
then show False by (metis n_s prod.collapse restart_full)
qed
end
subsection ‹Merging backjump and learning›
locale cdcl⇩N⇩O⇩T_merge_bj_learn_ops =
dpll_state trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T +
decide_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T +
forget_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T forget_cond +
propagate_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T propagate_conds
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
forget_cond :: "'v clause ⇒ 'st ⇒ bool" +
fixes backjump_l_cond :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ bool"
begin
inductive backjump_l where
backjump_l: "trail S = F' @ Decided K () # F
⟹ no_dup (trail S)
⟹ T ∼ prepend_trail (Propagated L ()) (reduce_trail_to⇩N⇩O⇩T F (add_cls⇩N⇩O⇩T (C' + {#L#}) S))
⟹ C ∈# clauses S
⟹ trail S ⊨as CNot C
⟹ undefined_lit F L
⟹ atm_of L ∈ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S))
⟹ clauses S ⊨pm C' + {#L#}
⟹ F ⊨as CNot C'
⟹ backjump_l_cond C C' L T
⟹ backjump_l S T"
inductive_cases backjump_lE: "backjump_l S T"
inductive cdcl⇩N⇩O⇩T_merged_bj_learn :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T: "decide⇩N⇩O⇩T S S' ⟹ cdcl⇩N⇩O⇩T_merged_bj_learn S S'" |
cdcl⇩N⇩O⇩T_merged_bj_learn_propagate⇩N⇩O⇩T: "propagate⇩N⇩O⇩T S S' ⟹ cdcl⇩N⇩O⇩T_merged_bj_learn S S'" |
cdcl⇩N⇩O⇩T_merged_bj_learn_backjump_l: "backjump_l S S' ⟹ cdcl⇩N⇩O⇩T_merged_bj_learn S S'" |
cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T: "forget⇩N⇩O⇩T S S' ⟹ cdcl⇩N⇩O⇩T_merged_bj_learn S S'"
lemma cdcl⇩N⇩O⇩T_merged_bj_learn_no_dup_inv:
"cdcl⇩N⇩O⇩T_merged_bj_learn S T ⟹ no_dup (trail S) ⟹ no_dup (trail T)"
apply (induction rule: cdcl⇩N⇩O⇩T_merged_bj_learn.induct)
using defined_lit_map apply fastforce
using defined_lit_map apply fastforce
apply (force simp: defined_lit_map elim!: backjump_lE)[]
using forget⇩N⇩O⇩T.simps apply auto[1]
done
end
locale cdcl⇩N⇩O⇩T_merge_bj_learn_proxy =
cdcl⇩N⇩O⇩T_merge_bj_learn_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds forget_conds "λC C' L' S. backjump_l_cond C C' L' S
∧ distinct_mset (C' + {#L'#}) ∧ ¬tautology (C' + {#L'#})"
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
forget_conds :: "'v clause ⇒ 'st ⇒ bool" and
backjump_l_cond :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ bool" +
fixes
inv :: "'st ⇒ bool"
assumes
bj_merge_can_jump:
"⋀S C F' K F L.
inv S
⟹ trail S = F' @ Decided K () # F
⟹ C ∈# clauses S
⟹ trail S ⊨as CNot C
⟹ undefined_lit F L
⟹ atm_of L ∈ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (F' @ Decided K () # F))
⟹ clauses S ⊨pm C' + {#L#}
⟹ F ⊨as CNot C'
⟹ ¬no_step backjump_l S" and
cdcl_merged_inv: "⋀S T. cdcl⇩N⇩O⇩T_merged_bj_learn S T ⟹ inv S ⟹ inv T"
begin
abbreviation backjump_conds where
"backjump_conds ≡ λ_ C L _ _. distinct_mset (C + {#L#}) ∧ ¬tautology (C + {#L#})"
sublocale dpll_with_backjumping_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv backjump_conds
proof (unfold_locales, goal_cases)
case 1
{ fix S S'
assume bj: "backjump_l S S'" and "no_dup (trail S)"
then obtain F' K F L C' C where
S': "S' ∼ prepend_trail (Propagated L ()) (reduce_trail_to⇩N⇩O⇩T F
(tl_trail(add_cls⇩N⇩O⇩T (C' + {#L#}) S)))"
and
tr_S: "trail S = F' @ Decided K () # F" and
C: "C ∈# clauses S" and
tr_S_C: "trail S ⊨as CNot C" and
undef_L: "undefined_lit F L" and
atm_L: "atm_of L ∈ atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S)" and
cls_S_C': "clauses S ⊨pm C' + {#L#}" and
F_C': "F ⊨as CNot C'" and
dist: "distinct_mset (C' + {#L#})" and
not_tauto: "¬ tautology (C' + {#L#})"
by (elim backjump_lE) simp
have "∃S'. backjumping_ops.backjump trail clauses prepend_trail tl_trail backjump_conds S S'"
apply rule
apply (rule backjumping_ops.backjump.intros)
apply unfold_locales
using tr_S apply simp
apply (rule state_eq⇩N⇩O⇩T_ref)
using C apply simp
using tr_S_C apply simp
using undef_L apply simp
using atm_L apply simp
using cls_S_C' apply simp
using F_C' apply simp
using dist not_tauto apply simp
done
} note H = this(1)
then show ?case using 1 bj_merge_can_jump by meson
qed
end
locale cdcl⇩N⇩O⇩T_merge_bj_learn_proxy2 =
cdcl⇩N⇩O⇩T_merge_bj_learn_proxy trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds forget_conds backjump_l_cond inv
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
inv :: "'st ⇒ bool" and
forget_conds :: "'v clause ⇒ 'st ⇒ bool" and
backjump_l_cond :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ bool"
begin
sublocale conflict_driven_clause_learning_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T
remove_cls⇩N⇩O⇩T propagate_conds inv backjump_conds "λC _. distinct_mset C ∧ ¬tautology C"
forget_conds
by unfold_locales
end
locale cdcl⇩N⇩O⇩T_merge_bj_learn =
cdcl⇩N⇩O⇩T_merge_bj_learn_proxy2 trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv forget_conds backjump_l_cond
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
inv :: "'st ⇒ bool" and
forget_conds :: "'v clause ⇒ 'st ⇒ bool" and
backjump_l_cond :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ bool" +
assumes
dpll_bj_inv: "⋀S T. dpll_bj S T ⟹ inv S ⟹ inv T" and
learn_inv: "⋀S T. learn S T ⟹ inv S ⟹ inv T"
begin
interpretation cdcl⇩N⇩O⇩T:
conflict_driven_clause_learning trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv backjump_conds "λC _. distinct_mset C ∧ ¬tautology C" forget_conds
apply unfold_locales
apply (simp only: cdcl⇩N⇩O⇩T.simps)
using cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T cdcl_merged_inv learn_inv
by (auto simp add: cdcl⇩N⇩O⇩T.simps dpll_bj_inv)
lemma backjump_l_learn_backjump:
assumes bt: "backjump_l S T" and inv: "inv S" and n_d: "no_dup (trail S)"
shows "∃C' L. learn S (add_cls⇩N⇩O⇩T (C' + {#L#}) S)
∧ backjump (add_cls⇩N⇩O⇩T (C' + {#L#}) S) T
∧ atms_of (C' + {#L#}) ⊆ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S))"
proof -
obtain C F' K F L l C' where
tr_S: "trail S = F' @ Decided K () # F" and
T: "T ∼ prepend_trail (Propagated L l) (reduce_trail_to⇩N⇩O⇩T F (add_cls⇩N⇩O⇩T (C' + {#L#}) S))" and
C_cls_S: "C ∈# clauses S" and
tr_S_CNot_C: "trail S ⊨as CNot C" and
undef: "undefined_lit F L" and
atm_L: "atm_of L ∈ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S))" and
clss_C: "clauses S ⊨pm C' + {#L#}" and
"F ⊨as CNot C'" and
distinct: "distinct_mset (C' + {#L#})" and
not_tauto: "¬ tautology (C' + {#L#})"
using bt inv by (elim backjump_lE) simp
have atms_C': "atms_of C' ⊆ atm_of ` (lits_of F)"
proof -
obtain ll :: "'v ⇒ ('v literal ⇒ 'v) ⇒ 'v literal set ⇒ 'v literal" where
"∀v f L. v ∉ f ` L ∨ v = f (ll v f L) ∧ ll v f L ∈ L"
by moura
then show ?thesis unfolding tr_S
by (metis (no_types) ‹F ⊨as CNot C'› atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
atms_of_def in_CNot_implies_uminus(2) mem_set_mset_iff subsetI)
qed
then have "atms_of (C' + {#L#}) ⊆ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S))"
using atm_L tr_S by auto
moreover have learn: "learn S (add_cls⇩N⇩O⇩T (C' + {#L#}) S)"
apply (rule learn.intros)
apply (rule clss_C)
using atms_C' atm_L apply (fastforce simp add: tr_S in_plus_implies_atm_of_on_atms_of_ms)[]
apply standard
apply (rule distinct)
apply (rule not_tauto)
apply simp
done
moreover have bj: "backjump (add_cls⇩N⇩O⇩T (C' + {#L#}) S) T"
apply (rule backjump.intros)
using ‹F ⊨as CNot C'› C_cls_S tr_S_CNot_C undef T distinct not_tauto n_d
by (auto simp: tr_S state_eq⇩N⇩O⇩T_def simp del: state_simp⇩N⇩O⇩T)
ultimately show ?thesis by auto
qed
lemma cdcl⇩N⇩O⇩T_merged_bj_learn_is_tranclp_cdcl⇩N⇩O⇩T:
"cdcl⇩N⇩O⇩T_merged_bj_learn S T ⟹ inv S ⟹ no_dup (trail S) ⟹ cdcl⇩N⇩O⇩T⇧+⇧+ S T"
proof (induction rule: cdcl⇩N⇩O⇩T_merged_bj_learn.induct)
case (cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T T)
then have "cdcl⇩N⇩O⇩T S T"
using bj_decide⇩N⇩O⇩T cdcl⇩N⇩O⇩T.simps by fastforce
then show ?case by auto
next
case (cdcl⇩N⇩O⇩T_merged_bj_learn_propagate⇩N⇩O⇩T T)
then have "cdcl⇩N⇩O⇩T S T"
using bj_propagate⇩N⇩O⇩T cdcl⇩N⇩O⇩T.simps by fastforce
then show ?case by auto
next
case (cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T T)
then have "cdcl⇩N⇩O⇩T S T"
using c_forget⇩N⇩O⇩T by blast
then show ?case by auto
next
case (cdcl⇩N⇩O⇩T_merged_bj_learn_backjump_l T) note bt = this(1) and inv = this(2) and
n_d = this(3)
obtain C' :: "'v literal multiset" and L :: "'v literal" where
f3: "learn S (add_cls⇩N⇩O⇩T (C' + {#L#}) S) ∧
backjump (add_cls⇩N⇩O⇩T (C' + {#L#}) S) T ∧
atms_of (C' + {#L#}) ⊆ atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S)"
using n_d backjump_l_learn_backjump[OF bt inv] by blast
then have f4: "cdcl⇩N⇩O⇩T S (add_cls⇩N⇩O⇩T (C' + {#L#}) S)"
using n_d c_learn by blast
have "cdcl⇩N⇩O⇩T (add_cls⇩N⇩O⇩T (C' + {#L#}) S) T"
using f3 n_d bj_backjump c_dpll_bj by blast
then show ?case
using f4 by (meson tranclp.r_into_trancl tranclp.trancl_into_trancl)
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T_and_inv:
"cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T ⟹ inv S ⟹ no_dup (trail S) ⟹ cdcl⇩N⇩O⇩T⇧*⇧* S T ∧ inv T"
proof (induction rule: rtranclp_induct)
case base
then show ?case by auto
next
case (step T U) note st =this(1) and cdcl⇩N⇩O⇩T = this(2) and IH = this(3)[OF this(4-)] and
inv = this(4) and n_d = this(5)
have "cdcl⇩N⇩O⇩T⇧*⇧* T U"
using cdcl⇩N⇩O⇩T_merged_bj_learn_is_tranclp_cdcl⇩N⇩O⇩T[OF cdcl⇩N⇩O⇩T] IH
cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_no_dup inv n_d by auto
then have "cdcl⇩N⇩O⇩T⇧*⇧* S U" using IH by fastforce
moreover have "inv U" using n_d IH ‹cdcl⇩N⇩O⇩T⇧*⇧* T U› cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_inv by blast
ultimately show ?case using st by fast
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T:
"cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T ⟹ inv S ⟹no_dup (trail S) ⟹ cdcl⇩N⇩O⇩T⇧*⇧* S T"
using rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T_and_inv by blast
lemma rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_inv:
"cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T ⟹ inv S ⟹ no_dup (trail S) ⟹ inv T"
using rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T_and_inv by blast
definition μ⇩C' :: "'v literal multiset set ⇒ 'st ⇒ nat" where
"μ⇩C' A T ≡ μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)"
definition μ⇩C⇩D⇩C⇩L'_merged :: "'v literal multiset set ⇒ 'st ⇒ nat" where
"μ⇩C⇩D⇩C⇩L'_merged A T ≡
((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μ⇩C' A T) * 2 + card (set_mset (clauses T))"
lemma cdcl⇩N⇩O⇩T_decreasing_measure':
assumes
"cdcl⇩N⇩O⇩T_merged_bj_learn S T" and
inv: "inv S" and
atm_clss: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atm_trail: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
fin_A: "finite A"
shows "μ⇩C⇩D⇩C⇩L'_merged A T < μ⇩C⇩D⇩C⇩L'_merged A S"
using assms(1)
proof induction
case (cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T T)
have "clauses S = clauses T"
using cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T.hyps by auto
moreover have
"(2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight T)
< (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight S)"
apply (rule dpll_bj_trail_mes_decreasing_prop)
using cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T fin_A atm_clss atm_trail n_d inv
by (simp_all add: bj_decide⇩N⇩O⇩T cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T.hyps)
ultimately show ?case
unfolding μ⇩C⇩D⇩C⇩L'_merged_def μ⇩C'_def by simp
next
case (cdcl⇩N⇩O⇩T_merged_bj_learn_propagate⇩N⇩O⇩T T)
have "clauses S = clauses T"
using cdcl⇩N⇩O⇩T_merged_bj_learn_propagate⇩N⇩O⇩T.hyps
by (simp add: bj_propagate⇩N⇩O⇩T inv dpll_bj_clauses)
moreover have
"(2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight T)
< (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight S)"
apply (rule dpll_bj_trail_mes_decreasing_prop)
using inv n_d atm_clss atm_trail fin_A by (simp_all add: bj_propagate⇩N⇩O⇩T
cdcl⇩N⇩O⇩T_merged_bj_learn_propagate⇩N⇩O⇩T.hyps)
ultimately show ?case
unfolding μ⇩C⇩D⇩C⇩L'_merged_def μ⇩C'_def by simp
next
case (cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T T)
have "card (set_mset (clauses T)) < card (set_mset (clauses S))"
using ‹forget⇩N⇩O⇩T S T› by (metis card_Diff1_less
cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T.hyps clauses_remove_cls⇩N⇩O⇩T finite_set_mset forget⇩N⇩O⇩TE
mem_set_mset_iff order_refl set_mset_minus_replicate_mset(1) state_eq⇩N⇩O⇩T_clauses)
moreover
have "trail S = trail T"
using ‹forget⇩N⇩O⇩T S T› by (auto elim: forget⇩N⇩O⇩TE)
then have
"(2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight T)
= (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight S)"
by auto
ultimately show ?case
unfolding μ⇩C⇩D⇩C⇩L'_merged_def μ⇩C'_def by simp
next
case (cdcl⇩N⇩O⇩T_merged_bj_learn_backjump_l T) note bj_l = this(1)
obtain C' L where
learn: "learn S (add_cls⇩N⇩O⇩T (C' + {#L#}) S)" and
bj: "backjump (add_cls⇩N⇩O⇩T (C' + {#L#}) S) T" and
atms_C: "atms_of (C' + {#L#}) ⊆ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (trail S))"
using bj_l inv backjump_l_learn_backjump n_d atm_clss atm_trail by blast
have card_T_S: "card (set_mset (clauses T)) ≤ 1+ card (set_mset (clauses S))"
using bj_l inv by (force elim!: backjump_lE simp: card_insert_if)
have
"((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight T))
< ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A))
(trail_weight (add_cls⇩N⇩O⇩T (C' + {#L#}) S)))"
apply (rule dpll_bj_trail_mes_decreasing_prop)
using bj bj_backjump apply blast
using cdcl⇩N⇩O⇩T.c_learn cdcl⇩N⇩O⇩T.cdcl⇩N⇩O⇩T_inv inv learn apply blast
using atms_C atm_clss atm_trail n_d clauses_add_cls⇩N⇩O⇩T apply simp apply fast
using atm_trail n_d apply simp
apply (simp add: n_d)
using fin_A apply simp
done
then have "((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight T))
< ((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A))
- μ⇩C (1 + card (atms_of_ms A)) (2 + card (atms_of_ms A)) (trail_weight S))"
using n_d by auto
then show ?case
using card_T_S unfolding μ⇩C⇩D⇩C⇩L'_merged_def μ⇩C'_def by linarith
qed
lemma wf_cdcl⇩N⇩O⇩T_merged_bj_learn:
assumes
fin_A: "finite A"
shows "wf {(T, S).
(inv S ∧ atms_of_msu (clauses S) ⊆ atms_of_ms A ∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A
∧ no_dup (trail S))
∧ cdcl⇩N⇩O⇩T_merged_bj_learn S T}"
apply (rule wfP_if_measure[of _ _ "μ⇩C⇩D⇩C⇩L'_merged A"])
using cdcl⇩N⇩O⇩T_decreasing_measure' fin_A by simp
lemma tranclp_cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_tranclp:
assumes
"cdcl⇩N⇩O⇩T_merged_bj_learn⇧+⇧+ S T" and
inv: "inv S" and
atm_clss: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atm_trail: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
fin_A[simp]: "finite A"
shows "(T, S) ∈ {(T, S).
(inv S ∧ atms_of_msu (clauses S) ⊆ atms_of_ms A ∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A
∧ no_dup (trail S))
∧ cdcl⇩N⇩O⇩T_merged_bj_learn S T}⇧+" (is "_ ∈ ?P⇧+")
using assms(1)
proof (induction rule: tranclp_induct)
case base
then show ?case using n_d atm_clss atm_trail inv by auto
next
case (step T U) note st = this(1) and cdcl⇩N⇩O⇩T = this(2) and IH = this(3)
have "cdcl⇩N⇩O⇩T⇧*⇧* S T"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T)
using st cdcl⇩N⇩O⇩T inv n_d atm_clss atm_trail inv by auto
have "inv T"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_inv)
using inv st cdcl⇩N⇩O⇩T n_d atm_clss atm_trail inv by auto
moreover have "atms_of_msu (clauses T) ⊆ atms_of_ms A"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound[OF ‹cdcl⇩N⇩O⇩T⇧*⇧* S T› inv n_d atm_clss atm_trail]
by fast
moreover have "atm_of ` (lits_of (trail T))⊆ atms_of_ms A"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound[OF ‹cdcl⇩N⇩O⇩T⇧*⇧* S T› inv n_d atm_clss atm_trail]
by fast
moreover have "no_dup (trail T)"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_no_dup[OF ‹cdcl⇩N⇩O⇩T⇧*⇧* S T› inv n_d] by fast
ultimately have "(U, T) ∈ ?P"
using cdcl⇩N⇩O⇩T by auto
then show ?case using IH by (simp add: trancl_into_trancl2)
qed
lemma wf_tranclp_cdcl⇩N⇩O⇩T_merged_bj_learn:
assumes "finite A"
shows "wf {(T, S).
(inv S ∧ atms_of_msu (clauses S) ⊆ atms_of_ms A ∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A
∧ no_dup (trail S))
∧ cdcl⇩N⇩O⇩T_merged_bj_learn⇧+⇧+ S T}"
apply (rule wf_subset)
apply (rule wf_trancl[OF wf_cdcl⇩N⇩O⇩T_merged_bj_learn])
using assms apply simp
using tranclp_cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_tranclp[OF _ _ _ _ _ ‹finite A›] by auto
lemma backjump_no_step_backjump_l:
"backjump S T ⟹ inv S ⟹ ¬no_step backjump_l S"
apply (elim backjumpE)
apply (rule bj_merge_can_jump)
apply auto[7]
by blast
lemma cdcl⇩N⇩O⇩T_merged_bj_learn_final_state:
fixes A :: "'v literal multiset set" and S T :: "'st"
assumes
n_s: "no_step cdcl⇩N⇩O⇩T_merged_bj_learn S" and
atms_S: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atms_trail: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
"finite A" and
inv: "inv S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows "unsatisfiable (set_mset (clauses S))
∨ (trail S ⊨asm clauses S ∧ satisfiable (set_mset (clauses S)))"
proof -
let ?N = "set_mset (clauses S)"
let ?M = "trail S"
consider
(sat) "satisfiable ?N" and "?M ⊨as ?N"
| (sat') "satisfiable ?N" and "¬ ?M ⊨as ?N"
| (unsat) "unsatisfiable ?N"
by auto
then show ?thesis
proof cases
case sat' note sat = this(1) and M = this(2)
obtain C where "C ∈ ?N" and "¬?M ⊨a C" using M unfolding true_annots_def by auto
obtain I :: "'v literal set" where
"I ⊨s ?N" and
cons: "consistent_interp I" and
tot: "total_over_m I ?N" and
atm_I_N: "atm_of `I ⊆ atms_of_ms ?N"
using sat unfolding satisfiable_def_min by auto
let ?I = "I ∪ {P| P. P ∈ lits_of ?M ∧ atm_of P ∉ atm_of ` I}"
let ?O = "{{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}"
have cons_I': "consistent_interp ?I"
using cons using ‹no_dup ?M› unfolding consistent_interp_def
by (auto simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set lits_of_def
dest!: no_dup_cannot_not_lit_and_uminus)
have tot_I': "total_over_m ?I (?N ∪ unmark ?M)"
using tot atms_of_s_def unfolding total_over_m_def total_over_set_def
by fastforce
have "{P |P. P ∈ lits_of ?M ∧ atm_of P ∉ atm_of ` I} ⊨s ?O"
using ‹I⊨s ?N› atm_I_N by (auto simp add: atm_of_eq_atm_of true_clss_def lits_of_def)
then have I'_N: "?I ⊨s ?N ∪ ?O"
using ‹I⊨s ?N› true_clss_union_increase by force
have tot': "total_over_m ?I (?N∪?O)"
using atm_I_N tot unfolding total_over_m_def total_over_set_def
by (force simp: image_iff lits_of_def dest!: is_decided_ex_Decided)
have atms_N_M: "atms_of_ms ?N ⊆ atm_of ` lits_of ?M"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain l :: 'v where
l_N: "l ∈ atms_of_ms ?N" and
l_M: "l ∉ atm_of ` lits_of ?M"
by auto
have "undefined_lit ?M (Pos l)"
using l_M by (metis Decided_Propagated_in_iff_in_lits_of
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set literal.sel(1))
have "decide⇩N⇩O⇩T S (prepend_trail (Decided (Pos l) ()) S)"
by (metis ‹undefined_lit ?M (Pos l)› decide⇩N⇩O⇩T.intros l_N literal.sel(1)
state_eq⇩N⇩O⇩T_ref)
then show False
using cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T n_s by blast
qed
have "?M ⊨as CNot C"
by (metis atms_N_M ‹C ∈ ?N› ‹¬ ?M ⊨a C› all_variables_defined_not_imply_cnot
atms_of_atms_of_ms_mono atms_of_ms_CNot_atms_of atms_of_ms_CNot_atms_of_ms subsetCE)
have "∃l ∈ set ?M. is_decided l"
proof (rule ccontr)
let ?O = "{{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}"
have θ[iff]: "⋀I. total_over_m I (?N ∪ ?O ∪ unmark ?M)
⟷ total_over_m I (?N ∪unmark ?M)"
unfolding total_over_set_def total_over_m_def atms_of_ms_def by auto
assume "¬ ?thesis"
then have [simp]:"{{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M}
= {{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M ∧ atm_of (lit_of L) ∉ atms_of_ms ?N}"
by auto
then have "?N ∪ ?O ⊨ps unmark ?M"
using all_decomposition_implies_propagated_lits_are_implied[OF decomp] by auto
then have "?I ⊨s unmark ?M"
using cons_I' I'_N tot_I' ‹?I ⊨s ?N ∪ ?O› unfolding θ true_clss_clss_def by blast
then have "lits_of ?M ⊆ ?I"
unfolding true_clss_def lits_of_def by auto
then have "?M ⊨as ?N"
using I'_N ‹C ∈ ?N› ‹¬ ?M ⊨a C› cons_I' atms_N_M
by (meson ‹trail S ⊨as CNot C› consistent_CNot_not rev_subsetD sup_ge1 true_annot_def
true_annots_def true_cls_mono_set_mset_l true_clss_def)
then show False using M by fast
qed
from List.split_list_first_propE[OF this] obtain K :: "'v literal" and d :: unit and
F F' :: "('v, unit, unit) ann_literal list" where
M_K: "?M = F' @ Decided K () # F" and
nm: "∀f∈set F'. ¬is_decided f"
unfolding is_decided_def by (metis (full_types) old.unit.exhaust)
let ?K = "Decided K ()::('v, unit, unit) ann_literal"
have "?K ∈ set ?M"
unfolding M_K by auto
let ?C = "image_mset lit_of {#L∈#mset ?M. is_decided L ∧ L≠?K#} :: 'v literal multiset"
let ?C' = "set_mset (image_mset (λL::'v literal. {#L#}) (?C+{#lit_of ?K#}))"
have "?N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M} ⊨ps unmark ?M"
using all_decomposition_implies_propagated_lits_are_implied[OF decomp] .
moreover have C': "?C' = {{#lit_of L#} |L. is_decided L ∧ L ∈ set ?M}"
unfolding M_K apply standard
apply force
using IntI by auto
ultimately have N_C_M: "?N ∪ ?C' ⊨ps unmark ?M"
by auto
have N_M_False: "?N ∪ (λL. {#lit_of L#}) ` (set ?M) ⊨ps {{#}}"
using M ‹?M ⊨as CNot C› ‹C∈?N› unfolding true_clss_clss_def true_annots_def Ball_def
true_annot_def by (metis consistent_CNot_not sup.orderE sup_commute true_clss_def
true_clss_singleton_lit_of_implies_incl true_clss_union true_clss_union_increase)
have "undefined_lit F K" using ‹no_dup ?M› unfolding M_K by (simp add: defined_lit_map)
moreover
have "?N ∪ ?C' ⊨ps {{#}}"
proof -
have A: "?N ∪ ?C' ∪ unmark ?M =
?N ∪ unmark ?M"
unfolding M_K by auto
show ?thesis
using true_clss_clss_left_right[OF N_C_M, of "{{#}}"] N_M_False unfolding A by auto
qed
have "?N ⊨p image_mset uminus ?C + {#-K#}"
unfolding true_clss_cls_def true_clss_clss_def total_over_m_def
proof (intro allI impI)
fix I
assume
tot: "total_over_set I (atms_of_ms (?N ∪ {image_mset uminus ?C+ {#- K#}}))" and
cons: "consistent_interp I" and
"I ⊨s ?N"
have "(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)"
using cons tot unfolding consistent_interp_def by (cases K) auto
have tot': "total_over_set I
(atm_of ` lit_of ` (set ?M ∩ {L. is_decided L ∧ L ≠ Decided K ()}))"
using tot by (auto simp add: atms_of_uminus_lit_atm_of_lit_of)
{ fix x :: "('v, unit, unit) ann_literal"
assume
a3: "lit_of x ∉ I" and
a1: "x ∈ set ?M" and
a4: "is_decided x" and
a5: "x ≠ Decided K ()"
then have "Pos (atm_of (lit_of x)) ∈ I ∨ Neg (atm_of (lit_of x)) ∈ I"
using a5 a4 tot' a1 unfolding total_over_set_def atms_of_s_def by blast
moreover have f6: "Neg (atm_of (lit_of x)) = - Pos (atm_of (lit_of x))"
by simp
ultimately have "- lit_of x ∈ I"
using f6 a3 by (metis (no_types) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
literal.sel(1))
} note H = this
have "¬I ⊨s ?C'"
using ‹?N ∪ ?C' ⊨ps {{#}}› tot cons ‹I ⊨s ?N›
unfolding true_clss_clss_def total_over_m_def
by (simp add: atms_of_uminus_lit_atm_of_lit_of atms_of_ms_single_image_atm_of_lit_of)
then show "I ⊨ image_mset uminus ?C + {#- K#}"
unfolding true_clss_def true_cls_def Bex_mset_def
using ‹(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)›
by (auto dest!: H)
qed
moreover have "F ⊨as CNot (image_mset uminus ?C)"
using nm unfolding true_annots_def CNot_def M_K by (auto simp add: lits_of_def)
ultimately have False
using bj_merge_can_jump[of S F' K F C "-K"
"image_mset uminus (image_mset lit_of {# L :# mset ?M. is_decided L ∧ L ≠ Decided K ()#})"]
‹C∈?N› n_s ‹?M ⊨as CNot C› bj_backjump inv unfolding M_K
by (auto simp: cdcl⇩N⇩O⇩T_merged_bj_learn.simps)
then show ?thesis by fast
qed auto
qed
lemma full_cdcl⇩N⇩O⇩T_merged_bj_learn_final_state:
fixes A :: "'v literal multiset set" and S T :: "'st"
assumes
full: "full cdcl⇩N⇩O⇩T_merged_bj_learn S T" and
atms_S: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atms_trail: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
"finite A" and
inv: "inv S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows "unsatisfiable (set_mset (clauses T))
∨ (trail T ⊨asm clauses T ∧ satisfiable (set_mset (clauses T)))"
proof -
have st: "cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T" and n_s: "no_step cdcl⇩N⇩O⇩T_merged_bj_learn T"
using full unfolding full_def by blast+
then have st: "cdcl⇩N⇩O⇩T⇧*⇧* S T"
using inv rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T_and_inv n_d by auto
have "atms_of_msu (clauses T) ⊆ atms_of_ms A" and "atm_of ` lits_of (trail T) ⊆ atms_of_ms A"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound[OF st inv n_d atms_S atms_trail] by blast+
moreover have "no_dup (trail T)"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_no_dup inv n_d st by blast
moreover have "inv T"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_inv inv st by blast
moreover have "all_decomposition_implies_m (clauses T) (get_all_decided_decomposition (trail T))"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_all_decomposition_implies inv st decomp n_d by blast
ultimately show ?thesis
using cdcl⇩N⇩O⇩T_merged_bj_learn_final_state[of T A] ‹finite A› n_s by fast
qed
end
subsubsection ‹Instantiations›
locale cdcl⇩N⇩O⇩T_with_backtrack_and_restarts =
conflict_driven_clause_learning_learning_before_backjump_only_distinct_learnt trail clauses
prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T propagate_conds inv backjump_conds
learn_restrictions forget_restrictions
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
inv :: "'st ⇒ bool" and
backjump_conds :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ 'st ⇒ bool" and
learn_restrictions forget_restrictions :: "'v clause ⇒ 'st ⇒ bool"
+
fixes f :: "nat ⇒ nat"
assumes
unbounded: "unbounded f" and f_ge_1: "⋀n. n ≥ 1 ⟹ f n ≥ 1" and
inv_restart:"⋀S T. inv S ⟹ T ∼ reduce_trail_to⇩N⇩O⇩T ([]::'a list) S ⟹ inv T"
begin
lemma bound_inv_inv:
assumes
"inv S" and
n_d: "no_dup (trail S)" and
atms_clss_S_A: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atms_trail_S_A:"atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
"finite A" and
cdcl⇩N⇩O⇩T: "cdcl⇩N⇩O⇩T S T"
shows
"atms_of_msu (clauses T) ⊆ atms_of_ms A" and
"atm_of ` lits_of (trail T) ⊆ atms_of_ms A" and
"finite A"
proof -
have "cdcl⇩N⇩O⇩T S T"
using ‹inv S› cdcl⇩N⇩O⇩T by linarith
then have "atms_of_msu (clauses T) ⊆ atms_of_msu (clauses S) ∪ atm_of ` lits_of (trail S)"
using ‹inv S›
by (meson conflict_driven_clause_learning_ops.cdcl⇩N⇩O⇩T_atms_of_ms_clauses_decreasing
conflict_driven_clause_learning_ops_axioms n_d)
then show "atms_of_msu (clauses T) ⊆ atms_of_ms A"
using atms_clss_S_A atms_trail_S_A by blast
next
show "atm_of ` lits_of (trail T) ⊆ atms_of_ms A"
by (meson ‹inv S› atms_clss_S_A atms_trail_S_A cdcl⇩N⇩O⇩T cdcl⇩N⇩O⇩T_atms_in_trail_in_set n_d)
next
show "finite A"
using ‹finite A› by simp
qed
sublocale cdcl⇩N⇩O⇩T_increasing_restarts_ops "λS T. T ∼ reduce_trail_to⇩N⇩O⇩T ([]::'a list) S" cdcl⇩N⇩O⇩T f
"λA S. atms_of_msu (clauses S) ⊆ atms_of_ms A ∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A ∧
finite A"
μ⇩C⇩D⇩C⇩L' "λS. inv S ∧ no_dup (trail S)"
μ⇩C⇩D⇩C⇩L'_bound
apply unfold_locales
apply (simp add: unbounded)
using f_ge_1 apply force
using bound_inv_inv apply meson
apply (rule cdcl⇩N⇩O⇩T_decreasing_measure'; simp)
apply (rule rtranclp_cdcl⇩N⇩O⇩T_μ⇩C⇩D⇩C⇩L'_bound; simp)
apply (rule rtranclp_μ⇩C⇩D⇩C⇩L'_bound_decreasing; simp)
apply auto[]
apply auto[]
using cdcl⇩N⇩O⇩T_inv cdcl⇩N⇩O⇩T_no_dup apply blast
using inv_restart apply auto[]
done
abbreviation cdcl⇩N⇩O⇩T_l where
"cdcl⇩N⇩O⇩T_l ≡
conflict_driven_clause_learning_ops.cdcl⇩N⇩O⇩T trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T
remove_cls⇩N⇩O⇩T propagate_conds (λ_ _ _ S T. backjump S T)
(λC S. distinct_mset C ∧ ¬ tautology C ∧ learn_restrictions C S
∧ (∃F K F' C' L. trail S = F' @ Decided K () # F ∧ C = C' + {#L#}
∧ F ⊨as CNot C' ∧ C' + {#L#} ∉# clauses S))
(λC S. ¬ (∃F' F K L. trail S = F' @ Decided K () # F ∧ F ⊨as CNot (C - {#L#}))
∧ forget_restrictions C S)"
lemma cdcl⇩N⇩O⇩T_with_restart_μ⇩C⇩D⇩C⇩L'_le_μ⇩C⇩D⇩C⇩L'_bound:
assumes
cdcl⇩N⇩O⇩T: "cdcl⇩N⇩O⇩T_restart (T, a) (V, b)" and
cdcl⇩N⇩O⇩T_inv:
"inv T"
"no_dup (trail T)" and
bound_inv:
"atms_of_msu (clauses T) ⊆ atms_of_ms A"
"atm_of ` lits_of (trail T) ⊆ atms_of_ms A"
"finite A"
shows "μ⇩C⇩D⇩C⇩L' A V ≤ μ⇩C⇩D⇩C⇩L'_bound A T"
using cdcl⇩N⇩O⇩T_inv bound_inv
proof (induction rule: cdcl⇩N⇩O⇩T_with_restart_induct[OF cdcl⇩N⇩O⇩T])
case (1 m S T n U) note U = this(3)
show ?case
apply (rule rtranclp_cdcl⇩N⇩O⇩T_μ⇩C⇩D⇩C⇩L'_bound_reduce_trail_to⇩N⇩O⇩T[of S T])
using ‹(cdcl⇩N⇩O⇩T ^^ m) S T› apply (fastforce dest!: relpowp_imp_rtranclp)
using 1 by auto
next
case (2 S T n) note full = this(2)
show ?case
apply (rule rtranclp_cdcl⇩N⇩O⇩T_μ⇩C⇩D⇩C⇩L'_bound)
using full 2 unfolding full1_def by force+
qed
lemma cdcl⇩N⇩O⇩T_with_restart_μ⇩C⇩D⇩C⇩L'_bound_le_μ⇩C⇩D⇩C⇩L'_bound:
assumes
cdcl⇩N⇩O⇩T: "cdcl⇩N⇩O⇩T_restart (T, a) (V, b)" and
cdcl⇩N⇩O⇩T_inv:
"inv T"
"no_dup (trail T)" and
bound_inv:
"atms_of_msu (clauses T) ⊆ atms_of_ms A"
"atm_of ` lits_of (trail T) ⊆ atms_of_ms A"
"finite A"
shows "μ⇩C⇩D⇩C⇩L'_bound A V ≤ μ⇩C⇩D⇩C⇩L'_bound A T"
using cdcl⇩N⇩O⇩T_inv bound_inv
proof (induction rule: cdcl⇩N⇩O⇩T_with_restart_induct[OF cdcl⇩N⇩O⇩T])
case (1 m S T n U) note U = this(3)
have "μ⇩C⇩D⇩C⇩L'_bound A T ≤ μ⇩C⇩D⇩C⇩L'_bound A S"
apply (rule rtranclp_μ⇩C⇩D⇩C⇩L'_bound_decreasing)
using ‹(cdcl⇩N⇩O⇩T ^^ m) S T› apply (fastforce dest: relpowp_imp_rtranclp)
using 1 by auto
then show ?case using U unfolding μ⇩C⇩D⇩C⇩L'_bound_def by auto
next
case (2 S T n) note full = this(2)
show ?case
apply (rule rtranclp_μ⇩C⇩D⇩C⇩L'_bound_decreasing)
using full 2 unfolding full1_def by force+
qed
sublocale cdcl⇩N⇩O⇩T_increasing_restarts _ _ _ _ _ _ f
"λS T. T ∼ reduce_trail_to⇩N⇩O⇩T ([]::'a list) S"
"λA S. atms_of_msu (clauses S) ⊆ atms_of_ms A
∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A ∧ finite A"
μ⇩C⇩D⇩C⇩L' cdcl⇩N⇩O⇩T
"λS. inv S ∧ no_dup (trail S)"
μ⇩C⇩D⇩C⇩L'_bound
apply unfold_locales
using cdcl⇩N⇩O⇩T_with_restart_μ⇩C⇩D⇩C⇩L'_le_μ⇩C⇩D⇩C⇩L'_bound apply simp
using cdcl⇩N⇩O⇩T_with_restart_μ⇩C⇩D⇩C⇩L'_bound_le_μ⇩C⇩D⇩C⇩L'_bound apply simp
done
lemma cdcl⇩N⇩O⇩T_restart_all_decomposition_implies:
assumes "cdcl⇩N⇩O⇩T_restart S T" and
"inv (fst S)" and
"no_dup (trail (fst S))"
"all_decomposition_implies_m (clauses (fst S)) (get_all_decided_decomposition (trail (fst S)))"
shows
"all_decomposition_implies_m (clauses (fst T)) (get_all_decided_decomposition (trail (fst T)))"
using assms apply (induction)
using rtranclp_cdcl⇩N⇩O⇩T_all_decomposition_implies by (auto dest!: tranclp_into_rtranclp
simp: full1_def)
lemma rtranclp_cdcl⇩N⇩O⇩T_restart_all_decomposition_implies:
assumes "cdcl⇩N⇩O⇩T_restart⇧*⇧* S T" and
inv: "inv (fst S)" and
n_d: "no_dup (trail (fst S))" and
decomp:
"all_decomposition_implies_m (clauses (fst S)) (get_all_decided_decomposition (trail (fst S)))"
shows
"all_decomposition_implies_m (clauses (fst T)) (get_all_decided_decomposition (trail (fst T)))"
using assms(1)
proof (induction rule: rtranclp_induct)
case base
then show ?case using decomp by simp
next
case (step T u) note st = this(1) and r = this(2) and IH = this(3)
have "inv (fst T)"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv[OF st] inv n_d by blast
moreover have "no_dup (trail (fst T))"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv[OF st] inv n_d by blast
ultimately show ?case
using cdcl⇩N⇩O⇩T_restart_all_decomposition_implies r IH n_d by fast
qed
lemma cdcl⇩N⇩O⇩T_restart_sat_ext_iff:
assumes
st: "cdcl⇩N⇩O⇩T_restart S T" and
n_d: "no_dup (trail (fst S))" and
inv: "inv (fst S)"
shows "I ⊨sextm clauses (fst S) ⟷ I ⊨sextm clauses(fst T)"
using assms
proof (induction)
case (restart_step m S T n U)
then show ?case
using rtranclp_cdcl⇩N⇩O⇩T_bj_sat_ext_iff n_d by (fastforce dest!: relpowp_imp_rtranclp)
next
case restart_full
then show ?case using rtranclp_cdcl⇩N⇩O⇩T_bj_sat_ext_iff unfolding full1_def
by (fastforce dest!: tranclp_into_rtranclp)
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_restart_sat_ext_iff:
assumes
st: "cdcl⇩N⇩O⇩T_restart⇧*⇧* S T" and
n_d: "no_dup (trail (fst S))" and
inv: "inv (fst S)"
shows "I ⊨sextm clauses (fst S) ⟷ I ⊨sextm clauses(fst T)"
using st
proof (induction)
case base
then show ?case by simp
next
case (step T U) note st = this(1) and r = this(2) and IH = this(3)
have "inv (fst T)"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv[OF st] inv n_d by blast+
moreover have "no_dup (trail (fst T))"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv rtranclp_cdcl⇩N⇩O⇩T_no_dup st inv n_d by blast
ultimately show ?case
using cdcl⇩N⇩O⇩T_restart_sat_ext_iff[OF r] IH by blast
qed
theorem full_cdcl⇩N⇩O⇩T_restart_backjump_final_state:
fixes A :: "'v literal multiset set" and S T :: "'st"
assumes
full: "full cdcl⇩N⇩O⇩T_restart (S, n) (T, m)" and
atms_S: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atms_trail: "atm_of ` lits_of (trail S) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
fin_A[simp]: "finite A" and
inv: "inv S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_decided_decomposition (trail S))"
shows "unsatisfiable (set_mset (clauses S))
∨ (lits_of (trail T) ⊨sextm clauses S ∧ satisfiable (set_mset (clauses S)))"
proof -
have st: "cdcl⇩N⇩O⇩T_restart⇧*⇧* (S, n) (T, m)" and
n_s: "no_step cdcl⇩N⇩O⇩T_restart (T, m)"
using full unfolding full_def by fast+
have binv_T: "atms_of_msu (clauses T) ⊆ atms_of_ms A" "atm_of ` lits_of (trail T) ⊆ atms_of_ms A"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_bound_inv[OF st, of A] inv n_d atms_S atms_trail
by auto
moreover have inv_T: "no_dup (trail T)" "inv T"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv[OF st] inv n_d by auto
moreover have "all_decomposition_implies_m (clauses T) (get_all_decided_decomposition (trail T))"
using rtranclp_cdcl⇩N⇩O⇩T_restart_all_decomposition_implies[OF st] inv n_d
decomp by auto
ultimately have T: "unsatisfiable (set_mset (clauses T))
∨ (trail T ⊨asm clauses T ∧ satisfiable (set_mset (clauses T)))"
using no_step_cdcl⇩N⇩O⇩T_restart_no_step_cdcl⇩N⇩O⇩T[of "(T, m)" A] n_s
cdcl⇩N⇩O⇩T_final_state[of T A] unfolding cdcl⇩N⇩O⇩T_NOT_all_inv_def by auto
have eq_sat_S_T:"⋀I. I ⊨sextm clauses S ⟷ I ⊨sextm clauses T"
using rtranclp_cdcl⇩N⇩O⇩T_restart_sat_ext_iff[OF st] inv n_d atms_S
atms_trail by auto
have cons_T: "consistent_interp (lits_of (trail T))"
using inv_T(1) distinctconsistent_interp by blast
consider
(unsat) "unsatisfiable (set_mset (clauses T))"
| (sat) "trail T ⊨asm clauses T" and "satisfiable (set_mset (clauses T))"
using T by blast
then show ?thesis
proof cases
case unsat
then have "unsatisfiable (set_mset (clauses S))"
using eq_sat_S_T consistent_true_clss_ext_satisfiable true_clss_imp_true_cls_ext
unfolding satisfiable_def by blast
then show ?thesis by fast
next
case sat
then have "lits_of (trail T) ⊨sextm clauses S"
using rtranclp_cdcl⇩N⇩O⇩T_restart_sat_ext_iff[OF st] inv n_d atms_S
atms_trail by (auto simp: true_clss_imp_true_cls_ext true_annots_true_cls)
moreover then have "satisfiable (set_mset (clauses S))"
using cons_T consistent_true_clss_ext_satisfiable by blast
ultimately show ?thesis by blast
qed
qed
end ― ‹end of ‹cdcl⇩N⇩O⇩T_with_backtrack_and_restarts› locale›
locale most_general_cdcl⇩N⇩O⇩T =
dpll_state trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T +
propagate_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T propagate_conds +
backjumping_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T "λ_ _ _ _ _. True"
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
inv :: "'st ⇒ bool"
begin
lemma backjump_bj_can_jump:
assumes
tr_S: "trail S = F' @ Decided K () # F" and
C: "C ∈# clauses S" and
tr_S_C: "trail S ⊨as CNot C" and
undef: "undefined_lit F L" and
atm_L: "atm_of L ∈ atms_of_msu (clauses S) ∪ atm_of ` (lits_of (F' @ Decided K () # F))" and
cls_S_C': "clauses S ⊨pm C' + {#L#}" and
F_C': "F ⊨as CNot C'"
shows "¬no_step backjump S"
using backjump.intros[OF tr_S _ C tr_S_C undef _ cls_S_C' F_C',
of "prepend_trail (Propagated L _) (reduce_trail_to⇩N⇩O⇩T F S)"] atm_L unfolding tr_S
by (auto simp: state_eq⇩N⇩O⇩T_def simp del: state_simp⇩N⇩O⇩T)
sublocale dpll_with_backjumping_ops _ _ _ _ _ _ _ inv "λ_ _ _ _ _. True"
using backjump_bj_can_jump by unfold_locales auto
end
text ‹The restart does only reset the trail, contrary to Weidenbach's version. But there is a forget
rule.›
locale cdcl⇩N⇩O⇩T_merge_bj_learn_with_backtrack_restarts =
cdcl⇩N⇩O⇩T_merge_bj_learn trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv forget_conds
"λC C' L' S. distinct_mset (C' + {#L'#}) ∧ backjump_l_cond C C' L' S"
for
trail :: "'st ⇒ ('v, unit, unit) ann_literals" and
clauses :: "'st ⇒ 'v clauses" and
prepend_trail :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T:: "'v clause ⇒ 'st ⇒ 'st" and
propagate_conds :: "('v, unit, unit) ann_literal ⇒ 'st ⇒ bool" and
inv :: "'st ⇒ bool" and
forget_conds :: "'v clause ⇒ 'st ⇒ bool" and
backjump_l_cond :: "'v clause ⇒ 'v clause ⇒ 'v literal ⇒ 'st ⇒ bool"
+
fixes f :: "nat ⇒ nat"
assumes
unbounded: "unbounded f" and f_ge_1: "⋀n. n ≥ 1 ⟹ f n ≥ 1" and
inv_restart:"⋀S T. inv S ⟹ T ∼ reduce_trail_to⇩N⇩O⇩T [] S ⟹ inv T"
begin
interpretation cdcl⇩N⇩O⇩T:
conflict_driven_clause_learning_ops trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv backjump_conds "(λC _. distinct_mset C ∧ ¬ tautology C)" forget_conds
by unfold_locales
interpretation cdcl⇩N⇩O⇩T:
conflict_driven_clause_learning trail clauses prepend_trail tl_trail add_cls⇩N⇩O⇩T remove_cls⇩N⇩O⇩T
propagate_conds inv backjump_conds "(λC _. distinct_mset C ∧ ¬ tautology C)" forget_conds
apply unfold_locales
using cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T cdcl_merged_inv learn_inv
by (auto simp add: cdcl⇩N⇩O⇩T.simps dpll_bj_inv)
definition "not_simplified_cls A = {#C ∈# A. tautology C ∨ ¬distinct_mset C#}"
lemma simple_clss_or_not_simplified_cls:
assumes "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
"x ∈# clauses S" and "finite A"
shows "x ∈ simple_clss (atms_of_ms A) ∨ x ∈# not_simplified_cls (clauses S)"
proof -
consider
(simpl) "¬tautology x" and "distinct_mset x"
| (n_simp) "tautology x ∨ ¬distinct_mset x"
by auto
then show ?thesis
proof cases
case simpl
then have "x ∈ simple_clss (atms_of_ms A)"
by (meson assms atms_of_atms_of_ms_mono atms_of_ms_finite simple_clss_mono
distinct_mset_not_tautology_implies_in_simple_clss finite_subset
mem_set_mset_iff subsetCE)
then show ?thesis by blast
next
case n_simp
then have "x ∈# not_simplified_cls (clauses S)"
using ‹x ∈# clauses S› unfolding not_simplified_cls_def by auto
then show ?thesis by blast
qed
qed
lemma cdcl⇩N⇩O⇩T_merged_bj_learn_clauses_bound:
assumes
"cdcl⇩N⇩O⇩T_merged_bj_learn S T" and
inv: "inv S" and
atms_clss: "atms_of_msu (clauses S) ⊆ atms_of_ms A" and
atms_trail: "atm_of `(lits_of (trail S)) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
fin_A[simp]: "finite A"
shows "set_mset (clauses T) ⊆ set_mset (not_simplified_cls (clauses S))
∪ simple_clss (atms_of_ms A)"
using assms
proof (induction rule: cdcl⇩N⇩O⇩T_merged_bj_learn.induct)
case cdcl⇩N⇩O⇩T_merged_bj_learn_decide⇩N⇩O⇩T
then show ?case using dpll_bj_clauses by (force dest!: simple_clss_or_not_simplified_cls)
next
case cdcl⇩N⇩O⇩T_merged_bj_learn_propagate⇩N⇩O⇩T
then show ?case using dpll_bj_clauses by (force dest!: simple_clss_or_not_simplified_cls)
next
case cdcl⇩N⇩O⇩T_merged_bj_learn_forget⇩N⇩O⇩T
then show ?case using clauses_remove_cls⇩N⇩O⇩T unfolding state_eq⇩N⇩O⇩T_def
by (force elim!: forget⇩N⇩O⇩TE dest: simple_clss_or_not_simplified_cls)
next
case (cdcl⇩N⇩O⇩T_merged_bj_learn_backjump_l T) note bj = this(1) and inv = this(2) and
atms_clss = this(3) and atms_trail = this(4) and n_d = this(5)
have "cdcl⇩N⇩O⇩T⇧*⇧* S T"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T)
using ‹backjump_l S T› inv cdcl⇩N⇩O⇩T_merged_bj_learn.simps n_d by blast+
have "atm_of `(lits_of (trail T)) ⊆ atms_of_ms A"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound[OF ‹cdcl⇩N⇩O⇩T⇧*⇧* S T›] inv atms_trail atms_clss
n_d by auto
have "atms_of_msu (clauses T) ⊆ atms_of_ms A"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound[OF ‹cdcl⇩N⇩O⇩T⇧*⇧* S T› inv n_d atms_clss atms_trail]
by fast
moreover have "no_dup (trail T)"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_no_dup[OF ‹cdcl⇩N⇩O⇩T⇧*⇧* S T› inv n_d] by fast
obtain F' K F L l C' C where
tr_S: "trail S = F' @ Decided K () # F" and
T: "T ∼ prepend_trail (Propagated L l) (reduce_trail_to⇩N⇩O⇩T F (add_cls⇩N⇩O⇩T (C' + {#L#}) S))" and
"C ∈# clauses S" and
"trail S ⊨as CNot C" and
undef: "undefined_lit F L" and
"atm_of L = atm_of K ∨ atm_of L ∈ atms_of_msu (clauses S)
∨ atm_of L ∈ atm_of ` (lits_of F' ∪ lits_of F)" and
"clauses S ⊨pm C' + {#L#}" and
"F ⊨as CNot C'" and
dist: "distinct_mset (C' + {#L#})" and
tauto: "¬ tautology (C' + {#L#})" and
"backjump_l_cond C C' L T"
using ‹backjump_l S T› apply (induction rule: backjump_l.induct) by auto
have "atms_of C' ⊆ atm_of ` (lits_of F)"
using ‹F ⊨as CNot C'› by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
atms_of_def image_subset_iff in_CNot_implies_uminus(2))
then have "atms_of (C'+{#L#}) ⊆ atms_of_ms A"
using T ‹atm_of ` lits_of (trail T) ⊆ atms_of_ms A› tr_S undef n_d by auto
then have "simple_clss (atms_of (C' + {#L#})) ⊆ simple_clss (atms_of_ms A)"
apply - by (rule simple_clss_mono) (simp_all)
then have "C' + {#L#} ∈ simple_clss (atms_of_ms A)"
using distinct_mset_not_tautology_implies_in_simple_clss[OF dist tauto]
by auto
then show ?case
using T inv atms_clss undef tr_S n_d
by (force dest!: simple_clss_or_not_simplified_cls)
qed
lemma cdcl⇩N⇩O⇩T_merged_bj_learn_not_simplified_decreasing:
assumes "cdcl⇩N⇩O⇩T_merged_bj_learn S T"
shows "(not_simplified_cls (clauses T)) ⊆# (not_simplified_cls (clauses S))"
using assms apply induction
prefer 4
unfolding not_simplified_cls_def apply (auto elim!: backjump_lE forget⇩N⇩O⇩TE)[3]
by (elim backjump_lE) auto
lemma rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_not_simplified_decreasing:
assumes "cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T"
shows "(not_simplified_cls (clauses T)) ⊆# (not_simplified_cls (clauses S))"
using assms apply induction
apply simp
by (drule cdcl⇩N⇩O⇩T_merged_bj_learn_not_simplified_decreasing) auto
lemma rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_clauses_bound:
assumes
"cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ atms_of_ms A" and
"atm_of `(lits_of (trail S)) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
finite[simp]: "finite A"
shows "set_mset (clauses T) ⊆ set_mset (not_simplified_cls (clauses S))
∪ simple_clss (atms_of_ms A)"
using assms(1-5)
proof induction
case base
then show ?case by (auto dest!: simple_clss_or_not_simplified_cls)
next
case (step T U) note st = this(1) and cdcl⇩N⇩O⇩T = this(2) and IH = this(3)[OF this(4-7)] and
inv = this(4) and atms_clss_S = this(5) and atms_trail_S = this(6) and finite_cls_S = this(7)
have st': "cdcl⇩N⇩O⇩T⇧*⇧* S T"
using inv rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T_and_inv st n_d by blast
have "inv T"
using inv rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_inv st n_d by blast
moreover
have "atms_of_msu (clauses T) ⊆ atms_of_ms A" and
"atm_of ` lits_of (trail T) ⊆ atms_of_ms A"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound[OF st'] inv atms_clss_S atms_trail_S n_d
by blast+
moreover moreover have "no_dup (trail T)"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_no_dup[OF ‹cdcl⇩N⇩O⇩T⇧*⇧* S T› inv n_d] by fast
ultimately have "set_mset (clauses U)
⊆ set_mset (not_simplified_cls (clauses T)) ∪ simple_clss (atms_of_ms A)"
using cdcl⇩N⇩O⇩T finite cdcl⇩N⇩O⇩T_merged_bj_learn_clauses_bound
by (auto intro!: cdcl⇩N⇩O⇩T_merged_bj_learn_clauses_bound)
moreover have "set_mset (not_simplified_cls (clauses T))
⊆ set_mset (not_simplified_cls (clauses S))"
using rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_not_simplified_decreasing[OF st] by auto
ultimately show ?case using IH inv atms_clss_S
by (auto dest!: simple_clss_or_not_simplified_cls)
qed
abbreviation μ⇩C⇩D⇩C⇩L'_bound where
"μ⇩C⇩D⇩C⇩L'_bound A T == ((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))) * 2
+ card (set_mset (not_simplified_cls(clauses T)))
+ 3 ^ card (atms_of_ms A) "
lemma rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_clauses_bound_card:
assumes
"cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T" and
"inv S" and
"atms_of_msu (clauses S) ⊆ atms_of_ms A" and
"atm_of `(lits_of (trail S)) ⊆ atms_of_ms A" and
n_d: "no_dup (trail S)" and
finite: "finite A"
shows "μ⇩C⇩D⇩C⇩L'_merged A T ≤ μ⇩C⇩D⇩C⇩L'_bound A S"
proof -
have "set_mset (clauses T) ⊆ set_mset (not_simplified_cls(clauses S))
∪ simple_clss (atms_of_ms A)"
using rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_clauses_bound[OF assms] .
moreover have "card (set_mset (not_simplified_cls(clauses S))
∪ simple_clss (atms_of_ms A))
≤ card (set_mset (not_simplified_cls(clauses S))) + 3 ^ card (atms_of_ms A)"
by (meson Nat.le_trans atms_of_ms_finite simple_clss_card card_Un_le finite
nat_add_left_cancel_le)
ultimately have "card (set_mset (clauses T))
≤ card (set_mset (not_simplified_cls(clauses S))) + 3 ^ card (atms_of_ms A)"
by (meson Nat.le_trans atms_of_ms_finite simple_clss_finite card_mono
finite_UnI finite_set_mset local.finite)
moreover have "((2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) - μ⇩C' A T) * 2
≤ (2 + card (atms_of_ms A)) ^ (1 + card (atms_of_ms A)) * 2"
by auto
ultimately show ?thesis unfolding μ⇩C⇩D⇩C⇩L'_merged_def by auto
qed
sublocale cdcl⇩N⇩O⇩T_increasing_restarts_ops "λS T. T ∼ reduce_trail_to⇩N⇩O⇩T ([]::'a list) S"
cdcl⇩N⇩O⇩T_merged_bj_learn f
"λA S. atms_of_msu (clauses S) ⊆ atms_of_ms A
∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A ∧ finite A"
μ⇩C⇩D⇩C⇩L'_merged
"λS. inv S ∧ no_dup (trail S)"
μ⇩C⇩D⇩C⇩L'_bound
apply unfold_locales
using unbounded apply simp
using f_ge_1 apply force
apply (blast dest!: cdcl⇩N⇩O⇩T_merged_bj_learn_is_tranclp_cdcl⇩N⇩O⇩T tranclp_into_rtranclp
cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound )
apply (simp add: cdcl⇩N⇩O⇩T_decreasing_measure')
using rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_clauses_bound_card apply blast
apply (drule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_not_simplified_decreasing)
apply (auto dest!: simp: card_mono set_mset_mono )[]
apply simp
apply auto[]
using cdcl⇩N⇩O⇩T_merged_bj_learn_no_dup_inv cdcl_merged_inv apply blast
apply (auto simp: inv_restart)[]
done
lemma cdcl⇩N⇩O⇩T_restart_μ⇩C⇩D⇩C⇩L'_merged_le_μ⇩C⇩D⇩C⇩L'_bound:
assumes
"cdcl⇩N⇩O⇩T_restart T V"
"inv (fst T)" and
"no_dup (trail (fst T))" and
"atms_of_msu (clauses (fst T)) ⊆ atms_of_ms A" and
"atm_of ` lits_of (trail (fst T)) ⊆ atms_of_ms A" and
"finite A"
shows "μ⇩C⇩D⇩C⇩L'_merged A (fst V) ≤ μ⇩C⇩D⇩C⇩L'_bound A (fst T)"
using assms
proof induction
case (restart_full S T n)
show ?case
unfolding fst_conv
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_clauses_bound_card)
using restart_full unfolding full1_def by (force dest!: tranclp_into_rtranclp)+
next
case (restart_step m S T n U) note st = this(1) and U = this(3) and inv = this(4) and
n_d = this(5) and atms_clss = this(6) and atms_trail = this(7) and finite = this(8)
then have st': "cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T"
by (blast dest: relpowp_imp_rtranclp)
then have st'': "cdcl⇩N⇩O⇩T⇧*⇧* S T"
using inv n_d apply - by (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T) auto
have "inv T"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_inv)
using inv st' n_d by auto
then have "inv U"
using U by (auto simp: inv_restart)
have "atms_of_msu (clauses T) ⊆ atms_of_ms A"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_trail_clauses_bound[OF st''] inv atms_clss atms_trail n_d
by simp
then have "atms_of_msu (clauses U) ⊆ atms_of_ms A"
using U by simp
have "not_simplified_cls (clauses U) ⊆# not_simplified_cls (clauses T)"
using ‹U ∼ reduce_trail_to⇩N⇩O⇩T [] T› by auto
moreover have "not_simplified_cls (clauses T) ⊆# not_simplified_cls (clauses S)"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_not_simplified_decreasing)
using ‹(cdcl⇩N⇩O⇩T_merged_bj_learn ^^ m) S T› by (auto dest!: relpowp_imp_rtranclp)
ultimately have U_S: "not_simplified_cls (clauses U) ⊆# not_simplified_cls (clauses S)"
by auto
have "(set_mset (clauses U))
⊆ set_mset (not_simplified_cls (clauses U)) ∪ simple_clss (atms_of_ms A)"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_clauses_bound)
apply simp
using ‹inv U› apply simp
using ‹atms_of_msu (clauses U) ⊆ atms_of_ms A› apply simp
using U apply simp
using U apply simp
using finite apply simp
done
then have f1: "card (set_mset (clauses U)) ≤ card (set_mset (not_simplified_cls (clauses U))
∪ simple_clss (atms_of_ms A))"
by (simp add: simple_clss_finite card_mono local.finite)
moreover have "set_mset (not_simplified_cls (clauses U)) ∪ simple_clss (atms_of_ms A)
⊆ set_mset (not_simplified_cls (clauses S)) ∪ simple_clss (atms_of_ms A)"
using U_S by auto
then have f2:
"card (set_mset (not_simplified_cls (clauses U)) ∪ simple_clss (atms_of_ms A))
≤ card (set_mset (not_simplified_cls (clauses S)) ∪ simple_clss (atms_of_ms A))"
by (simp add: simple_clss_finite card_mono local.finite)
moreover have "card (set_mset (not_simplified_cls (clauses S))
∪ simple_clss (atms_of_ms A))
≤ card (set_mset (not_simplified_cls (clauses S))) + card (simple_clss (atms_of_ms A))"
using card_Un_le by blast
moreover have "card (simple_clss (atms_of_ms A)) ≤ 3 ^ card (atms_of_ms A)"
using atms_of_ms_finite simple_clss_card local.finite by blast
ultimately have "card (set_mset (clauses U))
≤ card (set_mset (not_simplified_cls (clauses S))) + 3 ^ card (atms_of_ms A)"
by linarith
then show ?case unfolding μ⇩C⇩D⇩C⇩L'_merged_def by auto
qed
lemma cdcl⇩N⇩O⇩T_restart_μ⇩C⇩D⇩C⇩L'_bound_le_μ⇩C⇩D⇩C⇩L'_bound:
assumes
"cdcl⇩N⇩O⇩T_restart T V" and
"no_dup (trail (fst T))" and
"inv (fst T)" and
fin: "finite A"
shows "μ⇩C⇩D⇩C⇩L'_bound A (fst V) ≤ μ⇩C⇩D⇩C⇩L'_bound A (fst T)"
using assms(1-3)
proof induction
case (restart_full S T n)
have "not_simplified_cls (clauses T) ⊆# not_simplified_cls (clauses S)"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_not_simplified_decreasing)
using ‹full1 cdcl⇩N⇩O⇩T_merged_bj_learn S T› unfolding full1_def
by (auto dest: tranclp_into_rtranclp)
then show ?case by (auto simp: card_mono set_mset_mono)
next
case (restart_step m S T n U) note st = this(1) and U = this(3) and n_d =this(4) and inv = this(5)
then have st': "cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T"
by (blast dest: relpowp_imp_rtranclp)
then have st'': "cdcl⇩N⇩O⇩T⇧*⇧* S T"
using inv n_d apply - by (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T) auto
have "inv T"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_inv)
using inv st' n_d by auto
then have "inv U"
using U by (auto simp: inv_restart)
have "not_simplified_cls (clauses U) ⊆# not_simplified_cls (clauses T)"
using ‹U ∼ reduce_trail_to⇩N⇩O⇩T [] T› by auto
moreover have "not_simplified_cls (clauses T) ⊆# not_simplified_cls (clauses S)"
apply (rule rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_not_simplified_decreasing)
using ‹(cdcl⇩N⇩O⇩T_merged_bj_learn ^^ m) S T› by (auto dest!: relpowp_imp_rtranclp)
ultimately have U_S: "not_simplified_cls (clauses U) ⊆# not_simplified_cls (clauses S)"
by auto
then show ?case by (auto simp: card_mono set_mset_mono)
qed
sublocale cdcl⇩N⇩O⇩T_increasing_restarts _ _ _ _ _ _ f "λS T. T ∼ reduce_trail_to⇩N⇩O⇩T ([]::'a list) S"
"λA S. atms_of_msu (clauses S) ⊆ atms_of_ms A
∧ atm_of ` lits_of (trail S) ⊆ atms_of_ms A ∧ finite A"
μ⇩C⇩D⇩C⇩L'_merged cdcl⇩N⇩O⇩T_merged_bj_learn
"λS. inv S ∧ no_dup (trail S)"
"λA T. ((2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))) * 2
+ card (set_mset (not_simplified_cls(clauses T)))
+ 3 ^ card (atms_of_ms A)"
apply unfold_locales
using cdcl⇩N⇩O⇩T_restart_μ⇩C⇩D⇩C⇩L'_merged_le_μ⇩C⇩D⇩C⇩L'_bound apply force
using cdcl⇩N⇩O⇩T_restart_μ⇩C⇩D⇩C⇩L'_bound_le_μ⇩C⇩D⇩C⇩L'_bound by fastforce
lemma cdcl⇩N⇩O⇩T_restart_eq_sat_iff:
assumes
"cdcl⇩N⇩O⇩T_restart S T" and
"no_dup (trail (fst S))"
"inv (fst S)"
shows "I⊨sextm clauses (fst S) ⟷ I ⊨sextm clauses (fst T)"
using assms
proof (induction rule: cdcl⇩N⇩O⇩T_restart.induct)
case (restart_full S T n)
then have "cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T "
by (simp add: tranclp_into_rtranclp full1_def)
then show ?case
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_bj_sat_ext_iff restart_full.prems(1,2)
rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T by auto
next
case (restart_step m S T n U)
then have "cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T"
by (auto simp: tranclp_into_rtranclp full1_def dest!: relpowp_imp_rtranclp)
then have "I ⊨sextm clauses S ⟷ I ⊨sextm clauses T"
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_bj_sat_ext_iff restart_step.prems(1,2)
rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T by auto
moreover have "I ⊨sextm clauses T ⟷ I ⊨sextm clauses U"
using restart_step.hyps(3) by auto
ultimately show ?case by auto
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_restart_eq_sat_iff:
assumes
"cdcl⇩N⇩O⇩T_restart⇧*⇧* S T" and
inv: "inv (fst S)" and n_d: "no_dup(trail (fst S))"
shows "I⊨sextm clauses (fst S) ⟷ I ⊨sextm clauses (fst T)"
using assms(1)
proof (induction rule: rtranclp_induct)
case base
then show ?case by simp
next
case (step T U) note st = this(1) and cdcl = this(2) and IH = this(3)
have "inv (fst T)" and "no_dup (trail (fst T))"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv using st inv n_d by blast+
then have "I⊨sextm clauses (fst T) ⟷ I ⊨sextm clauses (fst U)"
using cdcl⇩N⇩O⇩T_restart_eq_sat_iff cdcl by blast
then show ?case using IH by blast
qed
lemma cdcl⇩N⇩O⇩T_restart_all_decomposition_implies_m:
assumes
"cdcl⇩N⇩O⇩T_restart S T" and
inv: "inv (fst S)" and n_d: "no_dup(trail (fst S))" and
"all_decomposition_implies_m (clauses (fst S))
(get_all_decided_decomposition (trail (fst S)))"
shows "all_decomposition_implies_m (clauses (fst T))
(get_all_decided_decomposition (trail (fst T)))"
using assms
proof (induction)
case (restart_full S T n) note full = this(1) and inv = this(2) and n_d = this(3) and
decomp = this(4)
have st: "cdcl⇩N⇩O⇩T_merged_bj_learn⇧*⇧* S T" and
n_s: "no_step cdcl⇩N⇩O⇩T_merged_bj_learn T"
using full unfolding full1_def by (fast dest: tranclp_into_rtranclp)+
have st': "cdcl⇩N⇩O⇩T⇧*⇧* S T"
using inv rtranclp_cdcl⇩N⇩O⇩T_merged_bj_learn_is_rtranclp_cdcl⇩N⇩O⇩T_and_inv st n_d by auto
have "inv T"
using rtranclp_cdcl⇩N⇩O⇩T_cdcl⇩N⇩O⇩T_inv[OF st] inv n_d by auto
then show ?case
using cdcl⇩N⇩O⇩T.rtranclp_cdcl⇩N⇩O⇩T_all_decomposition_implies[OF _ _ n_d decomp] st' inv by auto
next
case (restart_step m S T n U) note st = this(1) and U = this(3) and inv = this(4) and
n_d = this(5) and decomp = this(6)
show ?case using U by auto
qed
lemma rtranclp_cdcl⇩N⇩O⇩T_restart_all_decomposition_implies_m:
assumes
"cdcl⇩N⇩O⇩T_restart⇧*⇧* S T" and
inv: "inv (fst S)" and n_d: "no_dup(trail (fst S))" and
decomp: "all_decomposition_implies_m (clauses (fst S))
(get_all_decided_decomposition (trail (fst S)))"
shows "all_decomposition_implies_m (clauses (fst T))
(get_all_decided_decomposition (trail (fst T)))"
using assms
proof (induction)
case base
then show ?case using decomp by simp
next
case (step T U) note st = this(1) and cdcl = this(2) and IH = this(3)[OF this(4-)] and
inv = this(4) and n_d = this(5) and decomp = this(6)
have "inv (fst T)" and "no_dup (trail (fst T))"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv using st inv n_d by blast+
then show ?case
using cdcl⇩N⇩O⇩T_restart_all_decomposition_implies_m[OF cdcl] IH by auto
qed
lemma full_cdcl⇩N⇩O⇩T_restart_normal_form:
assumes
full: "full cdcl⇩N⇩O⇩T_restart S T" and
inv: "inv (fst S)" and n_d: "no_dup(trail (fst S))" and
decomp: "all_decomposition_implies_m (clauses (fst S))
(get_all_decided_decomposition (trail (fst S)))" and
atms_cls: "atms_of_msu (clauses (fst S)) ⊆ atms_of_ms A" and
atms_trail: "atm_of ` lits_of (trail (fst S)) ⊆ atms_of_ms A" and
fin: "finite A"
shows "unsatisfiable (set_mset (clauses (fst S)))
∨ lits_of (trail (fst T)) ⊨sextm clauses (fst S) ∧ satisfiable (set_mset (clauses (fst S)))"
proof -
have inv_T: "inv (fst T)" and n_d_T: "no_dup (trail (fst T))"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_cdcl⇩N⇩O⇩T_inv using full inv n_d unfolding full_def by blast+
moreover have
atms_cls_T: "atms_of_msu (clauses (fst T)) ⊆ atms_of_ms A" and
atms_trail_T: "atm_of ` lits_of (trail (fst T)) ⊆ atms_of_ms A"
using rtranclp_cdcl⇩N⇩O⇩T_with_restart_bound_inv[of S T A] full atms_cls atms_trail fin inv n_d
unfolding full_def by blast+
ultimately have "no_step cdcl⇩N⇩O⇩T_merged_bj_learn (fst T)"
apply -
apply (rule no_step_cdcl⇩N⇩O⇩T_restart_no_step_cdcl⇩N⇩O⇩T[of _ A])
using full unfolding full_def apply simp
apply simp
using fin apply simp
done
moreover have "all_decomposition_implies_m (clauses (fst T))
(get_all_decided_decomposition (trail (fst T)))"
using rtranclp_cdcl⇩N⇩O⇩T_restart_all_decomposition_implies_m[of S T] inv n_d decomp
full unfolding full_def by auto
ultimately have "unsatisfiable (set_mset (clauses (fst T)))
∨ trail (fst T) ⊨asm clauses (fst T) ∧ satisfiable (set_mset (clauses (fst T)))"
apply -
apply (rule cdcl⇩N⇩O⇩T_merged_bj_learn_final_state)
using atms_cls_T atms_trail_T fin n_d_T fin inv_T by blast+
then consider
(unsat) "unsatisfiable (set_mset (clauses (fst T)))"
| (sat) "trail (fst T) ⊨asm clauses (fst T)" and "satisfiable (set_mset (clauses (fst T)))"
by auto
then show "unsatisfiable (set_mset (clauses (fst S)))
∨ lits_of (trail (fst T)) ⊨sextm clauses (fst S) ∧ satisfiable (set_mset (clauses (fst S)))"
proof cases
case unsat
then have "unsatisfiable (set_mset (clauses (fst S)))"
unfolding satisfiable_def apply auto
using rtranclp_cdcl⇩N⇩O⇩T_restart_eq_sat_iff[of S T ] full inv n_d
consistent_true_clss_ext_satisfiable true_clss_imp_true_cls_ext
unfolding satisfiable_def full_def by blast
then show ?thesis by blast
next
case sat
then have "lits_of (trail (fst T)) ⊨sextm clauses (fst T)"
using true_clss_imp_true_cls_ext by (auto simp: true_annots_true_cls)
then have "lits_of (trail (fst T)) ⊨sextm clauses (fst S)"
using rtranclp_cdcl⇩N⇩O⇩T_restart_eq_sat_iff[of S T] full inv n_d unfolding full_def by blast
moreover then have "satisfiable (set_mset (clauses (fst S)))"
using consistent_true_clss_ext_satisfiable distinctconsistent_interp n_d_T by fast
ultimately show ?thesis by fast
qed
qed
corollary full_cdcl⇩N⇩O⇩T_restart_normal_form_init_state:
assumes
init_state: "trail S = []" "clauses S = N" and
full: "full cdcl⇩N⇩O⇩T_restart (S, 0) T" and
inv: "inv S"
shows "unsatisfiable (set_mset N)
∨ lits_of (trail (fst T)) ⊨sextm N ∧ satisfiable (set_mset N)"
using full_cdcl⇩N⇩O⇩T_restart_normal_form[of "(S, 0)" T] assms by auto
end
end