theory CDCL_W
imports CDCL_W_Level Weidenbach_Book_Base.Wellfounded_More
begin
chapter ‹Weidenbach's CDCL›
text ‹The organisation of the development is the following:
▪ @{file CDCL_W.thy} contains the specification of the rules: the rules and the strategy are
defined, and we proof the correctness of CDCL.
▪ @{file CDCL_W_Termination.thy} contains the proof of termination, based on the book.
▪ @{file CDCL_W_Merge.thy} contains a variant of the calculus: some rules of the raw calculus are
always applied together (like the rules analysing the conflict and then backtracking). This is
useful for the refinement from NOT.
▪ @{file CDCL_WNOT.thy} proves the inclusion of Weidenbach's version of CDCL in NOT's version. We
use here the version defined in @{file CDCL_W_Merge.thy}. We need this, because NOT's backjump
corresponds to multiple applications of three rules in Weidenbach's calculus. We show also the
termination of the calculus without strategy. There are two different refinement: on from NOT's to
Weidenbach's CDCL and another to W's CDCL with strategy.
We have some variants build on the top of Weidenbach's CDCL calculus:
▪ @{file CDCL_W_Incremental.thy} adds incrementality on the top of @{file CDCL_W.thy}. The way we
are doing it is not compatible with @{file CDCL_W_Merge.thy}, because we add conflicts and the
@{file CDCL_W_Merge.thy} cannot analyse conflicts added externally, since the conflict and
analyse are merged.
▪ @{file CDCL_W_Restart.thy} adds restart and forget while restarting. It is built on the top of
@{file CDCL_W_Merge.thy}.
›
section ‹Weidenbach's CDCL with Multisets›
declare upt.simps(2)[simp del]
subsection ‹The State›
text ‹We will abstract the representation of clause and clauses via two locales. We here use
multisets, contrary to @{file CDCL_W_Abstract_State.thy} where we assume only the existence of a
conversion to the state.›
locale state⇩W_ops =
fixes
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'b" and
trail :: "'st ⇒ ('v, 'v clause) ann_lits" and
init_clss :: "'st ⇒ 'v clauses" and
learned_clss :: "'st ⇒ 'v clauses" and
conflicting :: "'st ⇒ 'v clause option" and
cons_trail :: "('v, 'v clause) ann_lit ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_learned_cls :: "'v clause ⇒ 'st ⇒ 'st" and
remove_cls :: "'v clause ⇒ 'st ⇒ 'st" and
update_conflicting :: "'v clause option ⇒ 'st ⇒ 'st" and
init_state :: "'v clauses ⇒ 'st"
begin
abbreviation hd_trail :: "'st ⇒ ('v, 'v clause) ann_lit" where
"hd_trail S ≡ hd (trail S)"
definition clauses :: "'st ⇒ 'v clauses" where
"clauses S = init_clss S + learned_clss S"
abbreviation resolve_cls :: ‹'a literal ⇒ 'a clause ⇒ 'a clause ⇒ 'a clause› where
"resolve_cls L D' E ≡ remove1_mset (-L) D' ∪# remove1_mset L E"
abbreviation state_butlast :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses
× 'v clause option" where
"state_butlast S ≡ (trail S, init_clss S, learned_clss S, conflicting S)"
definition additional_info :: "'st ⇒ 'b" where
"additional_info S = (λ(_, _, _, _, D). D) (state S)"
end
text ‹We are using an abstract state to abstract away the detail of the implementation: we do not
need to know how the clauses are represented internally, we just need to know that they can be
converted to multisets.›
text ‹Weidenbach state is a five-tuple composed of:
▸ the trail is a list of decided literals;
▸ the initial set of clauses (that is not changed during the whole calculus);
▸ the learned clauses (clauses can be added or remove);
▸ the conflicting clause (if any has been found so far).›
text ‹
Contrary to the original version, we have removed the maximum level of the trail, since the
information is redundant and required an additional invariant.
There are two different clause representation: one for the conflicting clause (@{typ "'v clause"},
standing for conflicting clause) and one for the initial and learned clauses (@{typ "'v clause"},
standing for clause). The representation of the clauses annotating literals in the trail
is slightly different: being able to convert it to @{typ "'v clause"} is enough (needed for function
@{term "hd_trail"} below).
There are several axioms to state the independance of the different fields of the state: for
example, adding a clause to the learned clauses does not change the trail.›
locale state⇩W_no_state =
state⇩W_ops
state
trail init_clss learned_clss conflicting
cons_trail tl_trail add_learned_cls remove_cls
update_conflicting
init_state
for
state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) and
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'b" and
trail :: "'st ⇒ ('v, 'v clause) ann_lits" and
init_clss :: "'st ⇒ 'v clauses" and
learned_clss :: "'st ⇒ 'v clauses" and
conflicting :: "'st ⇒ 'v clause option" and
cons_trail :: "('v, 'v clause) ann_lit ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_learned_cls :: "'v clause ⇒ 'st ⇒ 'st" and
remove_cls :: "'v clause ⇒ 'st ⇒ 'st" and
update_conflicting :: "'v clause option ⇒ 'st ⇒ 'st" and
init_state :: "'v clauses ⇒ 'st" +
assumes
state_eq_ref[simp, intro]: ‹S ∼ S› and
state_eq_sym: ‹S ∼ T ⟷ T ∼ S› and
state_eq_trans: ‹S ∼ T ⟹ T ∼ U' ⟹ S ∼ U'› and
state_eq_state: ‹S ∼ T ⟹ state S = state T› and
cons_trail:
"⋀S'. state st = (M, S') ⟹
state (cons_trail L st) = (L # M, S')" and
tl_trail:
"⋀S'. state st = (M, S') ⟹ state (tl_trail st) = (tl M, S')" and
remove_cls:
"⋀S'. state st = (M, N, U, S') ⟹
state (remove_cls C st) =
(M, removeAll_mset C N, removeAll_mset C U, S')" and
add_learned_cls:
"⋀S'. state st = (M, N, U, S') ⟹
state (add_learned_cls C st) = (M, N, {#C#} + U, S')" and
update_conflicting:
"⋀S'. state st = (M, N, U, D, S') ⟹
state (update_conflicting E st) = (M, N, U, E, S')" and
init_state:
"state_butlast (init_state N) = ([], N, {#}, None)" and
cons_trail_state_eq:
‹S ∼ S' ⟹ cons_trail L S ∼ cons_trail L S'› and
tl_trail_state_eq:
‹S ∼ S' ⟹ tl_trail S ∼ tl_trail S'› and
add_learned_cls_state_eq:
‹S ∼ S' ⟹ add_learned_cls C S ∼ add_learned_cls C S'› and
remove_cls_state_eq:
‹S ∼ S' ⟹ remove_cls C S ∼ remove_cls C S'› and
update_conflicting_state_eq:
‹S ∼ S' ⟹ update_conflicting D S ∼ update_conflicting D S'› and
tl_trail_add_learned_cls_commute:
‹tl_trail (add_learned_cls C T) ∼ add_learned_cls C (tl_trail T)› and
tl_trail_update_conflicting:
‹tl_trail (update_conflicting D T) ∼ update_conflicting D (tl_trail T)› and
update_conflicting_update_conflicting:
‹⋀D D' S S'. S ∼ S' ⟹
update_conflicting D (update_conflicting D' S) ∼ update_conflicting D S'› and
update_conflicting_itself:
‹⋀D S'. conflicting S' = D ⟹ update_conflicting D S' ∼ S'›
locale state⇩W =
state⇩W_no_state
state_eq state
trail init_clss learned_clss conflicting
cons_trail tl_trail add_learned_cls remove_cls
update_conflicting
init_state
for
state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) and
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'b" and
trail :: "'st ⇒ ('v, 'v clause) ann_lits" and
init_clss :: "'st ⇒ 'v clauses" and
learned_clss :: "'st ⇒ 'v clauses" and
conflicting :: "'st ⇒ 'v clause option" and
cons_trail :: "('v, 'v clause) ann_lit ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_learned_cls :: "'v clause ⇒ 'st ⇒ 'st" and
remove_cls :: "'v clause ⇒ 'st ⇒ 'st" and
update_conflicting :: "'v clause option ⇒ 'st ⇒ 'st" and
init_state :: "'v clauses ⇒ 'st" +
assumes
state_prop[simp]:
‹state S = (trail S, init_clss S, learned_clss S, conflicting S, additional_info S)›
begin
lemma
trail_cons_trail[simp]:
"trail (cons_trail L st) = L # trail st" and
trail_tl_trail[simp]: "trail (tl_trail st) = tl (trail st)" and
trail_add_learned_cls[simp]:
"trail (add_learned_cls C st) = trail st" and
trail_remove_cls[simp]:
"trail (remove_cls C st) = trail st" and
trail_update_conflicting[simp]: "trail (update_conflicting E st) = trail st" and
init_clss_cons_trail[simp]:
"init_clss (cons_trail M st) = init_clss st"
and
init_clss_tl_trail[simp]:
"init_clss (tl_trail st) = init_clss st" and
init_clss_add_learned_cls[simp]:
"init_clss (add_learned_cls C st) = init_clss st" and
init_clss_remove_cls[simp]:
"init_clss (remove_cls C st) = removeAll_mset C (init_clss st)" and
init_clss_update_conflicting[simp]:
"init_clss (update_conflicting E st) = init_clss st" and
learned_clss_cons_trail[simp]:
"learned_clss (cons_trail M st) = learned_clss st" and
learned_clss_tl_trail[simp]:
"learned_clss (tl_trail st) = learned_clss st" and
learned_clss_add_learned_cls[simp]:
"learned_clss (add_learned_cls C st) = {#C#} + learned_clss st" and
learned_clss_remove_cls[simp]:
"learned_clss (remove_cls C st) = removeAll_mset C (learned_clss st)" and
learned_clss_update_conflicting[simp]:
"learned_clss (update_conflicting E st) = learned_clss st" and
conflicting_cons_trail[simp]:
"conflicting (cons_trail M st) = conflicting st" and
conflicting_tl_trail[simp]:
"conflicting (tl_trail st) = conflicting st" and
conflicting_add_learned_cls[simp]:
"conflicting (add_learned_cls C st) = conflicting st"
and
conflicting_remove_cls[simp]:
"conflicting (remove_cls C st) = conflicting st" and
conflicting_update_conflicting[simp]:
"conflicting (update_conflicting E st) = E" and
init_state_trail[simp]: "trail (init_state N) = []" and
init_state_clss[simp]: "init_clss (init_state N) = N" and
init_state_learned_clss[simp]: "learned_clss (init_state N) = {#}" and
init_state_conflicting[simp]: "conflicting (init_state N) = None"
using cons_trail[of st] tl_trail[of st] add_learned_cls[of st _ _ _ _ C]
update_conflicting[of st _ _ _ _ _ _]
remove_cls[of st _ _ _ _ C]
init_state[of N]
by auto
lemma
shows
clauses_cons_trail[simp]:
"clauses (cons_trail M S) = clauses S" and
clss_tl_trail[simp]: "clauses (tl_trail S) = clauses S" and
clauses_add_learned_cls_unfolded:
"clauses (add_learned_cls U S) = {#U#} + learned_clss S + init_clss S"
and
clauses_update_conflicting[simp]: "clauses (update_conflicting D S) = clauses S" and
clauses_remove_cls[simp]:
"clauses (remove_cls C S) = removeAll_mset C (clauses S)" and
clauses_add_learned_cls[simp]:
"clauses (add_learned_cls C S) = {#C#} + clauses S" and
clauses_init_state[simp]: "clauses (init_state N) = N"
by (auto simp: ac_simps replicate_mset_plus clauses_def intro: multiset_eqI)
lemma state_eq_trans': ‹S ∼ S' ⟹ T ∼ S' ⟹ T ∼ S›
by (meson state_eq_trans state_eq_sym)
abbreviation backtrack_lvl :: "'st ⇒ nat" where
‹backtrack_lvl S ≡ count_decided (trail S)›
named_theorems state_simp ‹contains all theorems of the form @{term ‹S ∼ T ⟹ P S = P T›}.
These theorems can cause a signefecant blow-up of the simp-space›
lemma
shows
state_eq_trail[state_simp]: "S ∼ T ⟹ trail S = trail T" and
state_eq_init_clss[state_simp]: "S ∼ T ⟹ init_clss S = init_clss T" and
state_eq_learned_clss[state_simp]: "S ∼ T ⟹ learned_clss S = learned_clss T" and
state_eq_conflicting[state_simp]: "S ∼ T ⟹ conflicting S = conflicting T" and
state_eq_clauses[state_simp]: "S ∼ T ⟹ clauses S = clauses T" and
state_eq_undefined_lit[state_simp]: "S ∼ T ⟹ undefined_lit (trail S) L = undefined_lit (trail T) L" and
state_eq_backtrack_lvl[state_simp]: "S ∼ T ⟹ backtrack_lvl S = backtrack_lvl T"
using state_eq_state unfolding clauses_def by auto
lemma state_eq_conflicting_None:
"S ∼ T ⟹ conflicting T = None ⟹ conflicting S = None"
using state_eq_state unfolding clauses_def by auto
text ‹We combine all simplification rules about @{term state_eq} in a single list of theorems. While
they are handy as simplification rule as long as we are working on the state, they also cause a
∗‹huge› slow-down in all other cases.›
declare state_simp[simp]
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 reduce_trail_to_induct:
assumes
‹⋀F S. length (trail S) = length F ⟹ P F S› and
‹⋀F S. trail S = [] ⟹ P F S› and
‹⋀F S. length (trail S) ≠ length F ⟹ trail S ≠ [] ⟹ P F (tl_trail S) ⟹ P F S›
shows
‹P F S›
apply (induction rule: reduce_trail_to.induct)
subgoal for F S using assms
by (cases ‹length (trail S) = length F›; cases ‹trail S = []›) auto
done
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, 'v clause) ann_lits" 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_trail[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 init_clss_update_trail[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_trail[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 conflicting_reduce_trail_to[simp]:
"conflicting (reduce_trail_to F S) = None ⟷ conflicting S = None"
apply (induction F S rule: reduce_trail_to.induct)
by (metis conflicting_update_trail)
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_trail_tl_trail_decomp[simp]:
"trail S = F' @ Decided K # F ⟹ trail (reduce_trail_to F S) = F "
apply (rule reduce_trail_to_skip_beginning[of _ "F' @ Decided K # []"])
by (cases F') (auto simp add: tl_append reduce_trail_to_skip_beginning)
lemma reduce_trail_to_add_learned_cls[simp]:
"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_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_length:
"length M = length M' ⟹ reduce_trail_to M S = reduce_trail_to M' S"
apply (induction M S rule: reduce_trail_to.induct)
by (simp add: reduce_trail_to.simps)
lemma trail_reduce_trail_to_drop:
"trail (reduce_trail_to F S) =
(if length (trail S) ≥ length F
then drop (length (trail S) - length F) (trail S)
else [])"
apply (induction F S rule: reduce_trail_to.induct)
apply (rename_tac F S, case_tac "trail S")
apply (auto; fail)
apply (rename_tac list, case_tac "Suc (length list) > length F")
prefer 2 apply (metis diff_is_0_eq drop_Cons' length_Cons nat_le_linear nat_less_le
reduce_trail_to_eq_length trail_reduce_trail_to_length_le)
apply (subgoal_tac "Suc (length list) - length F = Suc (length list - length F)")
by (auto simp add: reduce_trail_to_length_ne)
lemma in_get_all_ann_decomposition_trail_update_trail[simp]:
assumes H: "(L # M1, M2) ∈ set (get_all_ann_decomposition (trail S))"
shows "trail (reduce_trail_to M1 S) = M1"
proof -
obtain K where
L: "L = Decided K"
using H by (cases L) (auto dest!: in_get_all_ann_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])
(auto simp: tr_S L)
qed
lemma reduce_trail_to_state_eq:
‹S ∼ S' ⟹ length M = length M' ⟹ reduce_trail_to M S ∼ reduce_trail_to M' S'›
apply (induction M S arbitrary: M' S' rule: reduce_trail_to_induct)
apply ((auto;fail)+)[2]
by (simp add: reduce_trail_to_length_ne tl_trail_state_eq)
lemma conflicting_cons_trail_conflicting[iff]:
"conflicting (cons_trail L S) = None ⟷ conflicting S = None"
using conflicting_cons_trail[of L S] map_option_is_None by fastforce+
lemma conflicting_add_learned_cls_conflicting[iff]:
"conflicting (add_learned_cls C S) = None ⟷ conflicting S = None"
by fastforce+
lemma reduce_trail_to_compow_tl_trail_le:
assumes ‹length M < length (trail M')›
shows ‹reduce_trail_to M M' = (tl_trail^^(length (trail M') - length M)) M'›
proof -
have [simp]: ‹(∀ka. k ≠ Suc ka) ⟷ k = 0› for k
by (cases k) auto
show ?thesis
using assms
apply (induction M≡M S≡M' arbitrary: M M' rule: reduce_trail_to.induct)
subgoal for F S
by (subst reduce_trail_to.simps; cases ‹length F < length (trail S) - Suc 0›)
(auto simp: less_iff_Suc_add funpow_swap1)
done
qed
lemma reduce_trail_to_compow_tl_trail_eq:
‹length M = length (trail M') ⟹ reduce_trail_to M M' = (tl_trail^^(length (trail M') - length M)) M'›
by auto
lemma reduce_trail_to_compow_tl_trail:
‹length M ≤ length (trail M') ⟹ reduce_trail_to M M' = (tl_trail^^(length (trail M') - length M)) M'›
using reduce_trail_to_compow_tl_trail_eq[of M M']
reduce_trail_to_compow_tl_trail_le[of M M']
by (cases ‹length M < length (trail M')›) auto
lemma tl_trail_reduce_trail_to_cons:
‹length (L # M) < length (trail M') ⟹ tl_trail (reduce_trail_to (L # M) M') = reduce_trail_to M M'›
by (auto simp: reduce_trail_to_compow_tl_trail_le funpow_swap1
reduce_trail_to_compow_tl_trail_eq less_iff_Suc_add)
lemma compow_tl_trail_add_learned_cls_swap:
‹(tl_trail ^^ n) (add_learned_cls D S) ∼ add_learned_cls D ((tl_trail ^^ n) S)›
by (induction n)
(auto intro: tl_trail_add_learned_cls_commute state_eq_trans
tl_trail_state_eq)
lemma reduce_trail_to_add_learned_cls_state_eq:
‹length M ≤ length (trail S) ⟹
reduce_trail_to M (add_learned_cls D S) ∼ add_learned_cls D (reduce_trail_to M S)›
by (cases ‹length M < length (trail S)›)
(auto simp: compow_tl_trail_add_learned_cls_swap reduce_trail_to_compow_tl_trail_le
reduce_trail_to_compow_tl_trail_eq)
lemma compow_tl_trail_update_conflicting_swap:
‹(tl_trail ^^ n) (update_conflicting D S) ∼ update_conflicting D ((tl_trail ^^ n) S)›
by (induction n)
(auto intro: tl_trail_add_learned_cls_commute state_eq_trans
tl_trail_state_eq tl_trail_update_conflicting)
lemma reduce_trail_to_update_conflicting_state_eq:
‹length M ≤ length (trail S) ⟹
reduce_trail_to M (update_conflicting D S) ∼ update_conflicting D (reduce_trail_to M S)›
by (cases ‹length M < length (trail S)›)
(auto simp: compow_tl_trail_add_learned_cls_swap reduce_trail_to_compow_tl_trail_le
reduce_trail_to_compow_tl_trail_eq compow_tl_trail_update_conflicting_swap)
lemma
additional_info_cons_trail[simp]:
‹additional_info (cons_trail L S) = additional_info S› and
additional_info_tl_trail[simp]:
"additional_info (tl_trail S) = additional_info S" and
additional_info_add_learned_cls_unfolded:
"additional_info (add_learned_cls U S) = additional_info S" and
additional_info_update_conflicting[simp]:
"additional_info (update_conflicting D S) = additional_info S" and
additional_info_remove_cls[simp]:
"additional_info (remove_cls C S) = additional_info S" and
additional_info_add_learned_cls[simp]:
"additional_info (add_learned_cls C S) = additional_info S"
unfolding additional_info_def
using tl_trail[of S] cons_trail[of S] add_learned_cls[of S]
update_conflicting[of S] remove_cls[of S]
by (cases ‹state S›; auto; fail)+
lemma additional_info_reduce_trail_to[simp]:
‹additional_info (reduce_trail_to F S) = additional_info S›
by (induction F S rule: reduce_trail_to.induct)
(metis additional_info_tl_trail reduce_trail_to.simps)
lemma reduce_trail_to:
"state (reduce_trail_to F S) =
((if length (trail S) ≥ length F
then drop (length (trail S) - length F) (trail S)
else []), init_clss S, learned_clss S, conflicting S, additional_info S)"
proof (induction F S rule: reduce_trail_to.induct)
case (1 F S) note IH = this
show ?case
proof (cases "trail S")
case Nil
then show ?thesis using IH by (subst state_prop) auto
next
case (Cons L M)
show ?thesis
proof (cases "Suc (length M) > length F")
case True
then have "Suc (length M) - length F = Suc (length M - length F)"
by auto
then show ?thesis
using Cons True reduce_trail_to_length_ne[of S F] IH by (auto simp del: state_prop)
next
case False
then show ?thesis
using IH reduce_trail_to_length_ne[of S F] apply (subst state_prop)
by (simp add: trail_reduce_trail_to_drop)
qed
qed
qed
end
subsection ‹CDCL Rules›
text ‹Because of the strategy we will later use, we distinguish propagate, conflict from the other
rules›
locale conflict_driven_clause_learning⇩W =
state⇩W
state_eq
state
trail init_clss learned_clss conflicting
cons_trail tl_trail add_learned_cls remove_cls
update_conflicting
init_state
for
state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) and
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'b" and
trail :: "'st ⇒ ('v, 'v clause) ann_lits" and
init_clss :: "'st ⇒ 'v clauses" and
learned_clss :: "'st ⇒ 'v clauses" and
conflicting :: "'st ⇒ 'v clause option" and
cons_trail :: "('v, 'v clause) ann_lit ⇒ 'st ⇒ 'st" and
tl_trail :: "'st ⇒ 'st" and
add_learned_cls :: "'v clause ⇒ 'st ⇒ 'st" and
remove_cls :: "'v clause ⇒ 'st ⇒ 'st" and
update_conflicting :: "'v clause option ⇒ 'st ⇒ 'st" and
init_state :: "'v clauses ⇒ 'st"
begin
inductive propagate :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
propagate_rule: "conflicting S = None ⟹
E ∈# clauses S ⟹
L ∈# E ⟹
trail S ⊨as CNot (E - {#L#}) ⟹
undefined_lit (trail S) L ⟹
T ∼ cons_trail (Propagated L E) S ⟹
propagate S T"
inductive_cases propagateE: "propagate S T"
inductive conflict :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
conflict_rule: "
conflicting S = None ⟹
D ∈# clauses S ⟹
trail S ⊨as CNot D ⟹
T ∼ update_conflicting (Some D) S ⟹
conflict S T"
inductive_cases conflictE: "conflict S T"
inductive backtrack :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
backtrack_rule: "
conflicting S = Some (add_mset L D) ⟹
(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S)) ⟹
get_level (trail S) L = backtrack_lvl S ⟹
get_level (trail S) L = get_maximum_level (trail S) (add_mset L D') ⟹
get_maximum_level (trail S) D' ≡ i ⟹
get_level (trail S) K = i + 1 ⟹
D' ⊆# D ⟹
clauses S ⊨pm add_mset L D' ⟹
T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S))) ⟹
backtrack S T"
inductive_cases backtrackE: "backtrack S T"
text ‹Here is the normal backtrack rule from Weidenbach's book:›
inductive simple_backtrack :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
simple_backtrack_rule: "
conflicting S = Some (add_mset L D) ⟹
(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S)) ⟹
get_level (trail S) L = backtrack_lvl S ⟹
get_level (trail S) L = get_maximum_level (trail S) (add_mset L D) ⟹
get_maximum_level (trail S) D ≡ i ⟹
get_level (trail S) K = i + 1 ⟹
T ∼ cons_trail (Propagated L (add_mset L D))
(reduce_trail_to M1
(add_learned_cls (add_mset L D)
(update_conflicting None S))) ⟹
simple_backtrack S T"
inductive_cases simple_backtrackE: "simple_backtrack S T"
text ‹This is a generalised version of backtrack: It is general enough te also include
OCDCL's version.›
inductive backtrackg :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
backtrackg_rule: "
conflicting S = Some (add_mset L D) ⟹
(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S)) ⟹
get_level (trail S) L = backtrack_lvl S ⟹
get_level (trail S) L = get_maximum_level (trail S) (add_mset L D') ⟹
get_maximum_level (trail S) D' ≡ i ⟹
get_level (trail S) K = i + 1 ⟹
D' ⊆# D ⟹
T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S))) ⟹
backtrackg S T"
inductive_cases backtrackgE: "backtrackg S T"
inductive decide :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
decide_rule:
"conflicting S = None ⟹
undefined_lit (trail S) L ⟹
atm_of L ∈ atms_of_mm (init_clss S) ⟹
T ∼ cons_trail (Decided L) S ⟹
decide S T"
inductive_cases decideE: "decide S T"
inductive skip :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
skip_rule:
"trail S = Propagated L C' # M ⟹
conflicting S = Some E ⟹
-L ∉# E ⟹
E ≠ {#} ⟹
T ∼ tl_trail S ⟹
skip S T"
inductive_cases skipE: "skip S T"
text ‹@{term "get_maximum_level (Propagated L (C + {#L#}) # M) D = k ∨ k = 0"} (that was in a
previous version of the book) is equivalent to
@{term "get_maximum_level (Propagated L (C + {#L#}) # M) D = k"}, when the structural invariants
holds.›
inductive resolve :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
resolve_rule: "trail S ≠ [] ⟹
hd_trail S = Propagated L E ⟹
L ∈# E ⟹
conflicting S = Some D' ⟹
-L ∈# D' ⟹
get_maximum_level (trail S) ((remove1_mset (-L) D')) = backtrack_lvl S ⟹
T ∼ update_conflicting (Some (resolve_cls L D' E))
(tl_trail S) ⟹
resolve S T"
inductive_cases resolveE: "resolve S T"
text ‹
Christoph's version restricts restarts to the the case where ‹¬M⊨ N+U›. While it is possible to
implement this (by watching a clause), This is an unnecessary restriction.
›
inductive restart :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
restart: "state S = (M, N, U, None, S') ⟹
U' ⊆# U ⟹
state T = ([], N, U', None, S') ⟹
restart S T"
inductive_cases restartE: "restart S T"
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:
"conflicting S = None ⟹
C ∈# learned_clss S ⟹
¬(trail S) ⊨asm clauses S ⟹
C ∉ set (get_all_mark_of_propagated (trail S)) ⟹
C ∉# init_clss S ⟹
removeAll_mset C (clauses S) ⊨pm C ⟹
T ∼ remove_cls C S ⟹
forget S T"
inductive_cases forgetE: "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: "skip S S' ⟹ cdcl⇩W_bj S S'" |
resolve: "resolve S S' ⟹ cdcl⇩W_bj S S'" |
backtrack: "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: "decide S S' ⟹ cdcl⇩W_o S S'" |
bj: "cdcl⇩W_bj S S' ⟹ cdcl⇩W_o S S'"
inductive cdcl⇩W_restart :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
propagate: "propagate S S' ⟹ cdcl⇩W_restart S S'" |
conflict: "conflict S S' ⟹ cdcl⇩W_restart S S'" |
other: "cdcl⇩W_o S S' ⟹ cdcl⇩W_restart S S'"|
rf: "cdcl⇩W_rf S S' ⟹ cdcl⇩W_restart S S'"
lemma rtranclp_propagate_is_rtranclp_cdcl⇩W_restart:
"propagate⇧*⇧* S S' ⟹ cdcl⇩W_restart⇧*⇧* S S'"
apply (induction rule: rtranclp_induct)
apply (simp; fail)
apply (frule propagate)
using rtranclp_trans[of cdcl⇩W_restart] by blast
inductive cdcl⇩W :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
W_propagate: "propagate S S' ⟹ cdcl⇩W S S'" |
W_conflict: "conflict S S' ⟹ cdcl⇩W S S'" |
W_other: "cdcl⇩W_o S S' ⟹ cdcl⇩W S S'"
lemma cdcl⇩W_cdcl⇩W_restart:
"cdcl⇩W S T ⟹ cdcl⇩W_restart S T"
by (induction rule: cdcl⇩W.induct) (auto intro: cdcl⇩W_restart.intros simp del: state_prop)
lemma rtranclp_cdcl⇩W_cdcl⇩W_restart:
‹cdcl⇩W⇧*⇧* S T ⟹ cdcl⇩W_restart⇧*⇧* S T›
apply (induction rule: rtranclp_induct)
apply (auto; fail)[]
by (meson cdcl⇩W_cdcl⇩W_restart rtranclp.rtrancl_into_rtrancl)
lemma cdcl⇩W_restart_all_rules_induct[consumes 1, case_names propagate conflict forget restart decide
skip resolve backtrack]:
fixes S :: 'st
assumes
cdcl⇩W_restart: "cdcl⇩W_restart 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_restart.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_restart_all_induct[consumes 1, case_names propagate conflict forget restart decide skip
resolve backtrack]:
fixes S :: 'st
assumes
cdcl⇩W_restart: "cdcl⇩W_restart S S'" and
propagateH: "⋀C L T. conflicting S = None ⟹
C ∈# clauses S ⟹
L ∈# C ⟹
trail S ⊨as CNot (remove1_mset L C) ⟹
undefined_lit (trail S) L ⟹
T ∼ cons_trail (Propagated L C) S ⟹
P S T" and
conflictH: "⋀D T. conflicting S = None ⟹
D ∈# clauses S ⟹
trail S ⊨as CNot D ⟹
T ∼ update_conflicting (Some D) S ⟹
P S T" and
forgetH: "⋀C T. conflicting S = None ⟹
C ∈# learned_clss S ⟹
¬(trail S) ⊨asm clauses S ⟹
C ∉ set (get_all_mark_of_propagated (trail S)) ⟹
C ∉# init_clss S ⟹
removeAll_mset C (clauses S) ⊨pm C ⟹
T ∼ remove_cls C S ⟹
P S T" and
restartH: "⋀T U. conflicting S = None ⟹
state T = ([], init_clss S, U, None, additional_info S) ⟹
U ⊆# learned_clss S ⟹
P S T" and
decideH: "⋀L T. conflicting S = None ⟹
undefined_lit (trail S) L ⟹
atm_of L ∈ atms_of_mm (init_clss S) ⟹
T ∼ cons_trail (Decided L) S ⟹
P S T" and
skipH: "⋀L C' M E T.
trail S = Propagated L C' # M ⟹
conflicting S = Some E ⟹
-L ∉# E ⟹ E ≠ {#} ⟹
T ∼ tl_trail S ⟹
P S T" and
resolveH: "⋀L E M D T.
trail S = Propagated L E # M ⟹
L ∈# E ⟹
hd_trail S = Propagated L E ⟹
conflicting S = Some D ⟹
-L ∈# D ⟹
get_maximum_level (trail S) ((remove1_mset (-L) D)) = backtrack_lvl S ⟹
T ∼ update_conflicting
(Some (resolve_cls L D E)) (tl_trail S) ⟹
P S T" and
backtrackH: "⋀L D K i M1 M2 T D'.
conflicting S = Some (add_mset L D) ⟹
(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S)) ⟹
get_level (trail S) L = backtrack_lvl S ⟹
get_level (trail S) L = get_maximum_level (trail S) (add_mset L D') ⟹
get_maximum_level (trail S) D' ≡ i ⟹
get_level (trail S) K = i+1 ⟹
D' ⊆# D ⟹
clauses S ⊨pm add_mset L D' ⟹
T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S))) ⟹
P S T"
shows "P S S'"
using cdcl⇩W_restart
proof (induct S S' rule: cdcl⇩W_restart_all_rules_induct)
case (propagate S')
then show ?case
by (auto elim!: propagateE intro!: propagateH)
next
case (conflict S')
then show ?case
by (auto elim!: conflictE intro!: conflictH)
next
case (restart S')
then show ?case
by (auto elim!: restartE intro!: restartH)
next
case (decide T)
then show ?case
by (auto elim!: decideE intro!: decideH)
next
case (backtrack S')
then show ?case by (auto elim!: backtrackE intro!: backtrackH simp del: state_simp)
next
case (forget S')
then show ?case by (auto elim!: forgetE intro!: forgetH)
next
case (skip S')
then show ?case by (auto elim!: skipE intro!: skipH)
next
case (resolve S')
then show ?case
by (cases "trail S") (auto elim!: resolveE intro!: resolveH)
qed
lemma cdcl⇩W_o_induct[consumes 1, case_names decide skip resolve backtrack]:
fixes S :: "'st"
assumes cdcl⇩W_restart: "cdcl⇩W_o S T" and
decideH: "⋀L T. conflicting S = None ⟹ undefined_lit (trail S) L
⟹ atm_of L ∈ atms_of_mm (init_clss S)
⟹ T ∼ cons_trail (Decided L) S
⟹ P S T" and
skipH: "⋀L C' M E T.
trail S = Propagated L C' # M ⟹
conflicting S = Some E ⟹
-L ∉# E ⟹ E ≠ {#} ⟹
T ∼ tl_trail S ⟹
P S T" and
resolveH: "⋀L E M D T.
trail S = Propagated L E # M ⟹
L ∈# E ⟹
hd_trail S = Propagated L E ⟹
conflicting S = Some D ⟹
-L ∈# D ⟹
get_maximum_level (trail S) ((remove1_mset (-L) D)) = backtrack_lvl S ⟹
T ∼ update_conflicting
(Some (resolve_cls L D E)) (tl_trail S) ⟹
P S T" and
backtrackH: "⋀L D K i M1 M2 T D'.
conflicting S = Some (add_mset L D) ⟹
(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S)) ⟹
get_level (trail S) L = backtrack_lvl S ⟹
get_level (trail S) L = get_maximum_level (trail S) (add_mset L D') ⟹
get_maximum_level (trail S) D' ≡ i ⟹
get_level (trail S) K = i+1 ⟹
D' ⊆# D ⟹
clauses S ⊨pm add_mset L D' ⟹
T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S))) ⟹
P S T"
shows "P S T"
using cdcl⇩W_restart apply (induct T rule: cdcl⇩W_o.induct)
subgoal using assms(2) by (auto elim: decideE; fail)
subgoal apply (elim cdcl⇩W_bjE skipE resolveE backtrackE)
apply (frule skipH; simp; fail)
apply (cases "trail S"; auto elim!: resolveE intro!: resolveH; fail)
apply (frule backtrackH; simp; fail)
done
done
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)
lemma backtrack_backtrackg:
‹backtrack S T ⟹ backtrackg S T›
unfolding backtrack.simps backtrackg.simps
by blast
lemma simple_backtrack_backtrackg:
‹simple_backtrack S T ⟹ backtrackg S T›
unfolding simple_backtrack.simps backtrackg.simps
by blast
subsection ‹Structural Invariants›
subsubsection ‹Properties of the trail›
text ‹We here establish that:
▪ the consistency of the trail;
▪ the fact that there is no duplicate in the trail.›
text ‹
\begin{nit}
As one can see in the following proof, the properties of the levels are ∗‹required› to prove
\cwref{prop:prop:cdclconsis}{Item 1 page 94}. However, this point is only mentioned ∗‹later›,
and only in the proof of \cwref{prop:prop:cdclbacktrack}{Item 7 page 95}.
\end{nit}›
lemma backtrack_lit_skiped:
assumes
L: "get_level (trail S) L = backtrack_lvl S" and
M1: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
no_dup: "no_dup (trail S)" and
lev_K: "get_level (trail S) K = i + 1"
shows "undefined_lit M1 L"
proof (rule ccontr)
let ?M = "trail S"
assume L_in_M1: "¬ ?thesis"
obtain M2' where
Mc: "trail S = M2' @ M2 @ Decided K # M1"
using M1 by blast
have Kc: ‹undefined_lit M2' K› and KM2: ‹undefined_lit M2 K› ‹atm_of L ≠ atm_of K› and
‹undefined_lit M2' L› ‹undefined_lit M2 L›
using L_in_M1 no_dup unfolding Mc by (auto simp: atm_of_eq_atm_of dest: defined_lit_no_dupD)
then have g_M_eq_g_M1: "get_level ?M L = get_level M1 L"
using L_in_M1 unfolding Mc by auto
then have "get_level M1 L < Suc i"
using count_decided_ge_get_level[of M1 L] KM2 lev_K Kc unfolding Mc by auto
moreover have "Suc i ≤ backtrack_lvl S" using KM2 lev_K Kc unfolding Mc by (simp add: Mc)
ultimately show False using L g_M_eq_g_M1 by auto
qed
lemma cdcl⇩W_restart_distinctinv_1:
assumes
"cdcl⇩W_restart S S'" and
n_d: "no_dup (trail S)"
shows "no_dup (trail S')"
using assms(1)
proof (induct rule: cdcl⇩W_restart_all_induct)
case (backtrack L D K i M1 M2 T D') note decomp = this(2) and L = this(3) and lev_K = this(6) and
T = this(9)
obtain c where Mc: "trail S = c @ M2 @ Decided K # M1"
using decomp by auto
have "no_dup (M2 @ Decided K # M1)"
using Mc n_d by (auto dest: no_dup_appendD simp: defined_lit_map image_Un)
moreover have L_M1: "undefined_lit M1 L"
using backtrack_lit_skiped[of S L K M1 M2 i] L decomp lev_K n_d
unfolding defined_lit_map lits_of_def by fast
ultimately show ?case using decomp T n_d by (auto dest: no_dup_appendD)
qed (use n_d in auto)
text ‹\cwref{prop:prop:cdclconsis}{Item 1 page 94}›
lemma cdcl⇩W_restart_consistent_inv_2:
assumes
"cdcl⇩W_restart S S'" and
"no_dup (trail S)"
shows "consistent_interp (lits_of_l (trail S'))"
using cdcl⇩W_restart_distinctinv_1[OF assms] distinct_consistent_interp by fast
definition cdcl⇩W_M_level_inv :: "'st ⇒ bool" where
"cdcl⇩W_M_level_inv S ⟷
consistent_interp (lits_of_l (trail S))
∧ no_dup (trail S)"
lemma cdcl⇩W_M_level_inv_decomp:
assumes "cdcl⇩W_M_level_inv S"
shows
"consistent_interp (lits_of_l (trail S))" and
"no_dup (trail S)"
using assms unfolding cdcl⇩W_M_level_inv_def by fastforce+
lemma cdcl⇩W_restart_consistent_inv:
fixes S S' :: 'st
assumes
"cdcl⇩W_restart S S'" and
"cdcl⇩W_M_level_inv S"
shows "cdcl⇩W_M_level_inv S'"
using assms cdcl⇩W_restart_consistent_inv_2 cdcl⇩W_restart_distinctinv_1
unfolding cdcl⇩W_M_level_inv_def by meson+
lemma rtranclp_cdcl⇩W_restart_consistent_inv:
assumes
"cdcl⇩W_restart⇧*⇧* 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_restart_consistent_inv)
lemma tranclp_cdcl⇩W_restart_consistent_inv:
assumes
"cdcl⇩W_restart⇧+⇧+ 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_restart_consistent_inv)
lemma cdcl⇩W_M_level_inv_S0_cdcl⇩W_restart[simp]:
"cdcl⇩W_M_level_inv (init_state N)"
unfolding cdcl⇩W_M_level_inv_def by auto
lemma backtrack_ex_decomp:
assumes
M_l: "no_dup (trail S)" and
i_S: "i < backtrack_lvl S"
shows "∃K M1 M2. (Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S)) ∧
get_level (trail S) K = Suc i"
proof -
let ?M = "trail S"
have "i < count_decided (trail S)"
using i_S by auto
then obtain c K c' where tr_S: "trail S = c @ Decided K # c'" and
lev_K: "get_level (trail S) K = Suc i"
using le_count_decided_decomp[of "trail S" i] M_l by auto
obtain M1 M2 where "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))"
using Decided_cons_in_get_all_ann_decomposition_append_Decided_cons unfolding tr_S by fast
then show ?thesis using lev_K by blast
qed
lemma backtrack_lvl_backtrack_decrease:
assumes inv: "cdcl⇩W_M_level_inv S" and bt: "backtrack S T"
shows "backtrack_lvl T < backtrack_lvl S"
using inv bt le_count_decided_decomp[of "trail S" "backtrack_lvl T"]
unfolding cdcl⇩W_M_level_inv_def
by (fastforce elim!: backtrackE simp: append_assoc[of _ _ "_# _", symmetric]
simp del: append_assoc)
subsubsection ‹Compatibility with @{term state_eq}›
declare state_eq_trans[trans]
lemma propagate_state_eq_compatible:
assumes
propa: "propagate S T" and
SS': "S ∼ S'" and
TT': "T ∼ T'"
shows "propagate S' T'"
proof -
obtain C L where
conf: "conflicting S = None" and
C: "C ∈# clauses S" and
L: "L ∈# C" and
tr: "trail S ⊨as CNot (remove1_mset L C)" and
undef: "undefined_lit (trail S) L" and
T: "T ∼ cons_trail (Propagated L C) S"
using propa by (elim propagateE) auto
have C': "C ∈# clauses S'"
using SS' C
by (auto simp: clauses_def)
have T': ‹T' ∼ cons_trail (Propagated L C) S'›
using state_eq_trans[of T' T] SS' TT'
by (meson T cons_trail_state_eq state_eq_sym state_eq_trans)
show ?thesis
apply (rule propagate_rule[of _ C])
using SS' conf C' L tr undef TT' T T' by auto
qed
lemma conflict_state_eq_compatible:
assumes
confl: "conflict S T" and
TT': "T ∼ T'" and
SS': "S ∼ S'"
shows "conflict S' T'"
proof -
obtain D where
conf: "conflicting S = None" and
D: "D ∈# clauses S" and
tr: " trail S ⊨as CNot D" and
T: "T ∼ update_conflicting (Some D) S"
using confl by (elim conflictE) auto
have D': "D ∈# clauses S'"
using D SS' by fastforce
have T': ‹T' ∼ update_conflicting (Some D) S'›
using state_eq_trans[of T' T] SS' TT'
by (meson T update_conflicting_state_eq state_eq_sym state_eq_trans)
show ?thesis
apply (rule conflict_rule[of _ D])
using SS' conf D' tr TT' T T' by auto
qed
lemma backtrack_state_eq_compatible:
assumes
bt: "backtrack S T" and
SS': "S ∼ S'" and
TT': "T ∼ T'"
shows "backtrack S' T'"
proof -
obtain D L K i M1 M2 D' where
conf: "conflicting S = Some (add_mset L D)" and
decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
lev: "get_level (trail S) L = backtrack_lvl S" and
max: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
max_D: "get_maximum_level (trail S) D' ≡ i" and
lev_K: "get_level (trail S) K = Suc i" and
D'_D: ‹D' ⊆# D› and
NU_DL: ‹clauses S ⊨pm add_mset L D'› and
T: "T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S)))"
using bt by (elim backtrackE) metis
let ?D = ‹add_mset L D›
let ?D' = ‹add_mset L D'›
have D': "conflicting S' = Some ?D"
using SS' conf by (cases "conflicting S'") auto
have T'_S: "T' ∼ cons_trail (Propagated L ?D')
(reduce_trail_to M1 (add_learned_cls ?D'
(update_conflicting None S)))"
using T TT' state_eq_sym state_eq_trans by blast
have T': "T' ∼ cons_trail (Propagated L ?D')
(reduce_trail_to M1 (add_learned_cls ?D'
(update_conflicting None S')))"
apply (rule state_eq_trans[OF T'_S])
by (auto simp: cons_trail_state_eq reduce_trail_to_state_eq add_learned_cls_state_eq
update_conflicting_state_eq SS')
show ?thesis
apply (rule backtrack_rule[of _ L D K M1 M2 D' i])
subgoal by (rule D')
subgoal using TT' decomp SS' by auto
subgoal using lev TT' SS' by auto
subgoal using max TT' SS' by auto
subgoal using max_D TT' SS' by auto
subgoal using lev_K TT' SS' by auto
subgoal by (rule D'_D)
subgoal using NU_DL TT' SS' by auto
subgoal by (rule T')
done
qed
lemma decide_state_eq_compatible:
assumes
dec: "decide S T" and
SS': "S ∼ S'" and
TT': "T ∼ T'"
shows "decide S' T'"
using assms
proof -
obtain L :: "'v literal" where
f4: "undefined_lit (trail S) L"
"atm_of L ∈ atms_of_mm (init_clss S)"
"T ∼ cons_trail (Decided L) S"
using dec decide.simps by blast
have "cons_trail (Decided L) S' ∼ T'"
using f4 SS' TT' by (metis (no_types) cons_trail_state_eq state_eq_sym
state_eq_trans)
then show ?thesis
using f4 SS' TT' dec by (auto simp: decide.simps state_eq_sym)
qed
lemma skip_state_eq_compatible:
assumes
skip: "skip S T" and
SS': "S ∼ S'" and
TT': "T ∼ T'"
shows "skip S' T'"
proof -
obtain L C' M E where
tr: "trail S = Propagated L C' # M" and
raw: "conflicting S = Some E" and
L: "-L ∉# E" and
E: "E ≠ {#}" and
T: "T ∼ tl_trail S"
using skip by (elim skipE) simp
obtain E' where E': "conflicting S' = Some E'"
using SS' raw by (cases "conflicting S'") auto
have T': ‹T' ∼ tl_trail S'›
by (meson SS' T TT' state_eq_sym state_eq_trans tl_trail_state_eq)
show ?thesis
apply (rule skip_rule)
using tr raw L E T SS' apply (auto; fail)[]
using E' apply (simp; fail)
using E' SS' L raw E apply ((auto; fail)+)[2]
using T' by auto
qed
lemma resolve_state_eq_compatible:
assumes
res: "resolve S T" and
TT': "T ∼ T'" and
SS': "S ∼ S'"
shows "resolve S' T'"
proof -
obtain E D L where
tr: "trail S ≠ []" and
hd: "hd_trail S = Propagated L E" and
L: "L ∈# E" and
raw: "conflicting S = Some D" and
LD: "-L ∈# D" and
i: "get_maximum_level (trail S) ((remove1_mset (-L) D)) = backtrack_lvl S" and
T: "T ∼ update_conflicting (Some (resolve_cls L D E)) (tl_trail S)"
using assms by (elim resolveE) simp
obtain D' where
D': "conflicting S' = Some D'"
using SS' raw by fastforce
have [simp]: "D = D'"
using D' SS' raw state_simp(5) by fastforce
have T'T: "T' ∼ T"
using TT' state_eq_sym by auto
have T': ‹T' ∼ update_conflicting (Some (remove1_mset (- L) D' ∪# remove1_mset L E))
(tl_trail S')›
proof -
have "tl_trail S ∼ tl_trail S'"
using SS' by (auto simp: tl_trail_state_eq)
then show ?thesis
using T T'T ‹D = D'› state_eq_trans update_conflicting_state_eq by blast
qed
show ?thesis
apply (rule resolve_rule)
using tr SS' apply (simp; fail)
using hd SS' apply (simp; fail)
using L apply (simp; fail)
using D' apply (simp; fail)
using D' SS' raw LD apply (auto; fail)[]
using D' SS' raw LD i apply (auto; fail)[]
using T' by auto
qed
lemma forget_state_eq_compatible:
assumes
forget: "forget S T" and
SS': "S ∼ S'" and
TT': "T ∼ T'"
shows "forget S' T'"
proof -
obtain C where
conf: "conflicting S = None" and
C: "C ∈# learned_clss S" and
tr: "¬(trail S) ⊨asm clauses S" and
C1: "C ∉ set (get_all_mark_of_propagated (trail S))" and
C2: "C ∉# init_clss S" and
ent: ‹removeAll_mset C (clauses S) ⊨pm C› and
T: "T ∼ remove_cls C S"
using forget by (elim forgetE) simp
have T': ‹T' ∼ remove_cls C S'›
by (meson SS' T TT' remove_cls_state_eq state_eq_sym state_eq_trans)
show ?thesis
apply (rule forget_rule)
using SS' conf apply (simp; fail)
using C SS' apply (simp; fail)
using SS' tr apply (simp; fail)
using SS' C1 apply (simp; fail)
using SS' C2 apply (simp; fail)
using ent SS' apply (simp; fail)
using T' by auto
qed
lemma cdcl⇩W_restart_state_eq_compatible:
assumes
"cdcl⇩W_restart S T" and "¬restart S T" and
"S ∼ S'"
"T ∼ T'"
shows "cdcl⇩W_restart S' T'"
using assms by (meson backtrack backtrack_state_eq_compatible bj cdcl⇩W_restart.simps
cdcl⇩W_o_rule_cases cdcl⇩W_rf.cases conflict_state_eq_compatible decide decide_state_eq_compatible
forget forget_state_eq_compatible propagate_state_eq_compatible
resolve resolve_state_eq_compatible skip skip_state_eq_compatible state_eq_ref)
lemma cdcl⇩W_bj_state_eq_compatible:
assumes
"cdcl⇩W_bj S T"
"T ∼ T'"
shows "cdcl⇩W_bj S T'"
using assms by (meson backtrack backtrack_state_eq_compatible cdcl⇩W_bjE resolve
resolve_state_eq_compatible skip skip_state_eq_compatible state_eq_ref)
lemma tranclp_cdcl⇩W_bj_state_eq_compatible:
assumes
"cdcl⇩W_bj⇧+⇧+ S T"
"S ∼ S'" and
"T ∼ T'"
shows "cdcl⇩W_bj⇧+⇧+ S' T'"
using assms
proof (induction arbitrary: S' T')
case base
then show ?case
unfolding tranclp_unfold_end by (meson backtrack_state_eq_compatible cdcl⇩W_bj.simps
resolve_state_eq_compatible rtranclp_unfold skip_state_eq_compatible)
next
case (step T U) note IH = this(3)[OF this(4)]
have "cdcl⇩W_restart⇧+⇧+ S T"
using tranclp_mono[of cdcl⇩W_bj cdcl⇩W_restart] step.hyps(1) cdcl⇩W_restart.other cdcl⇩W_o.bj 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
lemma skip_unique:
"skip S T ⟹ skip S T' ⟹ T ∼ T'"
by (auto elim!: skipE intro: state_eq_trans')
lemma resolve_unique:
"resolve S T ⟹ resolve S T' ⟹ T ∼ T'"
by (fastforce intro: state_eq_trans' elim: resolveE)
text ‹The same holds for backtrack, but more invariants are needed.›
subsubsection ‹Conservation of some Properties›
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) (auto simp: inv 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!: tranclp_cdcl⇩W_restart_consistent_inv
dest: tranclp_mono_explicit[of cdcl⇩W_o _ _ cdcl⇩W_restart] cdcl⇩W_o_no_more_init_clss
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_restart_init_clss:
assumes
"cdcl⇩W_restart S T"
shows "init_clss S = init_clss T"
using assms by (induction rule: cdcl⇩W_restart_all_induct)
(auto simp: not_in_iff)
lemma rtranclp_cdcl⇩W_restart_init_clss:
"cdcl⇩W_restart⇧*⇧* S T ⟹ init_clss S = init_clss T"
by (induct rule: rtranclp_induct) (auto dest: cdcl⇩W_restart_init_clss rtranclp_cdcl⇩W_restart_consistent_inv)
lemma tranclp_cdcl⇩W_restart_init_clss:
"cdcl⇩W_restart⇧+⇧+ S T ⟹ init_clss S = init_clss T"
using rtranclp_cdcl⇩W_restart_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 belong to the clauses. We could also restrict it to entailment by the clauses, to
allow forgetting this clauses.›
definition (in state⇩W_ops) reasons_in_clauses :: ‹'st ⇒ bool› where
‹reasons_in_clauses (S :: 'st) ⟷
(set (get_all_mark_of_propagated (trail S)) ⊆ set_mset (clauses S))›
definition (in state⇩W_ops) cdcl⇩W_learned_clause :: ‹'st ⇒ bool› where
"cdcl⇩W_learned_clause (S :: 'st) ⟷
((∀T. conflicting S = Some T ⟶ clauses S ⊨pm T)
∧ reasons_in_clauses S)"
lemma cdcl⇩W_learned_clause_alt_def:
‹cdcl⇩W_learned_clause (S :: 'st) ⟷
((∀T. conflicting S = Some T ⟶ clauses S ⊨pm T)
∧ set (get_all_mark_of_propagated (trail S)) ⊆ set_mset (clauses S))›
by (auto simp: cdcl⇩W_learned_clause_def reasons_in_clauses_def)
lemma reasons_in_clauses_init_state[simp]: ‹reasons_in_clauses (init_state N)›
by (auto simp: reasons_in_clauses_def)
text ‹\cwref{prop:prop:cdclConflClause}{Item 3 page 95} for the inital state and some additional structural
properties about the trail.›
lemma cdcl⇩W_learned_clause_S0_cdcl⇩W_restart[simp]:
"cdcl⇩W_learned_clause (init_state N)"
unfolding cdcl⇩W_learned_clause_alt_def by auto
text ‹\cwref{prop:prop:cdclvaluation}{Item 4 page 95}›
lemma cdcl⇩W_restart_learned_clss:
assumes
"cdcl⇩W_restart 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)
proof (induct rule: cdcl⇩W_restart_all_induct)
case (backtrack L D K i M1 M2 T D') note decomp = this(2) and confl = this(1) and lev_K = this (6)
and T = this(9)
show ?case
using decomp learned confl T unfolding cdcl⇩W_learned_clause_alt_def reasons_in_clauses_def
by (auto dest!: get_all_ann_decomposition_exists_prepend)
next
case (resolve L C M D) note trail = this(1) and CL = this(2) and confl = this(4) and DL = this(5)
and lvl = this(6) and T = this(7)
moreover
have "clauses S ⊨pm add_mset L C"
using trail learned unfolding cdcl⇩W_learned_clause_alt_def clauses_def reasons_in_clauses_def
by (auto dest: true_clss_clss_in_imp_true_clss_cls)
moreover have "remove1_mset (- L) D + {#- L#} = D"
using DL by (auto simp: multiset_eq_iff)
moreover have "remove1_mset L C + {#L#} = C"
using CL by (auto simp: multiset_eq_iff)
ultimately show ?case
using learned T
by (auto dest: mk_disjoint_insert
simp add: cdcl⇩W_learned_clause_alt_def clauses_def reasons_in_clauses_def
intro!: true_clss_cls_union_mset_true_clss_cls_or_not_true_clss_cls_or[of _ L])
next
case (restart T)
then show ?case
using learned
by (auto
simp: clauses_def cdcl⇩W_learned_clause_alt_def reasons_in_clauses_def
dest: true_clss_clssm_subsetE)
next
case propagate
then show ?case using learned by (auto simp: cdcl⇩W_learned_clause_alt_def reasons_in_clauses_def)
next
case conflict
then show ?case using learned
by (fastforce simp: cdcl⇩W_learned_clause_alt_def clauses_def
true_clss_clss_in_imp_true_clss_cls reasons_in_clauses_def)
next
case (forget U)
then show ?case using learned
by (auto simp: cdcl⇩W_learned_clause_alt_def clauses_def reasons_in_clauses_def
split: if_split_asm)
qed (use learned in ‹auto simp: cdcl⇩W_learned_clause_alt_def clauses_def reasons_in_clauses_def›)
lemma rtranclp_cdcl⇩W_restart_learned_clss:
assumes
"cdcl⇩W_restart⇧*⇧* 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_restart_learned_clss intro: rtranclp_cdcl⇩W_restart_consistent_inv)
lemma cdcl⇩W_restart_reasons_in_clauses:
assumes
"cdcl⇩W_restart S S'" and
learned: "reasons_in_clauses S"
shows "reasons_in_clauses S'"
using assms(1) learned
by (induct rule: cdcl⇩W_restart_all_induct)
(auto simp: reasons_in_clauses_def dest!: get_all_ann_decomposition_exists_prepend)
lemma rtranclp_cdcl⇩W_restart_reasons_in_clauses:
assumes
"cdcl⇩W_restart⇧*⇧* S S'" and
learned: "reasons_in_clauses S"
shows "reasons_in_clauses S'"
using assms(1) learned
by (induct rule: rtranclp_induct)
(auto simp: cdcl⇩W_restart_reasons_in_clauses)
subsubsection ‹No alien atom in the state›
text ‹This invariant means that all the literals are in the set of clauses. These properties are
implicit in Weidenbach's book.›
definition "no_strange_atm S' ⟷
(∀T. conflicting S' = Some T ⟶ atms_of T ⊆ atms_of_mm (init_clss S'))
∧ (∀L mark. Propagated L mark ∈ set (trail S') ⟶ atms_of mark ⊆ atms_of_mm (init_clss S'))
∧ atms_of_mm (learned_clss S') ⊆ atms_of_mm (init_clss S')
∧ atm_of ` (lits_of_l (trail S')) ⊆ atms_of_mm (init_clss S')"
lemma no_strange_atm_decomp:
assumes "no_strange_atm S"
shows "conflicting S = Some T ⟹ atms_of T ⊆ atms_of_mm (init_clss S)"
and "(∀L mark. Propagated L mark ∈ set (trail S) ⟶ atms_of mark ⊆ atms_of_mm (init_clss S))"
and "atms_of_mm (learned_clss S) ⊆ atms_of_mm (init_clss S)"
and "atm_of ` (lits_of_l (trail S)) ⊆ atms_of_mm (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 propagate_no_strange_atm_inv:
assumes
"propagate S T" and
alien: "no_strange_atm S"
shows "no_strange_atm T"
using assms(1)
proof (induction rule: propagate.induct)
case (propagate_rule C L T) note confl = this(1) and C = this(2) and C_L = this(3) and
tr = this(4) and undef = this(5) and T = this(6)
have atm_CL: "atms_of C ⊆ atms_of_mm (init_clss S)"
using C alien unfolding no_strange_atm_def
by (auto simp: clauses_def dest!: multi_member_split)
show ?case
unfolding no_strange_atm_def
proof (intro conjI allI impI, goal_cases)
case (1 C)
then show ?case
using confl T undef by auto
next
case (2 L' mark')
then show ?case
using C_L T alien undef atm_CL unfolding no_strange_atm_def clauses_def by (auto 5 5)
next
case 3
show ?case using T alien undef unfolding no_strange_atm_def by auto
next
case 4
show ?case
using T alien undef C_L atm_CL unfolding no_strange_atm_def by (auto simp: atms_of_def)
qed
qed
lemma atms_of_ms_learned_clss_restart_state_in_atms_of_ms_learned_clssI:
"atms_of_mm (learned_clss S) ⊆ atms_of_mm (init_clss S) ⟹
x ∈ atms_of_mm (learned_clss T) ⟹
learned_clss T ⊆# learned_clss S ⟹
x ∈ atms_of_mm (init_clss S)"
by (meson atms_of_ms_mono contra_subsetD set_mset_mono)
lemma (in -) atms_of_subset_mset_mono: ‹D' ⊆# D ⟹ atms_of D' ⊆ atms_of D›
by (auto simp: atms_of_def)
lemma cdcl⇩W_restart_no_strange_atm_explicit:
assumes
"cdcl⇩W_restart S S'" and
lev: "cdcl⇩W_M_level_inv S" and
conf: "∀T. conflicting S = Some T ⟶ atms_of T ⊆ atms_of_mm (init_clss S)" and
decided: "∀L mark. Propagated L mark ∈ set (trail S)
⟶ atms_of mark ⊆ atms_of_mm (init_clss S)" and
learned: "atms_of_mm (learned_clss S) ⊆ atms_of_mm (init_clss S)" and
trail: "atm_of ` (lits_of_l (trail S)) ⊆ atms_of_mm (init_clss S)"
shows
"(∀T. conflicting S' = Some T ⟶ atms_of T ⊆ atms_of_mm (init_clss S')) ∧
(∀L mark. Propagated L mark ∈ set (trail S') ⟶ atms_of mark ⊆ atms_of_mm (init_clss S')) ∧
atms_of_mm (learned_clss S') ⊆ atms_of_mm (init_clss S') ∧
atm_of ` (lits_of_l (trail S')) ⊆ atms_of_mm (init_clss S')"
(is "?C S' ∧ ?M S' ∧ ?U S' ∧ ?V S'")
using assms(1)
proof (induct rule: cdcl⇩W_restart_all_induct)
case (propagate C L T) note confl = this(1) and C_L = this(2) and tr = this(3) and undef = this(4)
and T = this(5)
show ?case
using propagate_rule[OF propagate.hyps(1-3) _ propagate.hyps(5,6), simplified]
propagate.hyps(4) propagate_no_strange_atm_inv[of S T]
conf decided learned trail unfolding no_strange_atm_def by presburger
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 D_S = this(2) and T = this(4)
have D: "atm_of ` set_mset D ⊆ ⋃(atms_of ` (set_mset (clauses S)))"
using D_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 intro: atms_of_ms_learned_clss_restart_state_in_atms_of_ms_learned_clssI)
next
case (forget C T) note confl = this(1) and C = this(4) and C_le = this(5) and
T = this(7)
have H: "⋀L mark. Propagated L mark ∈ set (trail S) ⟹ atms_of mark ⊆ atms_of_mm (init_clss S)"
using decided by simp
show ?case unfolding clauses_def apply (intro conjI)
using conf confl T trail C unfolding clauses_def apply (auto dest!: H)[]
using T trail C C_le apply (auto dest!: H)[]
using T learned C_le atms_of_ms_remove_subset[of "set_mset (learned_clss S)"] apply auto[]
using T trail C_le apply (auto simp: clauses_def lits_of_def)[]
done
next
case (backtrack L D K i M1 M2 T D') note confl = this(1) and decomp = this(2) and
lev_K = this(6) and D_D' = this(7) and M1_D' = this(8) and T = this(9)
have "?C T"
using conf T decomp lev lev_K by (auto simp: cdcl⇩W_M_level_inv_decomp)
moreover have "set M1 ⊆ set (trail S)"
using decomp by auto
then have M: "?M T"
using decided conf confl T decomp lev lev_K D_D'
by (auto simp: image_subset_iff clauses_def cdcl⇩W_M_level_inv_decomp
dest!: atms_of_subset_mset_mono)
moreover have "?U T"
using learned decomp conf confl T lev lev_K D_D' unfolding clauses_def
by (auto simp: cdcl⇩W_M_level_inv_decomp dest: atms_of_subset_mset_mono)
moreover have "?V T"
using M conf confl trail T decomp lev lev_K
by (auto simp: cdcl⇩W_M_level_inv_decomp atms_of_def
dest!: get_all_ann_decomposition_exists_prepend)
ultimately show ?case by blast
next
case (resolve L C M D T) note trail_S = this(1) and confl = this(4) and T = this(7)
let ?T = "update_conflicting (Some (resolve_cls L D C)) (tl_trail S)"
have "?C ?T"
using confl trail_S conf decided by (auto dest!: in_atms_of_minusD)
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 simp
qed
lemma cdcl⇩W_restart_no_strange_atm_inv:
assumes "cdcl⇩W_restart S S'" and "no_strange_atm S" and "cdcl⇩W_M_level_inv S"
shows "no_strange_atm S'"
using cdcl⇩W_restart_no_strange_atm_explicit[OF assms(1)] assms(2,3) unfolding no_strange_atm_def
by fast
lemma rtranclp_cdcl⇩W_restart_no_strange_atm_inv:
assumes "cdcl⇩W_restart⇧*⇧* S S'" and "no_strange_atm S" and "cdcl⇩W_M_level_inv S"
shows "no_strange_atm S'"
using assms by (induction rule: rtranclp_induct)
(auto intro: cdcl⇩W_restart_no_strange_atm_inv rtranclp_cdcl⇩W_restart_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 also. Remark that we will show later
that there cannot be duplicate ∗‹clause›.›
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"
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" and "conflicting S = Some T"
shows "distinct_mset T"
using assms unfolding distinct_cdcl⇩W_state_def by auto
lemma distinct_cdcl⇩W_state_S0_cdcl⇩W_restart[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_restart S S'" and
lev_inv: "cdcl⇩W_M_level_inv S" and
"distinct_cdcl⇩W_state S"
shows "distinct_cdcl⇩W_state S'"
using assms(1,2,2,3)
proof (induct rule: cdcl⇩W_restart_all_induct)
case (backtrack L D K i M1 M2 D')
then show ?case
using lev_inv unfolding distinct_cdcl⇩W_state_def
by (auto dest: get_all_ann_decomposition_incl distinct_mset_mono 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 by auto
next
case resolve
then show ?case
by (auto simp add: distinct_cdcl⇩W_state_def distinct_mset_set_def clauses_def)
qed (auto simp: distinct_cdcl⇩W_state_def distinct_mset_set_def clauses_def
dest!: in_diffD)
lemma rtanclp_distinct_cdcl⇩W_state_inv:
assumes
"cdcl⇩W_restart⇧*⇧* 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_restart_consistent_inv by blast+
subsubsection ‹Conflicts and Annotations›
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 :: "'st ⇒ bool" where
"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 S T :: 'st and D D' :: ‹'v clause› and K L :: ‹'v literal› and i :: nat and
M1 M2:: ‹('v, 'v clause) ann_lits›
assumes
inv: "no_dup (trail S)" and
i: "get_maximum_level (trail S) D' ≡ i" and
decomp: "(Decided K # M1, M2)
∈ set (get_all_ann_decomposition (trail S))" and
S_lvl: "backtrack_lvl S = get_maximum_level (trail S) (add_mset L D')" and
S_confl: "conflicting S = Some D" and
lev_K: "get_level (trail S) K = Suc i" and
T: "T ∼ cons_trail K''
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S)))" and
confl: "∀T. conflicting S = Some T ⟶ trail S ⊨as CNot T" and
D_D': ‹D' ⊆# D›
shows "atms_of D' ⊆ atm_of ` lits_of_l (tl (trail T))"
proof (rule ccontr)
let ?k = "get_maximum_level (trail S) (add_mset L D')"
have "trail S ⊨as CNot D" using confl S_confl by auto
then have "trail S ⊨as CNot D'"
using D_D' by (auto simp: true_annots_true_cls_def_iff_negation_in_model)
then have vars_of_D: "atms_of D' ⊆ atm_of ` lits_of_l (trail S)" unfolding atms_of_def
by (meson image_subsetI true_annots_CNot_all_atms_defined)
obtain M0 where M: "trail S = M0 @ M2 @ Decided K # M1"
using decomp by auto
have max: "?k = count_decided (M0 @ M2 @ Decided K # M1)"
using S_lvl unfolding M by simp
assume a: "¬ ?thesis"
then obtain L' where
L': "L' ∈ atms_of D'" and
L'_notin_M1: "L' ∉ atm_of ` lits_of_l M1"
using T decomp inv by (auto simp: cdcl⇩W_M_level_inv_decomp)
obtain L'' where
"L'' ∈# D'" and
L'': "L' = atm_of L''"
using L' L'_notin_M1 unfolding atms_of_def by auto
then have L'_in: "defined_lit (M0 @ M2 @ Decided K # []) L''"
using vars_of_D L'_notin_M1 L' unfolding M
by (auto dest: in_atms_of_minusD
simp: defined_lit_append defined_lit_map lits_of_def image_Un)
have L''_M1: ‹undefined_lit M1 L''›
using L'_notin_M1 L'' by (auto simp: defined_lit_map lits_of_def)
have ‹undefined_lit (M0 @ M2) K›
using inv by (auto simp: cdcl⇩W_M_level_inv_def M)
then have "count_decided M1 = i"
using lev_K unfolding M by (auto simp: image_Un)
then have lev_L'':
"get_level (trail S) L'' = get_level (M0 @ M2 @ Decided K # []) L'' + i"
using L'_notin_M1 L''_M1 L'' get_level_skip_end[OF L'_in[unfolded L''], of M1] M by auto
moreover {
consider
(M0) "defined_lit M0 L''" |
(M2) "defined_lit M2 L''" |
(K) "L' = atm_of K"
using inv L'_in unfolding L''
by (auto simp: cdcl⇩W_M_level_inv_def defined_lit_append)
then have "get_level (M0 @ M2 @ Decided K # []) L'' ≥ Suc 0"
proof cases
case M0
then have "L' ≠ atm_of K"
using ‹undefined_lit (M0 @ M2) K› unfolding L'' by (auto simp: atm_of_eq_atm_of)
then show ?thesis using M0 unfolding L'' by auto
next
case M2
then have "undefined_lit (M0 @ Decided K # []) L''"
by (rule defined_lit_no_dupD(1))
(use inv in ‹auto simp: M L'' cdcl⇩W_M_level_inv_def no_dup_def›)
then show ?thesis using M2 unfolding L'' by (auto simp: image_Un)
next
case K
have "undefined_lit (M0 @ M2) L''"
by (rule defined_lit_no_dupD(3)[of ‹[Decided K]› _ M1])
(use inv K in ‹auto simp: M L'' cdcl⇩W_M_level_inv_def no_dup_def›)
then show ?thesis using K unfolding L'' by (auto simp: image_Un)
qed }
ultimately have "get_level (trail S) L'' ≥ i + 1"
using lev_L'' unfolding M 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_l M'" and
a3: "x ∈ atms_of D"
shows "x ∉ atm_of ` lits_of_l M"
using assms by (auto simp: atms_of_def no_dup_def atm_of_eq_atm_of lits_of_def)
lemma backtrack_M1_CNot_D':
fixes S T :: 'st and D D' :: ‹'v clause› and K L :: ‹'v literal› and i :: nat and
M1 M2:: ‹('v, 'v clause) ann_lits›
assumes
inv: "no_dup (trail S)" and
i: "get_maximum_level (trail S) D' ≡ i" and
decomp: "(Decided K # M1, M2)
∈ set (get_all_ann_decomposition (trail S))" and
S_lvl: "backtrack_lvl S = get_maximum_level (trail S) (add_mset L D')" and
S_confl: "conflicting S = Some D" and
lev_K: "get_level (trail S) K = Suc i" and
T: "T ∼ cons_trail K''
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S)))" and
confl: "∀T. conflicting S = Some T ⟶ trail S ⊨as CNot T" and
D_D': ‹D' ⊆# D›
shows "M1 ⊨as CNot D'" and
‹atm_of (lit_of K'') = atm_of L ⟹ no_dup (trail T)›
proof -
obtain M0 where M: "trail S = M0 @ M2 @ Decided K # M1"
using decomp by auto
have vars_of_D: "atms_of D' ⊆ atm_of ` lits_of_l M1"
using backtrack_atms_of_D_in_M1[OF assms] decomp T by auto
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_l (M0 @ M2 @ Decided K # [])"
using vars_of_D distinct_atms_of_incl_not_in_other[of "M0 @M2 @ Decided K # []" M1]
unfolding M by auto
have "trail S ⊨as CNot D"
using S_confl confl unfolding M true_annots_true_cls_def_iff_negation_in_model
by (auto dest!: in_diffD)
then have "trail S ⊨as CNot D'"
using D_D' unfolding true_annots_true_cls_def_iff_negation_in_model by auto
then show M1_D': "M1 ⊨as CNot D'"
using true_annots_remove_if_notin_vars[of "M0 @ M2 @ Decided K # []" M1 "CNot D'"]
vars_in_M1 S_confl confl unfolding M lits_of_def by simp
have M1: ‹count_decided M1 = i›
using lev_K inv i vars_in_M1 unfolding M
by simp
have lev_L: ‹get_level (trail S) L = backtrack_lvl S› and ‹i < backtrack_lvl S›
using S_lvl i lev_K
by (auto simp: max_def get_maximum_level_add_mset)
have ‹no_dup M1›
using T decomp inv by (auto simp: M dest: no_dup_appendD)
moreover have ‹undefined_lit M1 L›
using backtrack_lit_skiped[of S L, OF _ decomp]
using lev_L inv i M1 ‹i < backtrack_lvl S› unfolding M
by (auto simp: split: if_splits)
moreover have ‹atm_of (lit_of K'') = atm_of L ⟹
undefined_lit M1 L ⟷ undefined_lit M1 (lit_of K'')›
by (simp add: defined_lit_map)
ultimately show ‹atm_of (lit_of K'') = atm_of L ⟹ no_dup (trail T)›
using T decomp inv by auto
qed
text ‹\cwref{prop:prop:cdclPropLitsUnsat}{Item 5 page 95}›
lemma cdcl⇩W_restart_propagate_is_conclusion:
assumes
"cdcl⇩W_restart S S'" and
inv: "cdcl⇩W_M_level_inv S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_ann_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 (clauses S') (get_all_ann_decomposition (trail S'))"
using assms(1)
proof (induct rule: cdcl⇩W_restart_all_induct)
case restart
then show ?case by auto
next
case (forget C T) note C = this(2) and cls_C = this(6) and T = this(7)
show ?case
unfolding all_decomposition_implies_def Ball_def
proof (intro allI, clarify)
fix a b
assume "(a, b) ∈ set (get_all_ann_decomposition (trail T))"
then have "unmark_l a ∪ set_mset (clauses S) ⊨ps unmark_l b"
using decomp T by (auto simp add: all_decomposition_implies_def)
moreover {
have a1:"C ∈# clauses S"
using C by (auto simp: clauses_def)
have "clauses T = clauses (remove_cls C S)"
using T by auto
then have "clauses T ⊨psm clauses S"
using a1 by (metis (no_types) clauses_remove_cls cls_C insert_Diff order_refl
set_mset_minus_replicate_mset(1) true_clss_clss_def true_clss_clss_insert) }
ultimately show "unmark_l a ∪ set_mset (clauses T) ⊨ps unmark_l b"
using true_clss_clss_generalise_true_clss_clss by blast
qed
next
case conflict
then show ?case using decomp by auto
next
case (resolve L C M D) note tr = this(1) and T = this(7)
let ?decomp = "get_all_ann_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_ann_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_ann_decomposition M)
= insert (hd (get_all_ann_decomposition M)) (set (tl (get_all_ann_decomposition M)))"
by (cases "get_all_ann_decomposition M") auto
show ?case
using decomp tr T unfolding all_decomposition_implies_def
by (cases "hd (get_all_ann_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 L = this(3) and S_CNot_C = this(4) and
undef = this(5) and T = this(6)
obtain a y where ay: "hd (get_all_ann_decomposition (trail S)) = (a, y)"
by (cases "hd (get_all_ann_decomposition (trail S))")
then have M: "trail S = y @ a" using get_all_ann_decomposition_decomp by blast
have M': "set (get_all_ann_decomposition (trail S))
= insert (a, y) (set (tl (get_all_ann_decomposition (trail S))))"
using ay by (cases "get_all_ann_decomposition (trail S)") auto
have unm_ay: "unmark_l a ∪ set_mset (clauses S) ⊨ps unmark_l y"
using decomp ay unfolding all_decomposition_implies_def
by (cases "get_all_ann_decomposition (trail S)") fastforce+
then have a_Un_N_M: "unmark_l a ∪ set_mset (clauses S) ⊨ps unmark_l (trail S)"
unfolding M by (auto simp add: all_in_true_clss_clss image_Un)
have "unmark_l a ∪ set_mset (clauses S) ⊨p {#L#}" (is "?I ⊨p _")
proof (rule true_clss_cls_plus_CNot)
show "?I ⊨p add_mset L (remove1_mset L C)"
apply (rule true_clss_clss_in_imp_true_clss_cls[of _ "set_mset (clauses S)"])
using learned propa L by (auto simp: cdcl⇩W_learned_clause_alt_def true_annot_CNot_diff)
next
have "unmark_l (trail S) ⊨ps CNot (remove1_mset L C)"
using S_CNot_C by (blast dest: true_annots_true_clss_clss)
then show "?I ⊨ps CNot (remove1_mset L 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_ann_decomposition (y @ a)).
unmark_l Ls ∪ set_mset (clauses S) ⊨ps unmark_l seen ⟹
(aa, b) ∈ set (tl (get_all_ann_decomposition (y @ a))) ⟹
unmark_l aa ∪ set_mset (clauses S) ⊨ps unmark_l b"
by (metis (no_types, lifting) case_prod_conv get_all_ann_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 unm_ay ay by auto
next
case (backtrack L D K i M1 M2 T D') note conf = this(1) and decomp' = this(2) and
lev_L = this(3) and lev_K = this(6) and D_D' = this(7) and NU_LD' = this(8)
and T = this(9)
let ?D' = "remove1_mset L D"
have "∀l ∈ set M2. ¬is_decided l"
using get_all_ann_decomposition_snd_not_decided decomp' by blast
obtain M0 where M: "trail S = M0 @ M2 @ Decided K # M1"
using decomp' by auto
let ?D = ‹add_mset L D›
let ?D' = ‹add_mset L D'›
show ?case unfolding all_decomposition_implies_def
proof
fix x
assume "x ∈ set (get_all_ann_decomposition (trail T))"
then have x: "x ∈ set (get_all_ann_decomposition (Propagated L ?D' # M1))"
using T decomp' inv by (simp add: cdcl⇩W_M_level_inv_decomp)
let ?m = "get_all_ann_decomposition (Propagated L ?D' # M1)"
let ?hd = "hd ?m"
let ?tl = "tl ?m"
consider
(hd) "x = ?hd" |
(tl) "x ∈ set ?tl"
using x by (cases "?m") auto
then show "case x of (Ls, seen) ⇒ unmark_l Ls ∪ set_mset (clauses T) ⊨ps unmark_l seen"
proof cases
case tl
then have "x ∈ set (get_all_ann_decomposition (trail S))"
using tl_get_all_ann_decomposition_skip_some[of x] by (simp add: list.set_sel(2) M)
then show ?thesis
using decomp learned decomp confl alien inv T M
unfolding all_decomposition_implies_def cdcl⇩W_M_level_inv_def
by auto
next
case hd
obtain M1' M1'' where M1: "hd (get_all_ann_decomposition M1) = (M1', M1'')"
by (cases "hd (get_all_ann_decomposition M1)")
then have x': "x = (M1', Propagated L ?D' # M1'')"
using ‹x = ?hd› by auto
have "(M1', M1'') ∈ set (get_all_ann_decomposition (trail S))"
using M1[symmetric] hd_get_all_ann_decomposition_skip_some[OF M1[symmetric],
of "M0 @ M2"] unfolding M by fastforce
then have 1: "unmark_l M1' ∪ set_mset (clauses S) ⊨ps unmark_l M1''"
using decomp unfolding all_decomposition_implies_def by auto
have ‹no_dup (trail S)›
using inv unfolding cdcl⇩W_M_level_inv_def
by blast
then have M1_D': "M1 ⊨as CNot D'" and ‹no_dup (trail T)›
using backtrack_M1_CNot_D'[of S D' ‹i› K M1 M2 L ‹add_mset L D› T ‹Propagated L (add_mset L D')›]
confl inv backtrack by (auto simp: subset_mset_trans_add_mset)
have "M1 = M1'' @ M1'" by (simp add: M1 get_all_ann_decomposition_decomp)
have TT: "unmark_l M1' ∪ set_mset (clauses S) ⊨ps CNot D'"
using true_annots_true_clss_cls[OF ‹M1 ⊨as CNot D'›] true_clss_clss_left_right[OF 1]
unfolding ‹M1 = M1'' @ M1'› by (auto simp add: inf_sup_aci(5,7))
have T': "unmark_l M1' ∪ set_mset (clauses S) ⊨p ?D'" using NU_LD' by auto
moreover have "unmark_l M1' ∪ set_mset (clauses S) ⊨p {#L#}"
using true_clss_cls_plus_CNot[OF T' TT] by auto
ultimately show ?thesis
using T' T decomp' inv 1 unfolding x' by (simp add: cdcl⇩W_M_level_inv_decomp)
qed
qed
qed
lemma cdcl⇩W_restart_propagate_is_false:
assumes
"cdcl⇩W_restart S S'" and
lev: "cdcl⇩W_M_level_inv S" and
learned: "cdcl⇩W_learned_clause S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_ann_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)
proof (induct rule: cdcl⇩W_restart_all_induct)
case (propagate C L T) note LC = this(3) and confl = this(4) and undef = this(5) and T = this(6)
show ?case
proof (intro allI impI)
fix L' mark a b
assume "a @ Propagated L' mark # b = trail T"
then consider
(hd) "a = []" and "L = L'" and "mark = C" and "b = trail S" |
(tl) "tl a @ Propagated L' mark # b = trail S"
using T undef by (cases a) fastforce+
then show "b ⊨as CNot (mark - {#L'#}) ∧ L' ∈# mark"
using mark_confl confl LC by cases auto
qed
next
case (decide L) note undef[simp] = this(2) and T = this(4)
have ‹tl a @ Propagated La mark # b = trail S›
if ‹a @ Propagated La mark # b = Decided L # trail S› for a La mark b
using that by (cases 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 ‹b ⊨as CNot (mark - {#La#}) ∧ La ∈# mark›
if "a @ Propagated La mark # b = Propagated L C' # M" for La mark a b
using mark_confl that 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(7)
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#}) # a) @ Propagated L' mark # b
= Propagated L (C + {#L#}) # M"
using T tr_S by auto
then show "b ⊨as CNot (mark - {#L'#}) ∧ L' ∈# mark"
using mark_confl unfolding tr_S by (metis Cons_eq_appendI list.sel(3))
qed
next
case restart
then show ?case by auto
next
case forget
then show ?case using mark_confl by auto
next
case (backtrack L D K i M1 M2 T D') note conf = this(1) and decomp = this(2) and
lev_K = this(6) and D_D' = this(7) and M1_D' = this(8) and T = this(9)
have "∀l ∈ set M2. ¬is_decided l"
using get_all_ann_decomposition_snd_not_decided decomp by blast
obtain M0 where M: "trail S = M0 @ M2 @ Decided K # M1"
using decomp by auto
have [simp]: "trail (reduce_trail_to M1 (add_learned_cls D (update_conflicting None S))) = M1"
using decomp lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
let ?D = "add_mset L D"
let ?D' = "add_mset L D'"
have M1_D': "M1 ⊨as CNot D'"
using backtrack_M1_CNot_D'[of S D' ‹i› K M1 M2 L ‹add_mset L D› T ‹Propagated L (add_mset L D')›]
confl lev backtrack by (auto simp: subset_mset_trans_add_mset cdcl⇩W_M_level_inv_def)
show ?case
proof (intro allI impI)
fix La :: "'v literal" and mark :: "'v clause" and a b :: "('v, 'v clause) ann_lits"
assume "a @ Propagated La mark # b = trail T"
then consider
(hd_tr) "a = []" and
"(Propagated La mark :: ('v, 'v clause) ann_lit) = Propagated L ?D'" and
"b = M1" |
(tl_tr) "tl a @ Propagated La mark # b = M1"
using M T decomp lev by (cases a) (auto simp: cdcl⇩W_M_level_inv_def)
then show "b ⊨as CNot (mark - {#La#}) ∧ La ∈# mark"
proof cases
case hd_tr note A = this(1) and P = this(2) and b = this(3)
show "b ⊨as CNot (mark - {#La#}) ∧ La ∈# mark"
using P M1_D' b by auto
next
case tl_tr
then obtain c' where "c' @ Propagated La mark # b = trail S"
unfolding M by auto
then show "b ⊨as CNot (mark - {#La#}) ∧ La ∈# mark"
using mark_confl by auto
qed
qed
qed
lemma cdcl⇩W_conflicting_is_false:
assumes
"cdcl⇩W_restart 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_restart_all_induct)
case (skip L C' M D T) note tr_S = this(1) and confl = this(2) and L_D = this(3) and T = this(5)
have D: "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_l M"
using in_CNot_implies_uminus(2)[of L D "Propagated L C' # M"]
‹Propagated L C' # M ⊨as CNot D› by simp
then show False
using M_lev tr_S by (fastforce dest: cdcl⇩W_M_level_inv_decomp(2)
simp: Decided_Propagated_in_iff_in_lits_of_l)
qed
ultimately show ?case
using tr_S confl L_D T unfolding cdcl⇩W_M_level_inv_def
by (auto intro: true_annots_CNot_lit_of_notin_skip)
next
case (resolve L C M D T) note tr = this(1) and LC = this(2) and confl = this(4) and LD = this(5)
and T = this(7)
let ?C = "remove1_mset L C"
let ?D = "remove1_mset (-L) D"
show ?case
proof (intro allI impI)
fix T'
have "tl (trail S) ⊨as CNot ?C" using tr decided_confl by fastforce
moreover
have "distinct_mset (?D + {#- L#})" using confl dist LD
unfolding distinct_cdcl⇩W_state_def by auto
then have "-L ∉# ?D" using ‹distinct_mset (?D + {#- L#})› by auto
have "Propagated L (?C + {#L#}) # M ⊨as CNot ?D ∪ CNot {#- L#}"
using confl tr confl_inv LC by (metis CNot_plus LD insert_DiffM2)
then have "M ⊨as CNot ?D"
using M_lev ‹- L ∉# ?D› tr
unfolding cdcl⇩W_M_level_inv_def by (force intro: true_annots_lit_of_notin_skip)
moreover assume "conflicting T = Some T'"
ultimately show "trail T ⊨as CNot T'"
using tr T by auto
qed
qed (auto simp: M_lev 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_S0_cdcl⇩W_restart[simp]:
"cdcl⇩W_conflicting (init_state N)"
unfolding cdcl⇩W_conflicting_def by auto
definition cdcl⇩W_learned_clauses_entailed_by_init where
‹cdcl⇩W_learned_clauses_entailed_by_init S ⟷ init_clss S ⊨psm learned_clss S›
lemma cdcl⇩W_learned_clauses_entailed_init[simp]:
‹cdcl⇩W_learned_clauses_entailed_by_init (init_state N)›
by (auto simp: cdcl⇩W_learned_clauses_entailed_by_init_def)
lemma cdcl⇩W_learned_clauses_entailed:
assumes
cdcl⇩W_restart: "cdcl⇩W_restart S S'" and
2: "cdcl⇩W_learned_clause S" and
9: ‹cdcl⇩W_learned_clauses_entailed_by_init S›
shows ‹cdcl⇩W_learned_clauses_entailed_by_init S'›
using cdcl⇩W_restart 9
proof (induction rule: cdcl⇩W_restart_all_induct)
case backtrack
then show ?case
using assms unfolding cdcl⇩W_learned_clause_alt_def cdcl⇩W_learned_clauses_entailed_by_init_def
by (auto dest!: get_all_ann_decomposition_exists_prepend
simp: clauses_def cdcl⇩W_M_level_inv_decomp dest: true_clss_clss_left_right)
qed (auto simp: cdcl⇩W_learned_clauses_entailed_by_init_def elim: true_clss_clssm_subsetE)
lemma rtranclp_cdcl⇩W_learned_clauses_entailed:
assumes
cdcl⇩W_restart: "cdcl⇩W_restart⇧*⇧* S S'" and
2: "cdcl⇩W_learned_clause S" and
4: "cdcl⇩W_M_level_inv S" and
9: ‹cdcl⇩W_learned_clauses_entailed_by_init S›
shows ‹cdcl⇩W_learned_clauses_entailed_by_init S'›
using assms apply (induction rule: rtranclp_induct)
apply (simp; fail)
using cdcl⇩W_learned_clauses_entailed rtranclp_cdcl⇩W_restart_learned_clss by blast
subsubsection ‹Putting all the Invariants Together›
lemma cdcl⇩W_restart_all_inv:
assumes
cdcl⇩W_restart: "cdcl⇩W_restart S S'" and
1: "all_decomposition_implies_m (clauses S) (get_all_ann_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 (clauses S') (get_all_ann_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 (clauses S') (get_all_ann_decomposition (trail S'))"
using cdcl⇩W_restart_propagate_is_conclusion[OF cdcl⇩W_restart 4 1 2 _ 5] 8
unfolding cdcl⇩W_conflicting_def by blast
show S2: "cdcl⇩W_learned_clause S'" using cdcl⇩W_restart_learned_clss[OF cdcl⇩W_restart 2 4] .
show S4: "cdcl⇩W_M_level_inv S'" using cdcl⇩W_restart_consistent_inv[OF cdcl⇩W_restart 4] .
show S5: "no_strange_atm S'" using cdcl⇩W_restart_no_strange_atm_inv[OF cdcl⇩W_restart 5 4] .
show S7: "distinct_cdcl⇩W_state S'" using distinct_cdcl⇩W_state_inv[OF cdcl⇩W_restart 4 7] .
show S8: "cdcl⇩W_conflicting S'"
using cdcl⇩W_conflicting_is_false[OF cdcl⇩W_restart 4 _ _ 7] 8
cdcl⇩W_restart_propagate_is_false[OF cdcl⇩W_restart 4 2 1 _ 5] unfolding cdcl⇩W_conflicting_def
by fast
qed
lemma rtranclp_cdcl⇩W_restart_all_inv:
assumes
cdcl⇩W_restart: "rtranclp cdcl⇩W_restart S S'" and
1: "all_decomposition_implies_m (clauses S) (get_all_ann_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 (clauses S') (get_all_ann_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_restart_all_inv[OF H(2)]
H by presburger
case 2 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_restart_all_inv[OF H(2)]
H by presburger
case 3 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_restart_all_inv[OF H(2)]
H by presburger
case 4 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_restart_all_inv[OF H(2)]
H by presburger
case 5 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_restart_all_inv[OF H(2)]
H by presburger
case 6 with H(3-7)[OF this(1-6)] show ?case using cdcl⇩W_restart_all_inv[OF H(2)]
H by presburger
qed
lemma all_invariant_S0_cdcl⇩W_restart:
assumes "distinct_mset_mset N"
shows
"all_decomposition_implies_m (init_clss (init_state N))
(get_all_ann_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_l (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
text ‹\cwref{prop:prop:cdclUnsat}{Item 6 page 95}›
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 + U) (get_all_ann_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 + U))"
proof (rule ccontr)
assume "¬ unsatisfiable (set_mset (N + U))"
then obtain I where
I: "I ⊨s set_mset N" "I ⊨s set_mset U" and
cons: "consistent_interp I" and
tot: "total_over_m I (set_mset N)"
unfolding satisfiable_def by auto
have "atms_of_mm N ∪ atms_of_mm U = atms_of_mm N"
using atm_incl state unfolding total_over_m_def no_strange_atm_def
by (auto simp add: clauses_def)
then have tot_N: "total_over_m I (set_mset N)" using tot unfolding total_over_m_def by auto
moreover have "total_over_m I (set_mset (learned_clss S))"
using atm_incl state tot_N unfolding no_strange_atm_def total_over_m_def total_over_set_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 (auto simp add: clauses_def)
have l0: "{unmark L |L. is_decided L ∧ L ∈ set M} = {}" using decided by auto
have "atms_of_ms (set_mset (N+U) ∪ unmark_l M) = atms_of_mm N"
using atm_incl state unfolding no_strange_atm_def by auto
then have "total_over_m I (set_mset (N+U) ∪ unmark_l M)"
using tot unfolding total_over_m_def by auto
then have IM: "I ⊨s unmark_l M"
using all_decomposition_implies_propagated_lits_are_implied[OF inv] cons I
unfolding true_clss_clss_def l0 by auto
have "-K ∈ I" if "K ∈# D" for K
proof -
have "-K ∈ lits_of_l M"
using D that unfolding true_annots_def by force
then show "-K ∈ I" using IM true_clss_singleton_lit_of_implies_incl by fastforce
qed
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 ‹\cwref{prop:prop:cdclPropLitsUnsat}{Item 5 page 95}›
text ‹We have actually a much stronger theorem, namely
@{thm [source] 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_ann_decomposition M)"
and "∀m ∈ set M. ¬is_decided m"
shows "set_mset N ⊨ps unmark_l M"
proof -
have T: "{unmark 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
text ‹\cwref{prop:prop:cdclbacktrack}{Item 7 page 95} (part 1)›
lemma conflict_with_false_implies_unsat:
assumes
cdcl⇩W_restart: "cdcl⇩W_restart S S'" and
lev: "cdcl⇩W_M_level_inv S" and
[simp]: "conflicting S' = Some {#}" and
learned: "cdcl⇩W_learned_clause S" and
learned_entailed: ‹cdcl⇩W_learned_clauses_entailed_by_init S›
shows "unsatisfiable (set_mset (clauses S))"
using assms
proof -
have "cdcl⇩W_learned_clause S'" using cdcl⇩W_restart_learned_clss cdcl⇩W_restart learned lev by auto
then have entail_false: "clauses S' ⊨pm {#}" using assms(3) unfolding cdcl⇩W_learned_clause_alt_def by auto
moreover have entailed: ‹cdcl⇩W_learned_clauses_entailed_by_init S'›
using cdcl⇩W_learned_clauses_entailed[OF cdcl⇩W_restart learned learned_entailed] .
ultimately have "set_mset (init_clss S') ⊨ps {{#}}"
unfolding cdcl⇩W_learned_clauses_entailed_by_init_def
by (auto simp: clauses_def dest: true_clss_clss_left_right)
then have "clauses S ⊨pm {#}"
by (simp add: cdcl⇩W_restart_init_clss[OF assms(1)] clauses_def)
then show ?thesis unfolding satisfiable_def true_clss_cls_def by auto
qed
text ‹\cwref{prop:prop:cdclbacktrack}{Item 7 page 95} (part 2)›
lemma conflict_with_false_implies_terminated:
assumes "cdcl⇩W_restart S S'" and "conflicting S = Some {#}"
shows False
using assms by (induct rule: cdcl⇩W_restart_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_restart 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_restart_all_induct)
case (backtrack L D K i M1 M2 T D') note confl = this(1) and D_D' = this(7) and M1_D' = this(8) and
NU_LD' = this(9)
let ?D = ‹add_mset L D›
let ?D' = ‹add_mset L D'›
have "consistent_interp (lits_of_l (trail S))" using lev by (auto simp: cdcl⇩W_M_level_inv_decomp)
moreover {
have "trail S ⊨as CNot ?D"
using conflicting confl unfolding cdcl⇩W_conflicting_def by auto
then have "lits_of_l (trail S) ⊨s CNot ?D"
using true_annots_true_cls by blast }
ultimately have "¬tautology ?D" using consistent_CNot_not_tautology by blast
then have "¬tautology ?D'"
using D_D' not_tautology_mono[of ?D' ?D] by auto
then show ?case using backtrack no_tauto lev
by (auto simp: cdcl⇩W_M_level_inv_decomp split: if_split_asm)
next
case restart
then show ?case using state_eq_learned_clss no_tauto
by (auto intro: atms_of_ms_learned_clss_restart_state_in_atms_of_ms_learned_clssI)
qed (auto dest!: in_diffD)
definition "final_cdcl⇩W_restart_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_restart_state (S :: 'st)
⟷ (trail S ⊨asm init_clss S
∨ ((∀L ∈ atms_of_mm (init_clss S). L ∈ atm_of ` lits_of_l (trail S))
∧ (∃C ∈# init_clss S. trail S ⊨as CNot C)))"
subsection ‹CDCL Strong Completeness›
lemma cdcl⇩W_restart_can_do_step:
assumes
"consistent_interp (set M)" and
"distinct M" and
"atm_of ` (set M) ⊆ atms_of_mm N"
shows "∃S. rtranclp cdcl⇩W_restart (init_state N) S
∧ state_butlast S = (map (λL. Decided L) M, N, {#}, None)"
using assms
proof (induct M)
case Nil
then show ?case apply - by (auto intro!: exI[of _ "init_state N"])
next
case (Cons L M) note IH = this(1) and dist = this(2)
have "consistent_interp (set M)" and "distinct M" and "atm_of ` set M ⊆ atms_of_mm N"
using Cons.prems(1-3) unfolding consistent_interp_def by auto
then obtain S where
st: "cdcl⇩W_restart⇧*⇧* (init_state N) S" and
S: "state_butlast S = (map (λL. Decided L) M, N, {#}, None)"
using IH by blast
let ?S⇩0 = "cons_trail (Decided L) S"
have undef: "undefined_lit (map (λL. Decided L) 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_mm N" using Cons.prems(3) by auto
moreover have undef: "undefined_lit (trail S) L"
using S dist undef by (auto simp: defined_lit_map)
ultimately have "cdcl⇩W_restart S ?S⇩0"
using cdcl⇩W_restart.other[OF cdcl⇩W_o.decide[OF decide_rule[of S L ?S⇩0]]] S
by auto
then have "cdcl⇩W_restart⇧*⇧* (init_state N) ?S⇩0"
using st by auto
then show ?case
using S undef by (auto intro!: exI[of _ ?S⇩0] simp del: state_prop)
qed
text ‹\cwref{cdcl:completeness}{theorem 2.9.11 page 98}›
lemma cdcl⇩W_restart_strong_completeness:
assumes
MN: "set M ⊨sm N" and
cons: "consistent_interp (set M)" and
dist: "distinct M" and
atm: "atm_of ` (set M) ⊆ atms_of_mm N"
obtains S where
"state_butlast S = (map (λL. Decided L) M, N, {#}, None)" and
"rtranclp cdcl⇩W_restart (init_state N) S" and
"final_cdcl⇩W_restart_state S"
proof -
obtain S where
st: "rtranclp cdcl⇩W_restart (init_state N) S" and
S: "state_butlast S = (map (λL. Decided L) M, N, {#}, None)"
using cdcl⇩W_restart_can_do_step[OF cons dist atm] by auto
have "lits_of_l (map (λL. Decided L) M) = set M"
by (induct M, auto)
then have "map (λL. Decided L) M ⊨asm N" using MN true_annots_true_cls by metis
then have "final_cdcl⇩W_restart_state S"
using S unfolding final_cdcl⇩W_restart_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 necessary lead to a conclusive state. We have to add a
strategy:
▪ do propagate and conflict when possible;
▪ otherwise, do another rule (except forget and restart).›
subsubsection ‹Definition›
lemma tranclp_conflict:
"tranclp conflict S S' ⟹ conflict S S'"
by (induct rule: tranclp.induct) (auto elim!: conflictE)
lemma no_chained_conflict:
assumes "conflict S S'" and "conflict S' S''"
shows False
using assms unfolding conflict.simps
by (metis conflicting_update_conflicting option.distinct(1) state_eq_conflicting)
lemma tranclp_conflict_iff:
"full1 conflict S S' ⟷ conflict S S'"
by (auto simp: full1_def dest: tranclp_conflict no_chained_conflict)
lemma no_conflict_after_conflict:
"conflict S T ⟹ ¬conflict T U"
by (auto elim!: conflictE simp: conflict.simps)
lemma no_propagate_after_conflict:
"conflict S T ⟹ ¬propagate T U"
by (metis conflictE conflicting_update_conflicting option.distinct(1) propagate.cases
state_eq_conflicting)
inductive cdcl⇩W_stgy :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
conflict': "conflict S S' ⟹ cdcl⇩W_stgy S S'" |
propagate': "propagate S S' ⟹ cdcl⇩W_stgy S S'" |
other': "no_step conflict S ⟹ no_step propagate S ⟹ cdcl⇩W_o S S' ⟹ cdcl⇩W_stgy S S'"
lemma cdcl⇩W_stgy_cdcl⇩W: "cdcl⇩W_stgy S T ⟹ cdcl⇩W S T"
by (induction rule: cdcl⇩W_stgy.induct) (auto intro: cdcl⇩W.intros)
lemma cdcl⇩W_stgy_induct[consumes 1, case_names conflict propagate decide skip resolve backtrack]:
assumes
‹cdcl⇩W_stgy S T› and
‹⋀T. conflict S T ⟹ P T› and
‹⋀T. propagate S T ⟹ P T› and
‹⋀T. no_step conflict S ⟹ no_step propagate S ⟹ decide S T ⟹ P T› and
‹⋀T. no_step conflict S ⟹ no_step propagate S ⟹ skip S T ⟹ P T› and
‹⋀T. no_step conflict S ⟹ no_step propagate S ⟹ resolve S T ⟹ P T› and
‹⋀T. no_step conflict S ⟹ no_step propagate S ⟹ backtrack S T ⟹ P T›
shows
‹P T›
using assms(1) by (induction rule: cdcl⇩W_stgy.induct)
(auto simp: assms(2-) cdcl⇩W_o.simps cdcl⇩W_bj.simps)
lemma cdcl⇩W_stgy_cases[consumes 1, case_names conflict propagate decide skip resolve backtrack]:
assumes
‹cdcl⇩W_stgy S T› and
‹conflict S T ⟹ P› and
‹propagate S T ⟹ P› and
‹no_step conflict S ⟹ no_step propagate S ⟹ decide S T ⟹ P› and
‹no_step conflict S ⟹ no_step propagate S ⟹ skip S T ⟹ P› and
‹no_step conflict S ⟹ no_step propagate S ⟹ resolve S T ⟹ P› and
‹no_step conflict S ⟹ no_step propagate S ⟹ backtrack S T ⟹ P›
shows
‹P›
using assms(1) by (cases rule: cdcl⇩W_stgy.cases)
(auto simp: assms(2-) cdcl⇩W_o.simps cdcl⇩W_bj.simps)
subsubsection ‹Invariants›
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 by (induct rule: cdcl⇩W_stgy.induct) (blast intro: cdcl⇩W_restart_consistent_inv
cdcl⇩W_restart.intros)+
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_stgy_no_more_init_clss:
assumes "cdcl⇩W_stgy S S'"
shows "init_clss S = init_clss S'"
using assms cdcl⇩W_cdcl⇩W_restart cdcl⇩W_restart_init_clss cdcl⇩W_stgy_cdcl⇩W by blast
lemma rtranclp_cdcl⇩W_stgy_no_more_init_clss:
assumes "cdcl⇩W_stgy⇧*⇧* S 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)
subsubsection ‹Literal of highest level in conflicting clauses›
text ‹One important property of the @{term cdcl⇩W_restart} with strategy is that, whenever a conflict
takes place, there is at least a literal of level @{term k} involved (except if we have derived
the false clause). The reason is that we apply conflicts before a decision is taken.›
definition 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)"
declare conflict_is_false_with_level_def[simp]
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 = count_decided M1)"
lemma backtrack⇩W_rule:
assumes
confl: ‹conflicting S = Some (add_mset L D)› and
decomp: ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and
lev_L: ‹get_level (trail S) L = backtrack_lvl S› and
max_lev: ‹get_level (trail S) L = get_maximum_level (trail S) (add_mset L D)› and
max_D: ‹get_maximum_level (trail S) D ≡ i› and
lev_K: ‹get_level (trail S) K = i + 1› and
T: ‹T ∼ cons_trail (Propagated L (add_mset L D))
(reduce_trail_to M1
(add_learned_cls (add_mset L D)
(update_conflicting None S)))› and
lev_inv: "cdcl⇩W_M_level_inv S" and
conf: ‹cdcl⇩W_conflicting S› and
learned: ‹cdcl⇩W_learned_clause S›
shows ‹backtrack S T›
using confl decomp lev_L max_lev max_D lev_K
proof (rule backtrack_rule)
let ?i = "get_maximum_level (trail S) D"
let ?D = ‹add_mset L D›
show ‹D ⊆# D›
by simp
obtain M3 where
M3: ‹trail S = M3 @ M2 @ Decided K # M1›
using decomp by auto
have trail_S_D: ‹trail S ⊨as CNot ?D›
using conf confl unfolding cdcl⇩W_conflicting_def by auto
then have atms_E_M1: ‹atms_of D ⊆ atm_of ` lits_of_l M1›
using backtrack_atms_of_D_in_M1[OF _ _ decomp, of D ?i L ?D
‹cons_trail (Propagated L ?D) (reduce_trail_to M1 (add_learned_cls ?D (update_conflicting None S)))›
‹Propagated L (add_mset L D)›]
conf lev_K decomp max_lev lev_L confl T max_D lev_inv unfolding cdcl⇩W_M_level_inv_def
by auto
have n_d: ‹no_dup (M3 @ M2 @ Decided K # M1)›
using lev_inv no_dup_rev[of ‹rev M1 @ rev M2 @ rev M3›, unfolded rev_append]
by (auto simp: cdcl⇩W_M_level_inv_def M3)
then have n_d': ‹no_dup (M3 @ M2 @ M1)›
by auto
have atm_L_M1: ‹atm_of L ∉ atm_of ` lits_of_l M1›
using lev_L n_d defined_lit_no_dupD(2-3)[of M1 L M3 M2] count_decided_ge_get_level[of ‹Decided K # M1› L]
unfolding M3
by (auto simp: atm_of_eq_atm_of Decided_Propagated_in_iff_in_lits_of_l get_level_cons_if split: if_splits)
have ‹La ≠ L›‹- La ∉ lits_of_l M3› ‹- La ∉ lits_of_l M2› ‹-La ≠K› if ‹La∈#D› for La
proof -
have ‹-La ∈ lits_of_l (trail S)›
using trail_S_D that by (auto simp: true_annots_true_cls_def_iff_negation_in_model
dest!: get_all_ann_decomposition_exists_prepend)
moreover have ‹defined_lit M1 La›
using atms_E_M1 that by (auto simp: Decided_Propagated_in_iff_in_lits_of_l atms_of_def
dest!: atm_of_in_atm_of_set_in_uminus)
moreover have n_d': ‹no_dup (rev M1 @ rev M2 @ rev M3)›
by (rule same_mset_no_dup_iff[THEN iffD1, OF _ n_d']) auto
moreover have ‹no_dup (rev M3 @ rev M2 @ rev M1)›
by (rule same_mset_no_dup_iff[THEN iffD1, OF _ n_d']) auto
ultimately show ‹La ≠ L›‹- La ∉ lits_of_l M3› ‹- La ∉ lits_of_l M2› ‹-La ≠ K›
using defined_lit_no_dupD(2-3)[of ‹rev M1› La ‹rev M3› ‹rev M2›]
defined_lit_no_dupD(1)[of ‹rev M1› La ‹rev M3 @ rev M2›] atm_L_M1 n_d
by (auto simp: M3 Decided_Propagated_in_iff_in_lits_of_l atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set)
qed
show ‹clauses S ⊨pm add_mset L D›
using cdcl⇩W_learned_clause_alt_def confl learned by blast
show ‹T ∼ cons_trail (Propagated L (add_mset L D)) (reduce_trail_to M1 (add_learned_cls (add_mset L D) (update_conflicting None S)))›
using T by blast
qed
lemma backtrack_no_decomp:
assumes
S: "conflicting S = Some (add_mset L E)" and
L: "get_level (trail S) L = backtrack_lvl S" and
D: "get_maximum_level (trail S) E < backtrack_lvl S" and
bt: "backtrack_lvl S = get_maximum_level (trail S) (add_mset L E)" and
lev_inv: "cdcl⇩W_M_level_inv S" and
conf: ‹cdcl⇩W_conflicting S› and
learned: ‹cdcl⇩W_learned_clause S›
shows "∃S'. cdcl⇩W_o S S'" "∃S'. backtrack S S'"
proof -
have L_D: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L E)"
using L D bt by (simp add: get_maximum_level_plus)
let ?i = "get_maximum_level (trail S) E"
let ?D = ‹add_mset L E›
obtain K M1 M2 where
K: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
lev_K: "get_level (trail S) K = ?i + 1"
using backtrack_ex_decomp[of S ?i] D S lev_inv
unfolding cdcl⇩W_M_level_inv_def by auto
show ‹Ex (backtrack S)›
using backtrack⇩W_rule[OF S K L L_D _ lev_K] lev_inv conf learned by auto
then show ‹Ex (cdcl⇩W_o S)›
using bj by (auto simp: cdcl⇩W_bj.simps)
qed
lemma no_analyse_backtrack_Ex_simple_backtrack:
assumes
bt: ‹backtrack S T› and
lev_inv: "cdcl⇩W_M_level_inv S" and
conf: ‹cdcl⇩W_conflicting S› and
learned: ‹cdcl⇩W_learned_clause S› and
no_dup: ‹distinct_cdcl⇩W_state S› and
ns_s: ‹no_step skip S› and
ns_r: ‹no_step resolve S›
shows ‹Ex(simple_backtrack S)›
proof -
obtain D L K i M1 M2 D' where
confl: "conflicting S = Some (add_mset L D)" and
decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
lev: "get_level (trail S) L = backtrack_lvl S" and
max: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
max_D: "get_maximum_level (trail S) D' ≡ i" and
lev_K: "get_level (trail S) K = Suc i" and
D'_D: ‹D' ⊆# D› and
NU_DL: ‹clauses S ⊨pm add_mset L D'› and
T: "T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S)))"
using bt by (elim backtrackE) metis
have n_d: ‹no_dup (trail S)›
using lev_inv unfolding cdcl⇩W_M_level_inv_def by auto
have trail_S_Nil: ‹trail S ≠ []›
using decomp by auto
then have hd_in_annot: ‹lit_of (hd_trail S) ∈# mark_of (hd_trail S)› if ‹is_proped (hd_trail S)›
using conf that unfolding cdcl⇩W_conflicting_def
by (cases ‹trail S›; cases ‹hd (trail S)›) fastforce+
have max_D_L_hd: ‹get_maximum_level (trail S) D < get_level (trail S) L ∧ L = -lit_of (hd_trail S)›
proof cases
assume is_p: ‹is_proped (hd (trail S))›
then have ‹-lit_of (hd (trail S)) ∈# add_mset L D›
using ns_s trail_S_Nil confl skip_rule[of S ‹lit_of (hd (trail S))› _ _ ‹add_mset L D›]
by (cases ‹trail S›; cases ‹hd (trail S)›) auto
then have ‹get_maximum_level (trail S) (remove1_mset (- lit_of (hd_trail S)) (add_mset L D)) ≠ backtrack_lvl S›
using ns_r trail_S_Nil confl resolve_rule[of S ‹lit_of (hd (trail S))› ‹mark_of (hd_trail S)› ‹add_mset L D›] is_p
hd_in_annot
by (cases ‹trail S›; cases ‹hd (trail S)›) auto
then have lev_L_D: ‹get_maximum_level (trail S) (remove1_mset (- lit_of (hd_trail S)) (add_mset L D)) <
backtrack_lvl S›
using count_decided_ge_get_maximum_level[of ‹trail S› ‹remove1_mset (- lit_of (hd_trail S)) (add_mset L D)›]
by auto
then have ‹L = -lit_of (hd_trail S)›
using get_maximum_level_ge_get_level[of L ‹remove1_mset (- lit_of (hd_trail S)) (add_mset L D)›
‹trail S›] lev apply -
by (rule ccontr) auto
then show ?thesis
using lev_L_D lev by auto
next
assume is_p: ‹¬ is_proped (hd (trail S))›
obtain L' where
L': ‹L' ∈# add_mset L D› and
lev_L': ‹get_level (trail S) L' = backtrack_lvl S›
using lev by auto
moreover have uL'_trail: ‹-L' ∈ lits_of_l (trail S)›
using conf confl L' unfolding cdcl⇩W_conflicting_def true_annots_true_cls_def_iff_negation_in_model
by auto
moreover have ‹L' ∉ lits_of_l (trail S)›
using n_d uL'_trail by (blast dest: no_dup_consistentD)
ultimately have L'_hd: ‹L' = -lit_of (hd_trail S)›
using is_p trail_S_Nil by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: get_level_cons_if atm_of_eq_atm_of
split: if_splits)
have ‹distinct_mset (add_mset L D)›
using no_dup confl unfolding distinct_cdcl⇩W_state_def by auto
then have ‹L' ∉# remove1_mset L' (add_mset L D)›
using L' by (meson distinct_mem_diff_mset multi_member_last)
moreover have ‹-L' ∉# add_mset L D›
proof (rule ccontr)
assume ‹¬ ?thesis›
then have ‹L' ∈ lits_of_l (trail S)›
using conf confl trail_S_Nil unfolding cdcl⇩W_conflicting_def true_annots_true_cls_def_iff_negation_in_model
by auto
then show False
using n_d L'_hd by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: Decided_Propagated_in_iff_in_lits_of_l)
qed
ultimately have ‹atm_of (lit_of (Decided (- L'))) ∉ atms_of (remove1_mset L' (add_mset L D))›
using ‹- L' ∉# add_mset L D› by (auto simp: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
atms_of_def dest: in_diffD)
then have ‹get_maximum_level (Decided (-L') # tl (trail S)) (remove1_mset L' (add_mset L D)) =
get_maximum_level (tl (trail S)) (remove1_mset L' (add_mset L D))›
by (rule get_maximum_level_skip_first)
also have ‹get_maximum_level (tl (trail S)) (remove1_mset L' (add_mset L D)) < backtrack_lvl S›
using count_decided_ge_get_maximum_level[of ‹tl (trail S)› ‹remove1_mset L' (add_mset L D)›]
trail_S_Nil is_p by (cases ‹trail S›; cases ‹hd (trail S)›) auto
finally have lev_L'_L: ‹get_maximum_level (trail S) (remove1_mset L' (add_mset L D)) < backtrack_lvl S›
using trail_S_Nil is_p L'_hd by (cases ‹trail S›; cases ‹hd (trail S)›) auto
then have ‹L = L'›
using get_maximum_level_ge_get_level[of L ‹remove1_mset L' (add_mset L D)›
‹trail S›] L' lev_L' lev by auto
then show ?thesis
using lev_L'_L lev L'_hd by auto
qed
let ?i = ‹get_maximum_level (trail S) D›
obtain K' M1' M2' where
decomp': ‹(Decided K' # M1', M2') ∈ set (get_all_ann_decomposition (trail S))› and
lev_K': ‹get_level (trail S) K' = Suc ?i›
using backtrack_ex_decomp[of S ?i] lev_inv max_D_L_hd
unfolding lev cdcl⇩W_M_level_inv_def by blast
show ?thesis
apply standard
apply (rule simple_backtrack_rule[of S L D K' M1' M2' ‹get_maximum_level (trail S) D›
‹cons_trail (Propagated L (add_mset L D)) (reduce_trail_to M1' (add_learned_cls (add_mset L D) (update_conflicting None S)))›])
subgoal using confl by auto
subgoal using decomp' by auto
subgoal using lev .
subgoal using count_decided_ge_get_maximum_level[of ‹trail S› D] lev
by (auto simp: get_maximum_level_add_mset)
subgoal .
subgoal using lev_K' by simp
subgoal by simp
done
qed
lemma trail_begins_with_decided_conflicting_exists_backtrack:
assumes
confl_k: ‹conflict_is_false_with_level S› and
conf: ‹cdcl⇩W_conflicting S› and
level_inv: ‹cdcl⇩W_M_level_inv S› and
no_dup: ‹distinct_cdcl⇩W_state S› and
learned: ‹cdcl⇩W_learned_clause S› and
alien: ‹no_strange_atm S› and
tr_ne: ‹trail S ≠ []› and
L': ‹hd_trail S = Decided L'› and
nempty: ‹C ≠ {#}› and
confl: ‹conflicting S = Some C›
shows ‹Ex (backtrack S)› and ‹no_step skip S› and ‹no_step resolve S›
proof -
let ?M = "trail S"
let ?N = "init_clss S"
let ?k = "backtrack_lvl S"
let ?U = "learned_clss S"
obtain L D where
E'[simp]: "C = D + {#L#}" and
lev_L: "get_level ?M L = ?k"
using nempty confl by (metis (mono_tags) confl_k insert_DiffM2 conflict_is_false_with_level_def)
let ?D = "D + {#L#}"
have "?D ≠ {#}" by auto
have "?M ⊨as CNot ?D" using confl conf unfolding cdcl⇩W_conflicting_def by auto
then have "?M ≠ []" unfolding true_annots_def Ball_def true_annot_def true_cls_def by force
define M' where M': ‹M' = tl ?M›
have M: "?M = hd ?M # M'" using ‹?M ≠ []› list.collapse M' by fastforce
obtain k' where k': "k' + 1 = ?k"
using level_inv tr_ne L' unfolding cdcl⇩W_M_level_inv_def by (cases "trail S") auto
have n_s: "no_step conflict S" "no_step propagate S"
using confl by (auto elim!: conflictE propagateE)
have g_k: "get_maximum_level (trail S) D ≤ ?k"
using count_decided_ge_get_maximum_level[of ?M] level_inv unfolding cdcl⇩W_M_level_inv_def
by auto
have L'_L: "L' = -L"
proof (rule ccontr)
assume "¬ ?thesis"
moreover {
have "-L ∈ lits_of_l ?M"
using confl conf unfolding cdcl⇩W_conflicting_def by auto
then have ‹atm_of L ≠ atm_of L'›
using cdcl⇩W_M_level_inv_decomp(2)[OF level_inv] M calculation L'
by (auto simp: atm_of_eq_atm_of all_conj_distrib uminus_lit_swap lits_of_def no_dup_def) }
ultimately have "get_level (hd (trail S) # M') L = get_level (tl ?M) L"
using cdcl⇩W_M_level_inv_decomp(1)[OF level_inv] M unfolding consistent_interp_def
by (simp add: atm_of_eq_atm_of L' M'[symmetric])
moreover {
have "count_decided (trail S) = ?k"
using level_inv unfolding cdcl⇩W_M_level_inv_def by auto
then have count: "count_decided M' = ?k - 1"
using level_inv M by (auto simp add: L' M'[symmetric])
then have "get_level (tl ?M) L < ?k"
using count_decided_ge_get_level[of M' L] unfolding k'[symmetric] M' by auto }
finally show False using lev_L M unfolding M' by auto
qed
then have L: "hd ?M = Decided (-L)" using L' by auto
have H: "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 confl
by (metis E' add_diff_cancel_right' distinct_mem_diff_mset union_commute 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 "get_level (tl (trail S)) L = 0"
using level_inv L' M unfolding cdcl⇩W_M_level_inv_def
by (auto simp: image_iff L' L'_L)
moreover {
have ‹backtrack_lvl S = count_decided (hd ?M # tl ?M)›
unfolding M[symmetric] M'[symmetric] ..
then have "get_level (tl (trail S)) L'' < backtrack_lvl S"
using count_decided_ge_get_level[of ‹tl (trail S)› L'']
by (auto simp: image_iff L' L'_L) }
ultimately show False
using M[unfolded L' M'[symmetric]] L_k by (auto simp: L' L'_L)
qed
then have taut: "tautology (D + {#L#})"
using ‹L'' ∈# D› by (metis add.commute mset_subset_eqD mset_subset_eq_add_left
multi_member_this tautology_minus)
moreover have "consistent_interp (lits_of_l ?M)"
using level_inv unfolding cdcl⇩W_M_level_inv_def by auto
ultimately have "¬?M ⊨as CNot ?D"
by (metis ‹L'' = - L› ‹L'' ∈# D› add.commute consistent_interp_def
diff_union_cancelR in_CNot_implies_uminus(2) in_diffD multi_member_this)
moreover have "?M ⊨as CNot ?D"
using confl no_dup conf unfolding cdcl⇩W_conflicting_def by auto
ultimately show False by blast
qed
have confl_D: ‹conflicting S = Some (add_mset L D)›
using confl[unfolded E'] by simp
have "get_maximum_level (trail S) D < get_maximum_level (trail S) (add_mset L D)"
using H by (auto simp: get_maximum_level_plus lev_L max_def get_maximum_level_add_mset)
moreover have "backtrack_lvl S = get_maximum_level (trail S) (add_mset L D)"
using H by (auto simp: get_maximum_level_plus lev_L max_def get_maximum_level_add_mset)
ultimately show ‹Ex (backtrack S)›
using backtrack_no_decomp[OF confl_D _ ] level_inv alien conf learned
by (auto simp add: lev_L max_def n_s)
show ‹no_step resolve S›
using L by (auto elim!: resolveE)
show ‹no_step skip S›
using L by (auto elim!: skipE)
qed
lemma conflicting_no_false_can_do_step:
assumes
confl: ‹conflicting S = Some C› and
nempty: ‹C ≠ {#}› and
confl_k: ‹conflict_is_false_with_level S› and
conf: ‹cdcl⇩W_conflicting S› and
level_inv: ‹cdcl⇩W_M_level_inv S› and
no_dup: ‹distinct_cdcl⇩W_state S› and
learned: ‹cdcl⇩W_learned_clause S› and
alien: ‹no_strange_atm S› and
termi: ‹no_step cdcl⇩W_stgy S›
shows False
proof -
let ?M = "trail S"
let ?N = "init_clss S"
let ?k = "backtrack_lvl S"
let ?U = "learned_clss S"
define M' where ‹M' = tl ?M›
obtain L D where
E'[simp]: "C = D + {#L#}" and
lev_L: "get_level ?M L = ?k"
using nempty confl by (metis (mono_tags) confl_k insert_DiffM2 conflict_is_false_with_level_def)
let ?D = "D + {#L#}"
have "?D ≠ {#}" by auto
have "?M ⊨as CNot ?D" using confl conf 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 ≠ []› by fastforce
then have M: "?M = hd ?M # M'" unfolding M'_def .
have n_s: "no_step conflict S" "no_step propagate S"
using termi by (blast intro: cdcl⇩W_stgy.intros)+
have ‹no_step backtrack S›
using termi by (blast intro: cdcl⇩W_stgy.intros cdcl⇩W_o.intros cdcl⇩W_bj.intros)
then have not_is_decided: "¬ is_decided (hd ?M)"
using trail_begins_with_decided_conflicting_exists_backtrack(1)[OF confl_k conf level_inv no_dup
learned alien ‹?M ≠ []› _ nempty confl] by (cases ‹hd_trail S›) (auto)
have g_k: "get_maximum_level (trail S) D ≤ ?k"
using count_decided_ge_get_maximum_level[of ?M] level_inv unfolding cdcl⇩W_M_level_inv_def
by auto
let ?D = "add_mset L D"
have "?D ≠ {#}" by auto
have "?M ⊨as CNot ?D" using confl conf unfolding cdcl⇩W_conflicting_def by auto
then have "?M ≠ []" unfolding true_annots_def Ball_def true_annot_def true_cls_def by force
then obtain L' C where L'C: "hd_trail S = Propagated L' C"
using not_is_decided by (cases "hd_trail S") auto
then have "hd ?M = Propagated L' C"
using ‹?M ≠ []› by fastforce
then have M: "?M = Propagated L' C # M'" using M by simp
then have M': "?M = Propagated L' C # tl ?M" using M by simp
then obtain C' where C': "C = add_mset L' C'"
using conf M unfolding cdcl⇩W_conflicting_def by (metis append_Nil diff_single_eq_union)
have L'D: "-L' ∈# ?D"
using n_s alien level_inv termi skip_rule[OF M' confl]
by (auto dest: other' cdcl⇩W_o.intros cdcl⇩W_bj.intros)
obtain D' where D': "?D = add_mset (-L') D'" using L'D by (metis insert_DiffM)
then have "get_maximum_level (trail S) D' ≤ ?k"
using count_decided_ge_get_maximum_level[of "Propagated L' C # tl ?M"] M
level_inv unfolding cdcl⇩W_M_level_inv_def by auto
then consider
(D'_max_lvl) "get_maximum_level (trail S) D' = ?k" |
(D'_le_max_lvl) "get_maximum_level (trail S) D' < ?k"
using le_neq_implies_less by blast
then show False
proof cases
case g_D'_k: D'_max_lvl
then have f1: "get_maximum_level (trail S) D' = backtrack_lvl S"
using M by auto
then have "Ex (cdcl⇩W_o S)"
using resolve_rule[of S L' C , OF ‹trail S ≠ []› _ _ confl] conf
L'C L'D D' C' by (auto dest: cdcl⇩W_o.intros cdcl⇩W_bj.intros)
then show False
using n_s termi by (auto dest: other' cdcl⇩W_o.intros cdcl⇩W_bj.intros)
next
case a1: D'_le_max_lvl
then have f3: "get_maximum_level (trail S) D' < get_level (trail S) (-L')"
using a1 lev_L D' by (metis D' get_maximum_level_ge_get_level insert_noteq_member
not_less)
moreover have "get_level (trail S) L' = get_maximum_level (trail S) (D' + {#- L'#})"
using a1 by (auto simp add: get_maximum_level_add_mset max_def M)
ultimately show False
using M backtrack_no_decomp[of S "-L'" D'] confl level_inv n_s termi E' learned conf
by (auto simp: D' dest: other' cdcl⇩W_o.intros cdcl⇩W_bj.intros)
qed
qed
lemma cdcl⇩W_stgy_final_state_conclusive2:
assumes
termi: "no_step cdcl⇩W_stgy S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_ann_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 (clauses S)))
∨ (conflicting S = None ∧ trail S ⊨as set_mset (clauses S))"
proof -
let ?M = "trail S"
let ?N = "clauses S"
let ?k = "backtrack_lvl S"
let ?U = "learned_clss S"
consider
(None) "conflicting S = None"
| (Some_Empty) E where "conflicting S = Some E" and "E = {#}"
using conflicting_no_false_can_do_step[of S, OF _ _ confl_k confl level_inv no_dup learned alien] termi
by (cases "conflicting S", simp) auto
then show ?thesis
proof cases
case (Some_Empty E)
then have "conflicting S = Some {#}" by auto
then have unsat_clss_S: "unsatisfiable (set_mset (clauses S))"
using learned unfolding cdcl⇩W_learned_clause_alt_def true_clss_cls_def
conflict_is_false_with_level_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)
then show ?thesis using Some_Empty by (auto simp: clauses_def)
next
case None
have "?M ⊨asm ?N"
proof (rule ccontr)
assume MN: "¬ ?thesis"
have all_defined: "atm_of ` (lits_of_l ?M) = atms_of_mm ?N" (is "?A = ?B")
proof
show "?A ⊆ ?B" using alien unfolding no_strange_atm_def clauses_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[of S] decide_rule[of S ‹Pos l› ‹cons_trail (Decided (Pos l)) S›]
‹l ∈ ?B› None alien unfolding clauses_def no_strange_atm_def by fastforce
then show False
using termi by (blast intro: cdcl⇩W_stgy.intros)
qed
qed
obtain D where "¬ ?M ⊨a D" and "D ∈# ?N"
using MN unfolding lits_of_def true_annots_def Ball_def by auto
have "atms_of D ⊆ atm_of ` (lits_of_l ?M)"
using ‹D ∈# ?N› unfolding all_defined atms_of_ms_def by auto
then have "total_over_m (lits_of_l ?M) {D}"
using 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 ‹¬ trail S ⊨a D› unfolding true_annot_def true_annots_true_cls
by (fastforce simp: total_not_true_cls_true_clss_CNot)
then have "∃S'. conflict S S'"
using ‹trail S ⊨as CNot D› ‹D ∈# clauses S›
None unfolding clauses_def by (auto simp: conflict.simps clauses_def)
then show False
using termi by (blast intro: cdcl⇩W_stgy.intros)
qed
then show ?thesis
using None by auto
qed
qed
lemma cdcl⇩W_stgy_final_state_conclusive:
assumes
termi: "no_step cdcl⇩W_stgy S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_ann_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" and
learned_entailed: ‹cdcl⇩W_learned_clauses_entailed_by_init 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"
consider
(None) "conflicting S = None" |
(Some_Empty) E where "conflicting S = Some E" and "E = {#}"
using conflicting_no_false_can_do_step[of S, OF _ _ confl_k confl level_inv no_dup learned alien] termi
by (cases "conflicting S", simp) auto
then show ?thesis
proof cases
case (Some_Empty E)
then have "conflicting S = Some {#}" by auto
then have unsat_clss_S: "unsatisfiable (set_mset (clauses S))"
using learned learned_entailed unfolding cdcl⇩W_learned_clause_alt_def true_clss_cls_def
conflict_is_false_with_level_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)
then have "unsatisfiable (set_mset (init_clss S))"
proof -
have "atms_of_mm (learned_clss S) ⊆ atms_of_mm (init_clss S)"
using alien no_strange_atm_decomp(3) by blast
then have f3: "atms_of_ms (set_mset (init_clss S) ∪ set_mset (learned_clss S)) =
atms_of_mm (init_clss S)"
by auto
have "init_clss S ⊨psm learned_clss S"
using learned_entailed
unfolding cdcl⇩W_learned_clause_alt_def cdcl⇩W_learned_clauses_entailed_by_init_def by blast
then show ?thesis
using f3 unsat_clss_S
unfolding true_clss_clss_def total_over_m_def clauses_def satisfiable_def
by (metis (no_types) set_mset_union true_clss_union)
qed
then show ?thesis using Some_Empty by auto
next
case None
have "?M ⊨asm ?N"
proof (rule ccontr)
assume MN: "¬ ?thesis"
have all_defined: "atm_of ` (lits_of_l ?M) = atms_of_mm ?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_rule ‹l ∈ ?B› no_strange_atm_def None
by (metis literal.sel(1) state_eq_ref)
then show False
using termi by (blast intro: cdcl⇩W_stgy.intros)
qed
qed
obtain D where "¬ ?M ⊨a D" and "D ∈# ?N"
using MN unfolding lits_of_def true_annots_def Ball_def by auto
have "atms_of D ⊆ atm_of ` (lits_of_l ?M)"
using ‹D ∈# ?N› unfolding all_defined atms_of_ms_def by auto
then have "total_over_m (lits_of_l ?M) {D}"
using atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
by (fastforce simp: total_over_set_def)
then have M_CNot_D: "?M ⊨as CNot D"
using ‹¬ trail S ⊨a D› unfolding true_annot_def true_annots_true_cls
by (fastforce simp: total_not_true_cls_true_clss_CNot)
then have "∃S'. conflict S S'"
using M_CNot_D ‹D ∈# init_clss S›
None unfolding clauses_def by (auto simp: conflict.simps clauses_def)
then show False
using termi by (blast intro: cdcl⇩W_stgy.intros)
qed
then show ?thesis
using None by auto
qed
qed
lemma cdcl⇩W_stgy_tranclp_cdcl⇩W_restart:
"cdcl⇩W_stgy S S' ⟹ cdcl⇩W_restart⇧+⇧+ S S'"
by (simp add: cdcl⇩W_cdcl⇩W_restart cdcl⇩W_stgy_cdcl⇩W tranclp.r_into_trancl)
lemma tranclp_cdcl⇩W_stgy_tranclp_cdcl⇩W_restart:
"cdcl⇩W_stgy⇧+⇧+ S S' ⟹ cdcl⇩W_restart⇧+⇧+ S S'"
apply (induct rule: tranclp.induct)
using cdcl⇩W_stgy_tranclp_cdcl⇩W_restart apply blast
by (meson cdcl⇩W_stgy_tranclp_cdcl⇩W_restart tranclp_trans)
lemma rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart:
"cdcl⇩W_stgy⇧*⇧* S S' ⟹ cdcl⇩W_restart⇧*⇧* S S'"
using rtranclp_unfold[of cdcl⇩W_stgy S S'] tranclp_cdcl⇩W_stgy_tranclp_cdcl⇩W_restart[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)
case (resolve L C M D T) note tr_S = this(1) and confl = this(4) and LD = this(5) and T = this(7)
have uL_not_D: "-L ∉# remove1_mset (-L) D"
using n_d confl unfolding distinct_cdcl⇩W_state_def distinct_mset_def
by (metis distinct_cdcl⇩W_state_def distinct_mem_diff_mset multi_member_last n_d)
moreover {
have L_not_D: "L ∉# remove1_mset (-L) D"
proof (rule ccontr)
assume "¬ ?thesis"
then have "L ∈# D"
by (auto simp: in_remove1_mset_neq)
moreover have "Propagated L C # M ⊨as CNot D"
using conflicting confl tr_S unfolding cdcl⇩W_conflicting_def by auto
ultimately have "-L ∈ lits_of_l (Propagated L C # M)"
using in_CNot_implies_uminus(2) by blast
moreover have "no_dup (Propagated L C # M)"
using lev tr_S unfolding cdcl⇩W_M_level_inv_def by auto
ultimately show False unfolding lits_of_def
by (metis imageI insertCI list.simps(15) lit_of.simps(2) lits_of_def no_dup_consistentD)
qed
}
ultimately have g_D: "get_maximum_level (Propagated L C # M) (remove1_mset (-L) D)
= get_maximum_level M (remove1_mset (-L) D)"
by (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set atms_of_def)
have lev_L[simp]: "get_level M L = 0"
using lev unfolding cdcl⇩W_M_level_inv_def tr_S by (auto simp: lits_of_def)
have D: "get_maximum_level M (remove1_mset (-L) D) = backtrack_lvl S"
using resolve.hyps(6) LD unfolding tr_S by (auto simp: get_maximum_level_plus max_def g_D)
have "get_maximum_level M (remove1_mset L C) ≤ backtrack_lvl S"
using count_decided_ge_get_maximum_level[of M] lev unfolding tr_S cdcl⇩W_M_level_inv_def by auto
then have
"get_maximum_level M (remove1_mset (- L) D ∪# remove1_mset L C) = backtrack_lvl S"
by (auto simp: get_maximum_level_union_mset get_maximum_level_plus max_def D)
then show ?case
using tr_S get_maximum_level_exists_lit_of_max_level[of
"remove1_mset (- L) D ∪# remove1_mset L C" M] T
by auto
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_l M"
using ‹La ∈# D› in_CNot_implies_uminus(2)[of L D "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
next
case backtrack
then show ?case
by (auto split: if_split_asm simp: cdcl⇩W_M_level_inv_decomp lev)
qed auto
subsubsection ‹Strong completeness›
lemma propagate_high_levelE:
assumes "propagate S T"
obtains M' N' U L C where
"state_butlast S = (M', N', U, None)" and
"state_butlast T = (Propagated L (C + {#L#}) # M', N', U, None)" and
"C + {#L#} ∈# local.clauses S" and
"M' ⊨as CNot C" and
"undefined_lit (trail S) L"
proof -
obtain E L where
conf: "conflicting S = None" and
E: "E ∈# clauses S" and
LE: "L ∈# E" and
tr: "trail S ⊨as CNot (E - {#L#})" and
undef: "undefined_lit (trail S) L" and
T: "T ∼ cons_trail (Propagated L E) S"
using assms by (elim propagateE) simp
obtain M N U where
S: "state_butlast S = (M, N, U, None)"
using conf by auto
show thesis
using that[of M N U L "remove1_mset L E"] S T LE E tr undef
by auto
qed
lemma cdcl⇩W_propagate_conflict_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_l (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_l (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_l (trail Y) ⊆ set M"
by blast+
obtain M' N' U C L where
Y: "state_butlast Y = (M', N', U, None)" and
Z: "state_butlast Z = (Propagated L (C + {#L#}) # M', N', U, None)" and
C: "C + {#L#} ∈# clauses Y" and
M'_C: "M' ⊨as CNot C" and
"undefined_lit (trail Y) L"
using propa by (auto elim: propagate_high_levelE)
have "init_clss S = init_clss Y"
using st by induction (auto elim: propagateE)
then have [simp]: "N' = N" using NS Y Z by simp
have "learned_clss Y = {#}"
using st learned by induction (auto elim: propagateE)
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 NS ‹init_clss S = init_clss Y› ‹learned_clss Y = {#}›
unfolding true_clss_def clauses_def by fastforce
ultimately have "L ∈ set M" by (simp add: cons consistent_CNot_not)
then show ?case using LM len Y Z by auto
qed
lemma
assumes "propagate⇧*⇧* S X"
shows
rtranclp_propagate_init_clss: "init_clss X = init_clss S" and
rtranclp_propagate_learned_clss: "learned_clss X = learned_clss S"
using assms by (induction rule: rtranclp_induct) (auto elim: propagateE)
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_mm N" and
distM: "distinct M" and
length: "n ≤ length M"
shows
"∃M' S. length M' ≥ n ∧
lits_of_l M' ⊆ set M ∧
no_dup M' ∧
state_butlast S = (M', N, {#}, None) ∧
cdcl⇩W_stgy⇧*⇧* (init_state N) S"
using length
proof (induction n)
case 0
have "state_butlast (init_state N) = ([], N, {#}, None)"
by auto
moreover have
"0 ≤ length []" and
"lits_of_l [] ⊆ set M" and
"cdcl⇩W_stgy⇧*⇧* (init_state N) (init_state N)"
and "no_dup []"
by auto
ultimately show ?case by blast
next
case (Suc n) note IH = this(1) and n = this(2)
then obtain M' S where
l_M': "length M' ≥ n" and
M': "lits_of_l M' ⊆ set M" and
n_d[simp]: "no_dup M'" and
S: "state_butlast S = (M', N, {#}, None)" 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 cdcl⇩W_M_level_inv_S0_cdcl⇩W_restart rtranclp_cdcl⇩W_stgy_consistent_inv st apply blast
using cdcl⇩W_M_level_inv_S0_cdcl⇩W_restart no_strange_atm_S0 rtranclp_cdcl⇩W_restart_no_strange_atm_inv
rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart st by blast
{ assume no_step: "¬no_step propagate S"
then obtain S' where S': "propagate S S'"
by auto
have lev: "cdcl⇩W_M_level_inv S'"
using M S' rtranclp_cdcl⇩W_restart_consistent_inv rtranclp_propagate_is_rtranclp_cdcl⇩W_restart 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_l (trail S') ⊆ set M"
using S' cdcl⇩W_propagate_conflict_completeness[OF assms(1-3), of S] M' S
by (auto simp: comp_def)
moreover have "cdcl⇩W_stgy S S'" using S' by (simp add: cdcl⇩W_stgy.propagate')
moreover {
have "trail S = M'"
using S by (auto simp: comp_def rev_map)
then have "length (trail S') > n"
using S' l_M' by (auto elim: propagateE) }
moreover {
have stS': "cdcl⇩W_stgy⇧*⇧* (init_state N) S'"
using st cdcl⇩W_stgy.propagate'[OF S'] by (auto simp: r_into_rtranclp)
then have "init_clss S' = N"
using 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 S S' by (auto elim: propagateE)
have "state_butlast S' = (trail S', N, {#}, None)"
using S by auto }
moreover
have "cdcl⇩W_stgy⇧*⇧* (init_state N) S'"
apply (rule rtranclp.rtrancl_into_rtrancl)
using st apply simp
using ‹cdcl⇩W_stgy S S'› by simp
ultimately have ?case
apply -
apply (rule exI[of _ "trail S'"], rule exI[of _ S'])
by auto
}
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 n_d by blast
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: true_clss_def comp_def rev_map
clauses_def elim!: conflictE)
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_l M') = length M'"
by (induction M') (auto simp add: lits_of_def card_insert_if defined_lit_map)
then have "lits_of_l M' ⊂ set M"
using n M' n' lenM by auto
then obtain L where L: "L ∈ set M" and undef_m: "L ∉ lits_of_l M'" by auto
moreover have undef: "undefined_lit M' L"
using M' Decided_Propagated_in_iff_in_lits_of_l calculation(1,2) cons
consistent_interp_def by (metis (no_types, lifting) subset_eq)
moreover have "atm_of L ∈ atms_of_mm (init_clss S)"
using atm_incl calculation S by auto
ultimately have dec: "decide S (cons_trail (Decided L) S)"
using decide_rule[of S _ "cons_trail (Decided L) S"] S by auto
let ?S' = "cons_trail (Decided L) S"
have "lits_of_l (trail ?S') ⊆ set M" using L M' S undef by auto
moreover have "no_strange_atm ?S'"
using alien dec M by (meson cdcl⇩W_restart_no_strange_atm_inv decide other)
have "cdcl⇩W_M_level_inv ?S'"
using M dec rtranclp_mono[of decide cdcl⇩W_restart] by (meson cdcl⇩W_restart_consistent_inv
decide other)
then have lev'': "cdcl⇩W_M_level_inv ?S'"
using S rtranclp_cdcl⇩W_restart_consistent_inv rtranclp_propagate_is_rtranclp_cdcl⇩W_restart
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_l (trail ?S') ⊆ set M"
using S L M' S undef by simp
then have "Suc n ≤ length (trail ?S') ∧ lits_of_l (trail ?S') ⊆ set M"
using l_M' S undef by auto
moreover have S'': "state_butlast ?S' = (trail ?S', N, {#}, None)"
using S undef n_d'' lev'' by auto
moreover have "cdcl⇩W_stgy⇧*⇧* (init_state N) ?S'"
using S'' no_step no_confl st dec by (auto dest: decide cdcl⇩W_stgy.intros)
ultimately show ?thesis using 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_mm N" and
distM: "distinct M"
shows
"∃M' S. lits_of_l M' = set M ∧
state_butlast S = (M', N, {#}, None) ∧
cdcl⇩W_stgy⇧*⇧* (init_state N) S"
proof -
have ‹∃M' S. lits_of_l M' ⊆ set M ∧
no_dup M' ∧ length M' = n ∧
state_butlast S = (M', N, {#}, None) ∧
cdcl⇩W_stgy⇧*⇧* (init_state N) S›
if ‹n ≤ length M› for n :: nat
using that
proof (induction n)
case 0
then show ?case by (auto intro!: exI[of _ ‹init_state N›])
next
case (Suc n) note IH = this(1) and n_le_M = this(2)
then obtain M' S where
M': "lits_of_l M' ⊆ set M" and
n_d[simp]: "no_dup M'" and
S: "state_butlast S = (M', N, {#}, None)" and
st: "cdcl⇩W_stgy⇧*⇧* (init_state N) S" and
l_M': ‹length M' = n›
by auto
have
M: "cdcl⇩W_M_level_inv S" and
alien: "no_strange_atm S"
using cdcl⇩W_M_level_inv_S0_cdcl⇩W_restart rtranclp_cdcl⇩W_stgy_consistent_inv st apply blast
using cdcl⇩W_M_level_inv_S0_cdcl⇩W_restart no_strange_atm_S0 rtranclp_cdcl⇩W_restart_no_strange_atm_inv
rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart st by blast
{ assume no_step: "¬no_step propagate S"
then obtain S' where S': "propagate S S'"
by auto
have lev: "cdcl⇩W_M_level_inv S'"
using M S' rtranclp_cdcl⇩W_restart_consistent_inv rtranclp_propagate_is_rtranclp_cdcl⇩W_restart 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_l (trail S') ⊆ set M"
using S' cdcl⇩W_propagate_conflict_completeness[OF assms(1-3), of S] M' S
by (auto simp: comp_def)
moreover have "cdcl⇩W_stgy S S'" using S' by (simp add: cdcl⇩W_stgy.propagate')
moreover {
have "trail S = M'"
using S by (auto simp: comp_def rev_map)
then have "length (trail S') = Suc n"
using S' l_M' by (auto elim: propagateE) }
moreover {
have stS': "cdcl⇩W_stgy⇧*⇧* (init_state N) S'"
using st cdcl⇩W_stgy.propagate'[OF S'] by (auto simp: r_into_rtranclp)
then have "init_clss S' = N"
using 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 S S' by (auto elim: propagateE)
have "state_butlast S' = (trail S', N, {#}, None)"
using S by auto }
moreover
have "cdcl⇩W_stgy⇧*⇧* (init_state N) S'"
apply (rule rtranclp.rtrancl_into_rtrancl)
using st apply simp
using ‹cdcl⇩W_stgy S S'› by simp
ultimately have ?case
apply -
apply (rule exI[of _ "trail S'"], rule exI[of _ S'])
by auto
}
moreover { assume no_step: "no_step propagate S"
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: true_clss_def comp_def rev_map
clauses_def elim!: conflictE)
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_l M') = length M'"
by (induction M') (auto simp add: lits_of_def card_insert_if defined_lit_map)
then have "lits_of_l M' ⊂ set M"
using M' l_M' lenM n_le_M by auto
then obtain L where L: "L ∈ set M" and undef_m: "L ∉ lits_of_l M'" by auto
moreover have undef: "undefined_lit M' L"
using M' Decided_Propagated_in_iff_in_lits_of_l calculation(1,2) cons
consistent_interp_def by (metis (no_types, lifting) subset_eq)
moreover have "atm_of L ∈ atms_of_mm (init_clss S)"
using atm_incl calculation S by auto
ultimately have dec: "decide S (cons_trail (Decided L) S)"
using decide_rule[of S _ "cons_trail (Decided L) S"] S by auto
let ?S' = "cons_trail (Decided L) S"
have "lits_of_l (trail ?S') ⊆ set M" using L M' S undef by auto
moreover have "no_strange_atm ?S'"
using alien dec M by (meson cdcl⇩W_restart_no_strange_atm_inv decide other)
have "cdcl⇩W_M_level_inv ?S'"
using M dec rtranclp_mono[of decide cdcl⇩W_restart] by (meson cdcl⇩W_restart_consistent_inv
decide other)
then have lev'': "cdcl⇩W_M_level_inv ?S'"
using S rtranclp_cdcl⇩W_restart_consistent_inv rtranclp_propagate_is_rtranclp_cdcl⇩W_restart
by blast
then have n_d'': "no_dup (trail ?S')"
unfolding cdcl⇩W_M_level_inv_def by auto
have "Suc (length (trail S)) = length (trail ?S') ∧ lits_of_l (trail ?S') ⊆ set M"
using S L M' S undef by simp
then have "Suc n = length (trail ?S') ∧ lits_of_l (trail ?S') ⊆ set M"
using l_M' S undef by auto
moreover have S'': "state_butlast ?S' = (trail ?S', N, {#}, None)"
using S undef n_d'' lev'' by auto
moreover have "cdcl⇩W_stgy⇧*⇧* (init_state N) ?S'"
using S'' no_step no_confl st dec by (auto dest: decide cdcl⇩W_stgy.intros)
ultimately have ?case using n_d'' L M' by (auto intro!: exI[of _ ‹Decided L # trail S›] exI[of _ ‹?S'›])
}
ultimately show ?case by blast
qed
from this[of ‹length M›] obtain M' S where
M'_M: ‹lits_of_l M' ⊆ set M› and
n_d: ‹no_dup M'› and
‹length M' = length M› and
‹state_butlast S = (M', N, {#}, None) ∧ cdcl⇩W_stgy⇧*⇧* (init_state N) S›
by auto
moreover have ‹lits_of_l M' = set M›
apply (rule card_subset_eq)
subgoal by auto
subgoal using M'_M .
subgoal using M'_M n_d no_dup_length_eq_card_atm_of_lits_of_l[OF n_d] M'_M ‹finite (set M)› distinct_card[OF distM] calculation(3)
card_image_le[of ‹ lits_of_l M'› atm_of] card_seteq[OF ‹finite (set M)›, of ‹lits_of_l M'›]
by auto
done
ultimately show ?thesis
by (auto intro!: exI[of _ S])
qed
text ‹\cwref{cdcl:completeness}{theorem 2.9.11 page 98} (with strategy)›
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_mm N" and
distM: "distinct M"
shows
"∃M' k S.
lits_of_l M' = set M ∧
state_butlast S = (M', N, {#}, None) ∧
cdcl⇩W_stgy⇧*⇧* (init_state N) S ∧
final_cdcl⇩W_restart_state S"
proof -
from cdcl⇩W_stgy_strong_completeness_n[OF assms, of "length M"]
obtain M' T where
l: "length M ≤ length M'" and
M'_M: "lits_of_l M' ⊆ set M" and
no_dup: "no_dup M'" and
T: "state_butlast T = (M', N, {#}, None)" 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 simp: lits_of_def image_image no_dup_def) }
moreover have "card (lits_of_l M') = card (set ((map (λl. atm_of (lit_of l)) M')))"
using no_dup by (induction M') (auto simp add: defined_lit_map card_insert_if lits_of_def)
ultimately have "card (set M) ≤ card (lits_of_l M')" using l unfolding lits_of_def by auto
then have s: "set M = lits_of_l M'"
using M'_M card_seteq by blast
moreover {
have "M' ⊨asm N"
using MN s unfolding true_annots_def Ball_def true_annot_def true_clss_def by auto
then have "final_cdcl⇩W_restart_state T"
using T no_dup unfolding final_cdcl⇩W_restart_state_def by auto }
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 M' D. trail S = M' @ Decided K # M ⟶ 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
n_s: "no_step conflict S" and
lev: "cdcl⇩W_M_level_inv S" and
max_lev: "conflict_is_false_with_level S" and
smaller: "no_smaller_confl S"
shows "no_smaller_confl S'"
using assms(1,2) unfolding no_smaller_confl_def
proof (induct rule: cdcl⇩W_o_induct)
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 M' Da
assume "trail T = M'' @ Decided K # M'" and D: "Da ∈# local.clauses T"
then have "trail S = tl M'' @ Decided K # M'
∨ (M'' = [] ∧ Decided K # M' = Decided L # trail S)"
using T undef by (cases M'') auto
moreover {
assume "trail S = tl M'' @ Decided K # M'"
then have "¬M' ⊨as CNot Da"
using D T undef confl smaller unfolding no_smaller_confl_def smaller by fastforce
}
moreover {
assume "Decided K # M' = Decided L # trail S"
then have "¬M' ⊨as CNot Da" using smaller D confl T n_s by (auto simp: conflict.simps)
}
ultimately show "¬M' ⊨as CNot Da" by fast
qed
next
case resolve
then show ?case using smaller max_lev unfolding no_smaller_confl_def by auto
next
case skip
then show ?case using smaller max_lev unfolding no_smaller_confl_def by auto
next
case (backtrack L D K i M1 M2 T D') note confl = this(1) and decomp = this(2) and
T = this(9)
obtain c where M: "trail S = c @ M2 @ Decided K # M1"
using decomp by auto
show ?case
proof (intro allI impI)
fix M ia K' M' Da
assume "trail T = M' @ Decided K' # M"
then have "M1 = tl M' @ Decided K' # M"
using T decomp lev by (cases M') (auto simp: cdcl⇩W_M_level_inv_decomp)
let ?D' = ‹add_mset L D'›
let ?S' = "(cons_trail (Propagated L ?D')
(reduce_trail_to M1 (add_learned_cls ?D' (update_conflicting None S))))"
assume D: "Da ∈# clauses T"
moreover{
assume "Da ∈# clauses S"
then have "¬M ⊨as CNot Da" using ‹M1 = tl M' @ Decided K' # M› M confl smaller
unfolding no_smaller_confl_def by auto
}
moreover {
assume Da: "Da = add_mset L D'"
have "¬M ⊨as CNot Da"
proof (rule ccontr)
assume "¬ ?thesis"
then have "-L ∈ lits_of_l M"
unfolding Da by (simp add: in_CNot_implies_uminus(2))
then have "-L ∈ lits_of_l (Propagated L D # M1)"
using UnI2 ‹M1 = tl M' @ Decided K' # M›
by auto
moreover
have "backtrack S ?S'"
using backtrack_rule[OF backtrack.hyps(1-8) T] backtrack_state_eq_compatible[of S T S] T
by force
then have "cdcl⇩W_M_level_inv ?S'"
using cdcl⇩W_restart_consistent_inv[OF _ lev] other[OF bj]
by (auto intro: cdcl⇩W_bj.intros)
then have "no_dup (Propagated L D # M1)"
using decomp lev unfolding cdcl⇩W_M_level_inv_def by auto
ultimately show False
using Decided_Propagated_in_iff_in_lits_of_l defined_lit_map
by (auto simp: no_dup_def)
qed
}
ultimately show "¬M ⊨as CNot Da"
using T 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 elim: conflictE)
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 M'' D
assume M': "trail S' = M'' @ Decided K # M'"
and "D ∈# clauses S'"
obtain M N U C L where
S: "state_butlast S = (M, N, U, None)" and
S': "state_butlast S' = (Propagated L (C + {#L#}) # M, N, U, None)" and
"C + {#L#} ∈# clauses S" and
"M ⊨as CNot C" and
"undefined_lit M L"
using propagate by (auto elim: propagate_high_levelE)
have "tl M'' @ Decided K # M' = trail S" using M' S S'
by (metis Pair_inject list.inject list.sel(3) annotated_lit.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_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"
shows "no_smaller_confl S'"
using assms
proof (induct rule: cdcl⇩W_stgy.induct)
case (conflict' S')
then show ?case using conflict_no_smaller_confl_inv[of S S'] by blast
next
case (propagate' S')
then show ?case using propagate_no_smaller_confl_inv[of S S'] by blast
next
case (other' S')
then show ?case
using cdcl⇩W_o_no_smaller_confl_inv[of S] by auto
qed
lemma conflict_conflict_is_false_with_level:
assumes
conflict: "conflict S T" and
smaller: "no_smaller_confl S" and
M_lev: "cdcl⇩W_M_level_inv S"
shows "conflict_is_false_with_level T"
using conflict
proof (cases rule: conflict.cases)
case (conflict_rule D) note confl = this(1) and D = this(2) and not_D = this(3) and T = this(4)
then have [simp]: "conflicting T = Some D"
by auto
have M_lev_T: "cdcl⇩W_M_level_inv T"
using conflict M_lev by (auto simp: cdcl⇩W_restart_consistent_inv
dest: cdcl⇩W_restart.intros)
then have bt: "backtrack_lvl T = count_decided (trail T)"
unfolding cdcl⇩W_M_level_inv_def by auto
have n_d: "no_dup (trail T)"
using M_lev_T unfolding cdcl⇩W_M_level_inv_def by auto
show ?thesis
proof (rule ccontr, clarsimp)
assume
empty: "D ≠ {#}" and
lev: "∀L∈#D. get_level (trail T) L ≠ backtrack_lvl T"
moreover {
have "get_level (trail T) L ≤ backtrack_lvl T" if "L∈#D" for L
using that count_decided_ge_get_level[of "trail T" L] M_lev_T
unfolding cdcl⇩W_M_level_inv_def by auto
then have "get_level (trail T) L < backtrack_lvl T" if "L∈#D" for L
using lev that by fastforce } note lev' = this
ultimately have "count_decided (trail T) > 0"
using M_lev_T unfolding cdcl⇩W_M_level_inv_def by (cases D) fastforce+
then have ex: ‹∃x∈set (trail T). is_decided x›
unfolding no_dup_def count_decided_def by cases auto
have ‹∃M2 L M1. trail T = M2 @ Decided L # M1 ∧ (∀m∈set M2. ¬ is_decided m)›
by (rule split_list_first_propE[of "trail T" is_decided, OF ex])
(force elim!: is_decided_ex_Decided)
then obtain M2 L M1 where
tr_T: "trail T = M2 @ Decided L # M1" and nm: "∀m ∈ set M2. ¬ is_decided m"
by blast
moreover {
have "get_level (trail T) La = backtrack_lvl T" if "- La ∈ lits_of_l M2" for La
unfolding tr_T bt
apply (subst get_level_skip_end)
using that apply (simp add: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
Decided_Propagated_in_iff_in_lits_of_l; fail)
using nm bt tr_T by (simp add: count_decided_0_iff) }
moreover {
have tr: "M2 @ Decided L # M1 = (M2 @ [Decided L]) @ M1"
by auto
have "get_level (trail T) L = backtrack_lvl T"
using n_d nm unfolding tr_T tr bt
by (auto simp: image_image atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
atm_lit_of_set_lits_of_l count_decided_0_iff[symmetric]) }
moreover have "trail S = trail T"
using T by auto
ultimately have "M1 ⊨as CNot D"
using lev' not_D unfolding true_annots_true_cls_def_iff_negation_in_model
by (force simp: count_decided_0_iff[symmetric] get_level_def)
then show False
using smaller T tr_T D by (auto simp: no_smaller_confl_def)
qed
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
"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')
then have "no_smaller_confl S'"
using conflict'.hyps conflict_no_smaller_confl_inv n_l by blast
moreover have "conflict_is_false_with_level S'"
using conflict_conflict_is_false_with_level assms(4) conflict'.hyps n_l by blast
then show ?case by blast
next
case (propagate' S')
then show ?case by (auto elim: propagateE)
next
case (other' S') note n_s = this(1,2) and o = this(3) and lev = this(6)
show ?case
using cdcl⇩W_o_conflict_is_false_with_level_inv[OF o] other'.prems by blast
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
dist: "distinct_cdcl⇩W_state S" and
conflicting: "cdcl⇩W_conflicting S" and
decomp: "all_decomposition_implies_m (clauses S) (get_all_ann_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_restart
by (blast intro: rtranclp_cdcl⇩W_restart_consistent_inv)+
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_restart[OF st]
dist by auto
moreover have "cdcl⇩W_conflicting S'"
using rtranclp_cdcl⇩W_restart_all_inv(6)[of S S'] st alien conflicting decomp dist learned lev
rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart by blast
ultimately show ?case
using cdcl⇩W_stgy_no_smaller_confl[OF cdcl] cdcl⇩W_stgy_ex_lit_of_max_level[OF cdcl] cdcl
by (auto simp del: simp add: cdcl⇩W_stgy.simps elim!: propagateE)
qed
subsubsection ‹Final States are Conclusive›
text ‹\cwref{lem:prop:cdclsoundtermStates}{theorem 2.9.9 page 97}›
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')"
proof -
let ?S = "init_state N"
have
termi: "∀S''. ¬cdcl⇩W_stgy S' S''" and
step: "cdcl⇩W_stgy⇧*⇧* ?S S'" using full unfolding full_def by auto
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 (clauses S') (get_all_ann_decomposition (trail S'))"
using no_d tranclp_cdcl⇩W_stgy_tranclp_cdcl⇩W_restart[of ?S S'] step
rtranclp_cdcl⇩W_restart_all_inv(1-6)[of ?S S']
unfolding rtranclp_unfold by auto
have confl_k: "conflict_is_false_with_level S'"
using rtranclp_cdcl⇩W_stgy_no_smaller_confl_inv[OF step] no_d by auto
have learned_entailed: ‹cdcl⇩W_learned_clauses_entailed_by_init S'›
using rtranclp_cdcl⇩W_learned_clauses_entailed[of ‹?S› ‹S'›] step
by (simp add: rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart)
show ?thesis
using cdcl⇩W_stgy_final_state_conclusive[OF termi decomp learned level_inv alien no_dup confl
confl_k learned_entailed] .
qed
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)
apply (auto elim: conflictE; fail)[]
apply (auto elim: propagateE; fail)[]
using cdcl⇩W_o_fst_empty_conflicting_false by blast
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)
apply (auto elim: conflictE; fail)[]
apply (auto elim: propagateE; fail)[]
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
definition conflict_or_propagate :: "'st ⇒ 'st ⇒ bool" where
"conflict_or_propagate S T ⟷ conflict S T ∨ propagate S T"
declare conflict_or_propagate_def[simp]
lemma conflict_or_propagate_intros:
"conflict S T ⟹ conflict_or_propagate S T"
"propagate S T ⟹ conflict_or_propagate S T"
by auto
text ‹\cwref{lem:prop:cdclsoundtermStates}{theorem 2.9.9 page 97}›
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_l (trail S'))"
unfolding cdcl⇩W_M_level_inv_def by blast
moreover have "lits_of_l (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
subsection ‹Structural Invariant›
text ‹The condition that no learned clause is a tautology is overkill for the termination (in the
sense that the no-duplicate condition is enough), but it allows to reuse @{term simple_clss}.
The invariant contains all the structural invariants that holds,›
definition cdcl⇩W_all_struct_inv where
"cdcl⇩W_all_struct_inv S ⟷
no_strange_atm S ∧
cdcl⇩W_M_level_inv S ∧
(∀s ∈# learned_clss S. ¬tautology s) ∧
distinct_cdcl⇩W_state S ∧
cdcl⇩W_conflicting S ∧
all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S)) ∧
cdcl⇩W_learned_clause S"
lemma cdcl⇩W_all_struct_inv_inv:
assumes "cdcl⇩W_restart S S'" and "cdcl⇩W_all_struct_inv S"
shows "cdcl⇩W_all_struct_inv S'"
unfolding cdcl⇩W_all_struct_inv_def
proof (intro HOL.conjI)
show "no_strange_atm S'"
using cdcl⇩W_restart_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by auto
show "cdcl⇩W_M_level_inv S'"
using cdcl⇩W_restart_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "distinct_cdcl⇩W_state S'"
using cdcl⇩W_restart_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "cdcl⇩W_conflicting S'"
using cdcl⇩W_restart_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "all_decomposition_implies_m (clauses S') (get_all_ann_decomposition (trail S'))"
using cdcl⇩W_restart_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "cdcl⇩W_learned_clause S'"
using cdcl⇩W_restart_all_inv[OF assms(1)] assms(2) unfolding cdcl⇩W_all_struct_inv_def by fast
show "∀s∈#learned_clss S'. ¬ tautology s"
using assms(1)[THEN learned_clss_are_not_tautologies] assms(2)
unfolding cdcl⇩W_all_struct_inv_def by fast
qed
lemma rtranclp_cdcl⇩W_all_struct_inv_inv:
assumes "cdcl⇩W_restart⇧*⇧* S S'" and "cdcl⇩W_all_struct_inv S"
shows "cdcl⇩W_all_struct_inv S'"
using assms by induction (auto intro: cdcl⇩W_all_struct_inv_inv)
lemma cdcl⇩W_stgy_cdcl⇩W_all_struct_inv:
"cdcl⇩W_stgy S T ⟹ cdcl⇩W_all_struct_inv S ⟹ cdcl⇩W_all_struct_inv T"
by (meson cdcl⇩W_stgy_tranclp_cdcl⇩W_restart rtranclp_cdcl⇩W_all_struct_inv_inv rtranclp_unfold)
lemma rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv:
"cdcl⇩W_stgy⇧*⇧* S T ⟹ cdcl⇩W_all_struct_inv S ⟹ cdcl⇩W_all_struct_inv T"
by (induction rule: rtranclp_induct) (auto intro: cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)
lemma beginning_not_decided_invert:
assumes A: "M @ A = M' @ Decided K # H" and
nm: "∀m∈set M. ¬is_decided m"
shows "∃M. A = M @ Decided K # H"
proof -
have "A = drop (length M) (M' @ Decided K # H)"
using arg_cong[OF A, of "drop (length M)"] by auto
moreover have "drop (length M) (M' @ Decided K # H) = drop (length M) M' @ Decided K # H"
using nm by (metis (no_types, lifting) A drop_Cons' drop_append annotated_lit.disc(1) not_gr0
nth_append nth_append_length nth_mem zero_less_diff)
finally show ?thesis by fast
qed
subsection ‹Strategy-Specific Invariant›
definition cdcl⇩W_stgy_invariant where
"cdcl⇩W_stgy_invariant S ⟷
conflict_is_false_with_level S
∧ no_smaller_confl S"
lemma cdcl⇩W_stgy_cdcl⇩W_stgy_invariant:
assumes
cdcl⇩W_restart: "cdcl⇩W_stgy S T" and
inv_s: "cdcl⇩W_stgy_invariant S" and
inv: "cdcl⇩W_all_struct_inv S"
shows
"cdcl⇩W_stgy_invariant T"
unfolding cdcl⇩W_stgy_invariant_def cdcl⇩W_all_struct_inv_def apply (intro conjI)
apply (rule cdcl⇩W_stgy_ex_lit_of_max_level[of S])
using assms unfolding cdcl⇩W_stgy_invariant_def cdcl⇩W_all_struct_inv_def apply auto[7]
using cdcl⇩W_stgy_invariant_def cdcl⇩W_stgy_no_smaller_confl inv_s by blast
lemma rtranclp_cdcl⇩W_stgy_cdcl⇩W_stgy_invariant:
assumes
cdcl⇩W_restart: "cdcl⇩W_stgy⇧*⇧* S T" and
inv_s: "cdcl⇩W_stgy_invariant S" and
inv: "cdcl⇩W_all_struct_inv S"
shows
"cdcl⇩W_stgy_invariant T"
using assms apply induction
apply (simp; fail)
using cdcl⇩W_stgy_cdcl⇩W_stgy_invariant rtranclp_cdcl⇩W_all_struct_inv_inv
rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart by blast
lemma full_cdcl⇩W_stgy_inv_normal_form:
assumes
full: "full cdcl⇩W_stgy S T" and
inv_s: "cdcl⇩W_stgy_invariant S" and
inv: "cdcl⇩W_all_struct_inv S" and
learned_entailed: ‹cdcl⇩W_learned_clauses_entailed_by_init S›
shows "conflicting T = Some {#} ∧ unsatisfiable (set_mset (init_clss S))
∨ conflicting T = None ∧ trail T ⊨asm init_clss S ∧ satisfiable (set_mset (init_clss S))"
proof -
have "no_step cdcl⇩W_stgy T" and st: "cdcl⇩W_stgy⇧*⇧* S T"
using full unfolding full_def by blast+
moreover have "cdcl⇩W_all_struct_inv T" and inv_s: "cdcl⇩W_stgy_invariant T"
apply (metis rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart full full_def inv
rtranclp_cdcl⇩W_all_struct_inv_inv)
by (metis full full_def inv inv_s rtranclp_cdcl⇩W_stgy_cdcl⇩W_stgy_invariant)
moreover have ‹cdcl⇩W_learned_clauses_entailed_by_init T›
using inv learned_entailed unfolding cdcl⇩W_all_struct_inv_def
using rtranclp_cdcl⇩W_learned_clauses_entailed rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart[OF st]
by blast
ultimately have "conflicting T = Some {#} ∧ unsatisfiable (set_mset (init_clss T))
∨ conflicting T = None ∧ trail T ⊨asm init_clss T"
using cdcl⇩W_stgy_final_state_conclusive[of T] full
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_stgy_invariant_def full_def by fast
moreover have "consistent_interp (lits_of_l (trail T))"
using ‹cdcl⇩W_all_struct_inv T› unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
by auto
moreover have "init_clss S = init_clss T"
using inv unfolding cdcl⇩W_all_struct_inv_def
by (metis rtranclp_cdcl⇩W_stgy_no_more_init_clss full full_def)
ultimately show ?thesis
by (metis satisfiable_carac' true_annot_def true_annots_def true_clss_def)
qed
lemma full_cdcl⇩W_stgy_inv_normal_form2:
assumes
full: "full cdcl⇩W_stgy S T" and
inv_s: "cdcl⇩W_stgy_invariant S" and
inv: "cdcl⇩W_all_struct_inv S"
shows "conflicting T = Some {#} ∧ unsatisfiable (set_mset (clauses T))
∨ conflicting T = None ∧ satisfiable (set_mset (clauses T))"
proof -
have "no_step cdcl⇩W_stgy T" and st: "cdcl⇩W_stgy⇧*⇧* S T"
using full unfolding full_def by blast+
moreover have "cdcl⇩W_all_struct_inv T" and inv_s: "cdcl⇩W_stgy_invariant T"
apply (metis rtranclp_cdcl⇩W_stgy_rtranclp_cdcl⇩W_restart full full_def inv
rtranclp_cdcl⇩W_all_struct_inv_inv)
by (metis full full_def inv inv_s rtranclp_cdcl⇩W_stgy_cdcl⇩W_stgy_invariant)
ultimately have "conflicting T = Some {#} ∧ unsatisfiable (set_mset (clauses T))
∨ conflicting T = None ∧ trail T ⊨asm clauses T"
using cdcl⇩W_stgy_final_state_conclusive2[of T] full
unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_stgy_invariant_def full_def by fast
moreover have "consistent_interp (lits_of_l (trail T))"
using ‹cdcl⇩W_all_struct_inv T› unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
by auto
ultimately show ?thesis
by (metis satisfiable_carac' true_annot_def true_annots_def true_clss_def)
qed
subsection ‹Additional Invariant: No Smaller Propagation›
definition no_smaller_propa :: ‹'st ⇒ bool› where
"no_smaller_propa (S ::'st) ≡
(∀M K M' D L. trail S = M' @ Decided K # M ⟶ D + {#L#} ∈# clauses S ⟶ undefined_lit M L
⟶ ¬M ⊨as CNot D)"
lemma propagated_cons_eq_append_decide_cons:
"Propagated L E # Ms = M' @ Decided K # M ⟷
M' ≠ [] ∧ Ms = tl M' @ Decided K # M ∧ hd M' = Propagated L E"
by (metis (no_types, lifting) annotated_lit.disc(1) annotated_lit.disc(2) append_is_Nil_conv hd_append
list.exhaust_sel list.sel(1) list.sel(3) tl_append2)
lemma in_get_all_mark_of_propagated_in_trail:
‹C ∈ set (get_all_mark_of_propagated M) ⟷ (∃L. Propagated L C ∈ set M)›
by (induction M rule: ann_lit_list_induct) auto
lemma no_smaller_propa_tl:
assumes
‹no_smaller_propa S› and
‹trail S ≠ []› and
‹¬is_decided(hd_trail S)› and
‹trail U = tl (trail S)› and
‹clauses U = clauses S›
shows
‹no_smaller_propa U›
using assms by (cases ‹trail S›) (auto simp: no_smaller_propa_def)
lemmas rulesE =
skipE resolveE backtrackE propagateE conflictE decideE restartE forgetE backtrackgE
lemma decide_no_smaller_step:
assumes dec: ‹decide S T› and smaller_propa: ‹no_smaller_propa S› and
n_s: ‹no_step propagate S›
shows ‹no_smaller_propa T›
unfolding no_smaller_propa_def
proof clarify
fix M K M' D L
assume
tr: ‹trail T = M' @ Decided K # M› and
D: ‹D+{#L#} ∈# clauses T› and
undef: ‹undefined_lit M L› and
M: ‹M ⊨as CNot D›
then have "Ex (propagate S)"
apply (cases M')
using propagate_rule[of S "D+{#L#}" L "cons_trail (Propagated L (D + {#L#})) S"] dec
smaller_propa
by (auto simp: no_smaller_propa_def elim!: rulesE)
then show False
using n_s by blast
qed
lemma no_smaller_propa_reduce_trail_to:
‹no_smaller_propa S ⟹ no_smaller_propa (reduce_trail_to M1 S)›
unfolding no_smaller_propa_def
by (subst (asm) append_take_drop_id[symmetric, of _ ‹length (trail S) - length M1›])
(auto simp: trail_reduce_trail_to_drop
simp del: append_take_drop_id)
lemma backtrackg_no_smaller_propa:
assumes o: ‹backtrackg S T› and smaller_propa: ‹no_smaller_propa S› and
n_d: ‹no_dup (trail S)› and
n_s: ‹no_step propagate S› and
tr_CNot: ‹trail S ⊨as CNot (the (conflicting S))›
shows ‹no_smaller_propa T›
proof -
obtain D D' :: "'v clause" and K L :: "'v literal" and
M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat where
confl: "conflicting S = Some (add_mset L D)" and
decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
bt: "get_level (trail S) L = backtrack_lvl S" and
lev_L: "get_level (trail S) L = get_maximum_level (trail S) (add_mset L D')" and
i: "get_maximum_level (trail S) D' ≡ i" and
lev_K: "get_level (trail S) K = i + 1" and
D_D': ‹D' ⊆# D› and
T: "T ∼ cons_trail (Propagated L (add_mset L D'))
(reduce_trail_to M1
(add_learned_cls (add_mset L D')
(update_conflicting None S)))"
using o by (auto elim!: rulesE)
let ?D' = ‹add_mset L D'›
have [simp]: "trail (reduce_trail_to M1 S) = M1"
using decomp by auto
obtain M'' c where M'': "trail S = M'' @ tl (trail T)" and c: ‹M'' = c @ M2 @ [Decided K]›
using decomp T by auto
have M1: "M1 = tl (trail T)" and tr_T: "trail T = Propagated L ?D' # M1"
using decomp T by auto
have i_lvl: ‹i = backtrack_lvl T›
using no_dup_append_in_atm_notin[of ‹c @ M2› ‹Decided K # tl (trail T)› K]
n_d lev_K unfolding c M'' by (auto simp: image_Un tr_T)
from o show ?thesis
unfolding no_smaller_propa_def
proof clarify
fix M K' M' E' L'
assume
tr: ‹trail T = M' @ Decided K' # M› and
E: ‹E'+{#L'#} ∈# clauses T› and
undef: ‹undefined_lit M L'› and
M: ‹M ⊨as CNot E'›
have n_d_T: ‹no_dup (trail T)› and M1_D': "M1 ⊨as CNot D'"
using backtrack_M1_CNot_D'[OF n_d i decomp _ confl _ T] lev_K bt lev_L tr_CNot
confl D_D'
by (auto dest: subset_mset_trans_add_mset)
have False if D: ‹add_mset L D' = add_mset L' E'› and M_D: ‹M ⊨as CNot E'›
proof -
have ‹i ≠ 0›
using i_lvl tr T by auto
moreover
have "get_maximum_level M1 D' = i"
using T i n_d D_D' M1_D' unfolding M'' tr_T
by (subst (asm) get_maximum_level_skip_beginning)
(auto dest: defined_lit_no_dupD dest!: true_annots_CNot_definedD)
ultimately obtain L_max where
L_max_in: "L_max ∈# D'" and
lev_L_max: "get_level M1 L_max = i"
using i get_maximum_level_exists_lit_of_max_level[of D' M1]
by (cases D') auto
have count_dec_M: "count_decided M < i"
using T i_lvl unfolding tr by auto
have "- L_max ∉ lits_of_l M"
proof (rule ccontr)
assume ‹¬ ?thesis›
then have ‹undefined_lit (M' @ [Decided K']) L_max›
using n_d_T unfolding tr
by (auto dest: in_lits_of_l_defined_litD dest: defined_lit_no_dupD simp: atm_of_eq_atm_of)
then have "get_level (tl M' @ Decided K' # M) L_max < i"
apply (subst get_level_skip)
apply (cases M'; auto simp add: atm_of_eq_atm_of lits_of_def; fail)
using count_dec_M count_decided_ge_get_level[of M L_max] by auto
then show False
using lev_L_max tr unfolding tr_T by (auto simp: propagated_cons_eq_append_decide_cons)
qed
moreover have "- L ∉ lits_of_l M"
proof (rule ccontr)
define MM where ‹MM = tl M'›
assume ‹¬ ?thesis›
then have ‹- L ∉ lits_of_l (M' @ [Decided K'])›
using n_d_T unfolding tr by (auto simp: lits_of_def no_dup_def)
have ‹undefined_lit (M' @ [Decided K']) L›
apply (rule no_dup_uminus_append_in_atm_notin)
using n_d_T ‹¬ - L ∉ lits_of_l M› unfolding tr by auto
moreover have "M' = Propagated L ?D' # MM"
using tr_T MM_def by (metis hd_Cons_tl propagated_cons_eq_append_decide_cons tr)
ultimately show False
by simp
qed
moreover have "L_max ∈# D' ∨ L ∈# D'"
using D L_max_in by (auto split: if_splits)
ultimately show False
using M_D D by (auto simp: true_annots_true_cls true_clss_def add_mset_eq_add_mset)
qed
then show False
using M'' smaller_propa tr undef M T E
by (cases M') (auto simp: no_smaller_propa_def trivial_add_mset_remove_iff elim!: rulesE)
qed
qed
lemmas backtrack_no_smaller_propa = backtrackg_no_smaller_propa[OF backtrack_backtrackg]
lemma cdcl⇩W_stgy_no_smaller_propa:
assumes
cdcl: ‹cdcl⇩W_stgy S T› and
smaller_propa: ‹no_smaller_propa S› and
inv: ‹cdcl⇩W_all_struct_inv S›
shows ‹no_smaller_propa T›
using cdcl
proof (cases rule: cdcl⇩W_stgy_cases)
case conflict
then show ?thesis
using smaller_propa by (auto simp: no_smaller_propa_def elim!: rulesE)
next
case propagate
then show ?thesis
using smaller_propa by (auto simp: no_smaller_propa_def propagated_cons_eq_append_decide_cons
elim!: rulesE)
next
case skip
then show ?thesis
using smaller_propa by (auto intro: no_smaller_propa_tl elim!: rulesE)
next
case resolve
then show ?thesis
using smaller_propa by (auto intro: no_smaller_propa_tl elim!: rulesE)
next
case decide note n_s = this(1,2) and dec = this(3)
show ?thesis
using n_s dec decide_no_smaller_step[of S T] smaller_propa
by auto
next
case backtrack note n_s = this(1,2) and o = this(3)
have inv_T: "cdcl⇩W_all_struct_inv T"
using cdcl cdcl⇩W_stgy_cdcl⇩W_all_struct_inv inv by blast
have ‹trail S ⊨as CNot (the (conflicting S))› and ‹no_dup (trail S)›
using inv o unfolding cdcl⇩W_all_struct_inv_def
by (auto simp: cdcl⇩W_M_level_inv_def cdcl⇩W_conflicting_def
elim: rulesE)
then show ?thesis
using backtrack_no_smaller_propa[of S T] n_s o smaller_propa
by auto
qed
lemma rtranclp_cdcl⇩W_stgy_no_smaller_propa:
assumes
cdcl: ‹cdcl⇩W_stgy⇧*⇧* S T› and
smaller_propa: ‹no_smaller_propa S› and
inv: ‹cdcl⇩W_all_struct_inv S›
shows ‹no_smaller_propa T›
using cdcl apply (induction rule: rtranclp_induct)
subgoal using smaller_propa by simp
subgoal using inv by (auto intro: rtranclp_cdcl⇩W_stgy_cdcl⇩W_all_struct_inv
cdcl⇩W_stgy_no_smaller_propa)
done
lemma hd_trail_level_ge_1_length_gt_1:
fixes S :: 'st
defines M[symmetric, simp]: ‹M ≡ trail S›
defines L[symmetric, simp]: ‹L ≡ hd M›
assumes
smaller: ‹no_smaller_propa S› and
struct: ‹cdcl⇩W_all_struct_inv S› and
dec: ‹count_decided M ≥ 1› and
proped: ‹is_proped L›
shows ‹size (mark_of L) > 1›
proof (rule ccontr)
assume size_C: ‹¬ ?thesis›
have nd: ‹no_dup M›
using struct unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def M[symmetric]
by blast
obtain M' where M': ‹M = L # M'›
using dec L by (cases M) (auto simp del: L)
obtain K C where K: ‹L = Propagated K C›
using proped by (cases L) auto
obtain K' M1 M2 where decomp: ‹M = M2 @ Decided K' # M1›
using dec le_count_decided_decomp[of M 0] nd by auto
then have decomp': ‹M' = tl M2 @ Decided K' # M1›
unfolding M' K by (cases M2) auto
have ‹K ∈# C›
using struct unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def
M M' K by blast
then have C: ‹C = {#} + {#K#}›
using size_C K by (cases C) auto
have ‹undefined_lit M1 K›
using nd unfolding M' K decomp' by simp
moreover have ‹{#} + {#K#} ∈# clauses S›
using struct unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_learned_clause_alt_def M M' K C
reasons_in_clauses_def
by auto
moreover have ‹M1 ⊨as CNot {#}›
by auto
ultimately show False
using smaller unfolding no_smaller_propa_def M decomp
by blast
qed
subsection ‹More Invariants: Conflict is False if no decision›
text ‹If the level is higher than 0, then the conflict is not empty.›
definition conflict_non_zero_unless_level_0 :: ‹'st ⇒ bool› where
‹conflict_non_zero_unless_level_0 S ⟷
(conflicting S = Some {#} ⟶ count_decided (trail S) = 0)›
definition no_false_clause:: ‹'st ⇒ bool› where
‹no_false_clause S ⟷ (∀C ∈# clauses S. C ≠ {#})›
lemma cdcl⇩W_restart_no_false_clause:
assumes
‹cdcl⇩W_restart S T›
‹no_false_clause S›
shows ‹no_false_clause T›
using assms unfolding no_false_clause_def
by (induction rule: cdcl⇩W_restart_all_induct) (auto simp add: clauses_def)
text ‹
The proofs work smoothly thanks to the side-conditions about levels of the rule
\<^term>‹resolve›.
›
lemma cdcl⇩W_restart_conflict_non_zero_unless_level_0:
assumes
‹cdcl⇩W_restart S T›
‹no_false_clause S› and
‹conflict_non_zero_unless_level_0 S›
shows ‹conflict_non_zero_unless_level_0 T›
using assms by (induction rule: cdcl⇩W_restart_all_induct)
(auto simp add: conflict_non_zero_unless_level_0_def no_false_clause_def)
lemma rtranclp_cdcl⇩W_restart_no_false_clause:
assumes
‹cdcl⇩W_restart⇧*⇧* S T›
‹no_false_clause S›
shows ‹no_false_clause T›
using assms by (induction rule: rtranclp_induct) (auto intro: cdcl⇩W_restart_no_false_clause)
lemma rtranclp_cdcl⇩W_restart_conflict_non_zero_unless_level_0:
assumes
‹cdcl⇩W_restart⇧*⇧* S T›
‹no_false_clause S› and
‹conflict_non_zero_unless_level_0 S›
shows ‹conflict_non_zero_unless_level_0 T›
using assms by (induction rule: rtranclp_induct)
(auto intro: rtranclp_cdcl⇩W_restart_no_false_clause cdcl⇩W_restart_conflict_non_zero_unless_level_0)
definition propagated_clauses_clauses :: "'st ⇒ bool" where
‹propagated_clauses_clauses S ≡ ∀L K. Propagated L K ∈ set (trail S) ⟶ K ∈# clauses S›
lemma propagate_single_literal_clause_get_level_is_0:
assumes
smaller: ‹no_smaller_propa S› and
propa_tr: ‹Propagated L {#L#} ∈ set (trail S)› and
n_d: ‹no_dup (trail S)› and
propa: ‹propagated_clauses_clauses S›
shows ‹get_level (trail S) L = 0›
proof (rule ccontr)
assume H: ‹¬ ?thesis›
then obtain M M' K where
tr: ‹trail S = M' @ Decided K # M› and
nm: ‹∀m ∈ set M. ¬is_decided m›
using split_list_last_prop[of "trail S" is_decided]
by (auto simp: filter_empty_conv is_decided_def get_level_def dest!: List.set_dropWhileD)
have uL: ‹-L ∉ lits_of_l (trail S)›
using n_d propa_tr unfolding lits_of_def by (fastforce simp: no_dup_cannot_not_lit_and_uminus)
then have [iff]: ‹defined_lit M' L ⟷ L ∈ lits_of_l M'›
by (auto simp add: tr Decided_Propagated_in_iff_in_lits_of_l)
have ‹get_level M L = 0› for L
using nm by auto
have [simp]: ‹L ≠ -K›
using tr propa_tr n_d unfolding lits_of_def by (fastforce simp: no_dup_cannot_not_lit_and_uminus
in_set_conv_decomp)
have ‹L ∈ lits_of_l (M' @ [Decided K])›
apply (rule ccontr)
using H unfolding tr
apply (subst (asm) get_level_skip)
using uL tr apply (auto simp: atm_of_eq_atm_of Decided_Propagated_in_iff_in_lits_of_l; fail)[]
apply (subst (asm) get_level_skip_beginning)
using ‹get_level M L = 0› by (auto simp: atm_of_eq_atm_of uminus_lit_swap lits_of_def)
then have ‹undefined_lit M L›
using n_d unfolding tr by (auto simp: defined_lit_map lits_of_def image_Un no_dup_def)
moreover have "{#} + {#L#} ∈# clauses S"
using propa propa_tr unfolding propagated_clauses_clauses_def by auto
moreover have "M ⊨as CNot {#}"
by auto
ultimately show False
using smaller tr unfolding no_smaller_propa_def by blast
qed
subsubsection ‹Conflict Minimisation›
paragraph ‹Remove Literals of Level 0›
lemma conflict_minimisation_level_0:
fixes S :: 'st
defines D[simp]: ‹D ≡ the (conflicting S)›
defines [simp]: ‹M ≡ trail S›
defines ‹D' ≡ filter_mset (λL. get_level M L > 0) D›
assumes
ns_s: ‹no_step skip S› and
ns_r: ‹no_step resolve S› and
inv_s: "cdcl⇩W_stgy_invariant S" and
inv: "cdcl⇩W_all_struct_inv S" and
conf: ‹conflicting S ≠ None› ‹conflicting S ≠ Some {#}› and
M_nempty: ‹M ~= []›
shows
"clauses S ⊨pm D'" and
‹- lit_of (hd M) ∈# D'›
proof -
define D0 where D0: ‹D0 = filter_mset (λL. get_level M L = 0) D›
have D_D0_D': ‹D = D0 + D'›
using multiset_partition[of D ‹(λL. get_level M L = 0)›]
unfolding D0 D'_def by auto
have
confl: ‹cdcl⇩W_conflicting S› and
decomp: ‹all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S))› and
learned: ‹cdcl⇩W_learned_clause S› and
M_lev: ‹cdcl⇩W_M_level_inv S› and
alien: ‹no_strange_atm S›
using inv unfolding cdcl⇩W_all_struct_inv_def by fast+
have clss_D: ‹clauses S ⊨pm D›
using learned conf unfolding cdcl⇩W_learned_clause_alt_def by auto
have M_CNot_D: ‹trail S ⊨as CNot D› and m_confl: ‹every_mark_is_a_conflict S›
using conf confl unfolding cdcl⇩W_conflicting_def by auto
have n_d: ‹no_dup M›
using M_lev unfolding cdcl⇩W_M_level_inv_def by auto
have uhd_D: ‹- lit_of (hd M) ∈# D›
using ns_s ns_r conf M_nempty inv_s M_CNot_D n_d
unfolding cdcl⇩W_stgy_invariant_def conflict_is_false_with_level_def
by (cases ‹trail S›; cases ‹hd (trail S)›) (auto simp: skip.simps resolve.simps
get_level_cons_if atm_of_eq_atm_of true_annots_true_cls_def_iff_negation_in_model
uminus_lit_swap Decided_Propagated_in_iff_in_lits_of_l split: if_splits)
have count_dec_ge_0: ‹count_decided M > 0›
proof (rule ccontr)
assume H: ‹~ ?thesis›
then have ‹get_maximum_level M D = 0› for D
by (metis (full_types) count_decided_ge_get_maximum_level gr0I le_0_eq)
then show False
using ns_s ns_r conf M_nempty m_confl uhd_D H
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto 5 5 simp: skip.simps resolve.simps intro!: state_eq_ref)
qed
then obtain M0 K M1 where
M: ‹M = M1 @ Decided K # M0› and
lev_K: ‹get_level (trail S) K = Suc 0›
using backtrack_ex_decomp[of S 0, OF ] M_lev
by (auto dest!: get_all_ann_decomposition_exists_prepend
simp: cdcl⇩W_M_level_inv_def simp flip: append.assoc
simp del: append_assoc)
have count_M0: ‹count_decided M0 = 0›
using n_d lev_K unfolding M_def[symmetric] M by auto
have [simp]: ‹get_all_ann_decomposition M0 = [([], M0)]›
using count_M0 by (induction M0 rule: ann_lit_list_induct) auto
have [simp]: ‹get_all_ann_decomposition (M1 @ Decided K # M0) ≠ [([], M0)]› for M1 K M0
using length_get_all_ann_decomposition[of ‹M1 @ Decided K # M0›]
unfolding M by auto
have ‹last (get_all_ann_decomposition (M1 @ Decided K # M0)) = ([], M0)›
apply (induction M1 rule: ann_lit_list_induct)
subgoal by auto
subgoal by auto
subgoal for L m M1
by (cases ‹get_all_ann_decomposition (M1 @ Decided K # M0)›) auto
done
then have clss_S_M0: ‹set_mset (clauses S) ⊨ps unmark_l M0›
using decomp unfolding M_def[symmetric] M
by (cases ‹get_all_ann_decomposition (M1 @ Decided K # M0)› rule: rev_cases)
(auto simp: all_decomposition_implies_def)
have H: ‹total_over_m I (set_mset (clauses S) ∪ unmark_l M0) = total_over_m I (set_mset (clauses S))›
for I
using alien unfolding no_strange_atm_def total_over_m_def total_over_set_def
M_def[symmetric] M
by (auto simp: clauses_def)
have uL_M0_D0: ‹-L ∈ lits_of_l M0› if ‹L ∈# D0› for L
proof (rule ccontr)
assume L_M0: ‹~ ?thesis›
have ‹L ∈# D› and lev_L: ‹get_level M L = 0›
using that unfolding D_D0_D' unfolding D0 by auto
then have ‹-L ∈ lits_of_l M›
using M_CNot_D that by (auto simp: true_annots_true_cls_def_iff_negation_in_model)
then have ‹-L ∈ lits_of_l (M1 @ [Decided K])›
using L_M0 unfolding M by auto
then have ‹0 < get_level (M1 @ [Decided K]) L› and ‹defined_lit (M1 @ [Decided K]) L›
using get_level_last_decided_ge[of M1 K L] unfolding Decided_Propagated_in_iff_in_lits_of_l
by fast+
then show False
using n_d lev_L get_level_skip_end[of ‹M1 @ [Decided K]› L M0]
unfolding M by auto
qed
have clss_D0: ‹clauses S ⊨pm {#- L#}› if ‹L ∈# D0› for L
using that clss_S_M0 uL_M0_D0[of L] unfolding true_clss_clss_def H true_clss_cls_def
true_clss_def lits_of_def
by auto
have lD0D': ‹l ∈ atms_of D0 ⟹ l ∈ atms_of D› ‹l ∈ atms_of D' ⟹ l ∈ atms_of D› for l
unfolding D_D0_D' by auto
have
H1: ‹total_over_m I (set_mset (clauses S) ∪ {{#-L#}}) = total_over_m I (set_mset (clauses S))›
if ‹L ∈# D0› for L
using alien conf atm_of_lit_in_atms_of[OF that]
unfolding no_strange_atm_def total_over_m_def total_over_set_def
M_def[symmetric] M that by (auto 5 5 simp: clauses_def dest!: lD0D')
then have I_D0: ‹total_over_m I (set_mset (clauses S)) ⟶
consistent_interp I ⟶
Multiset.Ball (clauses S) ((⊨) I) ⟶ ~I ⊨ D0› for I
using clss_D0 unfolding true_clss_cls_def true_cls_def consistent_interp_def
true_cls_def true_cls_mset_def
apply auto
by (metis atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set literal.sel(1)
true_cls_def true_cls_mset_def true_lit_def uminus_Pos)
have
H1: ‹total_over_m I (set_mset (clauses S) ∪ {D0 + D'}) = total_over_m I (set_mset (clauses S))› and
H2: ‹total_over_m I (set_mset (clauses S) ∪ {D'}) = total_over_m I (set_mset (clauses S))› for I
using alien conf unfolding no_strange_atm_def total_over_m_def total_over_set_def
M_def[symmetric] M by (auto 5 5 simp: clauses_def dest!: lD0D')
show ‹clauses S ⊨pm D'›
using clss_D clss_D0 I_D0 unfolding D_D0_D' true_clss_cls_def true_clss_def H1 H2
by auto
have ‹0 < get_level (trail S) (lit_of (hd_trail S))›
apply (cases ‹trail S›)
using M_nempty count_dec_ge_0 by auto
then show ‹- lit_of (hd M) ∈# D'›
using uhd_D unfolding D'_def by auto
qed
lemma literals_of_level0_entailed:
assumes
struct_invs: ‹cdcl⇩W_all_struct_inv S› and
in_trail: ‹L ∈ lits_of_l (trail S)› and
lev: ‹get_level (trail S) L = 0›
shows
‹clauses S ⊨pm {#L#}›
proof -
have decomp: ‹all_decomposition_implies_m (clauses S) (get_all_ann_decomposition (trail S))›
using struct_invs unfolding cdcl⇩W_all_struct_inv_def
by fast
have L_trail: ‹{#L#} ∈ unmark_l (trail S)›
using in_trail by (auto simp: in_unmark_l_in_lits_of_l_iff)
have n_d: ‹no_dup (trail S)›
using struct_invs unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def
by fast
show ?thesis
proof (cases ‹count_decided (trail S) = 0›)
case True
have ‹get_all_ann_decomposition (trail S) = [([], trail S)]›
apply (rule no_decision_get_all_ann_decomposition)
using True by (auto simp: count_decided_0_iff)
then show ?thesis
using decomp L_trail
unfolding all_decomposition_implies_def
by (auto intro: true_clss_clss_in_imp_true_clss_cls)
next
case False
then obtain K M1 M2 M3 where
decomp': ‹(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))› and
lev_K: ‹get_level (trail S) K = Suc 0› and
M3: ‹trail S = M3 @ M2 @ Decided K # M1›
using struct_invs backtrack_ex_decomp[of S 0] n_d unfolding cdcl⇩W_all_struct_inv_def by blast
then have dec_M1: ‹count_decided M1 = 0›
using n_d by auto
define M2' where ‹M2' = M3 @ M2›
then have M3: ‹trail S = M2' @ Decided K # M1› using M3 by auto
have ‹get_all_ann_decomposition M1 = [([], M1)]›
apply (rule no_decision_get_all_ann_decomposition)
using dec_M1 by (auto simp: count_decided_0_iff)
then have ‹([], M1) ∈ set (get_all_ann_decomposition (trail S))›
using hd_get_all_ann_decomposition_skip_some[of Nil M1 M1 ‹_ @ _›] decomp'
by auto
then have ‹set_mset (clauses S) ⊨ps unmark_l M1›
using decomp
unfolding all_decomposition_implies_def by auto
moreover {
have ‹L ∈ lits_of_l M1›
using n_d lev M3 in_trail
by (cases ‹undefined_lit (M2' @ Decided K # []) L›) (auto dest: in_lits_of_l_defined_litD)
then have ‹{#L#} ∈ unmark_l M1›
using in_trail by (auto simp: in_unmark_l_in_lits_of_l_iff)
}
ultimately show ?thesis
unfolding all_decomposition_implies_def
by (auto intro: true_clss_clss_in_imp_true_clss_cls)
qed
qed
subsection ‹Some higher level use on the invariants›
text ‹In later refinement we mostly us the group invariants and don't try to be as specific
as above. The corresponding theorems are collected here.
›
lemma conflict_conflict_is_false_with_level_all_inv:
‹conflict S T ⟹
no_smaller_confl S ⟹
cdcl⇩W_all_struct_inv S ⟹
conflict_is_false_with_level T›
by (rule conflict_conflict_is_false_with_level) (auto simp: cdcl⇩W_all_struct_inv_def)
lemma cdcl⇩W_stgy_ex_lit_of_max_level_all_inv:
assumes
"cdcl⇩W_stgy S S'" and
n_l: "no_smaller_confl S" and
"conflict_is_false_with_level S" and
"cdcl⇩W_all_struct_inv S"
shows "conflict_is_false_with_level S'"
by (rule cdcl⇩W_stgy_ex_lit_of_max_level) (use assms in ‹auto simp: cdcl⇩W_all_struct_inv_def›)
lemma cdcl⇩W_o_conflict_is_false_with_level_inv_all_inv:
assumes
‹cdcl⇩W_o S T›
‹cdcl⇩W_all_struct_inv S›
‹conflict_is_false_with_level S›
shows ‹conflict_is_false_with_level T›
by (rule cdcl⇩W_o_conflict_is_false_with_level_inv)
(use assms in ‹auto simp: cdcl⇩W_all_struct_inv_def›)
lemma no_step_cdcl⇩W_total:
assumes
‹no_step cdcl⇩W S›
‹conflicting S = None›
‹no_strange_atm S›
shows ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain L where ‹L ∈ atms_of_mm (clauses S)› and ‹undefined_lit (trail S) (Pos L)›
by (auto simp: total_over_m_def total_over_set_def
Decided_Propagated_in_iff_in_lits_of_l)
then have ‹Ex (decide S)›
using decide_rule[of S ‹Pos L› ‹cons_trail (Decided (Pos L)) S›] assms
unfolding no_strange_atm_def clauses_def
by force
then show False
using assms by (auto simp: cdcl⇩W.simps cdcl⇩W_o.simps)
qed
lemma cdcl⇩W_Ex_cdcl⇩W_stgy:
assumes
‹cdcl⇩W S T›
shows ‹Ex(cdcl⇩W_stgy S)›
using assms by (meson assms cdcl⇩W.simps cdcl⇩W_stgy.simps)
lemma no_step_skip_hd_in_conflicting:
assumes
inv_s: ‹cdcl⇩W_stgy_invariant S› and
inv: ‹cdcl⇩W_all_struct_inv S› and
ns: ‹no_step skip S› and
confl: ‹conflicting S ≠ None› ‹conflicting S ≠ Some {#}›
shows ‹-lit_of (hd (trail S)) ∈# the (conflicting S)›
proof -
let
?M = ‹trail S› and
?N = ‹init_clss S› and
?U = ‹learned_clss S› and
?k = ‹backtrack_lvl S› and
?D = ‹conflicting S›
obtain D where D: ‹?D = Some D›
using confl by (cases ?D) auto
have M_D: ‹?M ⊨as CNot D›
using inv D unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_conflicting_def by auto
then have tr: ‹trail S ≠ []›
using confl D by auto
obtain L M where M: ‹?M = L # M›
using tr by (cases ‹?M›) auto
have conlf_k: ‹conflict_is_false_with_level S›
using inv_s unfolding cdcl⇩W_stgy_invariant_def by simp
then obtain L_k where
L_k: ‹L_k ∈# D› and lev_L_k: ‹get_level ?M L_k = ?k›
using confl D by auto
have dec: ‹?k = count_decided ?M›
using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
moreover {
have ‹no_dup ?M›
using inv unfolding cdcl⇩W_all_struct_inv_def cdcl⇩W_M_level_inv_def by auto
then have ‹-lit_of L ∉ lits_of_l M›
unfolding M by (auto simp: defined_lit_map lits_of_def uminus_lit_swap)
}
ultimately have L_D: ‹lit_of L ∉# D›
using M_D unfolding M by (auto simp add: true_annots_true_cls_def_iff_negation_in_model
uminus_lit_swap)
show ?thesis
proof (cases L)
case (Decided L') note L' = this(1)
moreover have ‹atm_of L' = atm_of L_k›
using lev_L_k count_decided_ge_get_level[of M L_k] unfolding M dec L'
by (auto simp: get_level_cons_if split: if_splits)
then have ‹L' = -L_k›
using L_k L_D L' by (auto simp: atm_of_eq_atm_of)
then show ?thesis using L_k unfolding D M L' by simp
next
case (Propagated L' C)
then show ?thesis
using ns confl by (auto simp: skip.simps M D)
qed
qed
lemma
fixes S
assumes
nss: ‹no_step skip S› and
nsr: ‹no_step resolve S› and
invs: ‹cdcl⇩W_all_struct_inv S› and
stgy: ‹cdcl⇩W_stgy_invariant S› and
confl: ‹conflicting S ≠ None› and
confl': ‹conflicting S ≠ Some {#}›
shows no_skip_no_resolve_single_highest_level:
‹the (conflicting S) =
add_mset (-(lit_of (hd (trail S)))) {#L ∈# the (conflicting S).
get_level (trail S) L < local.backtrack_lvl S#}› (is ?A) and
no_skip_no_resolve_level_lvl_nonzero:
‹0 < backtrack_lvl S› (is ?B) and
no_skip_no_resolve_level_get_maximum_lvl_le:
‹get_maximum_level (trail S) (remove1_mset (-(lit_of (hd (trail S)))) (the (conflicting S)))
< backtrack_lvl S› (is ?C)
proof -
define K where ‹K ≡ lit_of (hd (trail S))›
have K: ‹-K ∈# the (conflicting S)›
using no_step_skip_hd_in_conflicting[OF stgy invs nss confl confl']
unfolding K_def .
have
‹no_strange_atm S› and
lev: ‹cdcl⇩W_M_level_inv S› and
‹∀s∈#learned_clss S. ¬ tautology s› and
dist: ‹distinct_cdcl⇩W_state S› and
conf: ‹cdcl⇩W_conflicting S› and
‹all_decomposition_implies_m (local.clauses S)
(get_all_ann_decomposition (trail S))› and
learned: ‹cdcl⇩W_learned_clause S›
using invs unfolding cdcl⇩W_all_struct_inv_def
by auto
obtain D where
D[simp]: ‹conflicting S = Some (add_mset (-K) D)›
using confl K by (auto dest: multi_member_split)
have dist: ‹distinct_mset (the (conflicting S))›
using dist confl unfolding distinct_cdcl⇩W_state_def by auto
then have [iff]: ‹L ∉# remove1_mset L (the (conflicting S))› for L
by (meson distinct_mem_diff_mset union_single_eq_member)
from this[of K] have [simp]: ‹-K ∉# D› using dist by auto
have nd: ‹no_dup (trail S)›
using lev unfolding cdcl⇩W_M_level_inv_def by auto
have CNot: ‹trail S ⊨as CNot (add_mset (-K) D)›
using conf unfolding cdcl⇩W_conflicting_def
by fastforce
then have tr: ‹trail S ≠ []›
by auto
have [simp]: ‹K ∉# D›
using nd K_def tr CNot unfolding true_annots_true_cls_def_iff_negation_in_model
by (cases ‹trail S›)
(auto simp: uminus_lit_swap Decided_Propagated_in_iff_in_lits_of_l dest!: multi_member_split)
have H1:
‹0 < backtrack_lvl S›
proof (cases ‹is_proped (hd (trail S))›)
case proped: True
obtain C M where
[simp]: ‹trail S = Propagated K C # M›
using tr proped K_def
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: K_def)
have ‹a @ Propagated L mark # b = Propagated K C # M ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› for L mark a b
using conf unfolding cdcl⇩W_conflicting_def
by fastforce
from this[of ‹[]›] have [simp]: ‹K ∈# C› ‹M ⊨as CNot (remove1_mset K C)›
by auto
have [simp]: ‹get_maximum_level (Propagated K C # M) D = get_maximum_level M D›
by (rule get_maximum_level_skip_first)
(auto simp: atms_of_def atm_of_eq_atm_of uminus_lit_swap[symmetric])
have ‹get_maximum_level M D < count_decided M›
using nsr tr confl K proped count_decided_ge_get_maximum_level[of M D]
by (auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
then show ?thesis by simp
next
case proped: False
have ‹get_maximum_level (tl (trail S)) D < count_decided (trail S)›
using tr confl K proped count_decided_ge_get_maximum_level[of ‹tl (trail S)› D]
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
then show ?thesis
by simp
qed
show H2: ?C
proof (cases ‹is_proped (hd (trail S))›)
case proped: True
obtain C M where
[simp]: ‹trail S = Propagated K C # M›
using tr proped K_def
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: K_def)
have ‹a @ Propagated L mark # b = Propagated K C # M ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› for L mark a b
using conf unfolding cdcl⇩W_conflicting_def
by fastforce
from this[of ‹[]›] have [simp]: ‹K ∈# C› ‹M ⊨as CNot (remove1_mset K C)›
by auto
have [simp]: ‹get_maximum_level (Propagated K C # M) D = get_maximum_level M D›
by (rule get_maximum_level_skip_first)
(auto simp: atms_of_def atm_of_eq_atm_of uminus_lit_swap[symmetric])
have ‹get_maximum_level M D < count_decided M›
using nsr tr confl K proped count_decided_ge_get_maximum_level[of M D]
by (auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
then show ?thesis by simp
next
case proped: False
have ‹get_maximum_level (tl (trail S)) D = get_maximum_level (trail S) D›
apply (rule get_maximum_level_cong)
using K_def ‹- K ∉# D› ‹K ∉# D›
apply (cases ‹trail S›)
by (auto simp: get_level_cons_if atm_of_eq_atm_of)
moreover have ‹get_maximum_level (tl (trail S)) D < count_decided (trail S)›
using tr confl K proped count_decided_ge_get_maximum_level[of ‹tl (trail S)› D]
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
ultimately show ?thesis
by (simp add: K_def)
qed
have H:
‹get_level (trail S) L < local.backtrack_lvl S›
if ‹L ∈# remove1_mset (-K) (the (conflicting S))›
for L
proof (cases ‹is_proped (hd (trail S))›)
case proped: True
obtain C M where
[simp]: ‹trail S = Propagated K C # M›
using tr proped K_def
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: K_def)
have ‹a @ Propagated L mark # b = Propagated K C # M ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› for L mark a b
using conf unfolding cdcl⇩W_conflicting_def
by fastforce
from this[of ‹[]›] have [simp]: ‹K ∈# C› ‹M ⊨as CNot (remove1_mset K C)›
by auto
have [simp]: ‹get_maximum_level (Propagated K C # M) D = get_maximum_level M D›
by (rule get_maximum_level_skip_first)
(auto simp: atms_of_def atm_of_eq_atm_of uminus_lit_swap[symmetric])
have ‹get_maximum_level M D < count_decided M›
using nsr tr confl K that proped count_decided_ge_get_maximum_level[of M D]
by (auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
then show ?thesis
using get_maximum_level_ge_get_level[of L D M] that
by (auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
next
case proped: False
have L_K: ‹L ≠ - K› ‹-L ≠ K› ‹L ≠ -lit_of (hd (trail S))›
using that by (auto simp: uminus_lit_swap K_def[symmetric])
have ‹L ≠ lit_of (hd (trail S))›
using tr that K_def ‹K ∉# D›
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
have ‹get_maximum_level (tl (trail S)) D < count_decided (trail S)›
using tr confl K that proped count_decided_ge_get_maximum_level[of ‹tl (trail S)› D]
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
then show ?thesis
using get_maximum_level_ge_get_level[of L D ‹(trail S)›] that tr L_K ‹L ≠ lit_of (hd (trail S))›
count_decided_ge_get_level[of ‹tl (trail S)› L] proped
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
qed
have [simp]: ‹get_level (trail S) K = local.backtrack_lvl S›
using tr K_def
by (cases ‹trail S›; cases ‹hd (trail S)›)
(auto simp: resolve.simps get_level_cons_if atm_of_eq_atm_of)
show ?A
apply (rule distinct_set_mset_eq)
subgoal using dist by auto
subgoal using dist by (auto simp: distinct_mset_filter K_def[symmetric])
subgoal using H by (auto simp: K_def[symmetric])
done
show ?B
using H1 .
qed
end
end