theory CDCL_W
imports Partial_Annotated_Clausal_Logic List_More CDCL_W_Level Wellfounded_More
begin
declare set_mset_minus_replicate_mset[simp]
lemma Bex_set_set_Bex_set[iff]: "(∃x∈set_mset C. P) ⟷ (∃x∈#C. P)"
by auto
section ‹Weidenbach's CDCL›
declare upt.simps(2)[simp del]
subsection ‹The State›
locale state⇩W =
fixes
trail :: "'st ⇒ ('v, nat, 'v clause) ann_literals" and
init_clss :: "'st ⇒ 'v clauses" and
learned_clss :: "'st ⇒ 'v clauses" and
backtrack_lvl :: "'st ⇒ nat" and
conflicting :: "'st ⇒'v clause option" and
cons_trail :: "('v, nat, 'v clause) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒'st" and
add_init_cls :: "'v clause ⇒ 'st ⇒ 'st" and
add_learned_cls :: "'v clause ⇒ 'st ⇒ 'st" and
remove_cls :: "'v clause ⇒ 'st ⇒ 'st" and
update_backtrack_lvl :: "nat ⇒ 'st ⇒ 'st" and
update_conflicting :: "'v clause option ⇒ 'st ⇒ 'st" and
init_state :: "'v clauses ⇒ 'st" and
restart_state :: "'st ⇒ 'st"
assumes
trail_cons_trail[simp]:
"⋀L st. undefined_lit (trail st) (lit_of L) ⟹ trail (cons_trail L st) = L # trail st" and
trail_tl_trail[simp]: "⋀st. trail (tl_trail st) = tl (trail st)" and
trail_add_init_cls[simp]:
"⋀st C. no_dup (trail st) ⟹ trail (add_init_cls C st) = trail st" and
trail_add_learned_cls[simp]:
"⋀C st. no_dup (trail st) ⟹ trail (add_learned_cls C st) = trail st" and
trail_remove_cls[simp]:
"⋀C st. trail (remove_cls C st) = trail st" and
trail_update_backtrack_lvl[simp]: "⋀st C. trail (update_backtrack_lvl C st) = trail st" and
trail_update_conflicting[simp]: "⋀C st. trail (update_conflicting C st) = trail st" and
init_clss_cons_trail[simp]:
"⋀M st. undefined_lit (trail st) (lit_of M)⟹ init_clss (cons_trail M st) = init_clss st"
and
init_clss_tl_trail[simp]:
"⋀st. init_clss (tl_trail st) = init_clss st" and
init_clss_add_init_cls[simp]:
"⋀st C. no_dup (trail st) ⟹ init_clss (add_init_cls C st) = {#C#} + init_clss st" and
init_clss_add_learned_cls[simp]:
"⋀C st. no_dup (trail st) ⟹ init_clss (add_learned_cls C st) = init_clss st" and
init_clss_remove_cls[simp]:
"⋀C st. init_clss (remove_cls C st) = remove_mset C (init_clss st)" and
init_clss_update_backtrack_lvl[simp]:
"⋀st C. init_clss (update_backtrack_lvl C st) = init_clss st" and
init_clss_update_conflicting[simp]:
"⋀C st. init_clss (update_conflicting C st) = init_clss st" and
learned_clss_cons_trail[simp]:
"⋀M st. undefined_lit (trail st) (lit_of M) ⟹
learned_clss (cons_trail M st) = learned_clss st" and
learned_clss_tl_trail[simp]:
"⋀st. learned_clss (tl_trail st) = learned_clss st" and
learned_clss_add_init_cls[simp]:
"⋀st C. no_dup (trail st) ⟹ learned_clss (add_init_cls C st) = learned_clss st" and
learned_clss_add_learned_cls[simp]:
"⋀C st. no_dup (trail st) ⟹ learned_clss (add_learned_cls C st) = {#C#} + learned_clss st"
and
learned_clss_remove_cls[simp]:
"⋀C st. learned_clss (remove_cls C st) = remove_mset C (learned_clss st)" and
learned_clss_update_backtrack_lvl[simp]:
"⋀st C. learned_clss (update_backtrack_lvl C st) = learned_clss st" and
learned_clss_update_conflicting[simp]:
"⋀C st. learned_clss (update_conflicting C st) = learned_clss st" and
backtrack_lvl_cons_trail[simp]:
"⋀M st. undefined_lit (trail st) (lit_of M) ⟹
backtrack_lvl (cons_trail M st) = backtrack_lvl st" and
backtrack_lvl_tl_trail[simp]:
"⋀st. backtrack_lvl (tl_trail st) = backtrack_lvl st" and
backtrack_lvl_add_init_cls[simp]:
"⋀st C. no_dup (trail st) ⟹ backtrack_lvl (add_init_cls C st) = backtrack_lvl st" and
backtrack_lvl_add_learned_cls[simp]:
"⋀C st. no_dup (trail st) ⟹ backtrack_lvl (add_learned_cls C st) = backtrack_lvl st" and
backtrack_lvl_remove_cls[simp]:
"⋀C st. backtrack_lvl (remove_cls C st) = backtrack_lvl st" and
backtrack_lvl_update_backtrack_lvl[simp]:
"⋀st k. backtrack_lvl (update_backtrack_lvl k st) = k" and
backtrack_lvl_update_conflicting[simp]:
"⋀C st. backtrack_lvl (update_conflicting C st) = backtrack_lvl st" and
conflicting_cons_trail[simp]:
"⋀M st. undefined_lit (trail st) (lit_of M) ⟹
conflicting (cons_trail M st) = conflicting st" and
conflicting_tl_trail[simp]:
"⋀st. conflicting (tl_trail st) = conflicting st" and
conflicting_add_init_cls[simp]:
"⋀st C. no_dup (trail st) ⟹ conflicting (add_init_cls C st) = conflicting st" and
conflicting_add_learned_cls[simp]:
"⋀C st. no_dup (trail st) ⟹ conflicting (add_learned_cls C st) = conflicting st" and
conflicting_remove_cls[simp]:
"⋀C st. conflicting (remove_cls C st) = conflicting st" and
conflicting_update_backtrack_lvl[simp]:
"⋀st C. conflicting (update_backtrack_lvl C st) = conflicting st" and
conflicting_update_conflicting[simp]:
"⋀C st. conflicting (update_conflicting C st) = C" and
init_state_trail[simp]: "⋀N. trail (init_state N) = []" and
init_state_clss[simp]: "⋀N. init_clss (init_state N) = N" and
init_state_learned_clss[simp]: "⋀N. learned_clss (init_state N) = {#}" and
init_state_backtrack_lvl[simp]: "⋀N. backtrack_lvl (init_state N) = 0" and
init_state_conflicting[simp]: "⋀N. conflicting (init_state N) = None" and
trail_restart_state[simp]: "trail (restart_state S) = []" and
init_clss_restart_state[simp]: "init_clss (restart_state S) = init_clss S" and
learned_clss_restart_state[intro]: "learned_clss (restart_state S) ⊆# learned_clss S" and
backtrack_lvl_restart_state[simp]: "backtrack_lvl (restart_state S) = 0" and
conflicting_restart_state[simp]: "conflicting (restart_state S) = None"
begin
definition clauses :: "'st ⇒ 'v clauses" where
"clauses S = init_clss S + learned_clss S"
lemma
shows
clauses_cons_trail[simp]:
"undefined_lit (trail S) (lit_of M) ⟹clauses (cons_trail M S) = clauses S" and
clss_tl_trail[simp]: "clauses (tl_trail S) = clauses S" and
clauses_add_learned_cls_unfolded:
"no_dup (trail S) ⟹ clauses (add_learned_cls U S) = {#U#} + learned_clss S + init_clss S"
and
clauses_add_init_cls[simp]:
"no_dup (trail S) ⟹ clauses (add_init_cls N S) = {#N#} + init_clss S + learned_clss S" and
clauses_update_backtrack_lvl[simp]: "clauses (update_backtrack_lvl k S) = clauses S" and
clauses_update_conflicting[simp]: "clauses (update_conflicting D S) = clauses S" and
clauses_remove_cls[simp]:
"clauses (remove_cls C S) = clauses S - replicate_mset (count (clauses S) C) C" and
clauses_add_learned_cls[simp]:
"no_dup (trail S) ⟹ clauses (add_learned_cls C S) = {#C#} + clauses S" and
clauses_restart[simp]: "clauses (restart_state S) ⊆# clauses S" and
clauses_init_state[simp]: "⋀N. clauses (init_state N) = N"
prefer 9 using clauses_def learned_clss_restart_state apply fastforce
by (auto simp: ac_simps replicate_mset_plus clauses_def intro: multiset_eqI)
abbreviation state :: "'st ⇒ ('v, nat, 'v clause) ann_literal list × 'v clauses × 'v clauses
× nat × 'v clause option" where
"state S ≡ (trail S, init_clss S, learned_clss S, backtrack_lvl S, conflicting S)"
abbreviation incr_lvl :: "'st ⇒ 'st" where
"incr_lvl S ≡ update_backtrack_lvl (backtrack_lvl S + 1) S"
definition state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) where
"S ∼ T ⟷ state S = state T"
lemma state_eq_ref[simp, intro]:
"S ∼ S"
unfolding state_eq_def by auto
lemma state_eq_sym:
"S ∼ T ⟷ T ∼ S"
unfolding state_eq_def by auto
lemma state_eq_trans:
"S ∼ T ⟹ T ∼ U ⟹ S ∼ U"
unfolding state_eq_def by auto
lemma
shows
state_eq_trail: "S ∼ T ⟹ trail S = trail T" and
state_eq_init_clss: "S ∼ T ⟹ init_clss S = init_clss T" and
state_eq_learned_clss: "S ∼ T ⟹ learned_clss S = learned_clss T" and
state_eq_backtrack_lvl: "S ∼ T ⟹ backtrack_lvl S = backtrack_lvl T" and
state_eq_conflicting: "S ∼ T ⟹ conflicting S = conflicting T" and
state_eq_clauses: "S ∼ T ⟹ clauses S = clauses T" and
state_eq_undefined_lit: "S ∼ T ⟹ undefined_lit (trail S) L = undefined_lit (trail T) L"
unfolding state_eq_def clauses_def by auto
lemmas state_simp[simp] = state_eq_trail state_eq_init_clss state_eq_learned_clss
state_eq_backtrack_lvl state_eq_conflicting state_eq_clauses state_eq_undefined_lit
lemma atms_of_ms_learned_clss_restart_state_in_atms_of_ms_learned_clssI[intro]:
"x ∈ atms_of_msu (learned_clss (restart_state S)) ⟹ x ∈ atms_of_msu (learned_clss S)"
by (meson atms_of_ms_mono learned_clss_restart_state set_mset_mono subsetCE)
function reduce_trail_to :: "'a list ⇒ 'st ⇒ 'st" where
"reduce_trail_to F S =
(if length (trail S) = length F ∨ trail S = [] then S else reduce_trail_to F (tl_trail S))"
by fast+
termination
by (relation "measure (λ(_, S). length (trail S))") simp_all
declare reduce_trail_to.simps[simp del]
lemma
shows
reduce_trail_to_nil[simp]: "trail S = [] ⟹ reduce_trail_to F S = S" and
reduce_trail_to_eq_length[simp]: "length (trail S) = length F ⟹ reduce_trail_to F S = S"
by (auto simp: reduce_trail_to.simps)
lemma reduce_trail_to_length_ne:
"length (trail S) ≠ length F ⟹ trail S ≠ [] ⟹
reduce_trail_to F S = reduce_trail_to F (tl_trail S)"
by (auto simp: reduce_trail_to.simps)
lemma trail_reduce_trail_to_length_le:
assumes "length F > length (trail S)"
shows "trail (reduce_trail_to F S) = []"
using assms apply (induction F S rule: reduce_trail_to.induct)
by (metis (no_types, hide_lams) length_tl less_imp_diff_less less_irrefl trail_tl_trail
reduce_trail_to.simps)
lemma trail_reduce_trail_to_nil[simp]:
"trail (reduce_trail_to [] S) = []"
apply (induction "[]:: ('v, nat, 'v clause) ann_literals" S rule: reduce_trail_to.induct)
by (metis length_0_conv reduce_trail_to_length_ne reduce_trail_to_nil)
lemma clauses_reduce_trail_to_nil:
"clauses (reduce_trail_to [] S) = clauses S"
proof (induction "[]" S rule: reduce_trail_to.induct)
case (1 Sa)
then have "clauses (reduce_trail_to ([]::'a list) (tl_trail Sa)) = clauses (tl_trail Sa)
∨ trail Sa = []"
by fastforce
then show "clauses (reduce_trail_to ([]::'a list) Sa) = clauses Sa"
by (metis (no_types) length_0_conv reduce_trail_to_eq_length clss_tl_trail
reduce_trail_to_length_ne)
qed
lemma reduce_trail_to_skip_beginning:
assumes "trail S = F' @ F"
shows "trail (reduce_trail_to F S) = F"
using assms by (induction F' arbitrary: S) (auto simp: reduce_trail_to_length_ne)
lemma clauses_reduce_trail_to[simp]:
"clauses (reduce_trail_to F S) = clauses S"
apply (induction F S rule: reduce_trail_to.induct)
by (metis clss_tl_trail reduce_trail_to.simps)
lemma conflicting_update_trial[simp]:
"conflicting (reduce_trail_to F S) = conflicting S"
apply (induction F S rule: reduce_trail_to.induct)
by (metis conflicting_tl_trail reduce_trail_to.simps)
lemma backtrack_lvl_update_trial[simp]:
"backtrack_lvl (reduce_trail_to F S) = backtrack_lvl S"
apply (induction F S rule: reduce_trail_to.induct)
by (metis backtrack_lvl_tl_trail reduce_trail_to.simps)
lemma init_clss_update_trial[simp]:
"init_clss (reduce_trail_to F S) = init_clss S"
apply (induction F S rule: reduce_trail_to.induct)
by (metis init_clss_tl_trail reduce_trail_to.simps)
lemma learned_clss_update_trial[simp]:
"learned_clss (reduce_trail_to F S) = learned_clss S"
apply (induction F S rule: reduce_trail_to.induct)
by (metis learned_clss_tl_trail reduce_trail_to.simps)
lemma trail_eq_reduce_trail_to_eq:
"trail S = trail T ⟹ trail (reduce_trail_to F S) = trail (reduce_trail_to F T)"
apply (induction F S arbitrary: T rule: reduce_trail_to.induct)
by (metis trail_tl_trail reduce_trail_to.simps)
lemma reduce_trail_to_state_eq⇩N⇩O⇩T_compatible:
assumes ST: "S ∼ T"
shows "reduce_trail_to F S ∼ reduce_trail_to F T"
proof -
have "trail (reduce_trail_to F S) = trail (reduce_trail_to F T)"
using trail_eq_reduce_trail_to_eq[of S T F] ST by auto
then show ?thesis using ST by (auto simp del: state_simp simp: state_eq_def)
qed
lemma reduce_trail_to_trail_tl_trail_decomp[simp]:
"trail S = F' @ Decided K d # F ⟹ (trail (reduce_trail_to F S)) = F "
apply (rule reduce_trail_to_skip_beginning[of _ "F' @ Decided K d # []"])
by (cases F') (auto simp add:tl_append reduce_trail_to_skip_beginning)
lemma reduce_trail_to_add_learned_cls[simp]:
"no_dup (trail S) ⟹
trail (reduce_trail_to F (add_learned_cls C S)) = trail (reduce_trail_to F S)"
by (rule trail_eq_reduce_trail_to_eq) auto
lemma reduce_trail_to_add_init_cls[simp]:
"no_dup (trail S) ⟹
trail (reduce_trail_to F (add_init_cls C S)) = trail (reduce_trail_to F S)"
by (rule trail_eq_reduce_trail_to_eq) auto
lemma reduce_trail_to_remove_learned_cls[simp]:
"trail (reduce_trail_to F (remove_cls C S)) = trail (reduce_trail_to F S)"
by (rule trail_eq_reduce_trail_to_eq) auto
lemma reduce_trail_to_update_conflicting[simp]:
"trail (reduce_trail_to F (update_conflicting C S)) = trail (reduce_trail_to F S)"
by (rule trail_eq_reduce_trail_to_eq) auto
lemma reduce_trail_to_update_backtrack_lvl[simp]:
"trail (reduce_trail_to F (update_backtrack_lvl C S)) = trail (reduce_trail_to F S)"
by (rule trail_eq_reduce_trail_to_eq) auto
lemma in_get_all_decided_decomposition_decided_or_empty:
assumes "(a, b) ∈ set (get_all_decided_decomposition M)"
shows "a = [] ∨ (is_decided (hd a))"
using assms
proof (induct M arbitrary: a b)
case Nil then show ?case by simp
next
case (Cons m M)
show ?case
proof (cases m)
case (Decided l mark)
then show ?thesis using Cons by auto
next
case (Propagated l mark)
then show ?thesis using Cons by (cases "get_all_decided_decomposition M") force+
qed
qed
lemma in_get_all_decided_decomposition_trail_update_trail[simp]:
assumes H: "(L # M1, M2) ∈ set (get_all_decided_decomposition (trail S))"
shows "trail (reduce_trail_to M1 S) = M1"
proof -
obtain K mark where
L: "L = Decided K mark"
using H by (cases L) (auto dest!: in_get_all_decided_decomposition_decided_or_empty)
obtain c where
tr_S: "trail S = c @ M2 @ L # M1"
using H by auto
show ?thesis
by (rule reduce_trail_to_trail_tl_trail_decomp[of _ "c @ M2" K mark])
(auto simp: tr_S L)
qed
fun append_trail where
"append_trail [] S = S" |
"append_trail (L # M) S = append_trail M (cons_trail L S)"
lemma trail_append_trail:
"no_dup (M @ trail S) ⟹ trail (append_trail M S) = rev M @ trail S"
by (induction M arbitrary: S) (auto simp: defined_lit_map)
lemma init_clss_append_trail:
"no_dup (M @ trail S) ⟹ init_clss (append_trail M S) = init_clss S"
by (induction M arbitrary: S) (auto simp: defined_lit_map)
lemma learned_clss_append_trail:
"no_dup (M @ trail S) ⟹ learned_clss (append_trail M S) = learned_clss S"
by (induction M arbitrary: S) (auto simp: defined_lit_map)
lemma conflicting_append_trail:
"no_dup (M @ trail S) ⟹ conflicting (append_trail M S) = conflicting S"
by (induction M arbitrary: S) (auto simp: defined_lit_map)
lemma backtrack_lvl_append_trail:
"no_dup (M @ trail S) ⟹ backtrack_lvl (append_trail M S) = backtrack_lvl S"
by (induction M arbitrary: S) (auto simp: defined_lit_map)
lemma clauses_append_trail:
"no_dup (M @ trail S) ⟹ clauses (append_trail M S) = clauses S"
by (induction M arbitrary: S) (auto simp: defined_lit_map)
lemmas state_access_simp =
trail_append_trail init_clss_append_trail learned_clss_append_trail backtrack_lvl_append_trail
clauses_append_trail conflicting_append_trail
text ‹This function is useful for proofs to speak of a global trail change, but is a bad for
programs and code in general.›
fun delete_trail_and_rebuild where
"delete_trail_and_rebuild M S = append_trail (rev M) (reduce_trail_to ([]:: 'v list) S)"
end
subsection ‹Special Instantiation: using Triples as State›
subsection ‹CDCL Rules›
text ‹Because of the strategy we will later use, we distinguish propagate, conflict from the other
rules›
locale
cdcl⇩W =
state⇩W trail init_clss learned_clss backtrack_lvl conflicting cons_trail tl_trail add_init_cls
add_learned_cls remove_cls update_backtrack_lvl update_conflicting init_state
restart_state
for
trail :: "'st ⇒ ('v, nat, 'v clause) ann_literals" and
init_clss :: "'st ⇒ 'v clauses" and
learned_clss :: "'st ⇒ 'v clauses" and
backtrack_lvl :: "'st ⇒ nat" and
conflicting :: "'st ⇒'v clause option" and
cons_trail :: "('v, nat, 'v clause) ann_literal ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_init_cls :: "'v clause ⇒ 'st ⇒ 'st" and
add_learned_cls :: "'v clause ⇒ 'st ⇒ 'st" and
remove_cls :: "'v clause ⇒ 'st ⇒ 'st" and
update_backtrack_lvl :: "nat ⇒ 'st ⇒ 'st" and
update_conflicting :: "'v clause option ⇒ 'st ⇒ 'st" and
init_state :: "'v clauses ⇒ 'st" and
restart_state :: "'st ⇒ 'st"
begin
inductive propagate :: "'st ⇒ 'st ⇒ bool" where
propagate_rule[intro]:
"state S = (M, N, U, k, None) ⟹ C + {#L#} ∈# clauses S ⟹ M ⊨as CNot C
⟹ undefined_lit (trail S) L
⟹ T ∼ cons_trail (Propagated L (C + {#L#})) S
⟹ propagate S T"
inductive_cases propagateE[elim]: "propagate S T"
thm propagateE
inductive conflict :: "'st ⇒ 'st ⇒ bool" where
conflict_rule[intro]: "state S = (M, N, U, k, None) ⟹ D ∈# clauses S ⟹ M ⊨as CNot D
⟹ T ∼ update_conflicting (Some D) S
⟹ conflict S T"
inductive_cases conflictE[elim]: "conflict S S'"
inductive backtrack :: "'st ⇒ 'st ⇒ bool" where
backtrack_rule[intro]: "state S = (M, N, U, k, Some (D + {#L#}))
⟹ (Decided K (i+1) # M1, M2) ∈ set (get_all_decided_decomposition M)
⟹ get_level M L = k
⟹ get_level M L = get_maximum_level M (D+{#L#})
⟹ get_maximum_level M D = i
⟹ T ∼ cons_trail (Propagated L (D+{#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl i
(update_conflicting None S))))
⟹ backtrack S T"
inductive_cases backtrackE[elim]: "backtrack S S'"
thm backtrackE
inductive decide :: "'st ⇒ 'st ⇒ bool" where
decide_rule[intro]: "state S = (M, N, U, k, None)
⟹ undefined_lit M L ⟹ atm_of L ∈ atms_of_msu (init_clss S)
⟹ T ∼ cons_trail (Decided L (k+1)) (incr_lvl S)
⟹ decide S T"
inductive_cases decideE[elim]: "decide S S'"
thm decideE
inductive skip :: "'st ⇒ 'st ⇒ bool" where
skip_rule[intro]: "state S = (Propagated L C' # M, N, U, k, Some D) ⟹ -L ∉# D ⟹ D ≠ {#}
⟹ T ∼ tl_trail S
⟹ skip S T"
inductive_cases skipE[elim]: "skip S S'"
thm skipE
text ‹@{term "get_maximum_level (Propagated L (C + {#L#}) # M) D = k ∨ k = 0"} is equivalent to
@{term "get_maximum_level (Propagated L (C + {#L#}) # M) D = k"}›
inductive resolve :: "'st ⇒ 'st ⇒ bool" where
resolve_rule[intro]: "
state S = (Propagated L (C + {#L#}) # M, N, U, k, Some (D + {#-L#}))
⟹ get_maximum_level (Propagated L (C + {#L#}) # M) D = k
⟹ T ∼ update_conflicting (Some (D #∪ C)) (tl_trail S)
⟹ resolve S T"
inductive_cases resolveE[elim]: "resolve S S'"
thm resolveE
inductive restart :: "'st ⇒ 'st ⇒ bool" where
restart: "state S = (M, N, U, k, None) ⟹ ¬M ⊨asm clauses S
⟹ T ∼ restart_state S
⟹ restart S T"
inductive_cases restartE[elim]: "restart S T"
thm restartE
text ‹We add the condition @{term "C ∉# init_clss S"}, to maintain consistency even without the
strategy.›
inductive forget :: "'st ⇒ 'st ⇒ bool" where
forget_rule: "state S = (M, N, {#C#} + U, k, None)
⟹ ¬M ⊨asm clauses S
⟹ C ∉ set (get_all_mark_of_propagated (trail S))
⟹ C ∉# init_clss S
⟹ C ∈# learned_clss S
⟹ T ∼ remove_cls C S
⟹ forget S T"
inductive_cases forgetE[elim]: "forget S T"
inductive cdcl⇩W_rf :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
restart: "restart S T ⟹ cdcl⇩W_rf S T" |
forget: "forget S T ⟹ cdcl⇩W_rf S T"
inductive cdcl⇩W_bj :: "'st ⇒ 'st ⇒ bool" where
skip[intro]: "skip S S' ⟹ cdcl⇩W_bj S S'" |
resolve[intro]: "resolve S S' ⟹ cdcl⇩W_bj S S'" |
backtrack[intro]: "backtrack S S' ⟹ cdcl⇩W_bj S S'"
inductive_cases cdcl⇩W_bjE: "cdcl⇩W_bj S T"
inductive cdcl⇩W_o:: "'st ⇒ 'st ⇒ bool" for S :: 'st where
decide[intro]: "decide S S' ⟹ cdcl⇩W_o S S'" |
bj[intro]: "cdcl⇩W_bj S S' ⟹ cdcl⇩W_o S S'"
inductive cdcl⇩W :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
propagate: "propagate S S' ⟹ cdcl⇩W S S'" |
conflict: "conflict S S' ⟹ cdcl⇩W S S'" |
other: "cdcl⇩W_o S S' ⟹ cdcl⇩W S S'"|
rf: "cdcl⇩W_rf S S' ⟹ cdcl⇩W S S'"
lemma rtranclp_propagate_is_rtranclp_cdcl⇩W:
"propagate⇧*⇧* S S' ⟹ cdcl⇩W⇧*⇧* S S'"
by (induction rule: rtranclp_induct) (fastforce dest!: propagate)+
lemma cdcl⇩W_all_rules_induct[consumes 1, case_names propagate conflict forget restart decide skip
resolve backtrack]:
fixes S :: "'st"
assumes
cdcl⇩W: "cdcl⇩W S S'" and
propagate: "⋀T. propagate S T ⟹ P S T" and
conflict: "⋀T. conflict S T ⟹ P S T" and
forget: "⋀T. forget S T ⟹ P S T" and
restart: "⋀T. restart S T ⟹ P S T" and
decide: "⋀T. decide S T ⟹ P S T" and
skip: "⋀T. skip S T ⟹ P S T" and
resolve: "⋀T. resolve S T ⟹ P S T" and
backtrack: "⋀T. backtrack S T ⟹ P S T"
shows "P S S'"
using assms(1)
proof (induct S' rule: cdcl⇩W.induct)
case (propagate S') note propagate = this(1)
then show ?case using assms(2) by auto
next
case (conflict S')
then show ?case using assms(3) by auto
next
case (other S')
then show ?case
proof (induct rule: cdcl⇩W_o.induct)
case (decide U)
then show ?case using assms(6) by auto
next
case (bj S')
then show ?case using assms(7-9) by (induction rule: cdcl⇩W_bj.induct) auto
qed
next
case (rf S')
then show ?case
by (induct rule: cdcl⇩W_rf.induct) (fast dest: forget restart)+
qed
lemma cdcl⇩W_all_induct[consumes 1, case_names propagate conflict forget restart decide skip
resolve backtrack]:
fixes S :: "'st"
assumes
cdcl⇩W: "cdcl⇩W S S'" and
propagateH: "⋀C L T. C + {#L#} ∈# clauses S ⟹ trail S ⊨as CNot C
⟹ undefined_lit (trail S) L ⟹ conflicting S = None
⟹ T ∼ cons_trail (Propagated L (C + {#L#})) S
⟹ P S T" and
conflictH: "⋀D T. D ∈# clauses S ⟹ conflicting S = None ⟹ trail S ⊨as CNot D
⟹ T ∼ update_conflicting (Some D) S
⟹ P S T" and
forgetH: "⋀C T. ¬trail S ⊨asm clauses S
⟹ C ∉ set (get_all_mark_of_propagated (trail S))
⟹ C ∉# init_clss S
⟹ C ∈# learned_clss S
⟹ conflicting S = None
⟹ T ∼ remove_cls C S
⟹ P S T" and
restartH: "⋀T. ¬trail S ⊨asm clauses S
⟹ conflicting S = None
⟹ T ∼ restart_state S
⟹ P S T" and
decideH: "⋀L T. conflicting S = None ⟹ undefined_lit (trail S) L
⟹ atm_of L ∈ atms_of_msu (init_clss S)
⟹ T ∼ cons_trail (Decided L (backtrack_lvl S +1)) (incr_lvl S)
⟹ P S T" and
skipH: "⋀L C' M D T. trail S = Propagated L C' # M
⟹ conflicting S = Some D ⟹ -L ∉# D ⟹ D ≠ {#}
⟹ T ∼ tl_trail S
⟹ P S T" and
resolveH: "⋀L C M D T.
trail S = Propagated L ( (C + {#L#})) # M
⟹ conflicting S = Some (D + {#-L#})
⟹ get_maximum_level (Propagated L (C + {#L#}) # M) D = backtrack_lvl S
⟹ T ∼ (update_conflicting (Some (D #∪ C)) (tl_trail S))
⟹ P S T" and
backtrackH: "⋀K i M1 M2 L D T.
(Decided K (Suc i) # M1, M2) ∈ set (get_all_decided_decomposition (trail S))
⟹ get_level (trail S) L = backtrack_lvl S
⟹ conflicting S = Some (D + {#L#})
⟹ get_maximum_level (trail S) (D+{#L#}) = get_level (trail S) L
⟹ get_maximum_level (trail S) D ≡ i
⟹ T ∼ cons_trail (Propagated L (D+{#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl i
(update_conflicting None S))))
⟹ P S T"
shows "P S S'"
using cdcl⇩W
proof (induct S S' rule: cdcl⇩W_all_rules_induct)
case (propagate S')
then show ?case by (elim propagateE) (frule propagateH; simp)
next
case (conflict S')
then show ?case by (elim conflictE) (frule conflictH; simp)
next
case (restart S')
then show ?case by (elim restartE) (frule restartH; simp)
next
case (decide T)
then show ?case by (elim decideE) (frule decideH; simp)
next
case (backtrack S')
then show ?case by (elim backtrackE) (frule backtrackH; simp del: state_simp add: state_eq_def)
next
case (forget S')
then show ?case using forgetH by auto
next
case (skip S')
then show ?case using skipH by auto
next
case (resolve S')
then show ?case by (elim resolveE) (frule resolveH; simp)
qed
lemma cdcl⇩W_o_induct[consumes 1, case_names decide skip resolve backtrack]:
fixes S :: "'st"
assumes cdcl⇩W: "cdcl⇩W_o S T" and
decideH: "⋀L T. conflicting S = None ⟹ undefined_lit (trail S) L
⟹ atm_of L ∈ atms_of_msu (init_clss S)
⟹ T ∼ cons_trail (Decided L (backtrack_lvl S +1)) (incr_lvl S)
⟹ P S T" and
skipH: "⋀L C' M D T. trail S = Propagated L C' # M
⟹ conflicting S = Some D ⟹ -L ∉# D ⟹ D ≠ {#}
⟹ T ∼ tl_trail S
⟹ P S T" and
resolveH: "⋀L C M D T.
trail S = Propagated L ( (C + {#L#})) # M
⟹ conflicting S = Some (D + {#-L#})
⟹ get_maximum_level (Propagated L (C + {#L#}) # M) D = backtrack_lvl S
⟹ T ∼ update_conflicting (Some (D #∪ C)) (tl_trail S)
⟹ P S T" and
backtrackH: "⋀K i M1 M2 L D T.
(Decided K (Suc i) # M1, M2) ∈ set (get_all_decided_decomposition (trail S))
⟹ get_level (trail S) L = backtrack_lvl S
⟹ conflicting S = Some (D + {#L#})
⟹ get_level (trail S) L = get_maximum_level (trail S) (D+{#L#})
⟹ get_maximum_level (trail S) D ≡ i
⟹ T ∼ cons_trail (Propagated L (D+{#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl i
(update_conflicting None S))))
⟹ P S T"
shows "P S T"
using cdcl⇩W apply (induct T rule: cdcl⇩W_o.induct)
using assms(2) apply auto[1]
apply (elim cdcl⇩W_bjE skipE resolveE backtrackE)
apply (frule skipH; simp)
apply (frule resolveH; simp)
apply (frule backtrackH; simp_all del: state_simp add: state_eq_def)
done
thm cdcl⇩W_o.induct
lemma cdcl⇩W_o_all_rules_induct[consumes 1, case_names decide backtrack skip resolve]:
fixes S T :: 'st
assumes
"cdcl⇩W_o S T" and
"⋀T. decide S T ⟹ P S T" and
"⋀T. backtrack S T ⟹ P S T" and
"⋀T. skip S T ⟹ P S T" and
"⋀T. resolve S T ⟹ P S T"
shows "P S T"
using assms by (induct T rule: cdcl⇩W_o.induct) (auto simp: cdcl⇩W_bj.simps)
lemma cdcl⇩W_o_rule_cases[consumes 1, case_names decide backtrack skip resolve]:
fixes S T :: 'st
assumes
"cdcl⇩W_o S T" and
"decide S T ⟹ P" and
"backtrack S T ⟹ P" and
"skip S T ⟹ P" and
"resolve S T ⟹ P"
shows P
using assms by (auto simp: cdcl⇩W_o.simps cdcl⇩W_bj.simps)
subsection ‹Invariants›
subsubsection ‹Properties of the trail›
text ‹We here establish that:
* the marks are exactly 1..k where k is the level
* the consistency of the trail
* the fact that there is no duplicate in the trail.›
lemma backtrack_lit_skiped:
assumes L: "get_level (trail S) L = backtrack_lvl S"
and M1: "(Decided K (i + 1) # M1, M2) ∈ set (get_all_decided_decomposition (trail S))"
and no_dup: "no_dup (trail S)"
and bt_l: "backtrack_lvl S = length (get_all_levels_of_decided (trail S))"
and order: "get_all_levels_of_decided (trail S)
= rev ([1..<(1+length (get_all_levels_of_decided (trail S)))])"
shows "atm_of L ∉ atm_of ` lits_of M1"
proof
let ?M = "trail S"
assume L_in_M1: "atm_of L ∈ atm_of ` lits_of M1"
obtain c where Mc: "trail S = c @ M2 @ Decided K (i + 1) # M1" using M1 by blast
have "atm_of L ∉ atm_of ` lits_of c"
using L_in_M1 no_dup mk_disjoint_insert unfolding Mc lits_of_def by force
have g_M_eq_g_M1: "get_level ?M L = get_level M1 L"
using L_in_M1 unfolding Mc by auto
have g: "get_all_levels_of_decided M1 = rev [1..<Suc i]"
using order unfolding Mc
by (auto simp del: upt_simps dest!: append_cons_eq_upt_length_i
simp add: rev_swap[symmetric])
then have "Max (set (0 # get_all_levels_of_decided (rev M1))) < Suc i" by auto
then have "get_level M1 L < Suc i"
using get_rev_level_less_max_get_all_levels_of_decided[of "rev M1" 0 L] by linarith
moreover have "Suc i ≤ backtrack_lvl S" using bt_l by (simp add: Mc g)
ultimately show False using L g_M_eq_g_M1 by auto
qed
lemma cdcl⇩W_distinctinv_1:
assumes
"cdcl⇩W S S'" and
"no_dup (trail S)" and
"backtrack_lvl S = length (get_all_levels_of_decided (trail S))" and
"get_all_levels_of_decided (trail S) = rev [1..<1+length (get_all_levels_of_decided (trail S))]"
shows "no_dup (trail S')"
using assms
proof (induct rule: cdcl⇩W_all_induct)
case (backtrack K i M1 M2 L D T) note decomp = this(1) and L = this(2) and T = this(6) and
n_d = this(7)
obtain c where Mc: "trail S = c @ M2 @ Decided K (i + 1) # M1"
using decomp by auto
have "no_dup (M2 @ Decided K (i + 1) # M1)"
using Mc n_d by fastforce
moreover have "atm_of L ∉ (λl. atm_of (lit_of l)) ` set M1"
using backtrack_lit_skiped[of S L K i M1 M2] L decomp backtrack.prems
by (fastforce simp: lits_of_def)
moreover then have "undefined_lit M1 L"
by (simp add: defined_lit_map)
ultimately show ?case using decomp T n_d by simp
qed (auto simp: defined_lit_map)
lemma cdcl⇩W_consistent_inv_2:
assumes
"cdcl⇩W S S'" and
"no_dup (trail S)" and
"backtrack_lvl S = length (get_all_levels_of_decided (trail S))" and
"get_all_levels_of_decided (trail S) = rev [1..<1+length (get_all_levels_of_decided (trail S))]"
shows "consistent_interp (lits_of (trail S'))"
using cdcl⇩W_distinctinv_1[OF assms] distinctconsistent_interp by fast
lemma cdcl⇩W_o_bt:
assumes
"cdcl⇩W_o S S'" and
"backtrack_lvl S = length (get_all_levels_of_decided (trail S))" and
"get_all_levels_of_decided (trail S) =
rev ([1..<(1+length (get_all_levels_of_decided (trail S)))])" and
n_d[simp]: "no_dup (trail S)"
shows "backtrack_lvl S' = length (get_all_levels_of_decided (trail S'))"
using assms
proof (induct rule: cdcl⇩W_o_induct)
case (backtrack K i M1 M2 L D T) note decomp = this(1) and T = this(6) and level = this(8)
have [simp]: "trail (reduce_trail_to M1 S) = M1"
using decomp by auto
obtain c where M: "trail S = c @ M2 @ Decided K (i + 1) # M1" using decomp by auto
have "rev (get_all_levels_of_decided (trail S))
= [1..<1+ (length (get_all_levels_of_decided (trail S)))]"
using level by (auto simp: rev_swap[symmetric])
moreover have "atm_of L ∉ (λl. atm_of (lit_of l)) ` set M1"
using backtrack_lit_skiped[of S L K i M1 M2] backtrack(2,7,8,9) decomp
by (fastforce simp add: lits_of_def)
moreover then have "undefined_lit M1 L"
by (simp add: defined_lit_map)
moreover then have "no_dup (trail T)"
using T decomp n_d by (auto simp: defined_lit_map M)
ultimately show ?case
using T n_d unfolding M by (auto dest!: append_cons_eq_upt_length simp del: upt_simps)
qed auto
lemma cdcl⇩W_rf_bt:
assumes
"cdcl⇩W_rf S S'" and
"backtrack_lvl S = length (get_all_levels_of_decided (trail S))" and
"get_all_levels_of_decided (trail S) = rev [1..<(1+length (get_all_levels_of_decided (trail S)))]"
shows "backtrack_lvl S' = length (get_all_levels_of_decided (trail S'))"
using assms by (induct rule: cdcl⇩W_rf.induct) auto
lemma cdcl⇩W_bt:
assumes
"cdcl⇩W S S'" and
"backtrack_lvl S = length (get_all_levels_of_decided (trail S))" and
"get_all_levels_of_decided (trail S)
= rev ([1..<(1+length (get_all_levels_of_decided (trail S)))])" and
"no_dup (trail S)"
shows "backtrack_lvl S' = length (get_all_levels_of_decided (trail S'))"
using assms by (induct rule: cdcl⇩W.induct) (auto simp add: cdcl⇩W_o_bt cdcl⇩W_rf_bt)
lemma cdcl⇩W_bt_level':
assumes
"cdcl⇩W S S'" and
"backtrack_lvl S = length (get_all_levels_of_decided (trail S))" and
"get_all_levels_of_decided (trail S)
= rev ([1..<(1+length (get_all_levels_of_decided (trail S)))])" and
n_d: "no_dup (trail S)"
shows "get_all_levels_of_decided (trail S')
= rev ([1..<(1+length (get_all_levels_of_decided (trail S')))])"
using assms
proof (induct rule: cdcl⇩W_all_induct)
case (decide L T) note undef = this(2) and T = this(4)
let ?k = "backtrack_lvl S"
let ?M = "trail S"
let ?M' = "Decided L (?k + 1) # trail S"
have H: "get_all_levels_of_decided ?M = rev [Suc 0..<1+length (get_all_levels_of_decided ?M)]"
using decide.prems by simp
have k: "?k = length (get_all_levels_of_decided ?M)"
using decide.prems by auto
have "get_all_levels_of_decided ?M' = Suc ?k # get_all_levels_of_decided ?M" by simp
then have "get_all_levels_of_decided ?M' = Suc ?k #
rev [Suc 0..<1+length (get_all_levels_of_decided ?M)]"
using H by auto
moreover have "… = rev [Suc 0..< Suc (1+length (get_all_levels_of_decided ?M))]"
unfolding k by simp
finally show ?case using T undef by (auto simp add: defined_lit_map)
next
case (backtrack K i M1 M2 L D T) note decomp = this(1) and confli = this(2) and T =this(6) and
all_decided = this(8) and bt_lvl = this(7)
have "atm_of L ∉ (λl. atm_of (lit_of l)) ` set M1"
using backtrack_lit_skiped[of S L K i M1 M2] backtrack(2,7,8,9) decomp
by (fastforce simp add: lits_of_def)
moreover then have "undefined_lit M1 L"
by (simp add: defined_lit_map)
then have [simp]: "trail T = Propagated L (D + {#L#}) # M1"
using T decomp n_d by auto
obtain c where M: "trail S = c @ M2 @ Decided K (i + 1) # M1" using decomp by auto
have "get_all_levels_of_decided (rev (trail S))
= [Suc 0..<2+length (get_all_levels_of_decided c) + (length (get_all_levels_of_decided M2)
+ length (get_all_levels_of_decided M1))]"
using all_decided bt_lvl unfolding M by (auto simp add: rev_swap[symmetric] simp del: upt_simps)
then show ?case
using T by (auto simp add: rev_swap M dest!: append_cons_eq_upt(1) simp del: upt_simps)
qed auto
text ‹We write @{term "1+length (get_all_levels_of_decided (trail S))"} instead of
@{term "backtrack_lvl S"} to avoid non termination of rewriting.›
definition "cdcl⇩W_M_level_inv (S:: 'st) ⟷
consistent_interp (lits_of (trail S))
∧ no_dup (trail S)
∧ backtrack_lvl S = length (get_all_levels_of_decided (trail S))
∧ get_all_levels_of_decided (trail S)
= rev ([1..<1+length (get_all_levels_of_decided (trail S))])"
lemma cdcl⇩W_M_level_inv_decomp:
assumes "cdcl⇩W_M_level_inv S"
shows "consistent_interp (lits_of (trail S))"
and "no_dup (trail S)"
using assms unfolding cdcl⇩W_M_level_inv_def by fastforce+
lemma cdcl⇩W_consistent_inv:
fixes S S' :: 'st
assumes
"cdcl⇩W S S'" and
"cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_M_level_inv S'"
using assms cdcl⇩W_consistent_inv_2 cdcl⇩W_distinctinv_1 cdcl⇩W_bt cdcl⇩W_bt_level'
unfolding cdcl⇩W_M_level_inv_def by meson+
lemma rtranclp_cdcl⇩W_consistent_inv:
assumes "cdcl⇩W⇧*⇧* S S'"
and "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_M_level_inv S'"
using assms by (induct rule: rtranclp_induct)
(auto intro: cdcl⇩W_consistent_inv)
lemma tranclp_cdcl⇩W_consistent_inv:
assumes "cdcl⇩W⇧+⇧+ S S'"
and "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_M_level_inv S'"
using assms by (induct rule: tranclp_induct)
(auto intro: cdcl⇩W_consistent_inv)
lemma cdcl⇩W_M_level_inv_S0_cdcl⇩W[simp]:
"cdcl⇩W_M_level_inv (init_state N)"
unfolding cdcl⇩W_M_level_inv_def by auto
lemma cdcl⇩W_M_level_inv_get_level_le_backtrack_lvl:
assumes inv: "cdcl⇩W_M_level_inv S"
shows "get_level (trail S) L ≤ backtrack_lvl S"
proof -
have "get_all_levels_of_decided (trail S) = rev [1..<1 + backtrack_lvl S]"
using inv unfolding cdcl⇩W_M_level_inv_def by auto
then show ?thesis
using get_rev_level_less_max_get_all_levels_of_decided[of "rev (trail S)" 0 L]
by (auto simp: Max_n_upt)
qed
lemma backtrack_ex_decomp:
assumes M_l: "cdcl⇩W_M_level_inv S"
and i_S: "i < backtrack_lvl S"
shows "∃K M1 M2. (Decided K (i + 1) # M1, M2) ∈ set (get_all_decided_decomposition (trail S))"
proof -
let ?M = "trail S"
have
g: "get_all_levels_of_decided (trail S) = rev [Suc 0..<Suc (backtrack_lvl S)]"
using M_l unfolding cdcl⇩W_M_level_inv_def by simp_all
then have "i+1 ∈ set (get_all_levels_of_decided (trail S))"
using i_S by auto
then obtain c K c' where tr_S: "trail S = c @ Decided K (i + 1) # c'"
using in_get_all_levels_of_decided_iff_decomp[of "i+1" "trail S"] by auto
obtain M1 M2 where "(Decided K (i + 1) # M1, M2) ∈ set (get_all_decided_decomposition (trail S))"
unfolding tr_S apply (induct c rule: ann_literal_list_induct)
apply auto[2]
apply (rename_tac L m xs,
case_tac "hd (get_all_decided_decomposition (xs @ Decided K (Suc i) # c'))")
apply (case_tac "get_all_decided_decomposition (xs @ Decided K (Suc i) # c')")
by auto
then show ?thesis by blast
qed
subsubsection ‹Better-Suited Induction Principle›
text ‹We generalise the induction principle defined previously: the induction case for
@{term backtrack} now includes the assumption that @{term "undefined_lit M1 L"}. This helps
the simplifier and thus the automation.›
lemma backtrack_induction_lev[consumes 1, case_names M_devel_inv backtrack]:
assumes
bt: "backtrack S T" and
inv: "cdcl⇩W_M_level_inv S" and
backtrackH: "⋀K i M1 M2 L D T.
(Decided K (Suc i) # M1, M2) ∈ set (get_all_decided_decomposition (trail S))
⟹ get_level (trail S) L = backtrack_lvl S
⟹ conflicting S = Some (D + {#L#})
⟹ get_level (trail S) L = get_maximum_level (trail S) (D+{#L#})
⟹ get_maximum_level (trail S) D ≡ i
⟹ undefined_lit M1 L
⟹ T ∼ cons_trail (Propagated L (D+{#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl i
(update_conflicting None S))))
⟹ P S T"
shows "P S T"
proof -
obtain K i M1 M2 L D where
decomp: "(Decided K (Suc i) # M1, M2) ∈ set (get_all_decided_decomposition (trail S))" and
L: "get_level (trail S) L = backtrack_lvl S" and
confl: "conflicting S = Some (D + {#L#})" and
lev_L: "get_level (trail S) L = get_maximum_level (trail S) (D+{#L#})" and
lev_D: "get_maximum_level (trail S) D ≡ i" and
T: "T ∼ cons_trail (Propagated L (D+{#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl i
(update_conflicting None S))))"
using bt by (elim backtrackE) metis
have "atm_of L ∉ (λl. atm_of (lit_of l)) ` set M1"
using backtrack_lit_skiped[of S L K i M1 M2] L decomp bt confl lev_L lev_D inv
unfolding cdcl⇩W_M_level_inv_def
by (fastforce simp add: lits_of_def)
then have "undefined_lit M1 L"
by (auto simp: defined_lit_map)
then show ?thesis
using backtrackH[OF decomp L confl lev_L lev_D _ T] by simp
qed
lemmas backtrack_induction_lev2 = backtrack_induction_lev[consumes 2, case_names backtrack]
lemma cdcl⇩W_all_induct_lev_full:
fixes S :: "'st"
assumes
cdcl⇩W: "cdcl⇩W S S'" and
inv[simp]: "cdcl⇩W_M_level_inv S" and
propagateH: "⋀C L T. C + {#L#} ∈# clauses S ⟹ trail S ⊨as CNot C
⟹ undefined_lit (trail S) L ⟹ conflicting S = None
⟹ T ∼ cons_trail (Propagated L (C + {#L#})) S
⟹ cdcl⇩W_M_level_inv S
⟹ P S T" and
conflictH: "⋀D T. D ∈# clauses S ⟹ conflicting S = None ⟹ trail S ⊨as CNot D
⟹ T ∼ update_conflicting (Some D) S
⟹ P S T" and
forgetH: "⋀C T. ¬trail S ⊨asm clauses S
⟹ C ∉ set (get_all_mark_of_propagated (trail S))
⟹ C ∉# init_clss S
⟹ C ∈# learned_clss S
⟹ conflicting S = None
⟹ T ∼ remove_cls C S
⟹ cdcl⇩W_M_level_inv S
⟹ P S T" and
restartH: "⋀T. ¬trail S ⊨asm clauses S
⟹ conflicting S = None
⟹ T ∼ restart_state S
⟹ cdcl⇩W_M_level_inv S
⟹ P S T" and
decideH: "⋀L T. conflicting S = None ⟹ undefined_lit (trail S) L
⟹ atm_of L ∈ atms_of_msu (init_clss S)
⟹ T ∼ cons_trail (Decided L (backtrack_lvl S +1)) (incr_lvl S)
⟹ cdcl⇩W_M_level_inv S
⟹ P S T" and
skipH: "⋀L C' M D T. trail S = Propagated L C' # M
⟹ conflicting S = Some D ⟹ -L ∉# D ⟹ D ≠ {#}
⟹ T ∼ tl_trail S
⟹ cdcl⇩W_M_level_inv S
⟹ P S T" and
resolveH: "⋀L C M D T.
trail S = Propagated L ( (C + {#L#})) # M
⟹ conflicting S = Some (D + {#-L#})
⟹ get_maximum_level (Propagated L (C + {#L#}) # M) D = backtrack_lvl S
⟹ T ∼ (update_conflicting (Some (D #∪ C)) (tl_trail S))
⟹ cdcl⇩W_M_level_inv S
⟹ P S T" and
backtrackH: "⋀K i M1 M2 L D T.
(Decided K (Suc i) # M1, M2) ∈ set (get_all_decided_decomposition (trail S))
⟹ get_level (trail S) L = backtrack_lvl S
⟹ conflicting S = Some (D + {#L#})
⟹ get_maximum_level (trail S) (D+{#L#}) = get_level (trail S) L
⟹ get_maximum_level (trail S) D ≡ i
⟹ undefined_lit M1 L
⟹ T ∼ cons_trail (Propagated L (D+{#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl i
(update_conflicting None S))))
⟹ cdcl⇩W_M_level_inv S
⟹ P S T"
shows "P S S'"
using cdcl⇩W
proof (induct S' rule: cdcl⇩W_all_rules_induct)
case (propagate S')
then show ?case by (elim propagateE) (frule propagateH; simp)
next
case (conflict S')
then show ?case by (elim conflictE) (frule conflictH; simp)
next
case (restart S')
then show ?case by (elim restartE) (frule restartH; simp)
next
case (decide T)
then show ?case by (elim decideE) (frule decideH; simp)
next
case (backtrack S')
then show ?case
apply (induction rule: backtrack_induction_lev)
apply (rule inv)
by (rule backtrackH;
fastforce simp del: state_simp simp add: state_eq_def dest!: HOL.meta_eq_to_obj_eq)
next
case (forget S')
then show ?case using forgetH by auto
next
case (skip S')
then show ?case using skipH by auto
next
case (resolve S')
then show ?case by (elim resolveE) (frule resolveH; simp)
qed
lemmas cdcl⇩W_all_induct_lev2 = cdcl⇩W_all_induct_lev_full[consumes 2, case_names propagate conflict
forget restart decide skip resolve backtrack]
lemmas cdcl⇩W_all_induct_lev = cdcl⇩W_all_induct_lev_full[consumes 1, case_names lev_inv propagate
conflict forget restart decide skip resolve backtrack]
thm cdcl⇩W_o_induct
lemma cdcl⇩W_o_induct_lev[consumes 1, case_names M_lev decide skip resolve backtrack]:
fixes S :: "'st"
assumes
cdcl⇩W: "cdcl⇩W_o S T" and
inv[simp]: "cdcl⇩W_M_level_inv S" and
decideH: "⋀L T. conflicting S = None ⟹ undefined_lit (trail S) L
⟹ atm_of L ∈ atms_of_msu (init_clss S)
⟹ T ∼ cons_trail (Decided L (backtrack_lvl S +1)) (incr_lvl S)
⟹ cdcl⇩W_M_level_inv S
⟹ P S T" and
skipH: "⋀L C' M D T. trail S = Propagated L C' # M
⟹ conflicting S = Some D ⟹ -L ∉# D ⟹ D ≠ {#}
⟹ T ∼ tl_trail S
⟹ cdcl⇩W_M_level_inv S
⟹ P S T" and
resolveH: "⋀L C M D T.
trail S = Propagated L ( (C + {#L#})) # M
⟹ conflicting S = Some (D + {#-L#})
⟹ get_maximum_level (Propagated L (C + {#L#}) # M) D = backtrack_lvl S
⟹ T ∼ update_conflicting (Some (D #∪ C)) (tl_trail S)
⟹ cdcl⇩W_M_level_inv S
⟹ P S T" and
backtrackH: "⋀K i M1 M2 L D T.
(Decided K (Suc i) # M1, M2) ∈ set (get_all_decided_decomposition (trail S))
⟹ get_level (trail S) L = backtrack_lvl S
⟹ conflicting S = Some (D + {#L#})
⟹ get_level (trail S) L = get_maximum_level (trail S) (D+{#L#})
⟹ get_maximum_level (trail S) D ≡ i
⟹ undefined_lit M1 L
⟹ T ∼ cons_trail (Propagated L (D+{#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl i
(update_conflicting None S))))
⟹ cdcl⇩W_M_level_inv S
⟹ P S T"
shows "P S T"
using cdcl⇩W
proof (induct S T rule: cdcl⇩W_o_all_rules_induct)
case (decide T)
then show ?case by (elim decideE) (frule decideH; simp)
next
case (backtrack S')
then show ?case
using inv apply (induction rule: backtrack_induction_lev2)
by (rule backtrackH)
(fastforce simp del: state_simp simp add: state_eq_def dest!: HOL.meta_eq_to_obj_eq)+
next
case (skip S')
then show ?case using skipH by auto
next
case (resolve S')
then show ?case by (elim resolveE) (frule resolveH; simp)
qed
lemmas cdcl⇩W_o_induct_lev2 = cdcl⇩W_o_induct_lev[consumes 2, case_names decide skip resolve
backtrack]
subsubsection ‹Compatibility with @{term state_eq}›
lemma propagate_state_eq_compatible:
assumes
"propagate S T" and
"S ∼ S'" and
"T ∼ T'"
shows "propagate S' T'"
using assms apply (elim propagateE)
apply (rule propagate_rule)
by (auto simp: state_eq_def clauses_def simp del: state_simp)
lemma conflict_state_eq_compatible:
assumes
"conflict S T" and
"S ∼ S'" and
"T ∼ T'"
shows "conflict S' T'"
using assms apply (elim conflictE)
apply (rule conflict_rule)
by (auto simp: state_eq_def clauses_def simp del: state_simp)
lemma backtrack_state_eq_compatible:
assumes
"backtrack S T" and
"S ∼ S'" and
"T ∼ T'" and
inv: "cdcl⇩W_M_level_inv S"
shows "backtrack S' T'"
using assms apply (induction rule: backtrack_induction_lev)
using inv apply simp
apply (rule backtrack_rule)
apply auto[5]
by (auto simp: state_eq_def clauses_def cdcl⇩W_M_level_inv_def simp del: state_simp)
lemma decide_state_eq_compatible:
assumes
"decide S T" and
"S ∼ S'" and
"T ∼ T'"
shows "decide S' T'"
using assms apply (elim decideE)
apply (rule decide_rule)
by (auto simp: state_eq_def clauses_def simp del: state_simp)
lemma skip_state_eq_compatible:
assumes
"skip S T" and
"S ∼ S'" and
"T ∼ T'"
shows "skip S' T'"
using assms apply (elim skipE)
apply (rule skip_rule)
by (auto simp: state_eq_def clauses_def HOL.eq_sym_conv[of "_ # _" "trail _"]
simp del: state_simp dest: arg_cong[of "_ # trail _" "trail _" tl])
lemma resolve_state_eq_compatible:
assumes
"resolve S T" and
"S ∼ S'" and
"T ∼ T'"
shows "resolve S' T'"
using assms apply (elim resolveE)
apply (rule resolve_rule)
by (auto simp: state_eq_def clauses_def HOL.eq_sym_conv[of "_ # _" "trail _"]
simp del: state_simp dest: arg_cong[of "_ # trail _" "trail _" tl])
lemma forget_state_eq_compatible:
assumes
"forget S T" and
"S ∼ S'" and
"T ∼ T'"
shows "forget S' T'"
using assms apply (elim forgetE)
apply (rule forget_rule)
by (auto simp: state_eq_def clauses_def HOL.eq_sym_conv[of "{#_#} + _" "_"]
simp del: state_simp dest: arg_cong[of "_ # trail _" "trail _" tl])
lemma cdcl⇩W_state_eq_compatible:
assumes
"cdcl⇩W S T" and "¬restart S T" and
"S ∼ S'" and
"T ∼ T'" and
inv: "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W S' T'"
using assms by (meson assms backtrack_state_eq_compatible bj cdcl⇩W.simps cdcl⇩W_bj.simps
cdcl⇩W_o_rule_cases cdcl⇩W_rf.cases cdcl⇩W_rf.restart conflict_state_eq_compatible decide
decide_state_eq_compatible forget forget_state_eq_compatible
propagate_state_eq_compatible resolve_state_eq_compatible
skip_state_eq_compatible)
lemma cdcl⇩W_bj_state_eq_compatible:
assumes
"cdcl⇩W_bj S T" and "cdcl⇩W_M_level_inv S"
"S ∼ S'" and
"T ∼ T'"
shows "cdcl⇩W_bj S' T'"
using assms
by induction (auto
intro: skip_state_eq_compatible backtrack_state_eq_compatible resolve_state_eq_compatible)
lemma tranclp_cdcl⇩W_bj_state_eq_compatible:
assumes
"cdcl⇩W_bj⇧+⇧+ S T" and inv: "cdcl⇩W_M_level_inv S" and
"S ∼ S'" and
"T ∼ T'"
shows "cdcl⇩W_bj⇧+⇧+ S' T'"
using assms
proof (induction arbitrary: S' T')
case base
then show ?case
using cdcl⇩W_bj_state_eq_compatible by blast
next
case (step T U) note IH = this(3)[OF this(4-5)]
have "cdcl⇩W⇧+⇧+ S T"
using tranclp_mono[of cdcl⇩W_bj cdcl⇩W] other step.hyps(1) by blast
then have "cdcl⇩W_M_level_inv T"
using inv tranclp_cdcl⇩W_consistent_inv by blast
then have "cdcl⇩W_bj⇧+⇧+ T T'"
using ‹U ∼ T'› cdcl⇩W_bj_state_eq_compatible[of T U] ‹cdcl⇩W_bj T U› by auto
then show ?case
using IH[of T] by auto
qed
subsubsection ‹Conservation of some Properties›
lemma level_of_decided_ge_1:
assumes
"cdcl⇩W S S'" and
inv: "cdcl⇩W_M_level_inv S" and
"∀L l. Decided L l ∈ set (trail S) ⟶ l > 0"
shows "∀L l. Decided L l ∈ set (trail S') ⟶ l > 0"
using assms apply (induct rule: cdcl⇩W_all_induct_lev2)
by (auto dest: union_in_get_all_decided_decomposition_is_subset simp: cdcl⇩W_M_level_inv_decomp)
lemma cdcl⇩W_o_no_more_init_clss:
assumes
"cdcl⇩W_o S S'" and
inv: "cdcl⇩W_M_level_inv S"
shows "init_clss S = init_clss S'"
using assms by (induct rule: cdcl⇩W_o_induct_lev2) (auto simp: cdcl⇩W_M_level_inv_decomp)
lemma tranclp_cdcl⇩W_o_no_more_init_clss:
assumes
"cdcl⇩W_o⇧+⇧+ S S'" and
inv: "cdcl⇩W_M_level_inv S"
shows "init_clss S = init_clss S'"
using assms apply (induct rule: tranclp.induct)
by (auto dest: cdcl⇩W_o_no_more_init_clss
dest!: tranclp_cdcl⇩W_consistent_inv dest: tranclp_mono_explicit[of cdcl⇩W_o _ _ cdcl⇩W]
simp: other)
lemma rtranclp_cdcl⇩W_o_no_more_init_clss:
assumes
"cdcl⇩W_o⇧*⇧* S S'" and
inv: "cdcl⇩W_M_level_inv S"
shows "init_clss S = init_clss S'"
using assms unfolding rtranclp_unfold by (auto intro: tranclp_cdcl⇩W_o_no_more_init_clss)
lemma cdcl⇩W_init_clss:
"cdcl⇩W S T ⟹ cdcl⇩W_M_level_inv S ⟹ init_clss S = init_clss T"
by (induct rule: cdcl⇩W_all_induct_lev2) (auto simp: cdcl⇩W_M_level_inv_def)
lemma rtranclp_cdcl⇩W_init_clss:
"cdcl⇩W⇧*⇧* S T ⟹ cdcl⇩W_M_level_inv S ⟹ init_clss S = init_clss T"
by (induct rule: rtranclp_induct) (auto dest: cdcl⇩W_init_clss rtranclp_cdcl⇩W_consistent_inv)
lemma tranclp_cdcl⇩W_init_clss:
"cdcl⇩W⇧+⇧+ S T ⟹ cdcl⇩W_M_level_inv S ⟹ init_clss S = init_clss T"
using rtranclp_cdcl⇩W_init_clss[of S T] unfolding rtranclp_unfold by auto
subsubsection ‹Learned Clause›
text ‹This invariant shows that:
▪ the learned clauses are entailed by the initial set of clauses.
▪ the conflicting clause is entailed by the initial set of clauses.
▪ the marks are entailed by the clauses. A more precise version would be to show that either
these decided are learned or are in the set of clauses›
definition "cdcl⇩W_learned_clause (S:: 'st) ⟷
(init_clss S ⊨psm learned_clss S
∧ (∀T. conflicting S = Some T ⟶ init_clss S ⊨pm T)
∧ set (get_all_mark_of_propagated (trail S)) ⊆ set_mset (clauses S))"
lemma cdcl⇩W_learned_clause_S0_cdcl⇩W[simp]:
"cdcl⇩W_learned_clause (init_state N)"
unfolding cdcl⇩W_learned_clause_def by auto
lemma cdcl⇩W_learned_clss:
assumes
"cdcl⇩W S S'" and
learned: "cdcl⇩W_learned_clause S" and
lev_inv: "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_learned_clause S'"
using assms(1) lev_inv learned
proof (induct rule: cdcl⇩W_all_induct_lev2)
case (backtrack K i M1 M2 L D T) note decomp = this(1) and confl = this(3) and undef = this(6)
and T =this(7)
show ?case
using decomp confl learned undef T lev_inv unfolding cdcl⇩W_learned_clause_def
by (auto dest!: get_all_decided_decomposition_exists_prepend
simp: clauses_def cdcl⇩W_M_level_inv_decomp dest: true_clss_clss_left_right)
next
case (resolve L C M D) note trail = this(1) and confl = this(2) and lvl = this(3) and
T =this(4)
moreover
have "init_clss S ⊨psm learned_clss S"
using learned trail unfolding cdcl⇩W_learned_clause_def clauses_def by auto
then have "init_clss S ⊨pm C + {#L#}"
using trail learned unfolding cdcl⇩W_learned_clause_def clauses_def
by (auto dest: true_clss_clss_in_imp_true_clss_cls)
ultimately show ?case
using learned
by (auto dest: mk_disjoint_insert true_clss_clss_left_right
simp add: cdcl⇩W_learned_clause_def clauses_def
intro: true_clss_cls_union_mset_true_clss_cls_or_not_true_clss_cls_or)
next
case (restart T)
then show ?case
using learned_clss_restart_state[of T]
by (auto dest!: get_all_decided_decomposition_exists_prepend
simp: clauses_def state_eq_def cdcl⇩W_learned_clause_def
simp del: state_simp
dest: true_clss_clssm_subsetE)
next
case propagate
then show ?case using learned by (auto simp: cdcl⇩W_learned_clause_def clauses_def)
next
case conflict
then show ?case using learned
by (auto simp: cdcl⇩W_learned_clause_def clauses_def true_clss_clss_in_imp_true_clss_cls)
next
case forget
then show ?case
using learned by (auto simp: cdcl⇩W_learned_clause_def clauses_def split: split_if_asm)
qed (auto simp: cdcl⇩W_learned_clause_def clauses_def)
lemma rtranclp_cdcl⇩W_learned_clss:
assumes
"cdcl⇩W⇧*⇧* S S'" and
"cdcl⇩W_M_level_inv S"
"cdcl⇩W_learned_clause S"
shows "cdcl⇩W_learned_clause S'"
using assms by induction (auto dest: cdcl⇩W_learned_clss intro: rtranclp_cdcl⇩W_consistent_inv)
subsubsection ‹No alien atom in the state›
text ‹This invariant means that all the literals are in the set of clauses.›
definition "no_strange_atm S' ⟷ (
(∀T. conflicting S' = Some T ⟶ atms_of T ⊆ atms_of_msu (init_clss S'))
∧ (∀L mark. Propagated L mark ∈ set (trail S')
⟶ atms_of ( mark) ⊆ atms_of_msu (init_clss S'))
∧ atms_of_msu (learned_clss S') ⊆ atms_of_msu (init_clss S')
∧ atm_of ` (lits_of (trail S')) ⊆ atms_of_msu (init_clss S'))"
lemma no_strange_atm_decomp:
assumes "no_strange_atm S"
shows "conflicting S = Some T ⟹ atms_of T ⊆ atms_of_msu (init_clss S)"
and "(∀L mark. Propagated L mark ∈ set (trail S)
⟶ atms_of ( mark) ⊆ atms_of_msu (init_clss S))"
and "atms_of_msu (learned_clss S) ⊆ atms_of_msu (init_clss S)"
and "atm_of ` (lits_of (trail S)) ⊆ atms_of_msu (init_clss S)"
using assms unfolding no_strange_atm_def by blast+
lemma no_strange_atm_S0 [simp]: "no_strange_atm (init_state N)"
unfolding no_strange_atm_def by auto
lemma cdcl⇩W_no_strange_atm_explicit:
assumes
"cdcl⇩W S S'" and
lev: "cdcl⇩W_M_level_inv S" and
conf: "∀T. conflicting S = Some T ⟶ atms_of T ⊆ atms_of_msu (init_clss S)" and
decided: "∀L mark. Propagated L mark ∈ set (trail S)
⟶ atms_of mark ⊆ atms_of_msu (init_clss S)" and
learned: "atms_of_msu (learned_clss S) ⊆ atms_of_msu (init_clss S)" and
trail: "atm_of ` (lits_of (trail S)) ⊆ atms_of_msu (init_clss S)"
shows "(∀T. conflicting S' = Some T ⟶ atms_of T ⊆ atms_of_msu (init_clss S')) ∧
(∀L mark. Propagated L mark ∈ set (trail S')
⟶ atms_of ( mark) ⊆ atms_of_msu (init_clss S')) ∧
atms_of_msu (learned_clss S') ⊆ atms_of_msu (init_clss S') ∧
atm_of ` (lits_of (trail S')) ⊆ atms_of_msu (init_clss S')" (is "?C S' ∧ ?M S' ∧ ?U S' ∧ ?V S'")
using assms(1,2)
proof (induct rule: cdcl⇩W_all_induct_lev2)
case (propagate C L T) note C_L = this(1) and undef = this(3) and confl = this(4) and T =this(5)
have "?C (cons_trail (Propagated L (C + {#L#})) S)" using confl undef by auto
moreover
have "atms_of (C + {#L#}) ⊆ atms_of_msu (init_clss S)"
by (metis (no_types) atms_of_atms_of_ms_mono atms_of_ms_union clauses_def mem_set_mset_iff
C_L learned set_mset_union sup.orderE)
then have "?M (cons_trail (Propagated L (C + {#L#})) S)" using undef
by (simp add: decided)
moreover have "?U (cons_trail (Propagated L (C + {#L#})) S)"
using learned undef by auto
moreover have "?V (cons_trail (Propagated L (C + {#L#})) S)"
using C_L learned trail undef unfolding clauses_def
by (auto simp: in_plus_implies_atm_of_on_atms_of_ms)
ultimately show ?case using T by auto
next
case (decide L)
then show ?case using learned decided conf trail unfolding clauses_def by auto
next
case (skip L C M D)
then show ?case using learned decided conf trail by auto
next
case (conflict D T) note T =this(4)
have D: "atm_of ` set_mset D ⊆ ⋃(atms_of ` (set_mset (clauses S)))"
using ‹D ∈# clauses S› by (auto simp add: atms_of_def atms_of_ms_def)
moreover {
fix xa :: "'v literal"
assume a1: "atm_of ` set_mset D ⊆ (⋃x∈set_mset (init_clss S). atms_of x)
∪ (⋃x∈set_mset (learned_clss S). atms_of x)"
assume a2: "(⋃x∈set_mset (learned_clss S). atms_of x) ⊆ (⋃x∈set_mset (init_clss S). atms_of x)"
assume "xa ∈# D"
then have "atm_of xa ∈ UNION (set_mset (init_clss S)) atms_of"
using a2 a1 by (metis (no_types) Un_iff atm_of_lit_in_atms_of atms_of_def subset_Un_eq)
then have "∃m∈set_mset (init_clss S). atm_of xa ∈ atms_of m"
by blast
} note H = this
ultimately show ?case using conflict.prems T learned decided conf trail
unfolding atms_of_def atms_of_ms_def clauses_def
by (auto simp add: H )
next
case (restart T)
then show ?case using learned decided conf trail by auto
next
case (forget C T) note C = this(3) and C_le = this(4) and confl = this(5) and
T = this(6)
have H: "⋀L mark. Propagated L mark ∈ set (trail S) ⟹ atms_of mark ⊆ atms_of_msu (init_clss S)"
using decided by simp
show ?case unfolding clauses_def apply standard
using conf T trail C unfolding clauses_def apply (auto dest!: H)[]
apply standard
using T trail C apply (auto dest!: H)[]
apply standard
using T learned C C_le atms_of_ms_remove_subset[of "set_mset (learned_clss S)"] apply (auto)[]
using T trail C apply (auto simp: clauses_def lits_of_def)[]
done
next
case (backtrack K i M1 M2 L D T) note decomp = this(1) and confl = this(3) and undef= this(6)
and T =this(7)
have "?C T"
using conf T decomp undef lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
moreover have "set M1 ⊆ set (trail S)"
using backtrack.hyps(1) by auto
then have M: "?M T"
using decided conf undef confl T decomp lev
by (auto simp: image_subset_iff clauses_def cdcl⇩W_M_level_inv_decomp)
moreover have "?U T"
using learned decomp conf confl T undef lev unfolding clauses_def
by (auto simp: cdcl⇩W_M_level_inv_decomp)
moreover have "?V T"
using M conf confl trail T undef decomp lev by (force simp: cdcl⇩W_M_level_inv_decomp)
ultimately show ?case by blast
next
case (resolve L C M D T) note trail_S = this(1) and confl = this(2) and T = this(4)
let ?T = "update_conflicting (Some (remdups_mset (D + C))) (tl_trail S)"
have "?C ?T"
using confl trail_S conf decided by simp
moreover have "?M ?T"
using confl trail_S conf decided by auto
moreover have "?U ?T"
using trail learned by auto
moreover have "?V ?T"
using confl trail_S trail by auto
ultimately show ?case using T by auto
qed
lemma cdcl⇩W_no_strange_atm_inv:
assumes "cdcl⇩W S S'" and "no_strange_atm S" and "cdcl⇩W_M_level_inv S"
shows "no_strange_atm S'"
using cdcl⇩W_no_strange_atm_explicit[OF assms(1)] assms(2,3) unfolding no_strange_atm_def by fast
lemma rtranclp_cdcl⇩W_no_strange_atm_inv:
assumes "cdcl⇩W⇧*⇧* S S'" and "no_strange_atm S" and "cdcl⇩W_M_level_inv S"
shows "no_strange_atm S'"
using assms by induction (auto intro: cdcl⇩W_no_strange_atm_inv rtranclp_cdcl⇩W_consistent_inv)
subsubsection ‹No duplicates all around›
text ‹This invariant shows that there is no duplicate (no literal appearing twice in the formula).
The last part could be proven using the previous invariant moreover.›
definition "distinct_cdcl⇩W_state (S::'st)
⟷ ((∀T. conflicting S = Some T ⟶ distinct_mset T)
∧ distinct_mset_mset (learned_clss S)
∧ distinct_mset_mset (init_clss S)
∧ (∀L mark. (Propagated L mark ∈ set (trail S) ⟶ distinct_mset (mark))))"
lemma distinct_cdcl⇩W_state_decomp:
assumes "distinct_cdcl⇩W_state (S::'st)"
shows "∀T. conflicting S = Some T ⟶ distinct_mset T"
and "distinct_mset_mset (learned_clss S)"
and "distinct_mset_mset (init_clss S)"
and "∀L mark. (Propagated L mark ∈ set (trail S) ⟶ distinct_mset ( mark))"
using assms unfolding distinct_cdcl⇩W_state_def by blast+
lemma distinct_cdcl⇩W_state_decomp_2:
assumes "distinct_cdcl⇩W_state (S::'st)"
shows "conflicting S = Some T ⟹ distinct_mset T"
using assms unfolding distinct_cdcl⇩W_state_def by auto
lemma distinct_cdcl⇩W_state_S0_cdcl⇩W[simp]:
"distinct_mset_mset N ⟹ distinct_cdcl⇩W_state (init_state N)"
unfolding distinct_cdcl⇩W_state_def by auto
lemma distinct_cdcl⇩W_state_inv:
assumes
"cdcl⇩W S S'" and
"cdcl⇩W_M_level_inv S" and
"distinct_cdcl⇩W_state S"
shows "distinct_cdcl⇩W_state S'"
using assms
proof (induct rule: cdcl⇩W_all_induct_lev2)
case (backtrack K i M1 M2 L D)
then show ?case
unfolding distinct_cdcl⇩W_state_def
by (fastforce dest: get_all_decided_decomposition_incl simp: cdcl⇩W_M_level_inv_decomp)
next
case restart
then show ?case unfolding distinct_cdcl⇩W_state_def distinct_mset_set_def clauses_def
using learned_clss_restart_state[of S] by auto
next
case resolve
then show ?case
by (auto simp add: distinct_cdcl⇩W_state_def distinct_mset_set_def clauses_def
distinct_mset_single_add
intro!: distinct_mset_union_mset)
qed (auto simp add: distinct_cdcl⇩W_state_def distinct_mset_set_def clauses_def)
lemma rtanclp_distinct_cdcl⇩W_state_inv:
assumes
"cdcl⇩W⇧*⇧* S S'" and
"cdcl⇩W_M_level_inv S" and
"distinct_cdcl⇩W_state S"
shows "distinct_cdcl⇩W_state S'"
using assms apply (induct rule: rtranclp_induct)
using distinct_cdcl⇩W_state_inv rtranclp_cdcl⇩W_consistent_inv by blast+
subsubsection ‹Conflicts and co›
text ‹This invariant shows that each mark contains a contradiction only related to the previously
defined variable.›
abbreviation every_mark_is_a_conflict :: "'st ⇒ bool" where
"every_mark_is_a_conflict S ≡
∀L mark a b. a @ Propagated L mark # b = (trail S)
⟶ (b ⊨as CNot ( mark - {#L#}) ∧ L ∈# mark)"
definition "cdcl⇩W_conflicting S ≡
(∀T. conflicting S = Some T ⟶ trail S ⊨as CNot T)
∧ every_mark_is_a_conflict S"
lemma backtrack_atms_of_D_in_M1:
fixes M1 :: "('v, nat, 'v clause) ann_literals"
assumes
inv: "cdcl⇩W_M_level_inv S" and
undef: "undefined_lit M1 L" and
i: "get_maximum_level (trail S) D = i" and
decomp: "(Decided K (Suc i) # M1, M2)
∈ set (get_all_decided_decomposition (trail S))" and
S_lvl: "backtrack_lvl S = get_maximum_level (trail S) (D + {#L#})" and
S_confl: "conflicting S = Some (D + {#L#})" and
undef: "undefined_lit M1 L" and
T: "T ∼ (cons_trail (Propagated L (D+{#L#}))
(reduce_trail_to M1
(add_learned_cls (D + {#L#})
(update_backtrack_lvl i
(update_conflicting None S)))))" and
confl: "∀T. conflicting S = Some T ⟶ trail S ⊨as CNot T"
shows "atms_of D ⊆ atm_of ` lits_of (tl (trail T))"
proof (rule ccontr)
let ?k = "get_maximum_level (trail S) (D + {#L#})"
have "trail S ⊨as CNot D" using confl S_confl by auto
then have vars_of_D: "atms_of D ⊆ atm_of ` lits_of (trail S)" unfolding atms_of_def
by (meson image_subsetI mem_set_mset_iff true_annots_CNot_all_atms_defined)
obtain M0 where M: "trail S = M0 @ M2 @ Decided K (Suc i) # M1"
using decomp by auto
have max: "get_maximum_level (trail S) (D + {#L#})
= length (get_all_levels_of_decided (M0 @ M2 @ Decided K (Suc i) # M1))"
using inv unfolding cdcl⇩W_M_level_inv_def S_lvl M by simp
assume a: "¬ ?thesis"
then obtain L' where
L': "L' ∈ atms_of D" and
L'_notin_M1: "L' ∉ atm_of ` lits_of M1"
using T undef decomp inv by (auto simp: cdcl⇩W_M_level_inv_decomp)
then have L'_in: "L' ∈ atm_of ` lits_of (M0 @ M2 @ Decided K (i + 1) # [])"
using vars_of_D unfolding M by force
then obtain L'' where
"L'' ∈# D" and
L'': "L' = atm_of L''"
using L' L'_notin_M1 unfolding atms_of_def by auto
have lev_L'':
"get_level (trail S) L'' = get_rev_level (Decided K (Suc i) # rev M2 @ rev M0) (Suc i) L''"
using L'_notin_M1 L'' M by (auto simp del: get_rev_level.simps)
have "get_all_levels_of_decided (trail S) = rev [1..<1+?k]"
using inv S_lvl unfolding cdcl⇩W_M_level_inv_def by auto
then have "get_all_levels_of_decided (M0 @ M2)
= rev [Suc (Suc i)..<Suc (get_maximum_level (trail S) (D + {#L#}))]"
unfolding M by (auto simp:rev_swap[symmetric] dest!: append_cons_eq_upt_length_i_end)
then have M: "get_all_levels_of_decided M0 @ get_all_levels_of_decided M2
= rev [Suc (Suc i)..<Suc (length (get_all_levels_of_decided (M0 @ M2 @ Decided K (Suc i) # M1)))]"
unfolding max unfolding M by simp
have "get_rev_level (Decided K (Suc i) # rev (M0 @ M2)) (Suc i) L''
≥ Min (set ((Suc i) # get_all_levels_of_decided (Decided K (Suc i) # rev (M0 @ M2))))"
using get_rev_level_ge_min_get_all_levels_of_decided[of L''
"rev (M0 @ M2 @ [Decided K (Suc i)])" "Suc i"] L'_in
unfolding L'' by (fastforce simp add: lits_of_def)
also have "Min (set ((Suc i) # get_all_levels_of_decided (Decided K (Suc i) # rev (M0 @ M2))))
= Min (set ((Suc i) # get_all_levels_of_decided (rev (M0 @ M2))))" by auto
also have "… = Min (set ((Suc i) # get_all_levels_of_decided M0 @ get_all_levels_of_decided M2))"
by (simp add: Un_commute)
also have "… = Min (set ((Suc i) # [Suc (Suc i)..<2 + length (get_all_levels_of_decided M0)
+ (length (get_all_levels_of_decided M2) + length (get_all_levels_of_decided M1))]))"
unfolding M by (auto simp add: Un_commute)
also have "… = Suc i" by (auto intro: Min_eqI)
finally have "get_rev_level (Decided K (Suc i) # rev (M0 @ M2)) (Suc i) L'' ≥ Suc i" .
then have "get_level (trail S) L'' ≥ i + 1"
using lev_L'' by simp
then have "get_maximum_level (trail S) D ≥ i + 1"
using get_maximum_level_ge_get_level[OF ‹L'' ∈# D›, of "trail S"] by auto
then show False using i by auto
qed
lemma distinct_atms_of_incl_not_in_other:
assumes
a1: "no_dup (M @ M')" and a2:
"atms_of D ⊆ atm_of ` lits_of M'"
shows "∀x∈atms_of D. x ∉ atm_of ` lits_of M"
proof -
{ fix aa :: 'a
have ff1: "⋀l ms. undefined_lit ms l ∨ atm_of l
∈ set (map (λm. atm_of (lit_of (m::('a, 'b, 'c) ann_literal))) ms)"
by (simp add: defined_lit_map)
have ff2: "⋀a. a ∉ atms_of D ∨ a ∈ atm_of ` lits_of M'"
using a2 by (meson subsetCE)
have ff3: "⋀a. a ∉ set (map (λm. atm_of (lit_of m)) M')
∨ a ∉ set (map (λm. atm_of (lit_of m)) M)"
using a1 by (metis (lifting) IntI distinct_append empty_iff map_append)
have "∀L a f. ∃l. ((a::'a) ∉ f ` L ∨ (l::'a literal) ∈ L) ∧ (a ∉ f ` L ∨ f l = a)"
by blast
then have "aa ∉ atms_of D ∨ aa ∉ atm_of ` lits_of M"
using ff3 ff2 ff1 by (metis (no_types) Decided_Propagated_in_iff_in_lits_of) }
then show ?thesis
by blast
qed
lemma cdcl⇩W_propagate_is_conclusion:
assumes
"cdcl⇩W S S'" and
inv: "cdcl⇩W_M_level_inv S" and
decomp: "all_decomposition_implies_m (init_clss S) (get_all_decided_decomposition (trail S))" and
learned: "cdcl⇩W_learned_clause S" and
confl: "∀T. conflicting S = Some T ⟶ trail S ⊨as CNot T" and
alien: "no_strange_atm S"
shows "all_decomposition_implies_m (init_clss S') (get_all_decided_decomposition (trail S'))"
using assms(1,2)
proof (induct rule: cdcl⇩W_all_induct_lev2)
case restart
then show ?case by auto
next
case forget
then show ?case using decomp by auto
next
case conflict
then show ?case using decomp by auto
next
case (resolve L C M D) note tr = this(1) and T = this(4)
let ?decomp = "get_all_decided_decomposition M"
have M: "set ?decomp = insert (hd ?decomp) (set (tl ?decomp))"
by (cases ?decomp) auto
show ?case
using decomp tr T unfolding all_decomposition_implies_def
by (cases "hd (get_all_decided_decomposition M)")
(auto simp: M)
next
case (skip L C' M D) note tr = this(1) and T = this(5)
have M: "set (get_all_decided_decomposition M)
= insert (hd (get_all_decided_decomposition M)) (set (tl (get_all_decided_decomposition M)))"
by (cases "get_all_decided_decomposition M") auto
show ?case
using decomp tr T unfolding all_decomposition_implies_def
by (cases "hd (get_all_decided_decomposition M)")
(auto simp add: M)
next
case decide note S = this(1) and undef = this(2) and T = this(4)
show ?case using decomp T undef unfolding S all_decomposition_implies_def by auto
next
case (propagate C L T) note propa = this(2) and undef = this(3) and T =this(5)
obtain a y where ay: "hd (get_all_decided_decomposition (trail S)) = (a, y)"
by (cases "hd (get_all_decided_decomposition (trail S))")
then have M: "trail S = y @ a" using get_all_decided_decomposition_decomp by blast
have M': "set (get_all_decided_decomposition (trail S))
= insert (a, y) (set (tl (get_all_decided_decomposition (trail S))))"
using ay by (cases "get_all_decided_decomposition (trail S)") auto
have "unmark a ∪ set_mset (init_clss S) ⊨ps unmark y"
using decomp ay unfolding all_decomposition_implies_def
by (cases "get_all_decided_decomposition (trail S)") fastforce+
then have a_Un_N_M: "unmark a ∪ set_mset (init_clss S)
⊨ps unmark (trail S)"
unfolding M by (auto simp add: all_in_true_clss_clss image_Un)
have "unmark a ∪ set_mset (init_clss S) ⊨p {#L#}" (is "?I ⊨p _")
proof (rule true_clss_cls_plus_CNot)
show "?I ⊨p C + {#L#}"
using propa propagate.prems learned confl unfolding M
by (metis Un_iff cdcl⇩W_learned_clause_def clauses_def mem_set_mset_iff propagate.hyps(1)
set_mset_union true_clss_clss_in_imp_true_clss_cls true_clss_cs_mono_l2
union_trus_clss_clss)
next
have "(λm. {#lit_of m#}) ` set (trail S) ⊨ps CNot C"
using ‹(trail S) ⊨as CNot C› true_annots_true_clss_clss by blast
then show "?I ⊨ps CNot C"
using a_Un_N_M true_clss_clss_left_right true_clss_clss_union_l_r by blast
qed
moreover have "⋀aa b.
∀ (Ls, seen)∈set (get_all_decided_decomposition (y @ a)).
unmark Ls ∪ set_mset (init_clss S) ⊨ps unmark seen
⟹ (aa, b) ∈ set (tl (get_all_decided_decomposition (y @ a)))
⟹ unmark aa ∪ set_mset (init_clss S) ⊨ps unmark b"
by (metis (no_types, lifting) case_prod_conv get_all_decided_decomposition_never_empty_sym
list.collapse list.set_intros(2))
ultimately show ?case
using decomp T undef unfolding ay all_decomposition_implies_def
using M ‹unmark a ∪ set_mset (init_clss S) ⊨ps unmark y›
ay by auto
next
case (backtrack K i M1 M2 L D T) note decomp' = this(1) and lev_L = this(2) and conf = this(3) and
undef = this(6) and T = this(7)
have "∀l ∈ set M2. ¬is_decided l"
using get_all_decided_decomposition_snd_not_decided backtrack.hyps(1) by blast
obtain M0 where M: "trail S = M0 @ M2 @ Decided K (i + 1) # M1"
using decomp' by auto
show ?case unfolding all_decomposition_implies_def
proof
fix x
assume "x ∈set (get_all_decided_decomposition (trail T))"
then have x: "x ∈ set (get_all_decided_decomposition (Propagated L ((D + {#L#})) # M1))"
using T decomp' undef inv by (simp add: cdcl⇩W_M_level_inv_decomp)
let ?m = "get_all_decided_decomposition (Propagated L ((D + {#L#})) # M1)"
let ?hd = "hd ?m"
let ?tl = "tl ?m"
have "x = ?hd ∨ x ∈ set ?tl"
using x by (cases "?m") auto
moreover {
assume "x ∈ set ?tl"
then have "x ∈ set (get_all_decided_decomposition (trail S))"
using tl_get_all_decided_decomposition_skip_some[of x] by (simp add: list.set_sel(2) M)
then have "case x of (Ls, seen) ⇒ unmark Ls
∪ set_mset (init_clss (T))
⊨ps unmark seen"
using decomp learned decomp confl alien inv T undef M
unfolding all_decomposition_implies_def cdcl⇩W_M_level_inv_def
by auto
}
moreover {
assume "x = ?hd"
obtain M1' M1'' where M1: "hd (get_all_decided_decomposition M1) = (M1', M1'')"
by (cases "hd (get_all_decided_decomposition M1)")
then have x': "x = (M1', Propagated L ( (D + {#L#})) # M1'')"
using ‹x= ?hd› by auto
have "(M1', M1'') ∈ set (get_all_decided_decomposition (trail S))"
using M1[symmetric] hd_get_all_decided_decomposition_skip_some[OF M1[symmetric],
of "M0 @ M2" _ "i+1"] unfolding M by fastforce
then have 1: "unmark M1' ∪ set_mset (init_clss S)
⊨ps unmark M1''"
using decomp unfolding all_decomposition_implies_def by auto
moreover
have "trail S ⊨as CNot D" using conf confl by auto
then have vars_of_D: "atms_of D ⊆ atm_of ` lits_of (trail S)"
unfolding atms_of_def
by (meson image_subsetI mem_set_mset_iff true_annots_CNot_all_atms_defined)
have vars_of_D: "atms_of D ⊆ atm_of ` lits_of M1"
using backtrack_atms_of_D_in_M1[of S M1 L D i K M2 T] backtrack inv conf confl
by (auto simp: cdcl⇩W_M_level_inv_decomp)
have "no_dup (trail S)" using inv by (auto simp: cdcl⇩W_M_level_inv_decomp)
then have vars_in_M1:
"∀x ∈ atms_of D. x ∉ atm_of ` lits_of (M0 @ M2 @ Decided K (i + 1) # [])"
using vars_of_D distinct_atms_of_incl_not_in_other[of "M0 @M2 @ Decided K (i + 1) # []"
M1]
unfolding M by auto
have "M1 ⊨as CNot D"
using vars_in_M1 true_annots_remove_if_notin_vars[of "M0 @ M2 @ Decided K (i + 1) # []"
M1 "CNot D"] ‹trail S ⊨as CNot D› unfolding M lits_of_def by simp
have "M1 = M1'' @ M1'" by (simp add: M1 get_all_decided_decomposition_decomp)
have TT: "unmark M1' ∪ set_mset (init_clss S) ⊨ps CNot D"
using true_annots_true_clss_cls[OF ‹M1 ⊨as CNot D›] true_clss_clss_left_right[OF 1,
of "CNot D"] unfolding ‹M1 = M1'' @ M1'› by (auto simp add: inf_sup_aci(5,7))
have "init_clss S ⊨pm D + {#L#}"
using conf learned cdcl⇩W_learned_clause_def confl by blast
then have T': "unmark M1' ∪ set_mset (init_clss S) ⊨p D + {#L#}" by auto
have "atms_of (D + {#L#}) ⊆ atms_of_msu (clauses S)"
using alien conf unfolding no_strange_atm_def clauses_def by auto
then have "unmark M1' ∪ set_mset (init_clss S) ⊨p {#L#}"
using true_clss_cls_plus_CNot[OF T' TT] by auto
ultimately
have "case x of (Ls, seen) ⇒ unmark Ls
∪ set_mset (init_clss T)
⊨ps unmark seen" using T' T decomp' undef inv unfolding x'
by (simp add: cdcl⇩W_M_level_inv_decomp)
}
ultimately show "case x of (Ls, seen) ⇒ unmark Ls ∪ set_mset (init_clss T)
⊨ps unmark seen" using T by auto
qed
qed
lemma cdcl⇩W_propagate_is_false:
assumes
"cdcl⇩W S S'" and
lev: "cdcl⇩W_M_level_inv S" and
learned: "cdcl⇩W_learned_clause S" and
decomp: "all_decomposition_implies_m (init_clss S) (get_all_decided_decomposition (trail S))" and
confl: "∀T. conflicting S = Some T ⟶ trail S ⊨as CNot T" and
alien: "no_strange_atm S" and
mark_confl: "every_mark_is_a_conflict S"
shows "every_mark_is_a_conflict S'"
using assms(1,2)
proof (induct rule: cdcl⇩W_all_induct_lev2)
case (propagate C L T) note undef = this(3) and T =this(5)
show ?case
proof (intro allI impI)
fix L' mark a b
assume "a @ Propagated L' mark # b = trail T"
then have "(a=[] ∧ L = L' ∧ mark = C + {#L#} ∧ b = trail S)
∨ tl a @ Propagated L' mark # b = trail S"
using T undef by (cases a) fastforce+
moreover {
assume "tl a @ Propagated L' mark # b = trail S"
then have "b ⊨as CNot ( mark - {#L'#}) ∧ L' ∈# mark"
using mark_confl by auto
}
moreover {
assume "a=[]" and "L = L'" and " mark = C + {#L#}" and "b = trail S"
then have "b ⊨as CNot ( mark - {#L#}) ∧ L ∈# mark"
using ‹trail S ⊨as CNot C› by auto
}
ultimately show "b ⊨as CNot ( mark - {#L'#}) ∧ L' ∈# mark" by blast
qed
next
case (decide L) note undef[simp] = this(2) and T = this(4)
have "⋀a La mark b. a @ Propagated La mark # b = Decided L (backtrack_lvl S+1) # trail S
⟹ tl a @ Propagated La mark # b = trail S" by (case_tac a, auto)
then show ?case using mark_confl T unfolding decide.hyps(1) by fastforce
next
case (skip L C' M D T) note tr = this(1) and T = this(5)
show ?case
proof (intro allI impI)
fix L' mark a b
assume "a @ Propagated L' mark # b = trail T"
then have "a @ Propagated L' mark # b = M" using tr T by simp
then have "(Propagated L C' # a) @ Propagated L' mark # b = Propagated L C' # M" by auto
moreover have "∀La mark a b. a @ Propagated La mark # b = Propagated L C' # M
⟶ b ⊨as CNot ( mark - {#La#}) ∧ La ∈# mark"
using mark_confl unfolding skip.hyps(1) by simp
ultimately show "b ⊨as CNot ( mark - {#L'#}) ∧ L' ∈# mark" by blast
qed
next
case (conflict D)
then show ?case using mark_confl by simp
next
case (resolve L C M D T) note tr_S = this(1) and T = this(4)
show ?case unfolding resolve.hyps(1)
proof (intro allI impI)
fix L' mark a b
assume "a @ Propagated L' mark # b = trail T"
then have "Propagated L ( (C + {#L#})) # M
= (Propagated L ( (C + {#L#})) # a) @ Propagated L' mark # b"
using T tr_S by auto
then show "b ⊨as CNot ( mark - {#L'#}) ∧ L' ∈# mark"
using mark_confl unfolding resolve.hyps(1) by presburger
qed
next
case restart
then show ?case by auto
next
case forget
then show ?case using mark_confl by auto
next
case (backtrack K i M1 M2 L D T) note decomp = this(1) and conf = this(3) and undef = this(6) and
T =this(7)
have "∀l ∈ set M2. ¬is_decided l"
using get_all_decided_decomposition_snd_not_decided backtrack.hyps(1) by blast
obtain M0 where M: "trail S = M0 @ M2 @ Decided K (i + 1) # M1"
using backtrack.hyps(1) by auto
have [simp]: "trail (reduce_trail_to M1 (add_learned_cls (D + {#L#})
(update_backtrack_lvl i (update_conflicting None S)))) = M1"
using decomp lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
show ?case
proof (intro allI impI)
fix La mark a b
assume "a @ Propagated La mark # b = trail T"
then have "(a = [] ∧ Propagated La mark = Propagated L (D + {#L#}) ∧ b = M1)
∨ tl a @ Propagated La mark # b = M1"
using M T decomp undef by (cases a) (auto)
moreover {
assume A: "a = []" and
P: "Propagated La mark = Propagated L ( (D + {#L#}))" and
b: "b = M1"
have "trail S ⊨as CNot D" using conf confl by auto
then have vars_of_D: "atms_of D ⊆ atm_of ` lits_of (trail S)"
unfolding atms_of_def
by (meson image_subsetI mem_set_mset_iff true_annots_CNot_all_atms_defined)
have vars_of_D: "atms_of D ⊆ atm_of ` lits_of M1"
using backtrack_atms_of_D_in_M1[of S M1 L D i K M2 T] T backtrack lev confl by auto
have "no_dup (trail S)" using lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
then have vars_in_M1: "∀x ∈ atms_of D. x ∉
atm_of ` lits_of (M0 @ M2 @ Decided K (i + 1) # [])"
using vars_of_D distinct_atms_of_incl_not_in_other[of "M0 @ M2 @ Decided K (i + 1) # []"
M1] unfolding M by auto
have "M1 ⊨as CNot D"
using vars_in_M1 true_annots_remove_if_notin_vars[of "M0 @ M2 @ Decided K (i + 1) # []" M1
"CNot D"] ‹trail S ⊨as CNot D› unfolding M lits_of_def by simp
then have "b ⊨as CNot ( mark - {#La#}) ∧ La ∈# mark"
using P b by auto
}
moreover {
assume "tl a @ Propagated La mark # b = M1"
then obtain c' where "c' @ Propagated La mark # b = trail S" unfolding M by auto
then have "b ⊨as CNot (mark - {#La#}) ∧ La ∈# mark"
using mark_confl by blast
}
ultimately show "b ⊨as CNot (mark - {#La#}) ∧ La ∈# mark" by fast
qed
qed
lemma cdcl⇩W_conflicting_is_false:
assumes
"cdcl⇩W S S'" and
M_lev: "cdcl⇩W_M_level_inv S" and
confl_inv: "∀T. conflicting S = Some T ⟶ trail S ⊨as CNot T" and
decided_confl: "∀L mark a b. a @ Propagated L mark # b = (trail S)
⟶ (b ⊨as CNot (mark - {#L#}) ∧ L ∈# mark)" and
dist: "distinct_cdcl⇩W_state S"
shows "∀T. conflicting S' = Some T ⟶ trail S' ⊨as CNot T"
using assms(1,2)
proof (induct rule: cdcl⇩W_all_induct_lev2)
case (skip L C' M D) note tr_S = this(1) and T =this(5)
then have "Propagated L C' # M ⊨as CNot D" using assms skip by auto
moreover
have "L ∉# D"
proof (rule ccontr)
assume "¬ ?thesis"
then have "- L ∈ lits_of M"
using in_CNot_implies_uminus(2)[of D L "Propagated L C' # M"]
‹Propagated L C' # M ⊨as CNot D› by simp
then show False
by (metis M_lev cdcl⇩W_M_level_inv_decomp(1) consistent_interp_def insert_iff
lits_of_cons ann_literal.sel(2) skip.hyps(1))
qed
ultimately show ?case
using skip.hyps(1-3) true_annots_CNot_lit_of_notin_skip T unfolding cdcl⇩W_M_level_inv_def
by fastforce
next
case (resolve L C M D T) note tr = this(1) and confl = this(2) and T = this(4)
show ?case
proof (intro allI impI)
fix T'
have "tl (trail S) ⊨as CNot C" using tr assms(4) by fastforce
moreover
have "distinct_mset (D + {#- L#})" using confl dist
unfolding distinct_cdcl⇩W_state_def by auto
then have "-L ∉# D" unfolding distinct_mset_def by auto
have "M ⊨as CNot D"
proof -
have "Propagated L ( (C + {#L#})) # M ⊨as CNot D ∪ CNot {#- L#}"
using confl tr confl_inv by force
then show ?thesis
using M_lev ‹- L ∉# D› tr true_annots_lit_of_notin_skip
unfolding cdcl⇩W_M_level_inv_def by force
qed
moreover assume "conflicting T = Some T'"
ultimately
show "trail T ⊨as CNot T'"
using tr T by auto
qed
qed (auto simp: assms(2) cdcl⇩W_M_level_inv_decomp)
lemma cdcl⇩W_conflicting_decomp:
assumes "cdcl⇩W_conflicting S"
shows "∀T. conflicting S = Some T ⟶ trail S ⊨as CNot T"
and "∀L mark a b. a @ Propagated L mark # b = (trail S)
⟶ (b ⊨as CNot ( mark - {#L#}) ∧ L ∈# mark)"
using assms unfolding cdcl⇩W_conflicting_def by blast+
lemma cdcl⇩W_conflicting_decomp2:
assumes "cdcl⇩W_conflicting S" and "conflicting S = Some T"
shows "trail S ⊨as CNot T"
using assms unfolding cdcl⇩W_conflicting_def by blast+
lemma cdcl⇩W_conflicting_decomp2':
assumes
"cdcl⇩W_conflicting S" and
"conflicting S = Some D"
shows "trail S ⊨as CNot D"
using assms unfolding cdcl⇩W_conflicting_def by auto
lemma cdcl⇩W_conflicting_S0_cdcl⇩W[simp]:
"cdcl⇩W_conflicting (init_state N)"
unfolding cdcl⇩W_conflicting_def by auto
subsubsection ‹Putting all the invariants together›
lemma cdcl⇩W_all_inv:
assumes cdcl⇩W: "cdcl⇩W S S'" and
1: "all_decomposition_implies_m (init_clss S) (get_all_decided_decomposition (trail S))" and
2: "cdcl⇩W_learned_clause S" and
4: "cdcl⇩W_M_level_inv S" and
5: "no_strange_atm S" and
7: "distinct_cdcl⇩W_state S" and
8: "cdcl⇩W_conflicting S"
shows "all_decomposition_implies_m (init_clss S') (get_all_decided_decomposition (trail S'))"
and "cdcl⇩W_learned_clause S'"
and "cdcl⇩W_M_level_inv S'"
and "no_strange_atm S'"
and "distinct_cdcl⇩W_state S'"
and "cdcl⇩W_conflicting S'"
proof -
show S1: "all_decomposition_implies_m (init_clss S') (get_all_decided_decomposition (trail S'))"
using cdcl⇩W_propagate_is_conclusion[OF cdcl⇩W 4 1 2 _ 5] 8 unfolding cdcl⇩W_conflicting_def
by blast
show S2: "cdcl⇩W_learned_clause S'" using cdcl⇩W_learned_clss[OF cdcl⇩W 2 4] .
show S4: "cdcl⇩W_M_level_inv S'" using cdcl⇩W_consistent_inv[OF cdcl⇩W 4] .
show S5: "no_strange_atm S'" using cdcl⇩W_no_strange_atm_inv[OF cdcl⇩W 5 4] .
show S7: "distinct_cdcl⇩W_state S'" using distinct_cdcl⇩W_state_inv[OF cdcl⇩W 4 7] .
show S8: "cdcl⇩W_conflicting S'"
using cdcl⇩W_conflicting_is_false[OF cdcl⇩W 4 _ _ 7] 8 cdcl⇩W_propagate_is_false[OF cdcl⇩W 4 2 1 _
5]
unfolding cdcl⇩W_conflicting_def by fast
qed
lemma rtranclp_cdcl⇩W_all_inv:
assumes
cdcl⇩W: "rtranclp cdcl⇩W S S'" and
1: "all_decomposition_implies_m (init_clss S) (get_all_decided_decomposition (trail S))" and
2: "cdcl⇩W_learned_clause S" and
4: "cdcl⇩W_M_level_inv S" and
5: "no_strange_atm S" and
7: "distinct_cdcl⇩W_state S" and
8: "cdcl⇩W_conflicting S"
shows
"all_decomposition_implies_m (init_clss S') (get_all_decided_decomposition (trail S'))" and
"cdcl⇩W_learned_clause S'" and
"cdcl⇩W_M_level_inv S'" and
"no_strange_atm S'" and
"distinct_cdcl⇩W_state S'" and
"cdcl⇩W_conflicting S'"
using assms
proof (induct rule: rtranclp_induct)
case base
case 1 then show ?case by blast
case 2 then show ?case by blast
case 3 then show ?case by blast
case 4 then show ?case by blast
case 5 then show ?case by blast
case 6 then show ?case by blast
next
case (step S' S'') note H = this
case 1 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_all_inv[OF H(2)]
H by presburger
case 2 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_all_inv[OF H(2)]
H by presburger
case 3 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_all_inv[OF H(2)]
H by presburger
case 4 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_all_inv[OF H(2)]
H by presburger
case 5 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_all_inv[OF H(2)]
H by presburger
case 6 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_all_inv[OF H(2)]
H by presburger
qed
lemma all_invariant_S0_cdcl⇩W:
assumes "distinct_mset_mset N"
shows "all_decomposition_implies_m (init_clss (init_state N))
(get_all_decided_decomposition (trail (init_state N)))"
and "cdcl⇩W_learned_clause (init_state N)"
and "∀T. conflicting (init_state N) = Some T ⟶ (trail (init_state N))⊨as CNot T"
and "no_strange_atm (init_state N)"
and "consistent_interp (lits_of (trail (init_state N)))"
and "∀L mark a b. a @ Propagated L mark # b = trail (init_state N) ⟶
(b ⊨as CNot ( mark - {#L#}) ∧ L ∈# mark)"
and "distinct_cdcl⇩W_state (init_state N)"
using assms by auto
lemma cdcl⇩W_only_propagated_vars_unsat:
assumes
decided: "∀x ∈ set M. ¬ is_decided x" and
DN: "D ∈# clauses S" and
D: "M ⊨as CNot D" and
inv: "all_decomposition_implies_m N (get_all_decided_decomposition M)" and
state: "state S = (M, N, U, k, C)" and
learned_cl: "cdcl⇩W_learned_clause S" and
atm_incl: "no_strange_atm S"
shows "unsatisfiable (set_mset N)"
proof (rule ccontr)
assume "¬ unsatisfiable (set_mset N)"
then obtain I where
I: "I ⊨s set_mset N" and
cons: "consistent_interp I" and
tot: "total_over_m I (set_mset N)"
unfolding satisfiable_def by auto
have "atms_of_msu N ∪ atms_of_msu U = atms_of_msu N"
using atm_incl state unfolding total_over_m_def no_strange_atm_def
by (auto simp add: clauses_def)
then have "total_over_m I (set_mset N)" using tot unfolding total_over_m_def by auto
moreover have "N ⊨psm U" using learned_cl state unfolding cdcl⇩W_learned_clause_def by auto
ultimately have I_D: "I ⊨ D"
using I DN cons state unfolding true_clss_clss_def true_clss_def Ball_def
by (metis Un_iff ‹atms_of_msu N ∪ atms_of_msu U = atms_of_msu N› atms_of_ms_union clauses_def
mem_set_mset_iff prod.inject set_mset_union total_over_m_def)
have l0: "{{#lit_of L#} |L. is_decided L ∧ L ∈ set M} = {}" using decided by auto
have "atms_of_ms (set_mset N ∪ unmark M) = atms_of_msu N"
using atm_incl state unfolding no_strange_atm_def by auto
then have "total_over_m I (set_mset N ∪ (λa. {#lit_of a#}) ` (set M))"
using tot unfolding total_over_m_def by auto
then have "I ⊨s (λa. {#lit_of a#}) ` (set M)"
using all_decomposition_implies_propagated_lits_are_implied[OF inv] cons I
unfolding true_clss_clss_def l0 by auto
then have IM: "I ⊨s unmark M" by auto
{
fix K
assume "K ∈# D"
then have "-K ∈ lits_of M"
using D unfolding true_annots_def Ball_def CNot_def true_annot_def true_cls_def true_lit_def
Bex_mset_def by (metis (mono_tags, lifting) count_single less_not_refl mem_Collect_eq)
then have " -K ∈ I" using IM true_clss_singleton_lit_of_implies_incl lits_of_def by fastforce
}
then have "¬ I ⊨ D" using cons unfolding true_cls_def true_lit_def consistent_interp_def by auto
then show False using I_D by blast
qed
text ‹We have actually a much stronger theorem, namely
@{thm all_decomposition_implies_propagated_lits_are_implied}, that show that the only choices
we made are decided in the formula›
lemma
assumes "all_decomposition_implies_m N (get_all_decided_decomposition M)"
and "∀m ∈ set M. ¬is_decided m"
shows "set_mset N ⊨ps unmark M"
proof -
have T: "{{#lit_of L#} |L. is_decided L ∧ L ∈ set M} = {}" using assms(2) by auto
then show ?thesis
using all_decomposition_implies_propagated_lits_are_implied[OF assms(1)] unfolding T by simp
qed
lemma conflict_with_false_implies_unsat:
assumes
cdcl⇩W: "cdcl⇩W S S'" and
lev: "cdcl⇩W_M_level_inv S" and
[simp]: "conflicting S' = Some {#}" and
learned: "cdcl⇩W_learned_clause S"
shows "unsatisfiable (set_mset (init_clss S))"
using assms
proof -
have "cdcl⇩W_learned_clause S'" using cdcl⇩W_learned_clss cdcl⇩W learned lev by auto
then have "init_clss S' ⊨pm {#}" using assms(3) unfolding cdcl⇩W_learned_clause_def by auto
then have "init_clss S ⊨pm {#}"
using cdcl⇩W_init_clss[OF assms(1) lev] by auto
then show ?thesis unfolding satisfiable_def true_clss_cls_def by auto
qed
lemma conflict_with_false_implies_terminated:
assumes "cdcl⇩W S S'"
and "conflicting S = Some {#}"
shows "False"
using assms by (induct rule: cdcl⇩W_all_induct) auto
subsubsection ‹No tautology is learned›
text ‹This is a simple consequence of all we have shown previously. It is not strictly necessary,
but helps finding a better bound on the number of learned clauses.›
lemma learned_clss_are_not_tautologies:
assumes
"cdcl⇩W S S'" and
lev: "cdcl⇩W_M_level_inv S" and
conflicting: "cdcl⇩W_conflicting S" and
no_tauto: "∀s ∈# learned_clss S. ¬tautology s"
shows "∀s ∈# learned_clss S'. ¬tautology s"
using assms
proof (induct rule: cdcl⇩W_all_induct_lev2)
case (backtrack K i M1 M2 L D) note confl = this(3)
have "consistent_interp (lits_of (trail S))" using lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
moreover
have "trail S ⊨as CNot (D + {#L#})"
using conflicting confl unfolding cdcl⇩W_conflicting_def by auto
then have "lits_of (trail S) ⊨s CNot (D + {#L#})" using true_annots_true_cls by blast
ultimately have "¬tautology (D + {#L#})" using consistent_CNot_not_tautology by blast
then show ?case using backtrack no_tauto
by (auto simp: cdcl⇩W_M_level_inv_decomp split: split_if_asm)
next
case restart
then show ?case using learned_clss_restart_state state_eq_learned_clss no_tauto
by (metis (no_types, lifting) ball_msetE ball_msetI mem_set_mset_iff set_mset_mono subsetCE)
qed auto
definition "final_cdcl⇩W_state (S:: 'st)
⟷ (trail S ⊨asm init_clss S
∨ ((∀L ∈ set (trail S). ¬is_decided L) ∧
(∃C ∈# init_clss S. trail S ⊨as CNot C)))"
definition "termination_cdcl⇩W_state (S:: 'st)
⟷ (trail S ⊨asm init_clss S
∨ ((∀L ∈ atms_of_msu (init_clss S). L ∈ atm_of ` lits_of (trail S))
∧ (∃C ∈# init_clss S. trail S ⊨as CNot C)))"
subsection ‹CDCL Strong Completeness›
fun mapi :: "('a ⇒ nat ⇒ 'b) ⇒ nat ⇒ 'a list ⇒ 'b list" where
"mapi _ _ [] = []" |
"mapi f n (x # xs) = f x n # mapi f (n - 1) xs"
lemma mark_not_in_set_mapi[simp]: "L ∉ set M ⟹ Decided L k ∉ set (mapi Decided i M)"
by (induct M arbitrary: i) auto
lemma propagated_not_in_set_mapi[simp]: "L ∉ set M ⟹ Propagated L k ∉ set (mapi Decided i M)"
by (induct M arbitrary: i) auto
lemma image_set_mapi:
"f ` set (mapi g i M) = set (mapi (λx i. f (g x i)) i M)"
by (induction M arbitrary: i) auto
lemma mapi_map_convert:
"∀x i j. f x i = f x j ⟹ mapi f i M = map (λx. f x 0) M"
by (induction M arbitrary: i) auto
lemma defined_lit_mapi: "defined_lit (mapi Decided i M) L ⟷ atm_of L ∈ atm_of ` set M"
by (induction M) (auto simp: defined_lit_map image_set_mapi mapi_map_convert)
lemma cdcl⇩W_can_do_step:
assumes
"consistent_interp (set M)" and
"distinct M" and
"atm_of ` (set M) ⊆ atms_of_msu N"
shows "∃S. rtranclp cdcl⇩W (init_state N) S
∧ state S = (mapi Decided (length M) M, N, {#}, length M, None)"
using assms
proof (induct M)
case Nil
then show ?case by auto
next
case (Cons L M) note IH = this(1)
have "consistent_interp (set M)" and "distinct M" and "atm_of ` set M ⊆ atms_of_msu N"
using Cons.prems(1-3) unfolding consistent_interp_def by auto
then obtain S where
st: "cdcl⇩W⇧*⇧* (init_state N) S" and
S: "state S = (mapi Decided (length M) M, N, {#}, length M, None)"
using IH by auto
let ?S⇩0 = "incr_lvl (cons_trail (Decided L (length M +1)) S)"
have "undefined_lit (mapi Decided (length M) M) L"
using Cons.prems(1,2) unfolding defined_lit_def consistent_interp_def by fastforce
moreover have "init_clss S = N"
using S by blast
moreover have "atm_of L ∈ atms_of_msu N" using Cons.prems(3) by auto
moreover have undef: "undefined_lit (trail S) L"
using S ‹distinct (L#M)› calculation(1) by (auto simp: defined_lit_mapi defined_lit_map)
ultimately have "cdcl⇩W S ?S⇩0"
using cdcl⇩W.other[OF cdcl⇩W_o.decide[OF decide_rule[OF S,
of L ?S⇩0]]] S by (auto simp: state_eq_def simp del: state_simp)
then show ?case
using st S undef by (auto intro!: exI[of _ ?S⇩0])
qed
lemma cdcl⇩W_strong_completeness:
assumes
"set M ⊨s set_mset N" and
"consistent_interp (set M)" and
"distinct M" and
"atm_of ` (set M) ⊆ atms_of_msu N"
obtains S where
"state S = (mapi Decided (length M) M, N, {#}, length M, None)" and
"rtranclp cdcl⇩W (init_state N) S" and
"final_cdcl⇩W_state S"
proof -
obtain S where
st: "rtranclp cdcl⇩W (init_state N) S" and
S: "state S = (mapi Decided (length M) M, N, {#}, length M, None)"
using cdcl⇩W_can_do_step[OF assms(2-4)] by auto
have "lits_of (mapi Decided (length M) M) = set M"
by (induct M, auto)
then have "mapi Decided (length M) M ⊨asm N" using assms(1) true_annots_true_cls by metis
then have "final_cdcl⇩W_state S"
using S unfolding final_cdcl⇩W_state_def by auto
then show ?thesis using that st S by blast
qed
subsection ‹Higher level strategy›
text ‹The rules described previously do not lead to a conclusive state. We have to add a strategy.›
subsubsection ‹Definition›
lemma tranclp_conflict_iff[iff]:
"full1 conflict S S' ⟷ conflict S S'"
proof -
have "tranclp conflict S S' ⟹ conflict S S'"
unfolding full1_def by (induct rule: tranclp.induct) force+
then have "tranclp conflict S S' ⟹ conflict S S'" by (meson rtranclpD)
then show ?thesis unfolding full1_def by (metis conflictE option.simps(3)
conflicting_update_conflicting state_eq_conflicting tranclp.intros(1))
qed
inductive cdcl⇩W_cp :: "'st ⇒ 'st ⇒ bool" where
conflict'[intro]: "conflict S S' ⟹ cdcl⇩W_cp S S'" |
propagate': "propagate S S' ⟹ cdcl⇩W_cp S S'"
lemma rtranclp_cdcl⇩W_cp_rtranclp_cdcl⇩W:
"cdcl⇩W_cp⇧*⇧* S T ⟹ cdcl⇩W⇧*⇧* S T"
by (induction rule: rtranclp_induct) (auto simp: cdcl⇩W_cp.simps dest: cdcl⇩W.intros)
lemma cdcl⇩W_cp_state_eq_compatible:
assumes
"cdcl⇩W_cp S T" and
"S ∼ S'" and
"T ∼ T'"
shows "cdcl⇩W_cp S' T'"
using assms
apply (induction)
using conflict_state_eq_compatible apply auto[1]
using propagate' propagate_state_eq_compatible by auto
lemma tranclp_cdcl⇩W_cp_state_eq_compatible:
assumes
"cdcl⇩W_cp⇧+⇧+ S T" and
"S ∼ S'" and
"T ∼ T'"
shows "cdcl⇩W_cp⇧+⇧+ S' T'"
using assms
proof induction
case base
then show ?case
using cdcl⇩W_cp_state_eq_compatible by blast
next
case (step U V)
obtain ss :: 'st where
"cdcl⇩W_cp S ss ∧ cdcl⇩W_cp⇧*⇧* ss U"
by (metis (no_types) step(1) tranclpD)
then show ?case
by (meson cdcl⇩W_cp_state_eq_compatible rtranclp.rtrancl_into_rtrancl rtranclp_into_tranclp2
state_eq_ref step(2) step(4) step(5))
qed
lemma option_full_cdcl⇩W_cp:
"conflicting S ≠ None ⟹ full cdcl⇩W_cp S S"
unfolding full_def rtranclp_unfold tranclp_unfold by (auto simp add: cdcl⇩W_cp.simps)
lemma skip_unique:
"skip S T ⟹ skip S T' ⟹ T ∼ T'"
by (fastforce simp: state_eq_def simp del: state_simp)
lemma resolve_unique:
"resolve S T ⟹ resolve S T' ⟹ T ∼ T'"
by (fastforce simp: state_eq_def simp del: state_simp)
lemma cdcl⇩W_cp_no_more_clauses:
assumes "cdcl⇩W_cp S S'"
shows "clauses S = clauses S'"
using assms by (induct rule: cdcl⇩W_cp.induct) (auto elim!: conflictE propagateE)
lemma tranclp_cdcl⇩W_cp_no_more_clauses:
assumes "cdcl⇩W_cp⇧+⇧+ S S'"
shows "clauses S = clauses S'"
using assms by (induct rule: tranclp.induct) (auto dest: cdcl⇩W_cp_no_more_clauses)
lemma rtranclp_cdcl⇩W_cp_no_more_clauses:
assumes "cdcl⇩W_cp⇧*⇧* S S'"
shows "clauses S = clauses S'"
using assms by (induct rule: rtranclp_induct) (fastforce dest: cdcl⇩W_cp_no_more_clauses)+
lemma no_conflict_after_conflict:
"conflict S T ⟹ ¬conflict T U"
by fastforce
lemma no_propagate_after_conflict:
"conflict S T ⟹ ¬propagate T U"
by fastforce
lemma tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not:
assumes "cdcl⇩W_cp⇧+⇧+ S U"
shows "(propagate⇧+⇧+ S U ∧ conflicting U = None)
∨ (∃T D. propagate⇧*⇧* S T ∧ conflict T U ∧ conflicting U = Some D)"
proof -
have "propagate⇧+⇧+ S U ∨ (∃T. propagate⇧*⇧* S T ∧ conflict T U)"
using assms by induction
(force simp: cdcl⇩W_cp.simps tranclp_into_rtranclp dest: no_conflict_after_conflict
no_propagate_after_conflict)+
moreover
have "propagate⇧+⇧+ S U ⟹ conflicting U = None"
unfolding tranclp_unfold_end by auto
moreover
have "⋀T. conflict T U ⟹ ∃D. conflicting U = Some D"
by auto
ultimately show ?thesis by meson
qed
lemma cdcl⇩W_cp_conflicting_not_empty[simp]: "conflicting S = Some D ⟹ ¬cdcl⇩W_cp S S'"
proof
assume "cdcl⇩W_cp S S'" and "conflicting S = Some D"
then show False by (induct rule: cdcl⇩W_cp.induct) auto
qed
lemma no_step_cdcl⇩W_cp_no_conflict_no_propagate:
assumes "no_step cdcl⇩W_cp S"
shows "no_step conflict S" and "no_step propagate S"
using assms conflict' apply blast
by (meson assms conflict' propagate')
text ‹CDCL with the reasonable strategy: we fully propagate the conflict and propagate, then we
apply any other possible rule @{term "cdcl⇩W_o S S'"} and re-apply conflict and propagate
@{term "full cdcl⇩W_cp S' S''"}›
inductive cdcl⇩W_stgy :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
conflict': "full1 cdcl⇩W_cp S S' ⟹ cdcl⇩W_stgy S S'" |
other': "cdcl⇩W_o S S' ⟹ no_step cdcl⇩W_cp S ⟹ full cdcl⇩W_cp S' S'' ⟹ cdcl⇩W_stgy S S''"
subsubsection ‹Invariants›
text ‹These are the same invariants as before, but lifted›
lemma cdcl⇩W_cp_learned_clause_inv:
assumes "cdcl⇩W_cp S S'"
shows "learned_clss S = learned_clss S'"
using assms by (induct rule: cdcl⇩W_cp.induct) fastforce+
lemma rtranclp_cdcl⇩W_cp_learned_clause_inv:
assumes "cdcl⇩W_cp⇧*⇧* S S'"
shows "learned_clss S = learned_clss S'"
using assms by (induct rule: rtranclp_induct) (fastforce dest: cdcl⇩W_cp_learned_clause_inv)+
lemma tranclp_cdcl⇩W_cp_learned_clause_inv:
assumes "cdcl⇩W_cp⇧+⇧+ S S'"
shows "learned_clss S = learned_clss S'"
using assms by (simp add: rtranclp_cdcl⇩W_cp_learned_clause_inv tranclp_into_rtranclp)
lemma cdcl⇩W_cp_backtrack_lvl:
assumes "cdcl⇩W_cp S S'"
shows "backtrack_lvl S = backtrack_lvl S'"
using assms by (induct rule: cdcl⇩W_cp.induct) fastforce+
lemma rtranclp_cdcl⇩W_cp_backtrack_lvl:
assumes "cdcl⇩W_cp⇧*⇧* S S'"
shows "backtrack_lvl S = backtrack_lvl S'"
using assms by (induct rule: rtranclp_induct) (fastforce dest: cdcl⇩W_cp_backtrack_lvl)+
lemma cdcl⇩W_cp_consistent_inv:
assumes "cdcl⇩W_cp S S'"
and "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_M_level_inv S'"
using assms
proof (induct rule: cdcl⇩W_cp.induct)
case (conflict')
then show ?case using cdcl⇩W_consistent_inv cdcl⇩W.conflict by blast
next
case (propagate' S S')
have "cdcl⇩W S S'"
using propagate'.hyps(1) propagate by blast
then show "cdcl⇩W_M_level_inv S'"
using propagate'.prems(1) cdcl⇩W_consistent_inv propagate by blast
qed
lemma full1_cdcl⇩W_cp_consistent_inv:
assumes "full1 cdcl⇩W_cp S S'"
and "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_M_level_inv S'"
using assms unfolding full1_def
proof -
have "cdcl⇩W_cp⇧+⇧+ S S'" and "cdcl⇩W_M_level_inv S" using assms unfolding full1_def by auto
then show ?thesis by (induct rule: tranclp.induct) (blast intro: cdcl⇩W_cp_consistent_inv)+
qed
lemma rtranclp_cdcl⇩W_cp_consistent_inv:
assumes "rtranclp cdcl⇩W_cp S S'"
and "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_M_level_inv S'"
using assms unfolding full1_def
by (induction rule: rtranclp_induct) (blast intro: cdcl⇩W_cp_consistent_inv)+
lemma cdcl⇩W_stgy_consistent_inv:
assumes "cdcl⇩W_stgy S S'"
and "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_M_level_inv S'"
using assms apply (induct rule: cdcl⇩W_stgy.induct)
unfolding full_unfold by (blast intro: cdcl⇩W_consistent_inv full1_cdcl⇩W_cp_consistent_inv
cdcl⇩W.other)+
lemma rtranclp_cdcl⇩W_stgy_consistent_inv:
assumes "cdcl⇩W_stgy⇧*⇧* S S'"
and "cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_M_level_inv S'"
using assms by induction (auto dest!: cdcl⇩W_stgy_consistent_inv)
lemma cdcl⇩W_cp_no_more_init_clss:
assumes "cdcl⇩W_cp S S'"
shows "init_clss S = init_clss S'"
using assms by (induct rule: cdcl⇩W_cp.induct) auto
lemma tranclp_cdcl⇩W_cp_no_more_init_clss:
assumes "cdcl⇩W_cp⇧+⇧+ S S'"
shows "init_clss S = init_clss S'"
using assms by (induct rule: tranclp.induct) (auto dest: cdcl⇩W_cp_no_more_init_clss)
lemma cdcl⇩W_stgy_no_more_init_clss:
assumes "cdcl⇩W_stgy S S'" and "cdcl⇩W_M_level_inv S"
shows "init_clss S = init_clss S'"
using assms
apply (induct rule: cdcl⇩W_stgy.induct)
unfolding full1_def full_def apply (blast dest: tranclp_cdcl⇩W_cp_no_more_init_clss
tranclp_cdcl⇩W_o_no_more_init_clss)
by (metis cdcl⇩W_o_no_more_init_clss rtranclp_unfold tranclp_cdcl⇩W_cp_no_more_init_clss)
lemma rtranclp_cdcl⇩W_stgy_no_more_init_clss:
assumes "cdcl⇩W_stgy⇧*⇧* S S'" and "cdcl⇩W_M_level_inv S"
shows "init_clss S = init_clss S'"
using assms
apply (induct rule: rtranclp_induct, simp)
using cdcl⇩W_stgy_no_more_init_clss by (simp add: rtranclp_cdcl⇩W_stgy_consistent_inv)
lemma cdcl⇩W_cp_dropWhile_trail':
assumes "cdcl⇩W_cp S S'"
obtains M where "trail S' = M @ trail S" and " (∀l ∈ set M. ¬is_decided l)"
using assms by induction fastforce+
lemma rtranclp_cdcl⇩W_cp_dropWhile_trail':
assumes "cdcl⇩W_cp⇧*⇧* S S'"
obtains M :: "('v, nat, 'v clause) ann_literal list" where
"trail S' = M @ trail S" and "∀l ∈ set M. ¬is_decided l"
using assms by induction (fastforce dest!: cdcl⇩W_cp_dropWhile_trail')+
lemma cdcl⇩W_cp_dropWhile_trail:
assumes "cdcl⇩W_cp S S'"
shows "∃M. trail S' = M @ trail S ∧ (∀l ∈ set M. ¬is_decided l)"
using assms by induction fastforce+
lemma rtranclp_cdcl⇩W_cp_dropWhile_trail:
assumes "cdcl⇩W_cp⇧*⇧* S S'"
shows "∃M. trail S' = M @ trail S ∧ (∀l ∈ set M. ¬is_decided l)"
using assms by induction (fastforce dest: cdcl⇩W_cp_dropWhile_trail)+
text ‹This theorem can be seen a a termination theorem for @{term cdcl⇩W_cp}.›
lemma length_model_le_vars:
assumes
"no_strange_atm S" and
no_d: "no_dup (trail S)" and
"finite (atms_of_msu (init_clss S))"
shows "length (trail S) ≤ card (atms_of_msu (init_clss S))"
proof -
obtain M N U k D where S: "state S = (M, N, U, k, D)" by (cases "state S", auto)
have "finite (atm_of ` lits_of (trail S))"
using assms(1,3) unfolding S by (auto simp add: finite_subset)
have "length (trail S) = card (atm_of ` lits_of (trail S))"
using no_dup_length_eq_card_atm_of_lits_of no_d by blast
then show ?thesis using assms(1) unfolding no_strange_atm_def
by (auto simp add: assms(3) card_mono)
qed
lemma cdcl⇩W_cp_decreasing_measure:
assumes
cdcl⇩W: "cdcl⇩W_cp S T" and
M_lev: "cdcl⇩W_M_level_inv S" and
alien: "no_strange_atm S"
shows "(λS. card (atms_of_msu (init_clss S)) - length (trail S)
+ (if conflicting S = None then 1 else 0)) S
> (λS. card (atms_of_msu (init_clss S)) - length (trail S)
+ (if conflicting S = None then 1 else 0)) T"
using assms
proof -
have "length (trail T) ≤ card (atms_of_msu (init_clss T))"
apply (rule length_model_le_vars)
using cdcl⇩W_no_strange_atm_inv alien M_lev apply (meson cdcl⇩W cdcl⇩W.simps cdcl⇩W_cp.cases)
using M_lev cdcl⇩W cdcl⇩W_cp_consistent_inv cdcl⇩W_M_level_inv_def apply blast
using cdcl⇩W by (auto simp: cdcl⇩W_cp.simps)
with assms
show ?thesis by induction (auto split: split_if_asm)+
qed
lemma cdcl⇩W_cp_wf: "wf {(b,a). (cdcl⇩W_M_level_inv a ∧ no_strange_atm a)
∧ cdcl⇩W_cp a b}"
apply (rule wf_wf_if_measure'[of less_than _ _
"(λS. card (atms_of_msu (init_clss S)) - length (trail S)
+ (if conflicting S = None then 1 else 0))"])
apply simp
using cdcl⇩W_cp_decreasing_measure unfolding less_than_iff by blast
lemma rtranclp_cdcl⇩W_all_struct_inv_cdcl⇩W_cp_iff_rtranclp_cdcl⇩W_cp:
assumes
lev: "cdcl⇩W_M_level_inv S" and
alien: "no_strange_atm S"
shows "(λa b. (cdcl⇩W_M_level_inv a ∧ no_strange_atm a) ∧ cdcl⇩W_cp a b)⇧*⇧* S T
⟷ cdcl⇩W_cp⇧*⇧* S T"
(is "?I S T ⟷ ?C S T")
proof
assume
"?I S T"
then show "?C S T" by induction auto
next
assume
"?C S T"
then show "?I S T"
proof induction
case base
then show ?case by simp
next
case (step T U) note st = this(1) and cp = this(2) and IH = this(3)
have "cdcl⇩W⇧*⇧* S T"
by (metis rtranclp_unfold cdcl⇩W_cp_conflicting_not_empty cp st
rtranclp_propagate_is_rtranclp_cdcl⇩W tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not)
then have
"cdcl⇩W_M_level_inv T" and
"no_strange_atm T"
using ‹cdcl⇩W⇧*⇧* S T› apply (simp add: assms(1) rtranclp_cdcl⇩W_consistent_inv)
using ‹cdcl⇩W⇧*⇧* S T› alien rtranclp_cdcl⇩W_no_strange_atm_inv lev by blast
then have " (λa b. (cdcl⇩W_M_level_inv a ∧ no_strange_atm a)
∧ cdcl⇩W_cp a b)⇧*⇧* T U"
using cp by auto
then show ?case using IH by auto
qed
qed
lemma cdcl⇩W_cp_normalized_element:
assumes
lev: "cdcl⇩W_M_level_inv S" and
"no_strange_atm S"
obtains T where "full cdcl⇩W_cp S T"
proof -
let ?inv = "λa. (cdcl⇩W_M_level_inv a ∧ no_strange_atm a)"
obtain T where T: "full (λa b. ?inv a ∧ cdcl⇩W_cp a b) S T"
using cdcl⇩W_cp_wf wf_exists_normal_form[of "λa b. ?inv a ∧ cdcl⇩W_cp a b"]
unfolding full_def by blast
then have "cdcl⇩W_cp⇧*⇧* S T"
using rtranclp_cdcl⇩W_all_struct_inv_cdcl⇩W_cp_iff_rtranclp_cdcl⇩W_cp assms unfolding full_def
by blast
moreover
then have "cdcl⇩W⇧*⇧* S T"
using rtranclp_cdcl⇩W_cp_rtranclp_cdcl⇩W by blast
then have
"cdcl⇩W_M_level_inv T" and
"no_strange_atm T"
using ‹cdcl⇩W⇧*⇧* S T› apply (simp add: assms(1) rtranclp_cdcl⇩W_consistent_inv)
using ‹cdcl⇩W⇧*⇧* S T› assms(2) rtranclp_cdcl⇩W_no_strange_atm_inv lev by blast
then have "no_step cdcl⇩W_cp T"
using T unfolding full_def by auto
ultimately show thesis using that unfolding full_def by blast
qed
lemma in_atms_of_implies_atm_of_on_atms_of_ms:
"C + {#L#} ∈# A ⟹ x ∈ atms_of C ⟹ x ∈ atms_of_msu A"
by (metis add.commute atm_iff_pos_or_neg_lit atms_of_atms_of_ms_mono contra_subsetD
mem_set_mset_iff multi_member_skip)
lemma propagate_no_stange_atm:
assumes
"propagate S S'" and
"no_strange_atm S"
shows "no_strange_atm S'"
using assms by induction
(auto simp add: no_strange_atm_def clauses_def in_plus_implies_atm_of_on_atms_of_ms
in_atms_of_implies_atm_of_on_atms_of_ms)
lemma always_exists_full_cdcl⇩W_cp_step:
assumes "no_strange_atm S"
shows "∃S''. full cdcl⇩W_cp S S''"
using assms
proof (induct "card (atms_of_msu (init_clss S) - atm_of `lits_of (trail S))" arbitrary: S)
case 0 note card = this(1) and alien = this(2)
then have atm: "atms_of_msu (init_clss S) = atm_of ` lits_of (trail S)"
unfolding no_strange_atm_def by auto
{ assume a: "∃S'. conflict S S'"
then obtain S' where S': "conflict S S'" by metis
then have "∀S''. ¬cdcl⇩W_cp S' S''" by auto
then have ?case using a S' cdcl⇩W_cp.conflict' unfolding full_def by blast
}
moreover {
assume a: "∃S'. propagate S S'"
then obtain S' where "propagate S S'" by blast
then obtain M N U k C L where S: "state S = (M, N, U, k, None)"
and S': "state S' = (Propagated L ( (C + {#L#})) # M, N, U, k, None)"
and "C + {#L#} ∈# clauses S"
and "M ⊨as CNot C"
and "undefined_lit M L"
using propagate by auto
have "atms_of_msu U ⊆ atms_of_msu N" using alien S unfolding no_strange_atm_def by auto
then have "atm_of L ∈ atms_of_msu (init_clss S)"
using ‹C + {#L#} ∈# clauses S› S unfolding atms_of_ms_def clauses_def by force+
then have False using ‹undefined_lit M L› S unfolding atm unfolding lits_of_def
by (auto simp add: defined_lit_map)
}
ultimately show ?case by (metis cdcl⇩W_cp.cases full_def rtranclp.rtrancl_refl)
next
case (Suc n) note IH = this(1) and card = this(2) and alien = this(3)
{ assume a: "∃S'. conflict S S'"
then obtain S' where S': "conflict S S'" by metis
then have "∀S''. ¬cdcl⇩W_cp S' S''" by auto
then have ?case unfolding full_def Ex_def using S' cdcl⇩W_cp.conflict' by blast
}
moreover {
assume a: "∃S'. propagate S S'"
then obtain S' where propagate: "propagate S S'" by blast
then obtain M N U k C L where
S: "state S = (M, N, U, k, None)" and
S': "state S' = (Propagated L ( (C + {#L#})) # M, N, U, k, None)" and
"C + {#L#} ∈# clauses S" and
"M ⊨as CNot C" and
"undefined_lit M L"
by fastforce
then have "atm_of L ∉ atm_of ` lits_of M"
unfolding lits_of_def by (auto simp add: defined_lit_map)
moreover
have "no_strange_atm S'" using alien propagate propagate_no_stange_atm by blast
then have "atm_of L ∈ atms_of_msu N" using S' unfolding no_strange_atm_def by auto
then have "⋀A. {atm_of L} ⊆ atms_of_msu N - A ∨ atm_of L ∈ A" by force
moreover have "Suc n - card {atm_of L} = n" by simp
moreover have "card (atms_of_msu N - atm_of ` lits_of M) = Suc n"
using card S S' by simp
ultimately
have "card (atms_of_msu N - atm_of ` insert L (lits_of M)) = n"
by (metis (no_types) Diff_insert card_Diff_subset finite.emptyI finite.insertI image_insert)
then have "n = card (atms_of_msu (init_clss S') - atm_of ` lits_of (trail S'))"
using card S S' by simp
then have a1: "Ex (full cdcl⇩W_cp S')" using IH ‹no_strange_atm S'› by blast
have ?case
proof -
obtain S'' :: "'st" where
ff1: "cdcl⇩W_cp⇧*⇧* S' S'' ∧ no_step cdcl⇩W_cp S''"
using a1 unfolding full_def by blast
have "cdcl⇩W_cp⇧*⇧* S S''"
using ff1 cdcl⇩W_cp.intros(2)[OF propagate]
by (metis (no_types) converse_rtranclp_into_rtranclp)
then have "∃S''. cdcl⇩W_cp⇧*⇧* S S'' ∧ (∀S'''. ¬ cdcl⇩W_cp S'' S''')"
using ff1 by blast
then show ?thesis unfolding full_def
by meson
qed
}
ultimately show ?case unfolding full_def by (metis cdcl⇩W_cp.cases rtranclp.rtrancl_refl)
qed
subsubsection ‹Literal of highest level in conflicting clauses›
text ‹One important property of the @{term cdcl⇩W} with strategy is that, whenever a conflict takes
place, there is at least a literal of level k involved (except if we have derived the false
clause). The reason is that we apply conflicts before a decision is taken.›
abbreviation no_clause_is_false :: "'st ⇒ bool" where
"no_clause_is_false ≡
λS. (conflicting S = None ⟶ (∀D ∈# clauses S. ¬trail S ⊨as CNot D))"
abbreviation conflict_is_false_with_level :: "'st ⇒ bool" where
"conflict_is_false_with_level S ≡ ∀D. conflicting S = Some D ⟶ D ≠ {#}
⟶ (∃L ∈# D. get_level (trail S) L = backtrack_lvl S)"
lemma not_conflict_not_any_negated_init_clss:
assumes "∀ S'. ¬conflict S S'"
shows "no_clause_is_false S"
using assms state_eq_ref by blast
lemma full_cdcl⇩W_cp_not_any_negated_init_clss:
assumes "full cdcl⇩W_cp S S'"
shows "no_clause_is_false S'"
using assms not_conflict_not_any_negated_init_clss unfolding full_def by blast
lemma full1_cdcl⇩W_cp_not_any_negated_init_clss:
assumes "full1 cdcl⇩W_cp S S'"
shows "no_clause_is_false S'"
using assms not_conflict_not_any_negated_init_clss unfolding full1_def by blast
lemma cdcl⇩W_stgy_not_non_negated_init_clss:
assumes "cdcl⇩W_stgy S S'"
shows "no_clause_is_false S'"
using assms apply (induct rule: cdcl⇩W_stgy.induct)
using full1_cdcl⇩W_cp_not_any_negated_init_clss full_cdcl⇩W_cp_not_any_negated_init_clss by metis+
lemma rtranclp_cdcl⇩W_stgy_not_non_negated_init_clss:
assumes "cdcl⇩W_stgy⇧*⇧* S S'" and "no_clause_is_false S"
shows "no_clause_is_false S'"
using assms by (induct rule: rtranclp_induct) (auto simp: cdcl⇩W_stgy_not_non_negated_init_clss)
lemma cdcl⇩W_stgy_conflict_ex_lit_of_max_level:
assumes "cdcl⇩W_cp S S'"
and "no_clause_is_false S"
and "cdcl⇩W_M_level_inv S"
shows "conflict_is_false_with_level S'"
using assms
proof (induct rule: cdcl⇩W_cp.induct)
case conflict'
then show ?case by auto
next
case propagate'
then show ?case by auto
qed
lemma no_chained_conflict:
assumes "conflict S S'"
and "conflict S' S''"
shows False
using assms by fastforce
lemma rtranclp_cdcl⇩W_cp_propa_or_propa_confl:
assumes "cdcl⇩W_cp⇧*⇧* S U"
shows "propagate⇧*⇧* S U ∨ (∃T. propagate⇧*⇧* S T ∧ conflict T U)"
using assms
proof induction
case base
then show ?case by auto
next
case (step U V) note SU = this(1) and UV = this(2) and IH = this(3)
consider (confl) T where "propagate⇧*⇧* S T" and "conflict T U"
| (propa) "propagate⇧*⇧* S U" using IH by auto
then show ?case
proof cases
case confl
then have False using UV by auto
then show ?thesis by fast
next
case propa
also have "conflict U V ∨ propagate U V" using UV by (auto simp add: cdcl⇩W_cp.simps)
ultimately show ?thesis by force
qed
qed
lemma rtranclp_cdcl⇩W_co_conflict_ex_lit_of_max_level:
assumes full: "full cdcl⇩W_cp S U"
and cls_f: "no_clause_is_false S"
and "conflict_is_false_with_level S"
and lev: "cdcl⇩W_M_level_inv S"
shows "conflict_is_false_with_level U"
proof (intro allI impI)
fix D
assume confl: "conflicting U = Some D" and
D: "D ≠ {#}"
consider (CT) "conflicting S = None" | (SD) D' where "conflicting S = Some D'"
by (cases "conflicting S") auto
then show "∃L∈#D. get_level (trail U) L = backtrack_lvl U"
proof cases
case SD
then have "S = U"
by (metis (no_types) assms(1) cdcl⇩W_cp_conflicting_not_empty full_def rtranclpD tranclpD)
then show ?thesis using assms(3) confl D by blast-
next
case CT
have "init_clss U = init_clss S" and "learned_clss U = learned_clss S"
using assms(1) unfolding full_def
apply (metis (no_types) rtranclpD tranclp_cdcl⇩W_cp_no_more_init_clss)
by (metis (mono_tags, lifting) assms(1) full_def rtranclp_cdcl⇩W_cp_learned_clause_inv)
obtain T where "propagate⇧*⇧* S T" and TU: "conflict T U"
proof -
have f5: "U ≠ S"
using confl CT by force
then have "cdcl⇩W_cp⇧+⇧+ S U"
by (metis full full_def rtranclpD)
have "⋀p pa. ¬ propagate p pa ∨ conflicting pa =
(None::'v literal multiset option)"
by auto
then show ?thesis
using f5 that tranclp_cdcl⇩W_cp_propagate_with_conflict_or_not[OF ‹cdcl⇩W_cp⇧+⇧+ S U›]
full confl CT unfolding full_def by auto
qed
have "init_clss T = init_clss S" and "learned_clss T = learned_clss S"
using TU ‹init_clss U = init_clss S› ‹learned_clss U = learned_clss S› by auto
then have "D ∈# clauses S"
using TU confl by (fastforce simp: clauses_def)
then have "¬ trail S ⊨as CNot D"
using cls_f CT by simp
moreover
obtain M where tr_U: "trail U = M @ trail S" and nm: "∀m∈set M. ¬is_decided m"
by (metis (mono_tags, lifting) assms(1) full_def rtranclp_cdcl⇩W_cp_dropWhile_trail)
have "trail U ⊨as CNot D"
using TU confl by auto
ultimately obtain L where "L ∈# D" and "-L ∈ lits_of M"
unfolding tr_U CNot_def true_annots_def Ball_def true_annot_def true_cls_def by auto
moreover have inv_U: "cdcl⇩W_M_level_inv U"
by (metis cdcl⇩W_stgy.conflict' cdcl⇩W_stgy_consistent_inv full full_unfold lev)
moreover
have "backtrack_lvl U = backtrack_lvl S"
using full unfolding full_def by (auto dest: rtranclp_cdcl⇩W_cp_backtrack_lvl)
moreover
have "no_dup (trail U)"
using inv_U unfolding cdcl⇩W_M_level_inv_def by auto
{ fix x :: "('v, nat, 'v literal multiset) ann_literal" and
xb :: "('v, nat, 'v literal multiset) ann_literal"
assume a1: "atm_of L = atm_of (lit_of xb)"
moreover assume a2: "- L = lit_of x"
moreover assume a3: "(λl. atm_of (lit_of l)) ` set M
∩ (λl. atm_of (lit_of l)) ` set (trail S) = {}"
moreover assume a4: "x ∈ set M"
moreover assume a5: "xb ∈ set (trail S)"
moreover have "atm_of (- L) = atm_of L"
by auto
ultimately have False
by auto
}
then have LS: "atm_of L ∉ atm_of ` lits_of (trail S)"
using ‹-L ∈ lits_of M› ‹no_dup (trail U)› unfolding tr_U lits_of_def by auto
ultimately have "get_level (trail U) L = backtrack_lvl U"
proof (cases "get_all_levels_of_decided (trail S) ≠ []", goal_cases)
case 2 note LD = this(1) and LM = this(2) and inv_U = this(3) and US = this(4) and
LS = this(5) and ne = this(6)
have "backtrack_lvl S = 0"
using lev ne unfolding cdcl⇩W_M_level_inv_def by auto
moreover have "get_rev_level (rev M) 0 L = 0"
using nm by auto
ultimately show ?thesis using LS ne US unfolding tr_U
by (simp add: get_all_levels_of_decided_nil_iff_not_is_decided lits_of_def)
next
case 1 note LD = this(1) and LM = this(2) and inv_U = this(3) and US = this(4) and
LS = this(5) and ne = this(6)
have "hd (get_all_levels_of_decided (trail S)) = backtrack_lvl S"
using ne lev unfolding cdcl⇩W_M_level_inv_def
by (cases "get_all_levels_of_decided (trail S)") auto
moreover have "atm_of L ∈ atm_of ` lits_of M "
using ‹-L ∈ lits_of M› by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
lits_of_def)
ultimately show ?thesis
using nm ne unfolding tr_U
using get_level_skip_beginning_hd_get_all_levels_of_decided[OF LS, of M]
get_level_skip_in_all_not_decided[of "rev M" L "backtrack_lvl S"]
unfolding lits_of_def US
by auto
qed
then show "∃L∈#D. get_level (trail U) L = backtrack_lvl U"
using ‹L ∈# D› by blast
qed
qed
subsubsection ‹Literal of highest level in decided literals›
definition mark_is_false_with_level :: "'st ⇒ bool" where
"mark_is_false_with_level S' ≡
∀D M1 M2 L. M1 @ Propagated L D # M2 = trail S' ⟶ D - {#L#} ≠ {#}
⟶ (∃L. L ∈# D ∧ get_level (trail S') L = get_maximum_possible_level M1)"
definition no_more_propagation_to_do:: "'st ⇒ bool" where
"no_more_propagation_to_do S ≡
∀D M M' L. D + {#L#} ∈# clauses S ⟶ trail S = M' @ M ⟶ M ⊨as CNot D
⟶ undefined_lit M L ⟶ get_maximum_possible_level M < backtrack_lvl S
⟶ (∃L. L ∈# D ∧ get_level (trail S) L = get_maximum_possible_level M)"
lemma propagate_no_more_propagation_to_do:
assumes propagate: "propagate S S'"
and H: "no_more_propagation_to_do S"
and M: "cdcl⇩W_M_level_inv S"
shows "no_more_propagation_to_do S'"
using assms
proof -
obtain M N U k C L where
S: "state S = (M, N, U, k, None)" and
S': "state S' = (Propagated L ( (C + {#L#})) # M, N, U, k, None)" and
"C + {#L#} ∈# clauses S" and
"M ⊨as CNot C" and
"undefined_lit M L"
using propagate by auto
let ?M' = "Propagated L ( (C + {#L#})) # M"
show ?thesis unfolding no_more_propagation_to_do_def
proof (intro allI impI)
fix D M1 M2 L'
assume D_L: "D + {#L'#} ∈# clauses S'"
and "trail S' = M2 @ M1"
and get_max: "get_maximum_possible_level M1 < backtrack_lvl S'"
and "M1 ⊨as CNot D"
and undef: "undefined_lit M1 L'"
have "tl M2 @ M1 = trail S ∨ (M2 = [] ∧ M1 = Propagated L ( (C + {#L#})) # M)"
using ‹trail S' = M2 @ M1› S' S by (cases M2) auto
moreover {
assume "tl M2 @ M1 = trail S"
moreover have "D + {#L'#} ∈# clauses S" using D_L S S' unfolding clauses_def by auto
moreover have "get_maximum_possible_level M1 < backtrack_lvl S"
using get_max S S' by auto
ultimately obtain L' where "L' ∈# D" and
"get_level (trail S) L' = get_maximum_possible_level M1"
using H ‹M1 ⊨as CNot D› undef unfolding no_more_propagation_to_do_def by metis
moreover
{ have "cdcl⇩W_M_level_inv S'"
using cdcl⇩W_consistent_inv[OF _ M] cdcl⇩W.propagate[OF propagate] by blast
then have "no_dup ?M'" using S' unfolding cdcl⇩W_M_level_inv_def by auto
moreover
have "atm_of L' ∈ atm_of ` (lits_of M1)"
using ‹L' ∈# D› ‹M1 ⊨as CNot D› by (metis atm_of_uminus image_eqI
in_CNot_implies_uminus(2))
then have "atm_of L' ∈ atm_of ` (lits_of M)"
using ‹tl M2 @ M1 = trail S› S by auto
ultimately have "atm_of L ≠ atm_of L'" unfolding lits_of_def by auto
}
ultimately have "∃L' ∈# D. get_level (trail S') L' = get_maximum_possible_level M1"
using S S' by auto
}
moreover {
assume "M2 = []" and M1: "M1 = Propagated L ( (C + {#L#})) # M"
have "cdcl⇩W_M_level_inv S'"
using cdcl⇩W_consistent_inv[OF _ M] cdcl⇩W.propagate[OF propagate] by blast
then have "get_all_levels_of_decided (trail S') = rev ([Suc 0..<(Suc 0+k)])"
using S' unfolding cdcl⇩W_M_level_inv_def by auto
then have "get_maximum_possible_level M1 = backtrack_lvl S'"
using get_maximum_possible_level_max_get_all_levels_of_decided[of M1] S' M1
by (auto intro: Max_eqI)
then have False using get_max by auto
}
ultimately show "∃L. L ∈# D ∧ get_level (trail S') L = get_maximum_possible_level M1" by fast
qed
qed
lemma conflict_no_more_propagation_to_do:
assumes conflict: "conflict S S'"
and H: "no_more_propagation_to_do S"
and M: "cdcl⇩W_M_level_inv S"
shows "no_more_propagation_to_do S'"
using assms unfolding no_more_propagation_to_do_def conflict.simps by force
lemma cdcl⇩W_cp_no_more_propagation_to_do:
assumes conflict: "cdcl⇩W_cp S S'"
and H: "no_more_propagation_to_do S"
and M: "cdcl⇩W_M_level_inv S"
shows "no_more_propagation_to_do S'"
using assms
proof (induct rule: cdcl⇩W_cp.induct)
case (conflict' S S')
then show ?case using conflict_no_more_propagation_to_do[of S S'] by blast
next
case (propagate' S S') note S = this
show 1: "no_more_propagation_to_do S'"
using propagate_no_more_propagation_to_do[of S S'] S by blast
qed
lemma cdcl⇩W_then_exists_cdcl⇩W_stgy_step:
assumes
o: "cdcl⇩W_o S S'" and
alien: "no_strange_atm S" and
lev: "cdcl⇩W_M_level_inv S"
shows "∃S'. cdcl⇩W_stgy S S'"
proof -
obtain S'' where "full cdcl⇩W_cp S' S''"
using always_exists_full_cdcl⇩W_cp_step alien cdcl⇩W_no_strange_atm_inv cdcl⇩W_o_no_more_init_clss
o other lev by (meson cdcl⇩W_consistent_inv)
then show ?thesis
using assms by (metis always_exists_full_cdcl⇩W_cp_step cdcl⇩W_stgy.conflict' full_unfold other')
qed
lemma backtrack_no_decomp:
assumes S: "state S = (M, N, U, k, Some (D + {#L#}))"
and L: "get_level M L = k"
and D: "get_maximum_level M D < k"
and M_L: "cdcl⇩W_M_level_inv S"
shows "∃S'. cdcl⇩W_o S S'"
proof -
have L_D: "get_level M L = get_maximum_level M (D + {#L#})"
using L D by (simp add: get_maximum_level_plus)
let ?i = "get_maximum_level M D"
obtain K M1 M2 where K: "(Decided K (?i + 1) # M1, M2) ∈ set (get_all_decided_decomposition M)"
using backtrack_ex_decomp[OF M_L, of ?i] D S by auto
show ?thesis using backtrack_rule[OF S K L L_D] by (meson bj cdcl⇩W_bj.simps state_eq_ref)
qed
lemma cdcl⇩W_stgy_final_state_conclusive:
assumes termi: "∀S'. ¬cdcl⇩W_stgy S S'"
and decomp: "all_decomposition_implies_m (init_clss S) (get_all_decided_decomposition (trail S))"
and learned: "cdcl⇩W_learned_clause S"
and level_inv: "cdcl⇩W_M_level_inv S"
and alien: "no_strange_atm S"
and no_dup: "distinct_cdcl⇩W_state S"
and confl: "cdcl⇩W_conflicting S"
and confl_k: "conflict_is_false_with_level S"
shows "(conflicting S = Some {#} ∧ unsatisfiable (set_mset (init_clss S)))
∨ (conflicting S = None ∧ trail S ⊨as set_mset (init_clss S))"
proof -
let ?M = "trail S"
let ?N = "init_clss S"
let ?k = "backtrack_lvl S"
let ?U = "learned_clss S"
have "conflicting S = Some {#}
∨ conflicting S = None
∨ (∃D L. conflicting S = Some (D + {#L#}))"
apply (cases "conflicting S", auto)
by (rename_tac C, case_tac C, auto)
moreover {
assume "conflicting S = Some {#}"
then have "unsatisfiable (set_mset (init_clss S))"
using assms(3) unfolding cdcl⇩W_learned_clause_def true_clss_cls_def
by (metis (no_types, lifting) Un_insert_right atms_of_empty satisfiable_def
sup_bot.right_neutral total_over_m_insert total_over_set_empty true_cls_empty)
}
moreover {
assume "conflicting S = None"
{ assume "¬?M ⊨asm ?N"
have "atm_of ` (lits_of ?M) = atms_of_msu ?N" (is "?A = ?B")
proof
show "?A ⊆ ?B" using alien unfolding no_strange_atm_def by auto
show "?B ⊆ ?A"
proof (rule ccontr)
assume "¬?B ⊆ ?A"
then obtain l where "l ∈ ?B" and "l ∉ ?A" by auto
then have "undefined_lit ?M (Pos l)"
using ‹l ∉ ?A› unfolding lits_of_def by (auto simp add: defined_lit_map)
then have "∃S'. cdcl⇩W_o S S'"
using cdcl⇩W_o.decide decide.intros ‹l ∈ ?B› no_strange_atm_def
by (metis ‹conflicting S = None› literal.sel(1) state_eq_def)
then show False
using termi cdcl⇩W_then_exists_cdcl⇩W_stgy_step[OF _ alien] level_inv by blast
qed
qed
obtain D where "¬ ?M ⊨a D" and "D ∈# ?N"
using ‹¬?M ⊨asm ?N› unfolding lits_of_def true_annots_def Ball_def by auto
have "atms_of D ⊆ atm_of ` (lits_of ?M)"
using ‹D ∈# ?N› unfolding ‹atm_of ` (lits_of ?M) = atms_of_msu ?N› atms_of_ms_def
by (auto simp add: atms_of_def)
then have a1: "atm_of ` set_mset D ⊆ atm_of ` lits_of (trail S)"
by (auto simp add: atms_of_def lits_of_def)
have "total_over_m (lits_of ?M) {D}"
using ‹atms_of D ⊆ atm_of ` (lits_of ?M)› atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
by (fastforce simp: total_over_set_def)
then have "?M ⊨as CNot D"
using total_not_true_cls_true_clss_CNot ‹¬ trail S ⊨a D› true_annot_def
true_annots_true_cls by fastforce
then have False
proof -
obtain S' where
f2: "full cdcl⇩W_cp S S'"
by (meson alien always_exists_full_cdcl⇩W_cp_step level_inv)
then have "S' = S"
using cdcl⇩W_stgy.conflict'[of S] by (metis (no_types) full_unfold termi)
then show ?thesis
using f2 ‹D ∈# init_clss S› ‹conflicting S = None› ‹trail S ⊨as CNot D›
clauses_def full_cdcl⇩W_cp_not_any_negated_init_clss by auto
qed
}
then have "?M ⊨asm ?N" by blast
}
moreover {
assume "∃D L. conflicting S = Some (D + {#L#})"
then obtain D L where LD: "conflicting S = Some (D + {#L#})" and lev_L: "get_level ?M L = ?k"
by (metis (mono_tags) bex_msetE confl_k insert_DiffM2 multi_self_add_other_not_self
union_eq_empty)
let ?D = "D + {#L#}"
have "?D ≠ {#}" by auto
have "?M ⊨as CNot ?D" using confl LD unfolding cdcl⇩W_conflicting_def by auto
then have "?M ≠ []" unfolding true_annots_def Ball_def true_annot_def true_cls_def by force
{ have M: "?M = hd ?M # tl ?M" using ‹?M ≠ []› list.collapse by fastforce
assume decided: "is_decided (hd ?M)"
then obtain k' where k': "k' + 1 = ?k"
using level_inv M unfolding cdcl⇩W_M_level_inv_def
by (cases "hd (trail S)"; cases "trail S") auto
obtain L' l' where L': "hd ?M = Decided L' l'" using decided by (cases "hd ?M") auto
have decided_hd_tl: "get_all_levels_of_decided (hd (trail S) # tl (trail S))
= rev [1..<1 + length (get_all_levels_of_decided ?M)]"
using level_inv lev_L M unfolding cdcl⇩W_M_level_inv_def M[symmetric]
by blast
then have l'_tl: "l' # get_all_levels_of_decided (tl ?M)
= rev [1..<1 + length (get_all_levels_of_decided ?M)]" unfolding L' by simp
moreover have "… = length (get_all_levels_of_decided ?M)
# rev [1..<length (get_all_levels_of_decided ?M)]"
using M Suc_le_mono calculation by (fastforce simp add: upt.simps(2))
finally have
"l' = ?k" and
g_r: "get_all_levels_of_decided (tl (trail S))
= rev [1..<length (get_all_levels_of_decided (trail S))]"
using level_inv lev_L M unfolding cdcl⇩W_M_level_inv_def by auto
have *: "⋀list. no_dup list ⟹
- L ∈ lits_of list ⟹ atm_of L ∈ atm_of ` lits_of list"
by (metis atm_of_uminus imageI)
have "L' = -L"
proof (rule ccontr)
assume "¬ ?thesis"
moreover have "-L ∈ lits_of ?M" using confl LD unfolding cdcl⇩W_conflicting_def by auto
ultimately have "get_level (hd (trail S) # tl (trail S)) L = get_level (tl ?M) L"
using cdcl⇩W_M_level_inv_decomp(1)[OF level_inv] unfolding L' consistent_interp_def
by (metis (no_types, lifting) L' M atm_of_eq_atm_of get_level_skip_beginning insert_iff
lits_of_cons ann_literal.sel(1))
moreover
have "length (get_all_levels_of_decided (trail S)) = ?k"
using level_inv unfolding cdcl⇩W_M_level_inv_def by auto
then have "Max (set (0#get_all_levels_of_decided (tl (trail S)))) = ?k - 1"
unfolding g_r by (auto simp add: Max_n_upt)
then have "get_level (tl ?M) L < ?k"
using get_maximum_possible_level_ge_get_level[of "tl ?M" L]
by (metis One_nat_def add.right_neutral add_Suc_right diff_add_inverse2
get_maximum_possible_level_max_get_all_levels_of_decided k' le_imp_less_Suc
list.simps(15))
finally show False using lev_L M by auto
qed
have L: "hd ?M = Decided (-L) ?k" using ‹l' = ?k› ‹L' = -L› L' by auto
have g_a_l: "get_all_levels_of_decided ?M = rev [1..<1 + ?k]"
using level_inv lev_L M unfolding cdcl⇩W_M_level_inv_def by auto
have g_k: "get_maximum_level (trail S) D ≤ ?k"
using get_maximum_possible_level_ge_get_maximum_level[of ?M]
get_maximum_possible_level_max_get_all_levels_of_decided[of ?M]
by (auto simp add: Max_n_upt g_a_l)
have "get_maximum_level (trail S) D < ?k"
proof (rule ccontr)
assume "¬ ?thesis"
then have "get_maximum_level (trail S) D = ?k" using M g_k unfolding L by auto
then obtain L' where "L' ∈# D" and L_k: "get_level ?M L' = ?k"
using get_maximum_level_exists_lit[of ?k ?M D] unfolding k'[symmetric] by auto
have "L ≠ L'" using no_dup ‹L' ∈# D›
unfolding distinct_cdcl⇩W_state_def LD by (metis add.commute add_eq_self_zero
count_single count_union less_not_refl3 distinct_mset_def union_single_eq_member)
have "L' = -L"
proof (rule ccontr)
assume "¬ ?thesis"
then have "get_level ?M L' = get_level (tl ?M) L'"
using M ‹L ≠ L'› get_level_skip_beginning[of L' "hd ?M" "tl ?M"] unfolding L
by (auto simp: atm_of_eq_atm_of)
moreover have "… < ?k"
proof -
{ assume a1: "get_level (tl (trail S)) L' = backtrack_lvl S"
assume a2: "rev (get_all_levels_of_decided (tl (trail S))) =
[Suc 0..<backtrack_lvl S]"
have "k' + Suc 0 = backtrack_lvl S"
using k' by presburger
then have False
using a2 a1 by (metis (no_types) Max_n_upt Zero_neq_Suc add_diff_cancel_left'
add_diff_cancel_right' diff_is_0_eq
get_all_levels_of_decided_rev_eq_rev_get_all_levels_of_decided
get_rev_level_less_max_get_all_levels_of_decided list.set(2) set_upt)
}
then show ?thesis
using g_r get_rev_level_less_max_get_all_levels_of_decided[of "rev (tl ?M)" 0 L]
l'_tl calculation[symmetric] g_a_l L_k
by (auto simp: Max_n_upt cdcl⇩W_M_level_inv_def rev_swap[symmetric])
qed
finally show False using L_k by simp
qed
then have taut: "tautology (D + {#L#})"
using ‹L' ∈# D› by (metis add.commute mset_leD mset_le_add_left multi_member_this
tautology_minus)
have "consistent_interp (lits_of ?M)"
using level_inv unfolding cdcl⇩W_M_level_inv_def by auto
then have "¬?M ⊨as CNot ?D"
using taut by (metis (no_types) ‹L' = - L› ‹L' ∈# D› add.commute consistent_interp_def
in_CNot_implies_uminus(2) mset_leD mset_le_add_left multi_member_this)
moreover have "?M ⊨as CNot ?D"
using confl no_dup LD unfolding cdcl⇩W_conflicting_def by auto
ultimately show False by blast
qed
then have False
using backtrack_no_decomp[OF _ ‹get_level (trail S) L = backtrack_lvl S› _ level_inv]
LD alien termi by (metis cdcl⇩W_then_exists_cdcl⇩W_stgy_step level_inv)
}
moreover {
assume "¬is_decided (hd ?M)"
then obtain L' C where L'C: "hd ?M = Propagated L' C" by (cases "hd ?M", auto)
then have M: "?M = Propagated L' C # tl ?M" using ‹?M ≠ []› list.collapse by fastforce
then obtain C' where C': " C = C' + {#L'#}"
using confl unfolding cdcl⇩W_conflicting_def by (metis append_Nil diff_single_eq_union)
{ assume "-L' ∉# ?D"
then have False
using bj[OF cdcl⇩W_bj.skip[OF skip_rule[OF _ ‹-L' ∉# ?D› ‹?D ≠ {#}›, of S C "tl (trail S)" _
]]]
termi M by (metis LD alien cdcl⇩W_then_exists_cdcl⇩W_stgy_step state_eq_def level_inv)
}
moreover {
assume "-L' ∈# ?D"
then obtain D' where D': "?D = D' + {#-L'#}" by (metis insert_DiffM2)
have g_r: "get_all_levels_of_decided (Propagated L' C # tl (trail S))
= rev [Suc 0..<Suc (length (get_all_levels_of_decided (trail S)))]"
using level_inv M unfolding cdcl⇩W_M_level_inv_def by auto
have "Max (insert 0 (set (get_all_levels_of_decided (Propagated L' C # tl (trail S))))) = ?k"
using level_inv M unfolding g_r cdcl⇩W_M_level_inv_def set_rev
by (auto simp add:Max_n_upt)
then have "get_maximum_level (Propagated L' C # tl ?M) D' ≤ ?k"
using get_maximum_possible_level_ge_get_maximum_level[of "Propagated L' C # tl ?M"]
unfolding get_maximum_possible_level_max_get_all_levels_of_decided by auto
then have "get_maximum_level (Propagated L' C # tl ?M) D' = ?k
∨ get_maximum_level (Propagated L' C # tl ?M) D' < ?k"
using le_neq_implies_less by blast
moreover {
assume g_D'_k: "get_maximum_level (Propagated L' C # tl ?M) D' = ?k"
have False
proof -
have f1: "get_maximum_level (trail S) D' = backtrack_lvl S"
using M g_D'_k by auto
have "(trail S, init_clss S, learned_clss S, backtrack_lvl S, Some (D + {#L#}))
= state S"
by (metis (no_types) LD)
then have "cdcl⇩W_o S (update_conflicting (Some (D' #∪ C')) (tl_trail S))"
using f1 bj[OF cdcl⇩W_bj.resolve[OF resolve_rule[of S L' C' "tl ?M" ?N ?U ?k D']]]
C' D' M by (metis state_eq_def)
then show ?thesis
by (meson alien cdcl⇩W_then_exists_cdcl⇩W_stgy_step termi level_inv)
qed
}
moreover {
assume "get_maximum_level (Propagated L' C # tl ?M) D' < ?k"
then have False
proof -
assume a1: "get_maximum_level (Propagated L' C # tl (trail S)) D' < backtrack_lvl S"
obtain mm :: "'v literal multiset" and ll :: "'v literal" where
f2: "conflicting S = Some (mm + {#ll#})"
"get_level (trail S) ll = backtrack_lvl S"
using LD ‹get_level (trail S) L = backtrack_lvl S› by blast
then have f3: "get_maximum_level (trail S) D' ≤ get_level (trail S) ll"
using M a1 by force
have lev_neq: "get_level (trail S) ll ≠ get_maximum_level (trail S) D'"
using f2 M calculation(2) by presburger
have f1: "trail S = Propagated L' C # tl (trail S)"
"conflicting S = Some (D' + {#- L'#})"
using D' LD M by force+
have f2: "conflicting S = Some (mm + {#ll#}) "
"get_level (trail S) ll = backtrack_lvl S"
using f2 by force+
have "ll = - L'"
by (metis (no_types) D' LD lev_neq option.inject f2 f3 le_antisym
get_maximum_level_ge_get_level insert_noteq_member)
then show ?thesis
using f2 f1 M backtrack_no_decomp[of S]
by (metis (no_types) a1 alien cdcl⇩W_then_exists_cdcl⇩W_stgy_step level_inv termi)
qed
}
ultimately have False by blast
}
ultimately have False by blast
}
ultimately have False by blast
}
ultimately show ?thesis by blast
qed
lemma cdcl⇩W_cp_tranclp_cdcl⇩W:
"cdcl⇩W_cp S S' ⟹ cdcl⇩W⇧+⇧+ S S'"
apply (induct rule: cdcl⇩W_cp.induct)
by (meson cdcl⇩W.conflict cdcl⇩W.propagate tranclp.r_into_trancl tranclp.trancl_into_trancl)+
lemma tranclp_cdcl⇩W_cp_tranclp_cdcl⇩W:
"cdcl⇩W_cp⇧+⇧+ S S' ⟹ cdcl⇩W⇧+⇧+ S S'"
apply (induct rule: tranclp.induct)
apply (simp add: cdcl⇩W_cp_tranclp_cdcl⇩W)
by (meson cdcl⇩W_cp_tranclp_cdcl⇩W tranclp_trans)
lemma cdcl⇩W_stgy_tranclp_cdcl⇩W:
"cdcl⇩W_stgy S S' ⟹ cdcl⇩W⇧+⇧+ S S'"
proof (induct rule: cdcl⇩W_stgy.induct)
case conflict'
then show ?case
unfolding full1_def by (simp add: tranclp_cdcl⇩W_cp_tranclp_cdcl⇩W)
next
case (other' S' S'')
then have "S' = S'' ∨ cdcl⇩W_cp⇧+⇧+ S' S''"
by (simp add: rtranclp_unfold full_def)
then show ?case
using other' by (meson cdcl⇩W.other cdcl⇩W_axioms tranclp.r_into_trancl
tranclp_cdcl⇩W_cp_tranclp_cdcl⇩W tranclp_trans)
qed
lemma tranclp_cdcl⇩W_stgy_tranclp_cdcl⇩W:
"cdcl⇩W_stgy⇧+⇧+ S S' ⟹ cdcl⇩W⇧+⇧+ S S'"
apply (induct rule: tranclp.induct)
using cdcl⇩W_stgy_tranclp_cdcl⇩W apply blast
by (meson cdcl⇩W_stgy_tranclp_cdcl⇩W tranclp_trans)
lemma rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W:
"cdcl⇩W_stgy⇧*⇧* S S' ⟹ cdcl⇩W⇧*⇧* S S'"
using rtranclp_unfold[of cdcl⇩W_stgy S S'] tranclp_cdcl⇩W_stgy_tranclp_cdcl⇩W[of S S'] by auto
lemma cdcl⇩W_o_conflict_is_false_with_level_inv:
assumes
"cdcl⇩W_o S S'" and
lev: "cdcl⇩W_M_level_inv S" and
confl_inv: "conflict_is_false_with_level S" and
n_d: "distinct_cdcl⇩W_state S" and
conflicting: "cdcl⇩W_conflicting S"
shows "conflict_is_false_with_level S'"
using assms(1,2)
proof (induct rule: cdcl⇩W_o_induct_lev2)
case (resolve L C M D T) note tr_S = this(1) and confl = this(2) and T = this(4)
have "-L ∉# D" using n_d confl unfolding distinct_cdcl⇩W_state_def distinct_mset_def by auto
moreover have "L ∉# D"
proof (rule ccontr)
assume "¬ ?thesis"
moreover have "Propagated L (C + {#L#}) # M ⊨as CNot D"
using conflicting confl tr_S unfolding cdcl⇩W_conflicting_def by auto
ultimately have "-L ∈ lits_of (Propagated L ( (C + {#L#})) # M)"
using in_CNot_implies_uminus(2) by blast
moreover have "no_dup (Propagated L ( (C + {#L#})) # M)"
using lev tr_S unfolding cdcl⇩W_M_level_inv_def by auto
ultimately show False unfolding lits_of_def by (metis consistent_interp_def image_eqI
list.set_intros(1) lits_of_def ann_literal.sel(2) distinctconsistent_interp)
qed
ultimately
have g_D: "get_maximum_level (Propagated L (C + {#L#}) # M) D
= get_maximum_level M D"
proof -
have "∀a f L. ((a::'v) ∈ f ` L) = (∃l. (l::'v literal) ∈ L ∧ a = f l)"
by blast
then show ?thesis
using get_maximum_level_skip_first[of L D " (C + {#L#})" M] unfolding atms_of_def
by (metis (no_types) ‹- L ∉# D› ‹L ∉# D› atm_of_eq_atm_of mem_set_mset_iff)
qed
{ assume
"get_maximum_level (Propagated L (C + {#L#}) # M) D = backtrack_lvl S" and
"backtrack_lvl S > 0"
then have D: "get_maximum_level M D = backtrack_lvl S" unfolding g_D by blast
then have ?case
using tr_S ‹backtrack_lvl S > 0› get_maximum_level_exists_lit[of "backtrack_lvl S" M D] T
by auto
}
moreover {
assume [simp]: "backtrack_lvl S = 0"
have "⋀L. get_level M L = 0"
proof -
fix L
have "atm_of L ∉ atm_of ` (lits_of M) ⟹ get_level M L = 0" by auto
moreover {
assume "atm_of L ∈ atm_of ` (lits_of M)"
have g_r: "get_all_levels_of_decided M = rev [Suc 0..<Suc (backtrack_lvl S)]"
using lev tr_S unfolding cdcl⇩W_M_level_inv_def by auto
have "Max (insert 0 (set (get_all_levels_of_decided M))) = (backtrack_lvl S)"
unfolding g_r by (simp add: Max_n_upt)
then have "get_level M L = 0"
using get_maximum_possible_level_ge_get_level[of M L]
unfolding get_maximum_possible_level_max_get_all_levels_of_decided by auto
}
ultimately show "get_level M L = 0" by blast
qed
then have ?case using get_maximum_level_exists_lit_of_max_level[of "D#∪C" M] tr_S T
by (auto simp: Bex_mset_def)
}
ultimately show ?case using resolve.hyps(3) by blast
next
case (skip L C' M D T) note tr_S = this(1) and D = this(2) and T =this(5)
then obtain La where "La ∈# D" and "get_level (Propagated L C' # M) La = backtrack_lvl S"
using skip confl_inv by auto
moreover
have "atm_of La ≠ atm_of L"
proof (rule ccontr)
assume "¬ ?thesis"
then have La: "La = L" using ‹La ∈# D› ‹- L ∉# D› by (auto simp add: atm_of_eq_atm_of)
have "Propagated L C' # M ⊨as CNot D"
using conflicting tr_S D unfolding cdcl⇩W_conflicting_def by auto
then have "-L ∈ lits_of M"
using ‹La ∈# D› in_CNot_implies_uminus(2)[of D L "Propagated L C' # M"] unfolding La
by auto
then show False using lev tr_S unfolding cdcl⇩W_M_level_inv_def consistent_interp_def by auto
qed
then have "get_level (Propagated L C' # M) La = get_level M La" by auto
ultimately show ?case using D tr_S T by auto
qed (auto split: split_if_asm simp: cdcl⇩W_M_level_inv_decomp)
subsubsection ‹Strong completeness›
lemma cdcl⇩W_cp_propagate_confl:
assumes "cdcl⇩W_cp S T"
shows "propagate⇧*⇧* S T ∨ (∃S'. propagate⇧*⇧* S S' ∧ conflict S' T)"
using assms by induction blast+
lemma rtranclp_cdcl⇩W_cp_propagate_confl:
assumes "cdcl⇩W_cp⇧*⇧* S T"
shows "propagate⇧*⇧* S T ∨ (∃S'. propagate⇧*⇧* S S' ∧ conflict S' T)"
by (simp add: assms rtranclp_cdcl⇩W_cp_propa_or_propa_confl)
lemma cdcl⇩W_cp_propagate_completeness:
assumes MN: "set M ⊨s set_mset N" and
cons: "consistent_interp (set M)" and
tot: "total_over_m (set M) (set_mset N)" and
"lits_of (trail S) ⊆ set M" and
"init_clss S = N" and
"propagate⇧*⇧* S S'" and
"learned_clss S = {#}"
shows "length (trail S) ≤ length (trail S') ∧ lits_of (trail S') ⊆ set M"
using assms(6,4,5,7)
proof (induction rule: rtranclp_induct)
case base
then show ?case by auto
next
case (step Y Z)
note st = this(1) and propa = this(2) and IH = this(3) and lits' = this(4) and NS = this(5) and
learned = this(6)
then have len: "length (trail S) ≤ length (trail Y)" and LM: "lits_of (trail Y) ⊆ set M"
by blast+
obtain M' N' U k C L where
Y: "state Y = (M', N', U, k, None)" and
Z: "state Z = (Propagated L (C + {#L#}) # M', N', U, k, None)" and
C: "C + {#L#} ∈# clauses Y" and
M'_C: "M' ⊨as CNot C" and
"undefined_lit (trail Y) L"
using propa by auto
have "init_clss S = init_clss Y"
using st by induction auto
then have [simp]: "N' = N" using NS Y Z by simp
have "learned_clss Y = {#}"
using st learned by induction auto
then have [simp]: "U = {#}" using Y by auto
have "set M ⊨s CNot C"
using M'_C LM Y unfolding true_annots_def Ball_def true_annot_def true_clss_def true_cls_def
by force
moreover
have "set M ⊨ C + {#L#}"
using MN C learned Y unfolding true_clss_def clauses_def
by (metis NS ‹init_clss S = init_clss Y› ‹learned_clss Y = {#}› add.right_neutral
mem_set_mset_iff)
ultimately have "L ∈ set M" by (simp add: cons consistent_CNot_not)
then show ?case using LM len Y Z by auto
qed
lemma completeness_is_a_full1_propagation:
fixes S :: "'st" and M :: "'v literal list"
assumes MN: "set M ⊨s set_mset N"
and cons: "consistent_interp (set M)"
and tot: "total_over_m (set M) (set_mset N)"
and alien: "no_strange_atm S"
and learned: "learned_clss S = {#}"
and clsS[simp]: "init_clss S = N"
and lits: "lits_of (trail S) ⊆ set M"
shows "∃S'. propagate⇧*⇧* S S' ∧ full cdcl⇩W_cp S S'"
proof -
obtain S' where full: "full cdcl⇩W_cp S S'"
using always_exists_full_cdcl⇩W_cp_step alien by blast
then consider (propa) "propagate⇧*⇧* S S'"
| (confl) "∃X. propagate⇧*⇧* S X ∧ conflict X S'"
using rtranclp_cdcl⇩W_cp_propagate_confl unfolding full_def by blast
then show ?thesis
proof cases
case propa then show ?thesis using full by blast
next
case confl
then obtain X where
X: "propagate⇧*⇧* S X" and
Xconf: "conflict X S'"
by blast
have clsX: "init_clss X = init_clss S"
using X by induction auto
have learnedX: "learned_clss X = {#}" using X learned by induction auto
obtain E where
E: "E ∈# init_clss X + learned_clss X" and
Not_E: "trail X ⊨as CNot E"
using Xconf by (auto simp add: conflict.simps clauses_def)
have "lits_of (trail X) ⊆ set M"
using cdcl⇩W_cp_propagate_completeness[OF assms(1-3) lits _ X learned] learned by auto
then have MNE: "set M ⊨s CNot E"
using Not_E
by (fastforce simp add: true_annots_def true_annot_def true_clss_def true_cls_def)
have "¬ set M ⊨s set_mset N"
using E consistent_CNot_not[OF cons MNE]
unfolding learnedX true_clss_def unfolding clsX clsS by auto
then show ?thesis using MN by blast
qed
qed
text ‹See also @{thm rtranclp_cdcl⇩W_cp_dropWhile_trail}›
lemma rtranclp_propagate_is_trail_append:
"propagate⇧*⇧* S T ⟹ ∃c. trail T = c @ trail S"
by (induction rule: rtranclp_induct) auto
lemma rtranclp_propagate_is_update_trail:
"propagate⇧*⇧* S T ⟹ cdcl⇩W_M_level_inv S ⟹ T ∼ delete_trail_and_rebuild (trail T) S"
proof (induction rule: rtranclp_induct)
case base
then show ?case unfolding state_eq_def by (auto simp: cdcl⇩W_M_level_inv_decomp state_access_simp)
next
case (step T U) note IH=this(3)[OF this(4)]
moreover have "cdcl⇩W_M_level_inv U"
using rtranclp_cdcl⇩W_consistent_inv ‹propagate⇧*⇧* S T› ‹propagate T U›
rtranclp_mono[of propagate cdcl⇩W] cdcl⇩W_cp_consistent_inv propagate'
rtranclp_propagate_is_rtranclp_cdcl⇩W step.prems by blast
then have "no_dup (trail U)" unfolding cdcl⇩W_M_level_inv_def by auto
ultimately show ?case using ‹propagate T U› unfolding state_eq_def
by (fastforce simp: state_access_simp)
qed
lemma cdcl⇩W_stgy_strong_completeness_n:
assumes
MN: "set M ⊨s set_mset N" and
cons: "consistent_interp (set M)" and
tot: "total_over_m (set M) (set_mset N)" and
atm_incl: "atm_of ` (set M) ⊆ atms_of_msu N" and
distM: "distinct M" and
length: "n ≤ length M"
shows
"∃M' k S. length M' ≥ n ∧
lits_of M' ⊆ set M ∧
no_dup M' ∧
S ∼ update_backtrack_lvl k (append_trail (rev M') (init_state N)) ∧
cdcl⇩W_stgy⇧*⇧* (init_state N) S"
using length
proof (induction n)
case 0
have "update_backtrack_lvl 0 (append_trail (rev []) (init_state N)) ∼ init_state N"
by (auto simp: state_eq_def simp del: state_simp)
moreover have
"0 ≤ length []" and
"lits_of [] ⊆ set M" and
"cdcl⇩W_stgy⇧*⇧* (init_state N) (init_state N)"
and "no_dup []"
by (auto simp: state_eq_def simp del: state_simp)
ultimately show ?case using state_eq_sym by blast
next
case (Suc n) note IH = this(1) and n = this(2)
then obtain M' k S where
l_M': "length M' ≥ n" and
M': "lits_of M' ⊆ set M" and
n_d[simp]: "no_dup M'" and
S: "S ∼ update_backtrack_lvl k (append_trail (rev M') (init_state N))" and
st: "cdcl⇩W_stgy⇧*⇧* (init_state N) S"
by auto
have
M: "cdcl⇩W_M_level_inv S" and
alien: "no_strange_atm S"
using rtranclp_cdcl⇩W_consistent_inv[OF rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W[OF st]]
rtranclp_cdcl⇩W_no_strange_atm_inv[OF rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W[OF st]]
S unfolding state_eq_def cdcl⇩W_M_level_inv_def no_strange_atm_def by auto
{ assume no_step: "¬no_step propagate S"
obtain S' where S': "propagate⇧*⇧* S S'" and full: "full cdcl⇩W_cp S S'"
using completeness_is_a_full1_propagation[OF assms(1-3), of S] alien M' S
by (auto simp: state_access_simp)
have lev: "cdcl⇩W_M_level_inv S'"
using M S' rtranclp_cdcl⇩W_consistent_inv rtranclp_propagate_is_rtranclp_cdcl⇩W by blast
then have n_d'[simp]: "no_dup (trail S')"
unfolding cdcl⇩W_M_level_inv_def by auto
have "length (trail S) ≤ length (trail S') ∧ lits_of (trail S') ⊆ set M"
using S' full cdcl⇩W_cp_propagate_completeness[OF assms(1-3), of S] M' S
by (auto simp: state_access_simp)
moreover
have full: "full1 cdcl⇩W_cp S S'"
using full no_step no_step_cdcl⇩W_cp_no_conflict_no_propagate(2) unfolding full1_def full_def
rtranclp_unfold by blast
then have "cdcl⇩W_stgy S S'" by (simp add: cdcl⇩W_stgy.conflict')
moreover
have propa: "propagate⇧+⇧+ S S'" using S' full unfolding full1_def by (metis rtranclpD tranclpD)
have "trail S = M'" using S by (auto simp: state_access_simp)
with propa have "length (trail S') > n"
using l_M' propa by (induction rule: tranclp.induct) auto
moreover
have stS': "cdcl⇩W_stgy⇧*⇧* (init_state N) S'"
using st cdcl⇩W_stgy.conflict'[OF full] by auto
then have "init_clss S' = N" using stS' rtranclp_cdcl⇩W_stgy_no_more_init_clss by fastforce
moreover
have
[simp]:"learned_clss S' = {#}" and
[simp]: "init_clss S' = init_clss S" and
[simp]: "conflicting S' = None"
using tranclp_into_rtranclp[OF ‹propagate⇧+⇧+ S S'›] S
rtranclp_propagate_is_update_trail[of S S'] S M unfolding state_eq_def
by (auto simp: state_access_simp)
have S_S': "S' ∼ update_backtrack_lvl (backtrack_lvl S')
(append_trail (rev (trail S')) (init_state N))" using S
by (auto simp: state_eq_def state_access_simp simp del: state_simp)
have "cdcl⇩W_stgy⇧*⇧* (init_state (init_clss S')) S'"
apply (rule rtranclp.rtrancl_into_rtrancl)
using st unfolding ‹init_clss S' = N› apply simp
using ‹cdcl⇩W_stgy S S'› by simp
ultimately have ?case
apply -
apply (rule exI[of _ "trail S'"], rule exI[of _ "backtrack_lvl S'"], rule exI[of _ S'])
using S_S' by (auto simp: state_eq_def simp del: state_simp)
}
moreover {
assume no_step: "no_step propagate S"
have ?case
proof (cases "length M' ≥ Suc n")
case True
then show ?thesis using l_M' M' st M alien S by fastforce
next
case False
then have n': "length M' = n" using l_M' by auto
have no_confl: "no_step conflict S"
proof -
{ fix D
assume "D ∈# N" and "M' ⊨as CNot D"
then have "set M ⊨ D" using MN unfolding true_clss_def by auto
moreover have "set M ⊨s CNot D"
using ‹M' ⊨as CNot D› M'
by (metis le_iff_sup true_annots_true_cls true_clss_union_increase)
ultimately have False using cons consistent_CNot_not by blast
}
then show ?thesis using S by (auto simp: conflict.simps true_clss_def state_access_simp)
qed
have lenM: "length M = card (set M)" using distM by (induction M) auto
have "no_dup M'" using S M unfolding cdcl⇩W_M_level_inv_def by auto
then have "card (lits_of M') = length M'"
by (induction M') (auto simp add: lits_of_def card_insert_if)
then have "lits_of M' ⊂ set M"
using n M' n' lenM by auto
then obtain m where m: "m ∈ set M" and undef_m: "m ∉ lits_of M'" by auto
moreover have undef: "undefined_lit M' m"
using M' Decided_Propagated_in_iff_in_lits_of calculation(1,2) cons
consistent_interp_def by blast
moreover have "atm_of m ∈ atms_of_msu (init_clss S)"
using atm_incl calculation S by (auto simp: state_access_simp)
ultimately
have dec: "decide S (cons_trail (Decided m (k+1)) (incr_lvl S))"
using decide.intros[of S "rev M'" N _ k m
"cons_trail (Decided m (k + 1)) (incr_lvl S)"] S
by (auto simp: state_access_simp)
let ?S' = "cons_trail (Decided m (k+1)) (incr_lvl S)"
have "lits_of (trail ?S') ⊆ set M" using m M' S undef by (auto simp: state_access_simp)
moreover have "no_strange_atm ?S'"
using alien dec M by (meson cdcl⇩W_no_strange_atm_inv decide other)
ultimately obtain S'' where S'': "propagate⇧*⇧* ?S' S''" and full: "full cdcl⇩W_cp ?S' S''"
using completeness_is_a_full1_propagation[OF assms(1-3), of ?S'] S undef
by (auto simp: state_access_simp)
have "cdcl⇩W_M_level_inv ?S'"
using M dec rtranclp_mono[of decide cdcl⇩W] by (meson cdcl⇩W_consistent_inv decide other)
then have lev'': "cdcl⇩W_M_level_inv S''"
using S'' rtranclp_cdcl⇩W_consistent_inv rtranclp_propagate_is_rtranclp_cdcl⇩W by blast
then have n_d'': "no_dup (trail S'')"
unfolding cdcl⇩W_M_level_inv_def by auto
have "length (trail ?S') ≤ length (trail S'') ∧ lits_of (trail S'') ⊆ set M"
using S'' full cdcl⇩W_cp_propagate_completeness[OF assms(1-3), of ?S' S''] m M' S undef
by (simp add: state_access_simp)
then have "Suc n ≤ length (trail S'') ∧ lits_of (trail S'') ⊆ set M"
using l_M' S undef by (auto simp: state_access_simp)
moreover
have "cdcl⇩W_M_level_inv (cons_trail (Decided m (Suc (backtrack_lvl S)))
(update_backtrack_lvl (Suc (backtrack_lvl S)) S))"
using S ‹cdcl⇩W_M_level_inv (cons_trail (Decided m (k + 1)) (incr_lvl S))› by auto
then have S'': "S'' ∼ update_backtrack_lvl (backtrack_lvl S'')
(append_trail (rev (trail S'')) (init_state N))"
using rtranclp_propagate_is_update_trail[OF S''] S undef n_d'' lev''
by (auto simp del: state_simp simp: state_eq_def state_access_simp)
then have "cdcl⇩W_stgy⇧*⇧* (init_state N) S''"
using cdcl⇩W_stgy.intros(2)[OF decide[OF dec] _ full] no_step no_confl st
by (auto simp: cdcl⇩W_cp.simps)
ultimately show ?thesis using S'' n_d'' by blast
qed
}
ultimately show ?case by blast
qed
lemma cdcl⇩W_stgy_strong_completeness:
assumes MN: "set M ⊨s set_mset N"
and cons: "consistent_interp (set M)"
and tot: "total_over_m (set M) (set_mset N)"
and atm_incl: "atm_of ` (set M) ⊆ atms_of_msu N"
and distM: "distinct M"
shows
"∃M' k S.
lits_of M' = set M ∧
S ∼ update_backtrack_lvl k (append_trail (rev M') (init_state N)) ∧
cdcl⇩W_stgy⇧*⇧* (init_state N) S ∧
final_cdcl⇩W_state S"
proof -
from cdcl⇩W_stgy_strong_completeness_n[OF assms, of "length M"]
obtain M' k T where
l: "length M ≤ length M'" and
M'_M: "lits_of M' ⊆ set M" and
no_dup: "no_dup M'" and
T: "T ∼ update_backtrack_lvl k (append_trail (rev M') (init_state N))" and
st: "cdcl⇩W_stgy⇧*⇧* (init_state N) T"
by auto
have "card (set M) = length M" using distM by (simp add: distinct_card)
moreover
have "cdcl⇩W_M_level_inv T"
using rtranclp_cdcl⇩W_stgy_consistent_inv[OF st] T by auto
then have "card (set ((map (λl. atm_of (lit_of l)) M'))) = length M'"
using distinct_card no_dup by fastforce
moreover have "card (lits_of M') = card (set ((map (λl. atm_of (lit_of l)) M')))"
using no_dup unfolding lits_of_def apply (induction M') by (auto simp add: card_insert_if)
ultimately have "card (set M) ≤ card (lits_of M')" using l unfolding lits_of_def by auto
then have "set M = lits_of M'"
using M'_M card_seteq by blast
moreover
then have "M' ⊨asm N"
using MN unfolding true_annots_def Ball_def true_annot_def true_clss_def by auto
then have "final_cdcl⇩W_state T"
using T no_dup unfolding final_cdcl⇩W_state_def by (auto simp: state_access_simp)
ultimately show ?thesis using st T by blast
qed
subsubsection ‹No conflict with only variables of level less than backtrack level›
text ‹This invariant is stronger than the previous argument in the sense that it is a property about
all possible conflicts.›
definition "no_smaller_confl (S::'st) ≡
(∀M K i M' D. M' @ Decided K i # M = trail S ⟶ D ∈# clauses S
⟶ ¬M ⊨as CNot D)"
lemma no_smaller_confl_init_sate[simp]:
"no_smaller_confl (init_state N)" unfolding no_smaller_confl_def by auto
lemma cdcl⇩W_o_no_smaller_confl_inv:
fixes S S' :: "'st"
assumes
"cdcl⇩W_o S S'" and
lev: "cdcl⇩W_M_level_inv S" and
max_lev: "conflict_is_false_with_level S" and
smaller: "no_smaller_confl S" and
no_f: "no_clause_is_false S"
shows "no_smaller_confl S'"
using assms(1,2) unfolding no_smaller_confl_def
proof (induct rule: cdcl⇩W_o_induct_lev2)
case (decide L T) note confl = this(1) and undef = this(2) and T = this(4)
have [simp]: "clauses T = clauses S"
using T undef by auto
show ?case
proof (intro allI impI)
fix M'' K i M' Da
assume "M'' @ Decided K i # M' = trail T"
and D: "Da ∈# local.clauses T"
then have "tl M'' @ Decided K i # M' = trail S
∨ (M'' = [] ∧ Decided K i # M' = Decided L (backtrack_lvl S + 1) # trail S)"
using T undef by (cases M'') auto
moreover {
assume "tl M'' @ Decided K i # M' = trail S"
then have "¬M' ⊨as CNot Da"
using D T undef no_f confl smaller unfolding no_smaller_confl_def smaller by fastforce
}
moreover {
assume "Decided K i # M' = Decided L (backtrack_lvl S + 1) # trail S"
then have "¬M' ⊨as CNot Da" using no_f D confl T by auto
}
ultimately show "¬M' ⊨as CNot Da" by fast
qed
next
case resolve
then show ?case using smaller no_f max_lev unfolding no_smaller_confl_def by auto
next
case skip
then show ?case using smaller no_f max_lev unfolding no_smaller_confl_def by auto
next
case (backtrack K i M1 M2 L D T) note decomp = this(1) and confl = this(3) and undef = this(6)
and T =this(7)
obtain c where M: "trail S = c @ M2 @ Decided K (i+1) # M1"
using decomp by auto
show ?case
proof (intro allI impI)
fix M ia K' M' Da
assume "M' @ Decided K' ia # M = trail T"
then have "tl M' @ Decided K' ia # M = M1"
using T decomp undef lev by (cases M') (auto simp: cdcl⇩W_M_level_inv_decomp)
assume D: "Da ∈# clauses T"
moreover{
assume "Da ∈# clauses S"
then have "¬M ⊨as CNot Da" using ‹tl M' @ Decided K' ia # M = M1› M confl undef smaller
unfolding no_smaller_confl_def by auto
}
moreover {
assume Da: "Da = D + {#L#}"
have "¬M ⊨as CNot Da"
proof (rule ccontr)
assume "¬ ?thesis"
then have "-L ∈ lits_of M" unfolding Da by auto
then have "-L ∈ lits_of (Propagated L ((D + {#L#})) # M1)"
using UnI2 ‹tl M' @ Decided K' ia # M = M1›
by auto
moreover
have "backtrack S
(cons_trail (Propagated L (D + {#L#}))
(reduce_trail_to M1 (add_learned_cls (D + {#L#})
(update_backtrack_lvl i (update_conflicting None S)))))"
using backtrack.intros[of S] backtrack.hyps
by (force simp: state_eq_def simp del: state_simp)
then have "cdcl⇩W_M_level_inv
(cons_trail (Propagated L (D + {#L#}))
(reduce_trail_to M1 (add_learned_cls (D + {#L#})
(update_backtrack_lvl i (update_conflicting None S)))))"
using cdcl⇩W_consistent_inv[OF _ lev] other[OF bj] by auto
then have "no_dup (Propagated L (D + {#L#}) # M1)"
using decomp undef lev unfolding cdcl⇩W_M_level_inv_def by auto
ultimately show False by (metis consistent_interp_def distinctconsistent_interp
insertCI lits_of_cons ann_literal.sel(2))
qed
}
ultimately show "¬M ⊨as CNot Da"
using T undef ‹Da = D + {#L#} ⟹ ¬ M ⊨as CNot Da› decomp lev
unfolding cdcl⇩W_M_level_inv_def by fastforce
qed
qed
lemma conflict_no_smaller_confl_inv:
assumes "conflict S S'"
and "no_smaller_confl S"
shows "no_smaller_confl S'"
using assms unfolding no_smaller_confl_def by fastforce
lemma propagate_no_smaller_confl_inv:
assumes propagate: "propagate S S'"
and n_l: "no_smaller_confl S"
shows "no_smaller_confl S'"
unfolding no_smaller_confl_def
proof (intro allI impI)
fix M' K i M'' D
assume M': "M'' @ Decided K i # M' = trail S'"
and "D ∈# clauses S'"
obtain M N U k C L where
S: "state S = (M, N, U, k, None)" and
S': "state S' = (Propagated L ( (C + {#L#})) # M, N, U, k, None)" and
"C + {#L#} ∈# clauses S" and
"M ⊨as CNot C" and
"undefined_lit M L"
using propagate by auto
have "tl M'' @ Decided K i # M' = trail S" using M' S S'
by (metis Pair_inject list.inject list.sel(3) ann_literal.distinct(1) self_append_conv2
tl_append2)
then have "¬M' ⊨as CNot D "
using ‹D ∈# clauses S'› n_l S S' clauses_def unfolding no_smaller_confl_def by auto
then show "¬M' ⊨as CNot D" by auto
qed
lemma cdcl⇩W_cp_no_smaller_confl_inv:
assumes propagate: "cdcl⇩W_cp S S'"
and n_l: "no_smaller_confl S"
shows "no_smaller_confl S'"
using assms
proof (induct rule: cdcl⇩W_cp.induct)
case (conflict' S S')
then show ?case using conflict_no_smaller_confl_inv[of S S'] by blast
next
case (propagate' S S')
then show ?case using propagate_no_smaller_confl_inv[of S S'] by fastforce
qed
lemma rtrancp_cdcl⇩W_cp_no_smaller_confl_inv:
assumes propagate: "cdcl⇩W_cp⇧*⇧* S S'"
and n_l: "no_smaller_confl S"
shows "no_smaller_confl S'"
using assms
proof (induct rule: rtranclp_induct)
case base
then show ?case by simp
next
case (step S' S'')
then show ?case using cdcl⇩W_cp_no_smaller_confl_inv[of S' S''] by fast
qed
lemma trancp_cdcl⇩W_cp_no_smaller_confl_inv:
assumes propagate: "cdcl⇩W_cp⇧+⇧+ S S'"
and n_l: "no_smaller_confl S"
shows "no_smaller_confl S'"
using assms
proof (induct rule: tranclp.induct)
case (r_into_trancl S S')
then show ?case using cdcl⇩W_cp_no_smaller_confl_inv[of S S'] by blast
next
case (trancl_into_trancl S S' S'')
then show ?case using cdcl⇩W_cp_no_smaller_confl_inv[of S' S''] by fast
qed
lemma full_cdcl⇩W_cp_no_smaller_confl_inv:
assumes "full cdcl⇩W_cp S S'"
and n_l: "no_smaller_confl S"
shows "no_smaller_confl S'"
using assms unfolding full_def
using rtrancp_cdcl⇩W_cp_no_smaller_confl_inv[of S S'] by blast
lemma full1_cdcl⇩W_cp_no_smaller_confl_inv:
assumes "full1 cdcl⇩W_cp S S'"
and n_l: "no_smaller_confl S"
shows "no_smaller_confl S'"
using assms unfolding full1_def
using trancp_cdcl⇩W_cp_no_smaller_confl_inv[of S S'] by blast
lemma cdcl⇩W_stgy_no_smaller_confl_inv:
assumes "cdcl⇩W_stgy S S'"
and n_l: "no_smaller_confl S"
and "conflict_is_false_with_level S"
and "cdcl⇩W_M_level_inv S"
shows "no_smaller_confl S'"
using assms
proof (induct rule: cdcl⇩W_stgy.induct)
case (conflict' S')
then show ?case using full1_cdcl⇩W_cp_no_smaller_confl_inv[of S S'] by blast
next
case (other' S' S'')
have "no_smaller_confl S'"
using cdcl⇩W_o_no_smaller_confl_inv[OF other'.hyps(1) other'.prems(3,2,1)]
not_conflict_not_any_negated_init_clss other'.hyps(2) by blast
then show ?case using full_cdcl⇩W_cp_no_smaller_confl_inv[of S' S''] other'.hyps by blast
qed
lemma conflict_conflict_is_no_clause_is_false_test:
assumes "conflict S S'"
and "(∀D ∈# init_clss S + learned_clss S. trail S ⊨as CNot D
⟶ (∃L. L ∈# D ∧ get_level (trail S) L = backtrack_lvl S))"
shows "∀D ∈# init_clss S' + learned_clss S'. trail S' ⊨as CNot D
⟶ (∃L. L ∈# D ∧ get_level (trail S') L = backtrack_lvl S')"
using assms by auto
lemma is_conflicting_exists_conflict:
assumes "¬(∀D∈#init_clss S' + learned_clss S'. ¬ trail S' ⊨as CNot D)"
and "conflicting S' = None"
shows "∃S''. conflict S' S''"
using assms clauses_def not_conflict_not_any_negated_init_clss by fastforce
lemma cdcl⇩W_o_conflict_is_no_clause_is_false:
fixes S S' :: "'st"
assumes
"cdcl⇩W_o S S'" and
lev: "cdcl⇩W_M_level_inv S" and
max_lev: "conflict_is_false_with_level S" and
no_f: "no_clause_is_false S" and
no_l: "no_smaller_confl S"
shows "no_clause_is_false S'
∨ (conflicting S' = None
⟶ (∀D ∈# clauses S'. trail S' ⊨as CNot D
⟶ (∃L. L ∈# D ∧ get_level (trail S') L = backtrack_lvl S')))"
using assms(1,2)
proof (induct rule: cdcl⇩W_o_induct_lev2)
case (decide L T) note S = this(1) and undef = this(2) and T =this(4)
show ?case
proof (rule HOL.disjI2, clarify)
fix D
assume D: "D ∈# clauses T" and M_D: "trail T ⊨as CNot D"
let ?M = "trail S"
let ?M' = "trail T"
let ?k = "backtrack_lvl S"
have "¬?M ⊨as CNot D"
using no_f D S T undef by auto
have "-L ∈# D"
proof (rule ccontr)
assume "¬ ?thesis"
have "?M ⊨as CNot D"
unfolding true_annots_def Ball_def true_annot_def CNot_def true_cls_def
proof (intro allI impI)
fix x
assume x: "x ∈ {{#- L#} |L. L ∈# D}"
then obtain L' where L': "x = {#-L'#}" "L' ∈# D" by auto
obtain L'' where "L'' ∈# x" and "lits_of (Decided L (?k + 1) # ?M) ⊨l L''"
using M_D x T undef unfolding true_annots_def Ball_def true_annot_def CNot_def
true_cls_def Bex_mset_def by auto
show "∃L ∈# x. lits_of ?M ⊨l L" unfolding Bex_mset_def
by (metis ‹- L ∉# D› ‹L'' ∈# x› L' ‹lits_of (Decided L (?k + 1) # ?M) ⊨l L''›
count_single insertE less_numeral_extra(3) lits_of_cons ann_literal.sel(1)
true_lit_def uminus_of_uminus_id)
qed
then show False using ‹¬ ?M ⊨as CNot D› by auto
qed
have "atm_of L ∉ atm_of ` (lits_of ?M)"
using undef defined_lit_map unfolding lits_of_def by fastforce
then have "get_level (Decided L (?k + 1) # ?M) (-L) = ?k + 1" by simp
then show "∃La. La ∈# D ∧ get_level ?M' La = backtrack_lvl T"
using ‹-L ∈# D› T undef by auto
qed
next
case resolve
then show ?case by auto
next
case skip
then show ?case by auto
next
case (backtrack K i M1 M2 L D T) note decomp = this(1) and undef = this(6) and T =this(7)
show ?case
proof (rule HOL.disjI2, clarify)
fix Da
assume Da: "Da ∈# clauses T"
and M_D: "trail T ⊨as CNot Da"
obtain c where M: "trail S = c @ M2 @ Decided K (i + 1) # M1"
using decomp by auto
have tr_T: "trail T = Propagated L (D + {#L#}) # M1"
using T decomp undef lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
have "backtrack S T"
using backtrack.intros backtrack.hyps T by (force simp del: state_simp simp: state_eq_def)
then have lev': "cdcl⇩W_M_level_inv T"
using cdcl⇩W_consistent_inv lev other by blast
then have "- L ∉ lits_of M1"
unfolding cdcl⇩W_M_level_inv_def lits_of_def
proof -
have "consistent_interp (lits_of (trail S)) ∧ no_dup (trail S)
∧ backtrack_lvl S = length (get_all_levels_of_decided (trail S))
∧ get_all_levels_of_decided (trail S)
= rev [1..<1 + length (get_all_levels_of_decided (trail S))]"
using lev cdcl⇩W_M_level_inv_def by blast
then show "- L ∉ lit_of ` set M1"
by (metis (no_types) One_nat_def add.right_neutral add_Suc_right
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set backtrack.hyps(2)
cdcl⇩W.backtrack_lit_skiped cdcl⇩W_axioms decomp lits_of_def)
qed
{ assume "Da ∈# clauses S"
then have "¬M1 ⊨as CNot Da" using no_l M unfolding no_smaller_confl_def by auto
}
moreover {
assume Da: "Da = D + {#L#}"
have "¬M1 ⊨as CNot Da" using ‹- L ∉ lits_of M1› unfolding Da by simp
}
ultimately have "¬M1 ⊨as CNot Da"
using Da T undef decomp lev by (fastforce simp: cdcl⇩W_M_level_inv_decomp)
then have "-L ∈# Da"
using M_D ‹- L ∉ lits_of M1› in_CNot_implies_uminus(2)
true_annots_CNot_lit_of_notin_skip T unfolding tr_T
by (smt insert_iff lits_of_cons ann_literal.sel(2))
have g_M1: "get_all_levels_of_decided M1 = rev [1..<i+1]"
using lev lev' T decomp undef unfolding cdcl⇩W_M_level_inv_def by auto
have "no_dup (Propagated L (D + {#L#}) # M1)"
using lev lev' T decomp undef unfolding cdcl⇩W_M_level_inv_def by auto
then have L: "atm_of L ∉ atm_of ` lits_of M1" unfolding lits_of_def by auto
have "get_level (Propagated L ((D + {#L#})) # M1) (-L) = i"
using get_level_get_rev_level_get_all_levels_of_decided[OF L,
of "[Propagated L ((D + {#L#}))]"]
by (simp add: g_M1 split: if_splits)
then show "∃La. La ∈# Da ∧ get_level (trail T) La = backtrack_lvl T"
using ‹-L ∈# Da› T decomp undef lev by (auto simp: cdcl⇩W_M_level_inv_def)
qed
qed
lemma full1_cdcl⇩W_cp_exists_conflict_decompose:
assumes confl: "∃D∈#clauses S. trail S ⊨as CNot D"
and full: "full cdcl⇩W_cp S U"
and no_confl: "conflicting S = None"
shows "∃T. propagate⇧*⇧* S T ∧ conflict T U"
proof -
consider (propa) "propagate⇧*⇧* S U"
| (confl) T where "propagate⇧*⇧* S T" and "conflict T U"
using full unfolding full_def by (blast dest:rtranclp_cdcl⇩W_cp_propa_or_propa_confl)
then show ?thesis
proof cases
case confl
then show ?thesis by blast
next
case propa
then have "conflicting U = None"
using no_confl by induction auto
moreover have [simp]: "learned_clss U = learned_clss S" and
[simp]: "init_clss U = init_clss S"
using propa by induction auto
moreover
obtain D where D: "D∈#clauses U" and
trS: "trail S ⊨as CNot D"
using confl clauses_def by auto
obtain M where M: "trail U = M @ trail S"
using full rtranclp_cdcl⇩W_cp_dropWhile_trail unfolding full_def by meson
have tr_U: "trail U ⊨as CNot D"
apply (rule true_annots_mono)
using trS unfolding M by simp_all
have "∃V. conflict U V"
using ‹conflicting U = None› D clauses_def not_conflict_not_any_negated_init_clss tr_U
by blast
then have False using full cdcl⇩W_cp.conflict' unfolding full_def by blast
then show ?thesis by fast
qed
qed
lemma full1_cdcl⇩W_cp_exists_conflict_full1_decompose:
assumes confl: "∃D∈#clauses S. trail S ⊨as CNot D"
and full: "full cdcl⇩W_cp S U"
and no_confl: "conflicting S = None"
shows "∃T D. propagate⇧*⇧* S T ∧ conflict T U
∧ trail T ⊨as CNot D ∧ conflicting U = Some D ∧ D ∈# clauses S"
proof -
obtain T where propa: "propagate⇧*⇧* S T" and conf: "conflict T U"
using full1_cdcl⇩W_cp_exists_conflict_decompose[OF assms] by blast
have p: "learned_clss T = learned_clss S" "init_clss T = init_clss S"
using propa by induction auto
have c: "learned_clss U = learned_clss T" "init_clss U = init_clss T"
using conf by induction auto
obtain D where "trail T ⊨as CNot D ∧ conflicting U = Some D ∧ D ∈# clauses S"
using conf p c by (fastforce simp: clauses_def)
then show ?thesis
using propa conf by blast
qed
lemma cdcl⇩W_stgy_no_smaller_confl:
assumes "cdcl⇩W_stgy S S'"
and n_l: "no_smaller_confl S"
and "conflict_is_false_with_level S"
and "cdcl⇩W_M_level_inv S"
and "no_clause_is_false S"
and "distinct_cdcl⇩W_state S"
and "cdcl⇩W_conflicting S"
shows "no_smaller_confl S'"
using assms
proof (induct rule: cdcl⇩W_stgy.induct)
case (conflict' S')
show "no_smaller_confl S'"
using conflict'.hyps conflict'.prems(1) full1_cdcl⇩W_cp_no_smaller_confl_inv by blast
next
case (other' S' S'')
have lev': "cdcl⇩W_M_level_inv S'"
using cdcl⇩W_consistent_inv other other'.hyps(1) other'.prems(3) by blast
show "no_smaller_confl S''"
using cdcl⇩W_stgy_no_smaller_confl_inv[OF cdcl⇩W_stgy.other'[OF other'.hyps(1-3)]]
other'.prems(1-3) by blast
qed
lemma cdcl⇩W_stgy_ex_lit_of_max_level:
assumes "cdcl⇩W_stgy S S'"
and n_l: "no_smaller_confl S"
and "conflict_is_false_with_level S"
and "cdcl⇩W_M_level_inv S"
and "no_clause_is_false S"
and "distinct_cdcl⇩W_state S"
and "cdcl⇩W_conflicting S"
shows "conflict_is_false_with_level S'"
using assms
proof (induct rule: cdcl⇩W_stgy.induct)
case (conflict' S')
have "no_smaller_confl S'"
using conflict'.hyps conflict'.prems(1) full1_cdcl⇩W_cp_no_smaller_confl_inv by blast
moreover have "conflict_is_false_with_level S'"
using conflict'.hyps conflict'.prems(2-4)
rtranclp_cdcl⇩W_co_conflict_ex_lit_of_max_level[of S S']
unfolding full_def full1_def rtranclp_unfold by presburger
then show ?case by blast
next
case (other' S' S'')
have lev': "cdcl⇩W_M_level_inv S'"
using cdcl⇩W_consistent_inv other other'.hyps(1) other'.prems(3) by blast
moreover
have "no_clause_is_false S'
∨ (conflicting S' = None ⟶ (∀D∈#clauses S'. trail S' ⊨as CNot D
⟶ (∃L. L ∈# D ∧ get_level (trail S') L = backtrack_lvl S')))"
using cdcl⇩W_o_conflict_is_no_clause_is_false[of S S'] other'.hyps(1) other'.prems(1-4) by fast
moreover {
assume "no_clause_is_false S'"
{
assume "conflicting S' = None"
then have "conflict_is_false_with_level S'" by auto
moreover have "full cdcl⇩W_cp S' S''"
by (metis (no_types) other'.hyps(3))
ultimately have "conflict_is_false_with_level S''"
using rtranclp_cdcl⇩W_co_conflict_ex_lit_of_max_level[of S' S''] lev' ‹no_clause_is_false S'›
by blast
}
moreover
{
assume c: "conflicting S' ≠ None"
have "conflicting S ≠ None" using other'.hyps(1) c
by (induct rule: cdcl⇩W_o_induct) auto
then have "conflict_is_false_with_level S'"
using cdcl⇩W_o_conflict_is_false_with_level_inv[OF other'.hyps(1)]
other'.prems(3,5,6,2) by blast
moreover have "cdcl⇩W_cp⇧*⇧* S' S''" using other'.hyps(3) unfolding full_def by auto
then have "S' = S''" using c
by (induct rule: rtranclp_induct)
(fastforce intro: option.exhaust)+
ultimately have "conflict_is_false_with_level S''" by auto
}
ultimately have "conflict_is_false_with_level S''" by blast
}
moreover {
assume
confl: "conflicting S' = None" and
D_L: "∀D ∈# clauses S'. trail S' ⊨as CNot D
⟶ (∃L. L ∈# D ∧ get_level (trail S') L = backtrack_lvl S')"
{ assume "∀D∈#clauses S'. ¬ trail S' ⊨as CNot D"
then have "no_clause_is_false S'" using confl by simp
then have "conflict_is_false_with_level S''" using calculation(3) by presburger
}
moreover {
assume "¬(∀D∈#clauses S'. ¬ trail S' ⊨as CNot D)"
then obtain T D where
"propagate⇧*⇧* S' T" and
"conflict T S''" and
D: "D ∈# clauses S'" and
"trail S'' ⊨as CNot D" and
"conflicting S'' = Some D"
using full1_cdcl⇩W_cp_exists_conflict_full1_decompose[OF _ _ confl]
other'(3) by (metis (mono_tags, lifting) ball_msetI bex_msetI conflictE state_eq_trail
trail_update_conflicting)
obtain M where M: "trail S'' = M @ trail S'" and nm: "∀m∈set M. ¬is_decided m"
using rtranclp_cdcl⇩W_cp_dropWhile_trail other'(3) unfolding full_def by meson
have btS: "backtrack_lvl S'' = backtrack_lvl S'"
using other'.hyps(3) unfolding full_def by (metis rtranclp_cdcl⇩W_cp_backtrack_lvl)
have inv: "cdcl⇩W_M_level_inv S''"
by (metis (no_types) cdcl⇩W_stgy.conflict' cdcl⇩W_stgy_consistent_inv full_unfold lev'
other'.hyps(3))
then have nd: "no_dup (trail S'')"
by (metis (no_types) cdcl⇩W_M_level_inv_decomp(2))
have "conflict_is_false_with_level S''"
proof cases
assume "trail S' ⊨as CNot D"
moreover then obtain L where
"L ∈# D" and
lev_L: "get_level (trail S') L = backtrack_lvl S'"
using D_L D by blast
moreover
have LS': "-L ∈ lits_of (trail S')"
using ‹trail S' ⊨as CNot D› ‹L ∈# D› in_CNot_implies_uminus(2) by blast
{ fix x :: "('v, nat, 'v literal multiset) ann_literal" and
xb :: "('v, nat, 'v literal multiset) ann_literal"
assume a1: "x ∈ set (trail S')" and
a2: "xb ∈ set M" and
a3: "(λl. atm_of (lit_of l)) ` set M ∩ (λl. atm_of (lit_of l)) ` set (trail S')
= {}" and
a4: "- L = lit_of x" and
a5: "atm_of L = atm_of (lit_of xb)"
moreover have "atm_of (lit_of x) = atm_of L"
using a4 by (metis (no_types) atm_of_uminus)
ultimately have False
using a5 a3 a2 a1 by auto
}
then have "atm_of L ∉ atm_of ` lits_of M"
using nd LS' unfolding M by (auto simp add: lits_of_def)
then have "get_level (trail S'') L = get_level (trail S') L"
unfolding M by (simp add: lits_of_def)
ultimately show ?thesis using btS ‹conflicting S'' = Some D› by auto
next
assume "¬trail S' ⊨as CNot D"
then obtain L where "L ∈# D" and LM: "-L ∈ lits_of M"
using ‹trail S'' ⊨as CNot D›
by (auto simp add: CNot_def true_cls_def M true_annots_def true_annot_def
split: split_if_asm)
{ fix x :: "('v, nat, 'v literal multiset) ann_literal" and
xb :: "('v, nat, 'v literal multiset) ann_literal"
assume a1: "xb ∈ set (trail S')" and
a2: "x ∈ set M" and
a3: "atm_of L = atm_of (lit_of xb)" and
a4: "- L = lit_of x" and
a5: "(λl. atm_of (lit_of l)) ` set M ∩ (λl. atm_of (lit_of l)) ` set (trail S')
= {}"
moreover have "atm_of (lit_of xb) = atm_of (- L)"
using a3 by simp
ultimately have False
by auto }
then have LS': "atm_of L ∉ atm_of ` lits_of (trail S')"
using nd ‹L ∈# D› LM unfolding M by (auto simp add: lits_of_def)
show ?thesis
proof cases
assume ne: "get_all_levels_of_decided (trail S') = []"
have "backtrack_lvl S'' = 0"
using inv ne nm unfolding cdcl⇩W_M_level_inv_def M
by (simp add: get_all_levels_of_decided_nil_iff_not_is_decided)
moreover
have a1: "get_level M L = 0"
using nm by auto
then have "get_level (M @ trail S') L = 0"
by (metis LS' get_all_levels_of_decided_nil_iff_not_is_decided
get_level_skip_beginning_not_decided lits_of_def ne)
ultimately show ?thesis using ‹conflicting S'' = Some D› ‹L ∈# D› unfolding M
by auto
next
assume ne: "get_all_levels_of_decided (trail S') ≠ []"
have "hd (get_all_levels_of_decided (trail S')) = backtrack_lvl S'"
using ne lev' M nm unfolding cdcl⇩W_M_level_inv_def
by (cases "get_all_levels_of_decided (trail S')")
(simp_all add: get_all_levels_of_decided_nil_iff_not_is_decided[symmetric])
moreover have "atm_of L ∈ atm_of ` lits_of M "
using ‹-L ∈ lits_of M›
by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set lits_of_def)
ultimately show ?thesis
using nm ne ‹L∈#D› ‹conflicting S'' = Some D›
get_level_skip_beginning_hd_get_all_levels_of_decided[OF LS', of M]
get_level_skip_in_all_not_decided[of "rev M" L "backtrack_lvl S'"]
unfolding lits_of_def btS M
by auto
qed
qed
}
ultimately have "conflict_is_false_with_level S''" by blast
}
moreover
{
assume "conflicting S' ≠ None"
have "no_clause_is_false S'" using ‹conflicting S' ≠ None› by auto
then have "conflict_is_false_with_level S''" using calculation(3) by presburger
}
ultimately show ?case by fast
qed
lemma rtranclp_cdcl⇩W_stgy_no_smaller_confl_inv:
assumes
"cdcl⇩W_stgy⇧*⇧* S S'" and
n_l: "no_smaller_confl S" and
cls_false: "conflict_is_false_with_level S" and
lev: "cdcl⇩W_M_level_inv S" and
no_f: "no_clause_is_false S" and
dist: "distinct_cdcl⇩W_state S" and
conflicting: "cdcl⇩W_conflicting S" and
decomp: "all_decomposition_implies_m (init_clss S) (get_all_decided_decomposition (trail S))" and
learned: "cdcl⇩W_learned_clause S" and
alien: "no_strange_atm S"
shows "no_smaller_confl S' ∧ conflict_is_false_with_level S'"
using assms(1)
proof (induct rule: rtranclp_induct)
case base
then show ?case using n_l cls_false by auto
next
case (step S' S'') note st = this(1) and cdcl = this(2) and IH = this(3)
have "no_smaller_confl S'" and "conflict_is_false_with_level S'"
using IH by blast+
moreover have "cdcl⇩W_M_level_inv S'"
using st lev rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W
by (blast intro: rtranclp_cdcl⇩W_consistent_inv)+
moreover have "no_clause_is_false S'"
using st no_f rtranclp_cdcl⇩W_stgy_not_non_negated_init_clss by presburger
moreover have "distinct_cdcl⇩W_state S'"
using rtanclp_distinct_cdcl⇩W_state_inv[of S S'] lev rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W[OF st]
dist by auto
moreover have "cdcl⇩W_conflicting S'"
using rtranclp_cdcl⇩W_all_inv(6)[of S S'] st alien conflicting decomp dist learned lev
rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W by blast
ultimately show ?case
using cdcl⇩W_stgy_no_smaller_confl[OF cdcl] cdcl⇩W_stgy_ex_lit_of_max_level[OF cdcl] by fast
qed
subsubsection ‹Final States are Conclusive›
lemma full_cdcl⇩W_stgy_final_state_conclusive_non_false:
fixes S' :: "'st"
assumes full: "full cdcl⇩W_stgy (init_state N) S'"
and no_d: "distinct_mset_mset N"
and no_empty: "∀D∈#N. D ≠ {#}"
shows "(conflicting S' = Some {#} ∧ unsatisfiable (set_mset (init_clss S')))
∨ (conflicting S' = None ∧ trail S' ⊨asm init_clss S')"
proof -
let ?S = "init_state N"
have
termi: "∀S''. ¬cdcl⇩W_stgy S' S''" and
step: "cdcl⇩W_stgy⇧*⇧* (init_state N) S'" using full unfolding full_def by auto
moreover have
learned: "cdcl⇩W_learned_clause S'" and
level_inv: "cdcl⇩W_M_level_inv S'" and
alien: "no_strange_atm S'" and
no_dup: "distinct_cdcl⇩W_state S'" and
confl: "cdcl⇩W_conflicting S'" and
decomp: "all_decomposition_implies_m (init_clss S') (get_all_decided_decomposition (trail S'))"
using no_d tranclp_cdcl⇩W_stgy_tranclp_cdcl⇩W[of ?S S'] step rtranclp_cdcl⇩W_all_inv(1-6)[of ?S S']
unfolding rtranclp_unfold by auto
moreover
have "∀D∈#N. ¬ [] ⊨as CNot D" using no_empty by auto
then have confl_k: "conflict_is_false_with_level S'"
using rtranclp_cdcl⇩W_stgy_no_smaller_confl_inv[OF step] no_d by auto
show ?thesis
using cdcl⇩W_stgy_final_state_conclusive[OF termi decomp learned level_inv alien no_dup confl
confl_k] .
qed
lemma conflict_is_full1_cdcl⇩W_cp:
assumes cp: "conflict S S'"
shows "full1 cdcl⇩W_cp S S'"
proof -
have "cdcl⇩W_cp S S'" and "conflicting S' ≠ None" using cp cdcl⇩W_cp.intros by auto
then have "cdcl⇩W_cp⇧+⇧+ S S'" by blast
moreover have "no_step cdcl⇩W_cp S'"
using ‹conflicting S' ≠ None› by (metis cdcl⇩W_cp_conflicting_not_empty
option.exhaust)
ultimately show "full1 cdcl⇩W_cp S S'" unfolding full1_def by blast+
qed
lemma cdcl⇩W_cp_fst_empty_conflicting_false:
assumes "cdcl⇩W_cp S S'"
and "trail S = []"
and "conflicting S ≠ None"
shows False
using assms by (induct rule: cdcl⇩W_cp.induct) auto
lemma cdcl⇩W_o_fst_empty_conflicting_false:
assumes "cdcl⇩W_o S S'"
and "trail S = []"
and "conflicting S ≠ None"
shows False
using assms by (induct rule: cdcl⇩W_o_induct) auto
lemma cdcl⇩W_stgy_fst_empty_conflicting_false:
assumes "cdcl⇩W_stgy S S'"
and "trail S = []"
and "conflicting S ≠ None"
shows False
using assms apply (induct rule: cdcl⇩W_stgy.induct)
using tranclpD cdcl⇩W_cp_fst_empty_conflicting_false unfolding full1_def apply metis
using cdcl⇩W_o_fst_empty_conflicting_false by blast
thm cdcl⇩W_cp.induct[split_format(complete)]
lemma cdcl⇩W_cp_conflicting_is_false:
"cdcl⇩W_cp S S' ⟹ conflicting S = Some {#} ⟹ False"
by (induction rule: cdcl⇩W_cp.induct) auto
lemma rtranclp_cdcl⇩W_cp_conflicting_is_false:
"cdcl⇩W_cp⇧+⇧+ S S' ⟹ conflicting S = Some {#} ⟹ False"
apply (induction rule: tranclp.induct)
by (auto dest: cdcl⇩W_cp_conflicting_is_false)
lemma cdcl⇩W_o_conflicting_is_false:
"cdcl⇩W_o S S' ⟹ conflicting S = Some {#} ⟹ False"
by (induction rule: cdcl⇩W_o_induct) auto
lemma cdcl⇩W_stgy_conflicting_is_false:
"cdcl⇩W_stgy S S' ⟹ conflicting S = Some {#} ⟹ False"
apply (induction rule: cdcl⇩W_stgy.induct)
unfolding full1_def apply (metis (no_types) cdcl⇩W_cp_conflicting_not_empty tranclpD)
unfolding full_def by (metis conflict_with_false_implies_terminated other)
lemma rtranclp_cdcl⇩W_stgy_conflicting_is_false:
"cdcl⇩W_stgy⇧*⇧* S S' ⟹ conflicting S = Some {#} ⟹ S' = S"
apply (induction rule: rtranclp_induct)
apply simp
using cdcl⇩W_stgy_conflicting_is_false by blast
lemma full_cdcl⇩W_init_clss_with_false_normal_form:
assumes
"∀ m∈ set M. ¬is_decided m" and
"E = Some D" and
"state S = (M, N, U, 0, E)"
"full cdcl⇩W_stgy S S'" and
"all_decomposition_implies_m (init_clss S) (get_all_decided_decomposition (trail S))"
"cdcl⇩W_learned_clause S"
"cdcl⇩W_M_level_inv S"
"no_strange_atm S"
"distinct_cdcl⇩W_state S"
"cdcl⇩W_conflicting S"
shows "∃M''. state S' = (M'', N, U, 0, Some {#})"
using assms(10,9,8,7,6,5,4,3,2,1)
proof (induction M arbitrary: E D S)
case Nil
then show ?case
using rtranclp_cdcl⇩W_stgy_conflicting_is_false unfolding full_def cdcl⇩W_conflicting_def by auto
next
case (Cons L M) note IH = this(1) and full = this(8) and E = this(10) and inv = this(2-7) and
S = this(9) and nm = this(11)
obtain K p where K: "L = Propagated K p"
using nm by (cases L) auto
have "every_mark_is_a_conflict S" using inv unfolding cdcl⇩W_conflicting_def by auto
then have MpK: "M ⊨as CNot ( p - {#K#})" and Kp: "K ∈# p"
using S unfolding K by fastforce+
then have p: " p = ( p - {#K#}) + {#K#}"
by (auto simp add: multiset_eq_iff)
then have K': "L = Propagated K ( (( p - {#K#}) + {#K#}))"
using K by auto
consider (D) "D = {#}" | (D') "D ≠ {#}" by blast
then show ?case
proof cases
case D
then show ?thesis
using full rtranclp_cdcl⇩W_stgy_conflicting_is_false S unfolding full_def E D by auto
next
case D'
then have no_p: "no_step propagate S" and no_c: "no_step conflict S"
using S E by auto
then have "no_step cdcl⇩W_cp S" by (auto simp: cdcl⇩W_cp.simps)
have res_skip: "∃T. (resolve S T ∧ no_step skip S ∧ full cdcl⇩W_cp T T)
∨ (skip S T ∧ no_step resolve S ∧ full cdcl⇩W_cp T T)"
proof cases
assume "-lit_of L ∉# D"
then obtain T where sk: "skip S T" and res: "no_step resolve S"
using S that D' K unfolding skip.simps E by fastforce
have "full cdcl⇩W_cp T T"
using sk by (auto simp add: option_full_cdcl⇩W_cp)
then show ?thesis
using sk res by blast
next
assume LD: "¬-lit_of L ∉# D"
then have D: "Some D = Some ((D - {#-lit_of L#}) + {#-lit_of L#})"
by (auto simp add: multiset_eq_iff)
have "⋀L. get_level M L = 0"
by (simp add: nm)
then have "get_maximum_level (Propagated K (p - {#K#} + {#K#}) # M) (D - {#- K#}) = 0"
using LD get_maximum_level_exists_lit_of_max_level
proof -
obtain L' where "get_level (L#M) L' = get_maximum_level (L#M) D"
using LD get_maximum_level_exists_lit_of_max_level[of D "L#M"] by fastforce
then show ?thesis by (metis (mono_tags) K' bex_msetE get_level_skip_all_not_decided
get_maximum_level_exists_lit nm not_gr0)
qed
then obtain T where sk: "resolve S T" and res: "no_step skip S"
using resolve_rule[of S K " p - {#K#}" M N U 0 "(D - {#-K#})"
"update_conflicting (Some (remdups_mset (D - {#- K#} + (p - {#K#})))) (tl_trail S)"]
S unfolding K' D E by fastforce
have "full cdcl⇩W_cp T T"
using sk by (auto simp add: option_full_cdcl⇩W_cp)
then show ?thesis
using sk res by blast
qed
then have step_s: "∃T. cdcl⇩W_stgy S T"
using ‹no_step cdcl⇩W_cp S› other' by (meson bj resolve skip)
have "get_all_decided_decomposition (L # M) = [([], L#M)]"
using nm unfolding K apply (induction M rule: ann_literal_list_induct, simp)
by (rename_tac L l xs, case_tac "hd (get_all_decided_decomposition xs)", auto)+
then have no_b: "no_step backtrack S"
using nm S by auto
have no_d: "no_step decide S"
using S E by auto
have full_S_S: "full cdcl⇩W_cp S S"
using S E by (auto simp add: option_full_cdcl⇩W_cp)
then have no_f: "no_step (full1 cdcl⇩W_cp) S"
unfolding full_def full1_def rtranclp_unfold by (meson tranclpD)
obtain T where
s: "cdcl⇩W_stgy S T" and st: "cdcl⇩W_stgy⇧*⇧* T S'"
using full step_s full unfolding full_def by (metis rtranclp_unfold tranclpD)
have "resolve S T ∨ skip S T"
using s no_b no_d res_skip full_S_S unfolding cdcl⇩W_stgy.simps cdcl⇩W_o.simps full_unfold
full1_def
by (auto dest!: tranclpD simp: cdcl⇩W_bj.simps)
then obtain D' where T: "state T = (M, N, U, 0, Some D')"
using S E by auto
have st_c: "cdcl⇩W⇧*⇧* S T"
using E T rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W s by blast
have "cdcl⇩W_conflicting T"
using rtranclp_cdcl⇩W_all_inv(6)[OF st_c inv(6,5,4,3,2,1)] .
show ?thesis
apply (rule IH[of T])
using rtranclp_cdcl⇩W_all_inv(6)[OF st_c inv(6,5,4,3,2,1)] apply blast
using rtranclp_cdcl⇩W_all_inv(5)[OF st_c inv(6,5,4,3,2,1)] apply blast
using rtranclp_cdcl⇩W_all_inv(4)[OF st_c inv(6,5,4,3,2,1)] apply blast
using rtranclp_cdcl⇩W_all_inv(3)[OF st_c inv(6,5,4,3,2,1)] apply blast
using rtranclp_cdcl⇩W_all_inv(2)[OF st_c inv(6,5,4,3,2,1)] apply blast
using rtranclp_cdcl⇩W_all_inv(1)[OF st_c inv(6,5,4,3,2,1)] apply blast
apply (metis full_def st full)
using T E apply blast
apply auto[]
using nm by simp
qed
qed
lemma full_cdcl⇩W_stgy_final_state_conclusive_is_one_false:
fixes S' :: "'st"
assumes full: "full cdcl⇩W_stgy (init_state N) S'"
and no_d: "distinct_mset_mset N"
and empty: "{#} ∈# N"
shows "conflicting S' = Some {#} ∧ unsatisfiable (set_mset (init_clss S'))"
proof -
let ?S = "init_state N"
have "cdcl⇩W_stgy⇧*⇧* ?S S'" and "no_step cdcl⇩W_stgy S'" using full unfolding full_def by auto
then have plus_or_eq: "cdcl⇩W_stgy⇧+⇧+ ?S S' ∨ S' = ?S" unfolding rtranclp_unfold by auto
have "∃S''. conflict ?S S''" using empty not_conflict_not_any_negated_init_clss by force
then have cdcl⇩W_stgy: "∃S'. cdcl⇩W_stgy ?S S'"
using cdcl⇩W_cp.conflict'[of ?S] conflict_is_full1_cdcl⇩W_cp cdcl⇩W_stgy.intros(1) by metis
have "S' ≠ ?S" using ‹no_step cdcl⇩W_stgy S'› cdcl⇩W_stgy by blast
then obtain St:: 'st where St: "cdcl⇩W_stgy ?S St" and "cdcl⇩W_stgy⇧*⇧* St S'"
using plus_or_eq by (metis (no_types) ‹cdcl⇩W_stgy⇧*⇧* ?S S'› converse_rtranclpE)
have st: "cdcl⇩W⇧*⇧* ?S St"
by (simp add: rtranclp_unfold ‹cdcl⇩W_stgy ?S St› cdcl⇩W_stgy_tranclp_cdcl⇩W)
have "∃T. conflict ?S T"
using empty not_conflict_not_any_negated_init_clss by force
then have fullSt: "full1 cdcl⇩W_cp ?S St"
using St unfolding cdcl⇩W_stgy.simps by blast
then have bt: "backtrack_lvl St = (0::nat)"
using rtranclp_cdcl⇩W_cp_backtrack_lvl unfolding full1_def
by (fastforce dest!: tranclp_into_rtranclp)
have cls_St: "init_clss St = N"
using fullSt cdcl⇩W_stgy_no_more_init_clss[OF St] by auto
have "conflicting St ≠ None"
proof (rule ccontr)
assume "¬ ?thesis"
then have "∃T. conflict St T"
using empty cls_St[] conflict_rule[of St "trail St" N "learned_clss St" "backtrack_lvl St"
"{#}"]
by (auto simp: clauses_def)
then show False using fullSt unfolding full1_def by blast
qed
have 1: "∀m∈set (trail St). ¬ is_decided m"
using fullSt unfolding full1_def by (auto dest!: tranclp_into_rtranclp
rtranclp_cdcl⇩W_cp_dropWhile_trail)
have 2: "full cdcl⇩W_stgy St S'"
using ‹cdcl⇩W_stgy⇧*⇧* St S'› ‹no_step cdcl⇩W_stgy S'› bt unfolding full_def by auto
have 3: "all_decomposition_implies_m
(init_clss St)
(get_all_decided_decomposition
(trail St))"
using rtranclp_cdcl⇩W_all_inv(1)[OF st] no_d bt by simp
have 4: "cdcl⇩W_learned_clause St"
using rtranclp_cdcl⇩W_all_inv(2)[OF st] no_d bt bt by simp
have 5: "cdcl⇩W_M_level_inv St"
using rtranclp_cdcl⇩W_all_inv(3)[OF st] no_d bt by simp
have 6: "no_strange_atm St"
using rtranclp_cdcl⇩W_all_inv(4)[OF st] no_d bt by simp
have 7: "distinct_cdcl⇩W_state St"
using rtranclp_cdcl⇩W_all_inv(5)[OF st] no_d bt by simp
have 8: "cdcl⇩W_conflicting St"
using rtranclp_cdcl⇩W_all_inv(6)[OF st] no_d bt by simp
have "init_clss S' = init_clss St" and "conflicting S' = Some {#}"
using ‹conflicting St ≠ None› full_cdcl⇩W_init_clss_with_false_normal_form[OF 1, of _ _ St]
2 3 4 5 6 7 8 St apply (metis ‹cdcl⇩W_stgy⇧*⇧* St S'› rtranclp_cdcl⇩W_stgy_no_more_init_clss)
using ‹conflicting St ≠ None› full_cdcl⇩W_init_clss_with_false_normal_form[OF 1, of _ _ St _ _
S'] 2 3 4 5 6 7 8 by (metis bt option.exhaust prod.inject)
moreover have "init_clss S' = N"
using ‹cdcl⇩W_stgy⇧*⇧* (init_state N) S'› rtranclp_cdcl⇩W_stgy_no_more_init_clss by fastforce
moreover have "unsatisfiable (set_mset N)"
by (meson empty mem_set_mset_iff satisfiable_def true_cls_empty true_clss_def)
ultimately show ?thesis by auto
qed
lemma full_cdcl⇩W_stgy_final_state_conclusive:
fixes S' :: 'st
assumes full: "full cdcl⇩W_stgy (init_state N) S'" and no_d: "distinct_mset_mset N"
shows "(conflicting S' = Some {#} ∧ unsatisfiable (set_mset (init_clss S')))
∨ (conflicting S' = None ∧ trail S' ⊨asm init_clss S')"
using assms full_cdcl⇩W_stgy_final_state_conclusive_is_one_false
full_cdcl⇩W_stgy_final_state_conclusive_non_false by blast
lemma full_cdcl⇩W_stgy_final_state_conclusive_from_init_state:
fixes S' :: "'st"
assumes full: "full cdcl⇩W_stgy (init_state N) S'"
and no_d: "distinct_mset_mset N"
shows "(conflicting S' = Some {#} ∧ unsatisfiable (set_mset N))
∨ (conflicting S' = None ∧ trail S' ⊨asm N ∧ satisfiable (set_mset N))"
proof -
have N: "init_clss S' = N"
using full unfolding full_def by (auto dest: rtranclp_cdcl⇩W_stgy_no_more_init_clss)
consider
(confl) "conflicting S' = Some {#}" and "unsatisfiable (set_mset (init_clss S'))"
| (sat) "conflicting S' = None" and "trail S' ⊨asm init_clss S'"
using full_cdcl⇩W_stgy_final_state_conclusive[OF assms] by auto
then show ?thesis
proof cases
case confl
then show ?thesis by (auto simp: N)
next
case sat
have "cdcl⇩W_M_level_inv (init_state N)" by auto
then have "cdcl⇩W_M_level_inv S'"
using full rtranclp_cdcl⇩W_stgy_consistent_inv unfolding full_def by blast
then have "consistent_interp (lits_of (trail S'))" unfolding cdcl⇩W_M_level_inv_def by blast
moreover have "lits_of (trail S') ⊨s set_mset (init_clss S')"
using sat(2) by (auto simp add: true_annots_def true_annot_def true_clss_def)
ultimately have "satisfiable (set_mset (init_clss S'))" by simp
then show ?thesis using sat unfolding N by blast
qed
qed
end
end