theory DPLL_NOT imports CDCL_NOT begin section ‹DPLL as an instance of NOT› subsection ‹DPLL with simple backtrack› locale dpll_with_backtrack begin inductive backtrack :: "('v, unit, unit) ann_literal list × 'v clauses ⇒ ('v, unit, unit) ann_literal list × 'v clauses ⇒ bool" where "backtrack_split (fst S) = (M', L # M) ⟹ is_decided L ⟹ D ∈# snd S ⟹ fst S ⊨as CNot D ⟹ backtrack S (Propagated (- (lit_of L)) () # M, snd S)" inductive_cases backtrackE[elim]: "backtrack (M, N) (M', N')" lemma backtrack_is_backjump: fixes M M' :: "('v, unit, unit) ann_literal list" assumes backtrack: "backtrack (M, N) (M', N')" and no_dup: "(no_dup ∘ fst) (M, N)" and decomp: "all_decomposition_implies_m N (get_all_decided_decomposition M)" shows " ∃C F' K F L l C'. M = F' @ Decided K () # F ∧ M' = Propagated L l # F ∧ N = N' ∧ C ∈# N ∧ F' @ Decided K d # F ⊨as CNot C ∧ undefined_lit F L ∧ atm_of L ∈ atms_of_msu N ∪ atm_of ` lits_of (F' @ Decided K d # F) ∧ N ⊨pm C' + {#L#} ∧ F ⊨as CNot C'" proof - let ?S = "(M, N)" let ?T = "(M', N')" obtain F F' P L D where b_sp: "backtrack_split M = (F', L # F)" and "is_decided L" and "D ∈# snd ?S" and "M ⊨as CNot D" and bt: "backtrack ?S (Propagated (- (lit_of L)) P # F, N)" and M': "M' = Propagated (- (lit_of L)) P # F" and [simp]: "N' = N" using backtrackE[OF backtrack] by (metis backtrack fstI sndI) let ?K = "lit_of L" let ?C = "image_mset lit_of {#K∈#mset M. is_decided K ∧ K≠L#} :: 'v literal multiset" let ?C' = "set_mset (image_mset single (?C+{#?K#}))" obtain K where L: "L = Decided K ()" using ‹is_decided L› by (cases L) auto have M: "M = F' @ Decided K () # F" using b_sp by (metis L backtrack_split_list_eq fst_conv snd_conv) moreover have "F' @ Decided K () # F ⊨as CNot D" using ‹M⊨as CNot D› unfolding M . moreover have "undefined_lit F (-?K)" using no_dup unfolding M L by (simp add: defined_lit_map) moreover have "atm_of (-K) ∈ atms_of_msu N ∪ atm_of ` lits_of (F' @ Decided K d # F)" by auto moreover have "set_mset N ∪ ?C' ⊨ps {{#}}" proof - have A: "set_mset N ∪ ?C' ∪ unmark M = set_mset N ∪ unmark M" unfolding M L by auto have "set_mset N ∪ {{#lit_of L#} |L. is_decided L ∧ L ∈ set M} ⊨ps unmark M" using all_decomposition_implies_propagated_lits_are_implied[OF decomp] . moreover have C': "?C' = {{#lit_of L#} |L. is_decided L ∧ L ∈ set M}" unfolding M L apply standard apply force using IntI by auto ultimately have N_C_M: "set_mset N ∪ ?C' ⊨ps unmark M" by auto have "set_mset N ∪ (λL. {#lit_of L#}) ` (set M) ⊨ps {{#}}" unfolding true_clss_clss_def proof (intro allI impI, goal_cases) case (1 I) note tot = this(1) and cons = this(2) and I_N_M = this(3) have "I ⊨ D" using I_N_M ‹D ∈# snd ?S› unfolding true_clss_def by auto moreover have "I ⊨s CNot D" using ‹M ⊨as CNot D› unfolding M by (metis "1"(3) ‹M ⊨as CNot D› true_annots_true_cls true_cls_mono_set_mset_l true_clss_def true_clss_singleton_lit_of_implies_incl true_clss_union) ultimately show ?case using cons consistent_CNot_not by blast qed then show ?thesis using true_clss_clss_left_right[OF N_C_M, of "{{#}}"] unfolding A by auto qed have "N ⊨pm image_mset uminus ?C + {#-?K#}" unfolding true_clss_cls_def true_clss_clss_def total_over_m_def proof (intro allI impI) fix I assume tot: "total_over_set I (atms_of_ms (set_mset N ∪ {image_mset uminus ?C + {#- ?K#}})) " and cons: "consistent_interp I" and "I ⊨sm N" have "(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)" using cons tot unfolding consistent_interp_def L by (cases K) auto have tI: "total_over_set I (atm_of ` lit_of ` (set M ∩ {L. is_decided L ∧ L ≠ Decided K d}))" using tot by (auto simp add: L atms_of_uminus_lit_atm_of_lit_of) then have H: "⋀x. lit_of x ∉ I ⟹ x ∈ set M ⟹is_decided x ⟹ x ≠ Decided K d ⟹ -lit_of x ∈ I" proof - fix x :: "('v, unit, unit) ann_literal" assume a1: "x ≠ Decided K d" assume a2: "is_decided x" assume a3: "x ∈ set M" assume a4: "lit_of x ∉ I" have "atm_of (lit_of x) ∈ atm_of ` lit_of ` (set M ∩ {m. is_decided m ∧ m ≠ Decided K d})" using a3 a2 a1 by blast then have "Pos (atm_of (lit_of x)) ∈ I ∨ Neg (atm_of (lit_of x)) ∈ I" using tI unfolding total_over_set_def by blast then show "- lit_of x ∈ I" using a4 by (metis (no_types) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set literal.sel(1,2)) qed have "¬I ⊨s ?C'" using ‹set_mset N ∪ ?C' ⊨ps {{#}}› tot cons ‹I ⊨sm N› unfolding true_clss_clss_def total_over_m_def by (simp add: atms_of_uminus_lit_atm_of_lit_of atms_of_ms_single_image_atm_of_lit_of) then show "I ⊨ image_mset uminus ?C + {#- lit_of L#}" unfolding true_clss_def true_cls_def Bex_mset_def using ‹(K ∈ I ∧ -K ∉ I) ∨ (-K ∈ I ∧ K ∉ I)› unfolding L by (auto dest!: H) qed moreover have "set F' ∩ {K. is_decided K ∧ K ≠ L} = {}" using backtrack_split_fst_not_decided[of _ M] b_sp by auto then have "F ⊨as CNot (image_mset uminus ?C)" unfolding M CNot_def true_annots_def by (auto simp add: L lits_of_def) ultimately show ?thesis using M' ‹D ∈# snd ?S› L by force qed lemma backtrack_is_backjump': fixes M M' :: "('v, unit, unit) ann_literal list" assumes backtrack: "backtrack S T" and no_dup: "(no_dup ∘ fst) S" and decomp: "all_decomposition_implies_m (snd S) (get_all_decided_decomposition (fst S))" shows " ∃C F' K F L l C'. fst S = F' @ Decided K () # F ∧ T = (Propagated L l # F, snd S) ∧ C ∈# snd S ∧ fst S ⊨as CNot C ∧ undefined_lit F L ∧ atm_of L ∈ atms_of_msu (snd S) ∪ atm_of ` lits_of (fst S) ∧ snd S ⊨pm C' + {#L#} ∧ F ⊨as CNot C'" apply (cases S, cases T) using backtrack_is_backjump[of "fst S" "snd S" "fst T" "snd T"] assms by fastforce sublocale dpll_state fst snd "λL (M, N). (L # M, N)" "λ(M, N). (tl M, N)" "λC (M, N). (M, {#C#} + N)" "λC (M, N). (M, remove_mset C N)" by unfold_locales auto sublocale backjumping_ops fst snd "λL (M, N). (L # M, N)" "λ(M, N). (tl M, N)" "λC (M, N). (M, {#C#} + N)" "λC (M, N). (M, remove_mset C N)" "λ_ _ _ S T. backtrack S T" by unfold_locales lemma backtrack_is_backjump'': fixes M M' :: "('v, unit, unit) ann_literal list" assumes backtrack: "backtrack S T" and no_dup: "(no_dup ∘ fst) S" and decomp: "all_decomposition_implies_m (snd S) (get_all_decided_decomposition (fst S))" shows "backjump S T" proof - obtain C F' K F L l C' where 1: "fst S = F' @ Decided K () # F" and 2: "T = (Propagated L l # F, snd S)" and 3: "C ∈# snd S" and 4: "fst S ⊨as CNot C" and 5: "undefined_lit F L" and 6: "atm_of L ∈ atms_of_msu (snd S) ∪ atm_of ` lits_of (fst S)" and 7: "snd S ⊨pm C' + {#L#}" and 8: "F ⊨as CNot C'" using backtrack_is_backjump'[OF assms] by blast show ?thesis using backjump.intros[OF 1 _ 3 4 5 6 7 8] 2 backtrack 1 5 by (auto simp: state_eq⇩N⇩O⇩T_def simp del: state_simp⇩N⇩O⇩T) qed lemma can_do_bt_step: assumes M: "fst S = F' @ Decided K d # F" and "C ∈# snd S" and C: "fst S ⊨as CNot C" shows "¬ no_step backtrack S" proof - obtain L G' G where "backtrack_split (fst S) = (G', L # G)" unfolding M by (induction F' rule: ann_literal_list_induct) auto moreover then have "is_decided L" by (metis backtrack_split_snd_hd_decided list.distinct(1) list.sel(1) snd_conv) ultimately show ?thesis using backtrack.intros[of S G' L G C] ‹C ∈# snd S› C unfolding M by auto qed end sublocale dpll_with_backtrack ⊆ dpll_with_backjumping_ops fst snd "λL (M, N). (L # M, N)" "λ(M, N). (tl M, N)" "λC (M, N). (M, {#C#} + N)" "λC (M, N). (M, remove_mset C N)" "λ_ _. True" "λ(M, N). no_dup M ∧ all_decomposition_implies_m N (get_all_decided_decomposition M)" "λ_ _ _ S T. backtrack S T" by unfold_locales (metis (mono_tags, lifting) dpll_with_backtrack.backtrack_is_backjump'' dpll_with_backtrack.can_do_bt_step prod.case_eq_if comp_apply) sublocale dpll_with_backtrack ⊆ dpll_with_backjumping fst snd "λL (M, N). (L # M, N)" "λ(M, N). (tl M, N)" "λC (M, N). (M, {#C#} + N)" "λC (M, N). (M, remove_mset C N)" "λ_ _. True" "λ(M, N). no_dup M ∧ all_decomposition_implies_m N (get_all_decided_decomposition M)" "λ_ _ _ S T. backtrack S T" apply unfold_locales using dpll_bj_no_dup dpll_bj_all_decomposition_implies_inv apply fastforce done sublocale dpll_with_backtrack ⊆ conflict_driven_clause_learning_ops fst snd "λL (M, N). (L # M, N)" "λ(M, N). (tl M, N)" "λC (M, N). (M, {#C#} + N)" "λC (M, N). (M, remove_mset C N)" "λ_ _. True" "λ(M, N). no_dup M ∧ all_decomposition_implies_m N (get_all_decided_decomposition M)" "λ_ _ _ S T. backtrack S T" "λ_ _. False" "λ_ _. False" by unfold_locales sublocale dpll_with_backtrack ⊆ conflict_driven_clause_learning fst snd "λL (M, N). (L # M, N)" "λ(M, N). (tl M, N)" "λC (M, N). (M, {#C#} + N)" "λC (M, N). (M, remove_mset C N)" "λ_ _. True" "λ(M, N). no_dup M ∧ all_decomposition_implies_m N (get_all_decided_decomposition M)" "λ_ _ _ S T. backtrack S T" "λ_ _. False" "λ_ _. False" apply unfold_locales using cdcl⇩N⇩O⇩T.simps dpll_bj_inv forget⇩N⇩O⇩TE learn⇩N⇩O⇩TE by blast context dpll_with_backtrack begin lemma wf_tranclp_dpll_inital_state: assumes fin: "finite A" shows "wf {((M'::('v, unit, unit) ann_literals, N'::'v clauses), ([], N))|M' N' N. dpll_bj⇧+⇧+ ([], N) (M', N') ∧ atms_of_msu N ⊆ atms_of_ms A}" using wf_tranclp_dpll_bj[OF assms(1)] by (rule wf_subset) auto corollary full_dpll_final_state_conclusive: fixes M M' :: "('v, unit, unit) ann_literal list" assumes full: "full dpll_bj ([], N) (M', N')" shows "unsatisfiable (set_mset N) ∨ (M' ⊨asm N ∧ satisfiable (set_mset N))" using assms full_dpll_backjump_final_state[of "([],N)" "(M', N')" "set_mset N"] by auto corollary full_dpll_normal_form_from_init_state: fixes M M' :: "('v, unit, unit) ann_literal list" assumes full: "full dpll_bj ([], N) (M', N')" shows "M' ⊨asm N ⟷ satisfiable (set_mset N)" proof - have "no_dup M'" using rtranclp_dpll_bj_no_dup[of "([], N)" "(M', N')"] full unfolding full_def by auto then have "M' ⊨asm N ⟹ satisfiable (set_mset N)" using distinctconsistent_interp satisfiable_carac' true_annots_true_cls by blast then show ?thesis using full_dpll_final_state_conclusive[OF full] by auto qed lemma cdcl⇩N⇩O⇩T_is_dpll: "cdcl⇩N⇩O⇩T S T ⟷ dpll_bj S T" by (auto simp: cdcl⇩N⇩O⇩T.simps learn.simps forget⇩N⇩O⇩T.simps) text ‹Another proof of termination:› lemma "wf {(T, S). dpll_bj S T ∧ cdcl⇩N⇩O⇩T_NOT_all_inv A S}" unfolding cdcl⇩N⇩O⇩T_is_dpll[symmetric] by (rule wf_cdcl⇩N⇩O⇩T_no_learn_and_forget_infinite_chain) (auto simp: learn.simps forget⇩N⇩O⇩T.simps) end subsection ‹Adding restarts› locale dpll_withbacktrack_and_restarts = dpll_with_backtrack + fixes f :: "nat ⇒ nat" assumes unbounded: "unbounded f" and f_ge_1:"⋀n. n≥ 1 ⟹ f n ≥ 1" begin sublocale cdcl⇩N⇩O⇩T_increasing_restarts fst snd "λL (M, N). (L # M, N)" "λ(M, N). (tl M, N)" "λC (M, N). (M, {#C#} + N)" "λC (M, N). (M, remove_mset C N)" f "λ(_, N) S. S = ([], N)" "λA (M, N). atms_of_msu N ⊆ atms_of_ms A ∧ atm_of ` lits_of M ⊆ atms_of_ms A ∧ finite A ∧ all_decomposition_implies_m N (get_all_decided_decomposition M)" "λA T. (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A)) - μ⇩C (1+card (atms_of_ms A)) (2+card (atms_of_ms A)) (trail_weight T)" dpll_bj "λ(M, N). no_dup M ∧ all_decomposition_implies_m N (get_all_decided_decomposition M)" "λA _. (2+card (atms_of_ms A)) ^ (1+card (atms_of_ms A))" apply unfold_locales apply (rule unbounded) using f_ge_1 apply fastforce apply (smt dpll_bj_all_decomposition_implies_inv dpll_bj_atms_in_trail_in_set dpll_bj_clauses dpll_bj_no_dup prod.case_eq_if) apply (rule dpll_bj_trail_mes_decreasing_prop; auto) apply (rename_tac A T U, case_tac T, simp) apply (rename_tac A T U, case_tac U, simp) using dpll_bj_clauses dpll_bj_all_decomposition_implies_inv dpll_bj_no_dup by fastforce+ end end