Theory CDCL

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 ― ‹functions about the state:› ― ‹getter:› trail init_clss learned_clss conflicting ― ‹setter:› cons_trail tl_trail add_learned_cls remove_cls update_conflicting ― ‹Some specific states:› 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 ― ‹functions about the state:› ― ‹getter:› trail init_clss learned_clss conflicting ― ‹setter:› cons_trail tl_trail add_learned_cls remove_cls update_conflicting ― ‹Some specific states:› 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 (* non-standard to avoid name clash with NOT's clauses_tl_trail *) 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, opaque_lifting) 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 ― ‹end of ‹state_W› locale› 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 ― ‹functions for the state:› ― ‹access functions:› trail init_clss learned_clss conflicting ― ‹changing state:› cons_trail tl_trail add_learned_cls remove_cls update_conflicting ― ‹get state:› 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 (* \htmllink{cdcl-decide-def} *) 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 ∈ ⋃ (atms_of`(set_mset (init_clss S)))" 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: (* \htmllink{rtranclp_distinct_cdclW_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₀ = "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₀" using cdcl_W_restart.other[OF cdcl_W_o.decide[OF decide_rule[of S L ?S₀]]] S by auto then have "cdcl_W_restart^*^* (init_state N) ?S₀" using st by auto then show ?case using S undef by (auto intro!: exI[of _ ?S₀] 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: (* \htmllink{full_cdclW_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_cong: ‹S ∼ T ⟹ cdcl_W_all_struct_inv S ⟷ cdcl_W_all_struct_inv T› unfolding cdcl_W_all_struct_inv_def no_strange_atm_def cdcl_W_M_level_inv_def distinct_cdcl_W_state_def cdcl_W_learned_clause_def reasons_in_clauses_def cdcl_W_conflicting_def by auto 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_no_smaller_confl inv_s unfolding cdcl_W_stgy_invariant_def 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 unfolding no_smaller_propa_def by (cases ‹trail S›) (auto simp del: state_simp) 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 ― ‹TODO tune proof› 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

Theory CDCL_W