Theory DPLL_W_BnB

theory DPLL_W_BnB
imports
  CDCL_W_Optimal_Model
  CDCL.DPLL_W
begin

lemma [simp]: ‹backtrack_split M1 = (M', L # M) ⟹ is_decided L›
  by (metis backtrack_split_snd_hd_decided list.sel(1) list.simps(3) snd_conv)

lemma funpow_tl_append_skip_ge:
  ‹n ≥ length M' ⟹ ((tl ^^ n) (M' @ M)) = (tl ^^ (n - length M')) M›
  apply (induction n arbitrary: M')
  subgoal by auto
  subgoal for n M'
    by (cases M')
      (auto simp del: funpow.simps(2) simp: funpow_Suc_right)
  done

(*TODO MOVE*)
text ‹The following version is more suited than @{thm backtrack_split_some_is_decided_then_snd_has_hd}
 for direct use.›
lemma backtrack_split_some_is_decided_then_snd_has_hd':
  ‹l∈set M ⟹ is_decided l ⟹ ∃M' L' M''. backtrack_split M = (M'', L' # M')›
  by (metis backtrack_snd_empty_not_decided list.exhaust prod.collapse)

lemma total_over_m_entailed_or_conflict:
  shows ‹total_over_m M N ⟹ M ⊨s N ∨ (∃C ∈ N. M ⊨s CNot C)›
  by (metis Set.set_insert total_not_true_cls_true_clss_CNot total_over_m_empty total_over_m_insert true_clss_def)

text ‹The locales on DPLL should eventually be moved to the DPLL theory, but currently it is only a discount
  version (in particular, we cheat and don't use \<^text>‹S ∼ T› in the transition system below, even if it
  would be cleaner to do as as we de for CDCL).
›
locale dpll_ops =
  fixes
    trail :: ‹'st ⇒ 'v  dpll⇩W_ann_lits› and
    clauses :: ‹'st ⇒ 'v clauses› and
    tl_trail :: ‹'st ⇒ 'st› and
    cons_trail :: ‹'v  dpll⇩W_ann_lit ⇒ 'st ⇒ 'st› and
    state_eq  :: ‹'st ⇒ 'st ⇒ bool› (infix ‹∼› 50) and
    state :: ‹'st ⇒ 'v  dpll⇩W_ann_lits × 'v clauses × 'b›
begin

definition additional_info :: ‹'st ⇒ 'b› where
  ‹additional_info S = (λ(M, N, w). w) (state S)›

definition reduce_trail_to :: ‹'v  dpll⇩W_ann_lits ⇒ 'st ⇒ 'st› where
  ‹reduce_trail_to M S = (tl_trail ^^ (length (trail S) - length M)) S›


end


locale bnb_ops =
  fixes
    trail :: ‹'st ⇒ 'v  dpll⇩W_ann_lits› and
    clauses :: ‹'st ⇒ 'v clauses› and
    tl_trail :: ‹'st ⇒ 'st› and
    cons_trail :: ‹'v  dpll⇩W_ann_lit ⇒ 'st ⇒ 'st› and
    state_eq  :: ‹'st ⇒ 'st ⇒ bool› (infix ‹∼› 50) and
    state :: ‹'st ⇒ 'v  dpll⇩W_ann_lits × 'v clauses × 'a × 'b› and
    weight :: ‹'st ⇒ 'a› and
    update_weight_information :: ‹'v dpll⇩W_ann_lits ⇒ 'st ⇒ 'st› and
    is_improving_int :: ‹'v  dpll⇩W_ann_lits ⇒ 'v  dpll⇩W_ann_lits ⇒ 'v clauses ⇒ 'a ⇒ bool› and
    conflicting_clauses :: ‹'v clauses ⇒ 'a ⇒ 'v clauses›
begin


interpretation dpll: dpll_ops where
  trail = trail and
  clauses = clauses and
  tl_trail = tl_trail and
  cons_trail = cons_trail and
  state_eq = state_eq and
  state = state
  .

definition conflicting_clss :: ‹'st ⇒ 'v literal multiset multiset› where
  ‹conflicting_clss S = conflicting_clauses (clauses S) (weight S)›

definition abs_state where
  ‹abs_state S = (trail S, clauses S + conflicting_clss S)›

abbreviation is_improving where
  ‹is_improving M M' S ≡ is_improving_int M M' (clauses S) (weight S)›

definition state' :: ‹'st ⇒ 'v  dpll⇩W_ann_lits × 'v clauses × 'a × 'v clauses› where
  ‹state' S = (trail S, clauses S, weight S, conflicting_clss S)›

definition additional_info :: ‹'st ⇒ 'b› where
  ‹additional_info S = (λ(M, N, _, w). w) (state S)›


end


locale dpll⇩W_state =
  dpll_ops trail clauses
    tl_trail cons_trail state_eq state
  for
    trail :: ‹'st ⇒ 'v  dpll⇩W_ann_lits› and
    clauses :: ‹'st ⇒ 'v clauses› and
    tl_trail :: ‹'st ⇒ 'st› and
    cons_trail :: ‹'v  dpll⇩W_ann_lit ⇒ 'st ⇒ 'st› and
    state_eq  :: ‹'st ⇒ 'st ⇒ bool› (infix ‹∼› 50) and
    state :: ‹'st ⇒ 'v  dpll⇩W_ann_lits × 'v clauses × 'b› +
  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
    state:
       ‹state S = (trail S, clauses S, additional_info S)›
begin


lemma [simp]:
  ‹clauses (cons_trail uu S) = clauses S›
  ‹trail (cons_trail uu S) = uu # trail S›
  ‹trail (tl_trail S) = tl (trail S)›
  ‹clauses (tl_trail S) = clauses (S)›
  ‹additional_info (cons_trail L S) = additional_info S›
  ‹additional_info (tl_trail S) = additional_info S›
  using
    cons_trail[of S]
    tl_trail[of S]
  by (auto simp: state)

lemma state_simp[simp]:
  ‹T ∼ S ⟹ trail T = trail S›
  ‹T ∼ S ⟹ clauses T = clauses S›
  by (auto dest!: state_eq_state simp: state)


lemma state_tl_trail: ‹state (tl_trail S) = (tl (trail S), clauses S, additional_info S)›
  by (auto simp: state)

lemma state_tl_trail_comp_pow: ‹state ((tl_trail ^^ n) S) = ((tl ^^ n) (trail S), clauses S, additional_info S)›
  apply (induction n)
    using state apply fastforce
  apply (auto simp: state_tl_trail state)[]
  done

lemma reduce_trail_to_simps[simp]:
  ‹backtrack_split (trail S) = (M', L # M) ⟹ trail (reduce_trail_to M S) = M›
  ‹clauses (reduce_trail_to M S) = clauses S›
  ‹additional_info (reduce_trail_to M S) = additional_info S›
  using state_tl_trail_comp_pow[of ‹Suc (length M')› S] backtrack_split_list_eq[of ‹trail S›, symmetric]
  unfolding reduce_trail_to_def
  apply (auto simp: state funpow_tl_append_skip_ge)
  using state state_tl_trail_comp_pow apply auto
  done

inductive dpll_backtrack :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll_backtrack S T›
if
  ‹D ∈# clauses S› and
  ‹trail S ⊨as CNot D› and
  ‹backtrack_split (trail S) = (M', L # M)› and
  ‹T ∼cons_trail (Propagated (-lit_of L) ()) (reduce_trail_to M S)›

inductive dpll_propagate :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll_propagate S T›
if
  ‹add_mset L D ∈# clauses S› and
  ‹trail S ⊨as CNot D› and
  ‹undefined_lit (trail S) L›
  ‹T ∼ cons_trail (Propagated L ()) S›

inductive dpll_decide :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll_decide S T›
if
  ‹undefined_lit (trail S) L›
  ‹T ∼ cons_trail (Decided L) S›
  ‹atm_of L ∈ atms_of_mm (clauses S)›

inductive dpll :: ‹'st ⇒ 'st ⇒ bool› where
‹dpll S T› if ‹dpll_decide S T› |
‹dpll S T› if ‹dpll_propagate S T› |
‹dpll S T› if ‹dpll_backtrack S T›

lemma dpll_is_dpll⇩W:
  ‹dpll S T ⟹ dpll⇩W (trail S, clauses S) (trail T, clauses T)›
  apply (induction rule: dpll.induct)
  subgoal for S T
    apply (auto simp: dpll.simps dpll⇩W.simps dpll_decide.simps dpll_backtrack.simps dpll_propagate.simps
      dest!: multi_member_split[of _ ‹clauses S›])
    done
  subgoal for S T
    unfolding dpll.simps dpll⇩W.simps dpll_decide.simps dpll_backtrack.simps dpll_propagate.simps
    by auto
  subgoal for S T
    unfolding dpll⇩W.simps dpll_decide.simps dpll_backtrack.simps dpll_propagate.simps
    by (auto simp: state)
 done

end


locale bnb =
  bnb_ops trail clauses
    tl_trail cons_trail state_eq state weight update_weight_information is_improving_int conflicting_clauses
  for
    weight :: ‹'st ⇒ 'a› and
    update_weight_information :: ‹'v dpll⇩W_ann_lits ⇒ 'st ⇒ 'st› and
    is_improving_int :: ‹'v  dpll⇩W_ann_lits ⇒ 'v  dpll⇩W_ann_lits ⇒ 'v clauses ⇒ 'a ⇒ bool› and
    trail :: ‹'st ⇒ 'v  dpll⇩W_ann_lits› and
    clauses :: ‹'st ⇒ 'v clauses› and
    tl_trail :: ‹'st ⇒ 'st› and
    cons_trail :: ‹'v  dpll⇩W_ann_lit ⇒ 'st ⇒ 'st› and
    state_eq  :: ‹'st ⇒ 'st ⇒ bool› (infix ‹∼› 50) and
    conflicting_clauses :: ‹'v clauses ⇒ 'a ⇒ 'v clauses›and
    state :: ‹'st ⇒ 'v  dpll⇩W_ann_lits × 'v clauses × 'a × 'b› +
  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
    update_weight_information:
       ‹state S = (M, N, w, oth) ⟹
          ∃w'. state (update_weight_information M' S) = (M, N, w', oth)› and

    conflicting_clss_update_weight_information_mono:
      ‹dpll⇩W_all_inv (abs_state S) ⟹ is_improving M M' S ⟹
        conflicting_clss S ⊆# conflicting_clss (update_weight_information M' S)› and
    conflicting_clss_update_weight_information_in:
      ‹is_improving M M' S ⟹ negate_ann_lits M' ∈# conflicting_clss (update_weight_information M' S)› and
    atms_of_conflicting_clss:
      ‹atms_of_mm (conflicting_clss S) ⊆ atms_of_mm (clauses S)› and
    state:
       ‹state S = (trail S, clauses S, weight S, additional_info S)›
begin

lemma [simp]: ‹DPLL_W.clauses (abs_state S) = clauses S + conflicting_clss S›
  ‹DPLL_W.trail (abs_state S) = trail S›
  by (auto simp: abs_state_def)


lemma [simp]: ‹trail (update_weight_information M' S) = trail S›
  using update_weight_information[of S]
  by (auto simp: state)

lemma [simp]:
  ‹clauses (update_weight_information M' S) = clauses S›
  ‹weight (cons_trail uu S) = weight S›
  ‹clauses (cons_trail uu S) = clauses S›
  ‹conflicting_clss (cons_trail uu S) = conflicting_clss S›
  ‹trail (cons_trail uu S) = uu # trail S›
  ‹trail (tl_trail S) = tl (trail S)›
  ‹clauses (tl_trail S) = clauses (S)›
  ‹weight (tl_trail S) = weight (S)›
  ‹conflicting_clss (tl_trail S) = conflicting_clss (S)›
  ‹additional_info (cons_trail L S) = additional_info S›
  ‹additional_info (tl_trail S) = additional_info S›
  ‹additional_info (update_weight_information M' S) = additional_info S›
  using update_weight_information[of S]
    cons_trail[of S]
    tl_trail[of S]
  by (auto simp: state conflicting_clss_def)

lemma state_simp[simp]:
  ‹T ∼ S ⟹ trail T = trail S›
  ‹T ∼ S ⟹ clauses T = clauses S›
  ‹T ∼ S ⟹ weight T = weight S›
  ‹T ∼ S ⟹ conflicting_clss T = conflicting_clss S›
  by (auto dest!: state_eq_state simp: state conflicting_clss_def)

interpretation dpll: dpll_ops trail clauses tl_trail cons_trail state_eq state
  .

interpretation dpll: dpll⇩W_state trail clauses tl_trail cons_trail state_eq state
  apply standard
  apply (auto dest: state_eq_sym[THEN iffD1] intro: state_eq_trans dest: state_eq_state)
  apply (auto simp: state cons_trail dpll.additional_info_def)
  done

lemma [simp]:
  ‹conflicting_clss (dpll.reduce_trail_to M S) = conflicting_clss S›
  ‹weight (dpll.reduce_trail_to M S) = weight S›
  using dpll.reduce_trail_to_simps(2-)[of M S] state[of S]
  unfolding dpll.additional_info_def
  apply (auto simp: )
  by (smt conflicting_clss_def dpll.reduce_trail_to_simps(2) dpll.state dpll_ops.additional_info_def
    old.prod.inject state)+

inductive backtrack_opt :: ‹'st ⇒ 'st ⇒ bool› where
backtrack_opt: "backtrack_split (trail S) = (M', L # M) ⟹ is_decided L ⟹ D ∈# conflicting_clss S
  ⟹ trail S ⊨as CNot D
  ⟹ T ∼cons_trail (Propagated (-lit_of L) ()) (dpll.reduce_trail_to M S)
  ⟹ backtrack_opt S T"


text ‹
  In the definition below the \<^term>‹state' T = (Propagated L () # trail
  S, clauses S, weight S, conflicting_clss S)› are not necessary, but
  avoids to change the DPLL formalisation with proper locales, as we
  did for CDCL.

  The DPLL calculus looks slightly more general than the CDCL calculus
  because we can take any conflicting clause from \<^term>‹conflicting_clss S›.
  However, this does not make a difference for the trail, as we backtrack
  to the last decision independantly of the conflict.
›
inductive dpll⇩W_core :: ‹'st ⇒ 'st ⇒ bool› for S T where
propagate: ‹dpll.dpll_propagate S T ⟹ dpll⇩W_core S T› |
decided: ‹dpll.dpll_decide S T ⟹ dpll⇩W_core S T › |
backtrack: ‹dpll.dpll_backtrack S T ⟹ dpll⇩W_core S T› |
backtrack_opt: ‹backtrack_opt S T ⟹ dpll⇩W_core S T›

inductive_cases dpll⇩W_coreE: ‹dpll⇩W_core S T›

inductive dpll⇩W_bound :: ‹'st ⇒ 'st ⇒ bool› where
update_info:
  ‹is_improving M M' S ⟹ T ∼ (update_weight_information M' S)
   ⟹ dpll⇩W_bound S T›

inductive dpll⇩W_bnb :: ‹'st ⇒ 'st ⇒ bool› where
dpll:
  ‹dpll⇩W_bnb S T›
  if ‹dpll⇩W_core S T› |
bnb:
  ‹dpll⇩W_bnb S T›
  if ‹dpll⇩W_bound S T›


inductive_cases dpll⇩W_bnbE: ‹dpll⇩W_bnb S T›

lemma dpll⇩W_core_is_dpll⇩W:
  ‹dpll⇩W_core S T ⟹ dpll⇩W (abs_state S) (abs_state T)›
  supply abs_state_def[simp] state'_def[simp]
  apply (induction rule: dpll⇩W_core.induct)
  subgoal
    by (auto simp: dpll⇩W.simps dpll.dpll_propagate.simps)
  subgoal
    by (auto simp: dpll⇩W.simps dpll.dpll_decide.simps)
  subgoal
    by (auto simp: dpll⇩W.simps dpll.dpll_backtrack.simps)
  subgoal
    by (auto simp: dpll⇩W.simps backtrack_opt.simps)
  done

lemma dpll⇩W_core_abs_state_all_inv:
  ‹dpll⇩W_core S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ dpll⇩W_all_inv (abs_state T)›
  by (auto dest!: dpll⇩W_core_is_dpll⇩W intro: dpll⇩W_all_inv)

lemma dpll⇩W_core_same_weight:
  ‹dpll⇩W_core S T ⟹ weight S = weight T›
  supply abs_state_def[simp] state'_def[simp]
  apply (induction rule: dpll⇩W_core.induct)
  subgoal
    by (auto simp: dpll⇩W.simps dpll.dpll_propagate.simps)
  subgoal
    by (auto simp: dpll⇩W.simps dpll.dpll_decide.simps)
  subgoal
    by (auto simp: dpll⇩W.simps dpll.dpll_backtrack.simps)
  subgoal
    by (auto simp: dpll⇩W.simps backtrack_opt.simps)
  done

lemma dpll⇩W_bound_trail:
    ‹dpll⇩W_bound S T ⟹ trail S = trail T› and
   dpll⇩W_bound_clauses:
    ‹dpll⇩W_bound S T ⟹ clauses S = clauses T› and
  dpll⇩W_bound_conflicting_clss:
    ‹dpll⇩W_bound S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ conflicting_clss S ⊆# conflicting_clss T›
  subgoal
    by (induction rule: dpll⇩W_bound.induct)
     (auto simp: dpll⇩W_all_inv_def state dest!: conflicting_clss_update_weight_information_mono)
  subgoal
    by (induction rule: dpll⇩W_bound.induct)
     (auto simp: dpll⇩W_all_inv_def state dest!: conflicting_clss_update_weight_information_mono)
  subgoal
    by (induction rule: dpll⇩W_bound.induct)
      (auto simp: state conflicting_clss_def
        dest!: conflicting_clss_update_weight_information_mono)
  done

lemma dpll⇩W_bound_abs_state_all_inv:
  ‹dpll⇩W_bound S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ dpll⇩W_all_inv (abs_state T)›
  using dpll⇩W_bound_conflicting_clss[of S T] dpll⇩W_bound_clauses[of S T]
   atms_of_conflicting_clss[of T] atms_of_conflicting_clss[of S]
  apply (auto simp: dpll⇩W_all_inv_def dpll⇩W_bound_trail lits_of_def image_image
    intro: all_decomposition_implies_mono[OF set_mset_mono] dest: dpll⇩W_bound_conflicting_clss)
  by (blast intro: all_decomposition_implies_mono)

lemma dpll⇩W_bnb_abs_state_all_inv:
  ‹dpll⇩W_bnb S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ dpll⇩W_all_inv (abs_state T)›
  by (auto elim!: dpll⇩W_bnb.cases intro: dpll⇩W_bound_abs_state_all_inv dpll⇩W_core_abs_state_all_inv)

lemma rtranclp_dpll⇩W_bnb_abs_state_all_inv:
  ‹dpll⇩W_bnb⇧*⇧* S T ⟹ dpll⇩W_all_inv (abs_state S) ⟹ dpll⇩W_all_inv (abs_state T)›
  by (induction rule: rtranclp_induct)
   (auto simp: dpll⇩W_bnb_abs_state_all_inv)

lemma dpll⇩W_core_clauses:
  ‹dpll⇩W_core S T ⟹ clauses S = clauses T›
  supply abs_state_def[simp] state'_def[simp]
  apply (induction rule: dpll⇩W_core.induct)
  subgoal
    by (auto simp: dpll⇩W.simps dpll.dpll_propagate.simps)
  subgoal
    by (auto simp: dpll⇩W.simps dpll.dpll_decide.simps)
  subgoal
    by (auto simp: dpll⇩W.simps  dpll.dpll_backtrack.simps)
  subgoal
    by (auto simp: dpll⇩W.simps  backtrack_opt.simps)
  done

lemma dpll⇩W_bnb_clauses:
  ‹dpll⇩W_bnb S T ⟹ clauses S = clauses T›
  by (auto elim!: dpll⇩W_bnbE simp: dpll⇩W_bound_clauses dpll⇩W_core_clauses)

lemma rtranclp_dpll⇩W_bnb_clauses:
  ‹dpll⇩W_bnb⇧*⇧* S T ⟹ clauses S = clauses T›
  by (induction rule: rtranclp_induct)
    (auto simp:  dpll⇩W_bnb_clauses)


lemma atms_of_clauses_conflicting_clss[simp]:
  ‹atms_of_mm (clauses S) ∪ atms_of_mm (conflicting_clss S) = atms_of_mm (clauses S)›
  using atms_of_conflicting_clss[of S] by blast

lemma wf_dpll⇩W_bnb_bnb: (* \htmllink{wf_dpll_bnb} *)
  assumes improve: ‹⋀S T. dpll⇩W_bound S T ⟹ clauses S = N ⟹ (ν (weight T), ν (weight S)) ∈ R› and
    wf_R: ‹wf R›
  shows ‹wf {(T, S). dpll⇩W_all_inv (abs_state S) ∧ dpll⇩W_bnb S T ∧
      clauses S = N}›
    (is ‹wf ?A›)
proof -
  let ?R = ‹{(T, S). (ν (weight T), ν (weight S)) ∈ R}›

  have ‹wf {(T, S). dpll⇩W_all_inv S ∧ dpll⇩W S T}›
    by (rule wf_dpll⇩W)
  from wf_if_measure_f[OF this, of abs_state]
  have wf: ‹wf {(T, S).  dpll⇩W_all_inv (abs_state S) ∧
      dpll⇩W (abs_state S) (abs_state T) ∧ weight S = weight T}›
    (is ‹wf ?CDCL›)
    by (rule wf_subset) auto
  have ‹wf (?R ∪ ?CDCL)›
    apply (rule wf_union_compatible)
    subgoal by (rule wf_if_measure_f[OF wf_R, of ‹λx. ν (weight x)›])
    subgoal by (rule wf)
    subgoal by (auto simp: dpll⇩W_core_same_weight)
    done

  moreover have ‹?A ⊆ ?R ∪ ?CDCL›
    by (auto elim!: dpll⇩W_bnbE dest: dpll⇩W_core_abs_state_all_inv dpll⇩W_core_is_dpll⇩W
      simp: dpll⇩W_core_same_weight improve)
  ultimately show ?thesis
    by (rule wf_subset)
qed


lemma [simp]:
  ‹weight ((tl_trail ^^ n) S) = weight S›
  ‹trail ((tl_trail ^^ n) S) = (tl ^^ n) (trail S)›
  ‹clauses ((tl_trail ^^ n) S) = clauses S›
  ‹conflicting_clss ((tl_trail ^^ n) S) = conflicting_clss S›
  using dpll.state_tl_trail_comp_pow[of n S]
  apply (auto simp: state conflicting_clss_def)
  apply (metis (mono_tags, lifting) Pair_inject dpll.state state)+
  done

lemma dpll⇩W_core_Ex_propagate:
  ‹add_mset L C ∈# clauses S ⟹ trail S ⊨as CNot C ⟹ undefined_lit (trail S) L ⟹
    Ex (dpll⇩W_core S)› and
   dpll⇩W_core_Ex_decide:
   "undefined_lit (trail S) L ⟹ atm_of L ∈ atms_of_mm (clauses S) ⟹
     Ex (dpll⇩W_core S)" and
    dpll⇩W_core_Ex_backtrack: "backtrack_split (trail S) = (M', L' # M) ⟹ is_decided L' ⟹ D ∈# clauses S ⟹
   trail S ⊨as CNot D ⟹ Ex (dpll⇩W_core S)" and
    dpll⇩W_core_Ex_backtrack_opt: "backtrack_split (trail S) = (M', L' # M) ⟹ is_decided L' ⟹ D ∈# conflicting_clss S
  ⟹ trail S ⊨as CNot D ⟹
   Ex (dpll⇩W_core S)"
  subgoal
    by (rule exI[of _ ‹cons_trail (Propagated L ()) S›])
     (fastforce simp: dpll⇩W_core.simps state_eq_ref dpll.dpll_propagate.simps)
  subgoal
    by (rule exI[of _ ‹cons_trail (Decided L) S›])
      (auto simp: dpll⇩W_core.simps state'_def dpll.dpll_decide.simps dpll.dpll_backtrack.simps
        backtrack_opt.simps dpll.dpll_propagate.simps)
  subgoal
    using backtrack_split_list_eq[of ‹trail S›, symmetric] apply -
    apply (rule exI[of _ ‹cons_trail (Propagated (-lit_of L') ()) (dpll.reduce_trail_to M S)›])
    apply (auto simp: dpll⇩W_core.simps state'_def funpow_tl_append_skip_ge
       dpll.dpll_decide.simps dpll.dpll_backtrack.simps backtrack_opt.simps
        dpll.dpll_propagate.simps)
    done
  subgoal
    using backtrack_split_list_eq[of ‹trail S›, symmetric] apply -
    apply (rule exI[of _ ‹cons_trail (Propagated (-lit_of L') ()) (dpll.reduce_trail_to M S)›])
    apply (auto simp: dpll⇩W_core.simps state'_def funpow_tl_append_skip_ge
       dpll.dpll_decide.simps dpll.dpll_backtrack.simps backtrack_opt.simps
        dpll.dpll_propagate.simps)
    done
  done


text ‹
  Unlike the CDCL case, we do not need assumptions on improve. The reason behind it is that
  we do not need any strategy on propagation and decisions.
›
lemma no_step_dpll_bnb_dpll⇩W:
  assumes
    ns: ‹no_step dpll⇩W_bnb S› and
    struct_invs: ‹dpll⇩W_all_inv (abs_state S)›
  shows ‹no_step dpll⇩W (abs_state S)›
proof -
  have no_decide: ‹atm_of L ∈ atms_of_mm (clauses S) ⟹
                  defined_lit (trail S) L› for L
    using spec[OF ns, of ‹cons_trail _ S›]
    apply (fastforce simp: dpll⇩W_bnb.simps total_over_m_def total_over_set_def
      dpll⇩W_core.simps state'_def
       dpll.dpll_decide.simps dpll.dpll_backtrack.simps backtrack_opt.simps
       dpll.dpll_propagate.simps)
    done
  have [intro]: ‹is_decided L ⟹
       backtrack_split (trail S) = (M', L # M) ⟹
       trail S ⊨as CNot D ⟹ D ∈# clauses S ⟹ False› for M' L M D
    using dpll⇩W_core_Ex_backtrack[of S M' L M D] ns
    by (auto simp: dpll⇩W_bnb.simps)
  have [intro]: ‹is_decided L ⟹
       backtrack_split (trail S) = (M', L # M) ⟹
       trail S ⊨as CNot D ⟹ D ∈# conflicting_clss S ⟹ False› for M' L M D
    using dpll⇩W_core_Ex_backtrack_opt[of S M' L M D] ns
    by (auto simp: dpll⇩W_bnb.simps)
  have tot: ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))›
    using no_decide
    by (force simp: total_over_m_def total_over_set_def state'_def
      Decided_Propagated_in_iff_in_lits_of_l)
  have [simp]: ‹add_mset L C ∈# clauses S ⟹ defined_lit (trail S) L› for L C
     using no_decide
    by (auto dest!: multi_member_split)
  have [simp]: ‹add_mset L C ∈# conflicting_clss S ⟹ defined_lit (trail S) L› for L C
     using no_decide atms_of_conflicting_clss[of S]
    by (auto dest!: multi_member_split)
  show ?thesis
    by (auto simp: dpll⇩W.simps no_decide)
qed


context
  assumes can_always_improve:
     ‹⋀S. trail S ⊨asm clauses S ⟹ (∀C ∈# conflicting_clss S. ¬ trail S ⊨as CNot C) ⟹
       dpll⇩W_all_inv (abs_state S) ⟹
       total_over_m (lits_of_l (trail S)) (set_mset (clauses S)) ⟹ Ex (dpll⇩W_bound S)›
begin

lemma no_step_dpll⇩W_bnb_conflict:
  assumes
    ns: ‹no_step dpll⇩W_bnb S› and
    invs: ‹dpll⇩W_all_inv (abs_state S)›
  shows ‹∃C ∈# clauses S + conflicting_clss S. trail S ⊨as CNot C› (is ?A) and
      ‹count_decided (trail S) = 0› and
     ‹unsatisfiable (set_mset (clauses S + conflicting_clss S))›
proof (rule ccontr)
  have no_decide: ‹atm_of L ∈ atms_of_mm (clauses S) ⟹ defined_lit (trail S) L› for L
    using spec[OF ns, of ‹cons_trail _ S›]
    apply (fastforce simp: dpll⇩W_bnb.simps total_over_m_def total_over_set_def
      dpll⇩W_core.simps state'_def 
       dpll.dpll_decide.simps dpll.dpll_backtrack.simps backtrack_opt.simps
       dpll.dpll_propagate.simps)
    done
  have tot: ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))›
    using no_decide
    by (force simp: total_over_m_def total_over_set_def state'_def
      Decided_Propagated_in_iff_in_lits_of_l)
  have dec0: ‹count_decided (trail S) = 0› if ent: ‹?A›
  proof -
    obtain C where
      ‹C ∈# clauses S + conflicting_clss S› and
      ‹trail S ⊨as CNot C›
      using ent tot ns invs
      by (auto simp: dpll⇩W_bnb.simps)
    then show ‹count_decided (trail S) = 0›
      using ns  dpll⇩W_core_Ex_backtrack[of S _ _ _ C]  dpll⇩W_core_Ex_backtrack_opt[of S _ _ _ C]
      unfolding count_decided_0_iff
      apply clarify
      apply (frule backtrack_split_some_is_decided_then_snd_has_hd'[of _ ‹trail S›], assumption)
     apply (auto simp: dpll⇩W_bnb.simps count_decided_0_iff)
     done
   qed

  show A: False if ‹¬?A›
  proof -
    have ‹trail S ⊨a C› if ‹C ∈# clauses S + conflicting_clss S› for C
    proof -
      have ‹¬ trail S ⊨as CNot C›
        using ‹¬?A› that by (auto dest!: multi_member_split)
      then show ‹?thesis›
        using tot that
        total_not_true_cls_true_clss_CNot[of ‹lits_of_l (trail S)› C]
          apply (auto simp: true_annots_def simp del: true_clss_def_iff_negation_in_model  dest!: multi_member_split )
          using true_annot_def apply blast
          using true_annot_def apply blast
        by (metis Decided_Propagated_in_iff_in_lits_of_l atms_of_clauses_conflicting_clss atms_of_ms_union
          in_m_in_literals no_decide set_mset_union that true_annot_def true_cls_add_mset)
    qed
    then have ‹trail S ⊨asm clauses S + conflicting_clss S›
      by (auto simp: true_annots_def  dest!: multi_member_split )
    then show ?thesis
      using can_always_improve[of S] ‹¬?A› tot invs ns by (auto simp: dpll⇩W_bnb.simps)
  qed
  then show ‹count_decided (trail S) = 0›
    using dec0 by blast
  moreover have ?A
    using A by blast
  ultimately show ‹unsatisfiable (set_mset (clauses S + conflicting_clss S))›
    using only_propagated_vars_unsat[of ‹trail S› _  ‹set_mset (clauses S + conflicting_clss S)›] invs
    unfolding dpll⇩W_all_inv_def count_decided_0_iff
   by auto
qed


end

inductive dpll⇩W_core_stgy :: ‹'st ⇒ 'st ⇒ bool› for S T where
propagate: ‹dpll.dpll_propagate S T ⟹ dpll⇩W_core_stgy S T› |
decided: ‹dpll.dpll_decide S T ⟹ no_step dpll.dpll_propagate S  ⟹ dpll⇩W_core_stgy S T › |
backtrack: ‹dpll.dpll_backtrack S T ⟹ dpll⇩W_core_stgy S T› |
backtrack_opt: ‹backtrack_opt S T ⟹ dpll⇩W_core_stgy S T›

lemma dpll⇩W_core_stgy_dpll⇩W_core: ‹dpll⇩W_core_stgy S T ⟹ dpll⇩W_core S T›
  by (induction rule: dpll⇩W_core_stgy.induct)
    (auto intro: dpll⇩W_core.intros)

lemma rtranclp_dpll⇩W_core_stgy_dpll⇩W_core: ‹dpll⇩W_core_stgy⇧*⇧* S T ⟹ dpll⇩W_core⇧*⇧* S T›
  by (induction rule: rtranclp_induct)
    (auto dest: dpll⇩W_core_stgy_dpll⇩W_core)

lemma no_step_stgy_iff: ‹no_step dpll⇩W_core_stgy S ⟷ no_step dpll⇩W_core S›
  by (auto simp: dpll⇩W_core_stgy.simps dpll⇩W_core.simps)

lemma full_dpll⇩W_core_stgy_dpll⇩W_core: ‹full dpll⇩W_core_stgy S T ⟹ full dpll⇩W_core S T›
  unfolding full_def by (simp add: no_step_stgy_iff rtranclp_dpll⇩W_core_stgy_dpll⇩W_core)

lemma dpll⇩W_core_stgy_clauses:
  ‹dpll⇩W_core_stgy S T ⟹ clauses T = clauses S›
  by (induction rule: dpll⇩W_core_stgy.induct)
   (auto simp: dpll.dpll_propagate.simps dpll.dpll_decide.simps dpll.dpll_backtrack.simps
      backtrack_opt.simps)

lemma rtranclp_dpll⇩W_core_stgy_clauses:
  ‹dpll⇩W_core_stgy⇧*⇧* S T ⟹ clauses T = clauses S›
  by (induction rule: rtranclp_induct)
    (auto dest: dpll⇩W_core_stgy_clauses)


end

end