theory CDCL_W_Optimal_Model
imports CDCL.CDCL_W_Abstract_State "HOL-Library.Extended_Nat" Weidenbach_Book_Base.Explorer
begin
section ‹CDCL Extensions›
text ‹
A counter-example for the original version from the book has been found (see below). There is no
simple fix, except taking complete models.
Based on Dominik Zimmer's thesis, we later reduced the problem of finding partial models to
finding total models. We later switched to the more elegant dual rail encoding (thanks to the
reviewer).
›
subsection ‹Optimisations›
notation image_mset (infixr "`#" 90)
text ‹The initial version was supposed to work on partial models directly. I found a counterexample
while writing the proof:
\nitpicking{
\shortrules{Propagate}{$(M;N;U;k;\top;O)$}{$(ML^{C\lor L};N;U;k;\top;O)$}
provided $C\lor L\in (N\cup U)$, $M\models \neg C$, $L$ is undefined in $M$.
\bigskip
\shortrules{Decide}{$(M;N;U;k;\top;O)$}{$(ML^{k+1};N;U;k+1;\top;O)$}
provided $L$ is undefined in $M$, contained in $N$.
\bigskip
\shortrules{ConflSat}{$(M;N;U;k;\top;O)$}{$(M;N;U;k;D;O)$}
provided $D\in (N\cup U)$ and $M\models \neg D$.
\bigskip
\shortrules{ConflOpt}{$(M;N;U;k;\top;O)$}{$(M;N;U;k;\neg M;O)$}
provided $O\neq\epsilon$ and $\operatorname{cost}(M) \geq \operatorname{cost}(O)$.
\bigskip
\shortrules{Skip}{$(ML^{C\lor L};N;U;k;D;O)$}{$(M;N;U;k;D;O)$}
provided $D\not\in\{\top,\bot\}$ and $\neg L$ does not occur in $D$.
\bigskip
\shortrules{Resolve}{$(ML^{C\lor L};N;U;k;D\lor-(L);O)$}{$(M;N;U;k;D\lor C;O)$}
provided $D$ is of level $k$.
\bigskip
\shortrules{Backtrack}{$(M_1K^{i+1}M_2;N;U;k;D\lor L;O)$}{$(M_1L^{D\vee L};N;U\cup\{D\lor L\};i;
\top;O)$}
provided $L$ is of level $k$ and $D$ is of level $i$.
\bigskip
\shortrules{Improve}{$(M;N;U;k;\top;O)$}{$(M;N;U;k;\top;M)$}
provided $M\models N$ and $O=\epsilon$ or $\operatorname{cost}(M)<\operatorname{cost}(O)$.
}
{This calculus does not always find the model with minimum cost. Take for example the following
cost function:
\[\operatorname{cost}: \left\{
\begin{array}{c@ {\rightarrow}c}
P & 3\\
\neg P & 1\\
Q & 1\\
\neg Q & 1\\
\end{array}
\right.\]
and the clauses $N = \{P\lor Q\}$. We can then do the following transitions:
$(\epsilon, N, \varnothing, \top, \infty)$
\shortrules{Decide}{}{$(P^1, N, \varnothing, \top, \infty)$}
\shortrules{Improve}{}{$(P^1, N, \varnothing, \top, (P, 3))$}
\shortrules{conflictOpt}{}{$(P^1, N, \varnothing, \neg P, (P, 3))$}
\shortrules{backtrack}{}{$({\neg P}^{\neg P}, N, \{\neg P\}, \top, (P, 3))$}
\shortrules{propagate}{}{$({\neg P}^{\neg P}Q^{P\lor Q}, N, \{\neg P\}, \top, (P, 3))$}
\shortrules{improve}{}{$({\neg P}^{\neg P}Q^{P\lor Q}, N, \{\neg P\}, \top, (\neg P\, Q, 2))$}
\shortrules{conflictOpt}{}{$({\neg P}^{\neg P}Q^{P\lor Q}, N, \{\neg P\}, P \lor \neg Q, (\neg P\,
Q, 2))$}
\shortrules{resolve}{}{$({\neg P}^{\neg P}, N, \{\neg P\}, P, (\neg P\, Q, 2))$}
\shortrules{resolve}{}{$(\epsilon, N, \{\neg P\}, \bot, (\neg P\, Q, 3))$}
However, the optimal model is $Q$.
}
›
text ‹
The idea of the proof (explained of the example of the optimising CDCL) is the following:
▸ We start with a calculus OCDCL on \<^term>‹(M, N, U, D, Op)›.
▸ This extended to a state \<^term>‹(M, N + all_models_of_higher_cost, U, D, Op)›.
▸ Each transition step of OCDCL is mapped to a step in CDCL over the abstract state. The abstract
set of clauses might be unsatisfiable, but we only use it to prove the invariants on the
state. Only adding clause cannot be mapped to a transition over the abstract state, but adding
clauses does not break the invariants (as long as the additional clauses do not contain
duplicate literals).
▸ The last proofs are done over CDCLopt.
We abstract about how the optimisation is done in the locale below: We define a calculus
\<^term>‹cdcl_bnb› (for branch-and-bounds). It is parametrised by how the conflicting clauses are
generated and the improvement criterion.
We later instantiate it with the optimisation calculus from Weidenbach's book.
›
subsubsection ‹Helper libraries›
lemma (in -) Neg_atm_of_itself_uminus_iff: ‹Neg (atm_of xa) ≠ - xa ⟷ is_neg xa›
by (cases xa) auto
lemma (in -) Pos_atm_of_itself_uminus_iff: ‹Pos (atm_of xa) ≠ - xa ⟷ is_pos xa›
by (cases xa) auto
definition model_on :: ‹'v partial_interp ⇒ 'v clauses ⇒ bool› where
‹model_on I N ⟷ consistent_interp I ∧ atm_of ` I ⊆ atms_of_mm N›
subsubsection ‹CDCL BNB›
locale conflict_driven_clause_learning_with_adding_init_clause_cost⇩W_no_state =
state⇩W_no_state
state_eq state
trail init_clss learned_clss conflicting
cons_trail tl_trail add_learned_cls remove_cls
update_conflicting
init_state
for
state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) and
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'a × '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" +
fixes
update_weight_information :: "('v, 'v clause) ann_lits ⇒ 'st ⇒ 'st" and
is_improving_int :: "('v, 'v clause) ann_lits ⇒ ('v, 'v clause) ann_lits ⇒ 'v clauses ⇒ 'a ⇒ bool" and
conflicting_clauses :: "'v clauses ⇒ 'a ⇒ 'v clauses" and
weight :: ‹'st ⇒ 'a›
begin
abbreviation is_improving where
‹is_improving M M' S ≡ is_improving_int M M' (init_clss S) (weight S)›
definition additional_info' :: "'st ⇒ 'b" where
"additional_info' S = (λ(_, _, _, _, _, D). D) (state S)"
definition conflicting_clss :: ‹'st ⇒ 'v literal multiset multiset› where
‹conflicting_clss S = conflicting_clauses (init_clss S) (weight S)›
definition abs_state
:: "'st ⇒ ('v, 'v clause) ann_lit list × 'v clauses × 'v clauses × 'v clause option"
where
‹abs_state S = (trail S, init_clss S + conflicting_clss S, learned_clss S,
conflicting S)›
end
locale conflict_driven_clause_learning_with_adding_init_clause_cost⇩W_ops =
conflict_driven_clause_learning_with_adding_init_clause_cost⇩W_no_state
state_eq state
trail init_clss learned_clss conflicting
cons_trail tl_trail add_learned_cls remove_cls
update_conflicting
init_state
update_weight_information is_improving_int conflicting_clauses weight
for
state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) and
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'a × '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" and
update_weight_information :: "('v, 'v clause) ann_lits ⇒ 'st ⇒ 'st" and
is_improving_int :: "('v, 'v clause) ann_lits ⇒ ('v, 'v clause) ann_lits ⇒ 'v clauses ⇒
'a ⇒ bool" and
conflicting_clauses :: "'v clauses ⇒ 'a ⇒ 'v clauses" and
weight :: ‹'st ⇒ 'a› +
assumes
state_prop':
‹state S = (trail S, init_clss S, learned_clss S, conflicting S, weight S, additional_info' S)›
and
update_weight_information:
‹state S = (M, N, U, C, w, other) ⟹
∃w'. state (update_weight_information T S) = (M, N, U, C, w', other)› and
atms_of_conflicting_clss:
‹atms_of_mm (conflicting_clss S) ⊆ atms_of_mm (init_clss S)› and
distinct_mset_mset_conflicting_clss:
‹distinct_mset_mset (conflicting_clss S)› and
conflicting_clss_update_weight_information_mono:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_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)›
begin
sublocale conflict_driven_clause_learning⇩W where
state_eq = state_eq and
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state
apply unfold_locales
unfolding additional_info'_def additional_info_def by (auto simp: state_prop')
declare reduce_trail_to_skip_beginning[simp]
lemma state_eq_weight[state_simp, simp]: ‹S ∼ T ⟹ weight S = weight T›
apply (drule state_eq_state)
apply (subst (asm) state_prop')
apply (subst (asm) state_prop')
by simp
lemma conflicting_clause_state_eq[state_simp, simp]:
‹S ∼ T ⟹ conflicting_clss S = conflicting_clss T›
unfolding conflicting_clss_def by auto
lemma
weight_cons_trail[simp]:
‹weight (cons_trail L S) = weight S› and
weight_update_conflicting[simp]:
‹weight (update_conflicting C S) = weight S› and
weight_tl_trail[simp]:
‹weight (tl_trail S) = weight S› and
weight_add_learned_cls[simp]:
‹weight (add_learned_cls D S) = weight S›
using cons_trail[of S _ _ L] update_conflicting[of S] tl_trail[of S] add_learned_cls[of S]
by (auto simp: state_prop')
lemma update_weight_information_simp[simp]:
‹trail (update_weight_information C S) = trail S›
‹init_clss (update_weight_information C S) = init_clss S›
‹learned_clss (update_weight_information C S) = learned_clss S›
‹clauses (update_weight_information C S) = clauses S›
‹backtrack_lvl (update_weight_information C S) = backtrack_lvl S›
‹conflicting (update_weight_information C S) = conflicting S›
using update_weight_information[of S] unfolding clauses_def
by (subst (asm) state_prop', subst (asm) state_prop'; force)+
lemma
conflicting_clss_cons_trail[simp]: ‹conflicting_clss (cons_trail K S) = conflicting_clss S› and
conflicting_clss_tl_trail[simp]: ‹conflicting_clss (tl_trail S) = conflicting_clss S› and
conflicting_clss_add_learned_cls[simp]:
‹conflicting_clss (add_learned_cls D S) = conflicting_clss S› and
conflicting_clss_update_conflicting[simp]:
‹conflicting_clss (update_conflicting E S) = conflicting_clss S›
unfolding conflicting_clss_def by auto
inductive conflict_opt :: "'st ⇒ 'st ⇒ bool" for S T :: 'st where
conflict_opt_rule:
‹conflict_opt S T›
if
‹negate_ann_lits (trail S) ∈# conflicting_clss S›
‹conflicting S = None›
‹T ∼ update_conflicting (Some (negate_ann_lits (trail S))) S›
inductive_cases conflict_optE: ‹conflict_opt S T›
inductive improvep :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
improve_rule:
‹improvep S T›
if
‹is_improving (trail S) M' S› and
‹conflicting S = None› and
‹T ∼ update_weight_information M' S›
inductive_cases improveE: ‹improvep S T›
lemma invs_update_weight_information[simp]:
‹no_strange_atm (update_weight_information C S) = (no_strange_atm S)›
‹cdcl⇩W_M_level_inv (update_weight_information C S) = cdcl⇩W_M_level_inv S›
‹distinct_cdcl⇩W_state (update_weight_information C S) = distinct_cdcl⇩W_state S›
‹cdcl⇩W_conflicting (update_weight_information C S) = cdcl⇩W_conflicting S›
‹cdcl⇩W_learned_clause (update_weight_information C S) = cdcl⇩W_learned_clause S›
unfolding no_strange_atm_def cdcl⇩W_M_level_inv_def distinct_cdcl⇩W_state_def cdcl⇩W_conflicting_def
cdcl⇩W_learned_clause_alt_def cdcl⇩W_all_struct_inv_def by auto
lemma conflict_opt_cdcl⇩W_all_struct_inv:
assumes ‹conflict_opt S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using assms atms_of_conflicting_clss[of T] atms_of_conflicting_clss[of S]
apply (induction rule: conflict_opt.cases)
by (auto simp add: cdcl⇩W_restart_mset.no_strange_atm_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
true_annots_true_cls_def_iff_negation_in_model
in_negate_trial_iff cdcl⇩W_restart_mset_state cdcl⇩W_restart_mset.clauses_def
distinct_mset_mset_conflicting_clss abs_state_def
intro!: true_clss_cls_in)
lemma reduce_trail_to_update_weight_information[simp]:
‹trail (reduce_trail_to M (update_weight_information M' S)) = trail (reduce_trail_to M S)›
unfolding trail_reduce_trail_to_drop by auto
lemma additional_info_weight_additional_info': ‹additional_info S = (weight S, additional_info' S)›
using state_prop[of S] state_prop'[of S] by auto
lemma
weight_reduce_trail_to[simp]: ‹weight (reduce_trail_to M S) = weight S› and
additional_info'_reduce_trail_to[simp]: ‹additional_info' (reduce_trail_to M S) = additional_info' S›
using additional_info_reduce_trail_to[of M S] unfolding additional_info_weight_additional_info'
by auto
lemma conflicting_clss_reduce_trail_to[simp]: ‹conflicting_clss (reduce_trail_to M S) = conflicting_clss S›
unfolding conflicting_clss_def by auto
lemma improve_cdcl⇩W_all_struct_inv:
assumes ‹improvep S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using assms atms_of_conflicting_clss[of T] atms_of_conflicting_clss[of S]
proof (induction rule: improvep.cases)
case (improve_rule M' T)
moreover have ‹all_decomposition_implies
(set_mset (init_clss S) ∪ set_mset (conflicting_clss S) ∪ set_mset (learned_clss S))
(get_all_ann_decomposition (trail S)) ⟹
all_decomposition_implies
(set_mset (init_clss S) ∪ set_mset (conflicting_clss (update_weight_information M' S)) ∪
set_mset (learned_clss S))
(get_all_ann_decomposition (trail S))›
apply (rule all_decomposition_implies_mono)
using improve_rule conflicting_clss_update_weight_information_mono[of S ‹trail S› M'] inv
by (auto dest: multi_member_split)
ultimately show ?case
using conflicting_clss_update_weight_information_mono[of S ‹trail S› M']
by (auto 6 2 simp add: cdcl⇩W_restart_mset.no_strange_atm_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
true_annots_true_cls_def_iff_negation_in_model
in_negate_trial_iff cdcl⇩W_restart_mset_state cdcl⇩W_restart_mset.clauses_def
image_Un distinct_mset_mset_conflicting_clss abs_state_def
simp del: append_assoc
dest: no_dup_appendD consistent_interp_unionD)
qed
text ‹\<^term>‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant› is too restrictive:
\<^term>‹cdcl⇩W_restart_mset.no_smaller_confl› is needed but does not hold(at least, if cannot
ensure that conflicts are found as soon as possible).›
lemma improve_no_smaller_conflict:
assumes ‹improvep S T› and
‹no_smaller_confl S›
shows ‹no_smaller_confl T› and ‹conflict_is_false_with_level T›
using assms apply (induction rule: improvep.induct)
unfolding cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
by (auto simp: cdcl⇩W_restart_mset_state no_smaller_confl_def cdcl⇩W_restart_mset.clauses_def
exists_lit_max_level_in_negate_ann_lits)
lemma conflict_opt_no_smaller_conflict:
assumes ‹conflict_opt S T› and
‹no_smaller_confl S›
shows ‹no_smaller_confl T› and ‹conflict_is_false_with_level T›
using assms by (induction rule: conflict_opt.induct)
(auto simp: cdcl⇩W_restart_mset_state no_smaller_confl_def cdcl⇩W_restart_mset.clauses_def
exists_lit_max_level_in_negate_ann_lits cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def)
fun no_confl_prop_impr where
‹no_confl_prop_impr S ⟷
no_step propagate S ∧ no_step conflict S›
text ‹We use a slighlty generalised form of backtrack to make conflict clause minimisation possible.›
inductive obacktrack :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
obacktrack_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 + conflicting_clss 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))) ⟹
obacktrack S T›
inductive_cases obacktrackE: ‹obacktrack S T›
inductive cdcl_bnb_bj :: "'st ⇒ 'st ⇒ bool" where
skip: "skip S S' ⟹ cdcl_bnb_bj S S'" |
resolve: "resolve S S' ⟹ cdcl_bnb_bj S S'" |
backtrack: "obacktrack S S' ⟹ cdcl_bnb_bj S S'"
inductive_cases cdcl_bnb_bjE: "cdcl_bnb_bj S T"
inductive ocdcl⇩W_o :: "'st ⇒ 'st ⇒ bool" for S :: 'st where
decide: "decide S S' ⟹ ocdcl⇩W_o S S'" |
bj: "cdcl_bnb_bj S S' ⟹ ocdcl⇩W_o S S'"
inductive cdcl_bnb :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
cdcl_conflict: "conflict S S' ⟹ cdcl_bnb S S'" |
cdcl_propagate: "propagate S S' ⟹ cdcl_bnb S S'" |
cdcl_improve: "improvep S S' ⟹ cdcl_bnb S S'" |
cdcl_conflict_opt: "conflict_opt S S' ⟹ cdcl_bnb S S'" |
cdcl_other': "ocdcl⇩W_o S S' ⟹ cdcl_bnb S S'"
inductive cdcl_bnb_stgy :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
cdcl_bnb_conflict: "conflict S S' ⟹ cdcl_bnb_stgy S S'" |
cdcl_bnb_propagate: "propagate S S' ⟹ cdcl_bnb_stgy S S'" |
cdcl_bnb_improve: "improvep S S' ⟹ cdcl_bnb_stgy S S'" |
cdcl_bnb_conflict_opt: "conflict_opt S S' ⟹ cdcl_bnb_stgy S S'" |
cdcl_bnb_other': "ocdcl⇩W_o S S' ⟹ no_confl_prop_impr S ⟹ cdcl_bnb_stgy S S'"
lemma ocdcl⇩W_o_induct[consumes 1, case_names decide skip resolve backtrack]:
fixes S :: "'st"
assumes cdcl⇩W_restart: "ocdcl⇩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 + conflicting_clss 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: ocdcl⇩W_o.induct)
subgoal using assms(2) by (auto elim: decideE; fail)
subgoal apply (elim cdcl_bnb_bjE skipE resolveE obacktrackE)
apply (frule skipH; simp; fail)
apply (cases "trail S"; auto elim!: resolveE intro!: resolveH; fail)
apply (frule backtrackH; simp; fail)
done
done
lemma obacktrack_backtrackg: ‹obacktrack S T ⟹ backtrackg S T›
unfolding obacktrack.simps backtrackg.simps
by blast
subsubsection ‹Pluging into normal CDCL›
lemma cdcl_bnb_no_more_init_clss:
‹cdcl_bnb S S' ⟹ init_clss S = init_clss S'›
by (induction rule: cdcl_bnb.cases)
(auto simp: improvep.simps conflict.simps propagate.simps
conflict_opt.simps ocdcl⇩W_o.simps obacktrack.simps skip.simps resolve.simps cdcl_bnb_bj.simps
decide.simps)
lemma rtranclp_cdcl_bnb_no_more_init_clss:
‹cdcl_bnb⇧*⇧* S S' ⟹ init_clss S = init_clss S'›
by (induction rule: rtranclp_induct)
(auto dest: cdcl_bnb_no_more_init_clss)
lemma conflict_opt_conflict:
‹conflict_opt S T ⟹ cdcl⇩W_restart_mset.conflict (abs_state S) (abs_state T)›
by (induction rule: conflict_opt.cases)
(auto intro!: cdcl⇩W_restart_mset.conflict_rule[of _ ‹negate_ann_lits (trail S)›]
simp: cdcl⇩W_restart_mset.clauses_def cdcl⇩W_restart_mset_state
true_annots_true_cls_def_iff_negation_in_model abs_state_def
in_negate_trial_iff)
lemma conflict_conflict:
‹conflict S T ⟹ cdcl⇩W_restart_mset.conflict (abs_state S) (abs_state T)›
by (induction rule: conflict.cases)
(auto intro!: cdcl⇩W_restart_mset.conflict_rule
simp: clauses_def cdcl⇩W_restart_mset.clauses_def cdcl⇩W_restart_mset_state
true_annots_true_cls_def_iff_negation_in_model abs_state_def
in_negate_trial_iff)
lemma propagate_propagate:
‹propagate S T ⟹ cdcl⇩W_restart_mset.propagate (abs_state S) (abs_state T)›
by (induction rule: propagate.cases)
(auto intro!: cdcl⇩W_restart_mset.propagate_rule
simp: clauses_def cdcl⇩W_restart_mset.clauses_def cdcl⇩W_restart_mset_state
true_annots_true_cls_def_iff_negation_in_model abs_state_def
in_negate_trial_iff)
lemma decide_decide:
‹decide S T ⟹ cdcl⇩W_restart_mset.decide (abs_state S) (abs_state T)›
by (induction rule: decide.cases)
(auto intro!: cdcl⇩W_restart_mset.decide_rule
simp: clauses_def cdcl⇩W_restart_mset.clauses_def cdcl⇩W_restart_mset_state
true_annots_true_cls_def_iff_negation_in_model abs_state_def
in_negate_trial_iff)
lemma skip_skip:
‹skip S T ⟹ cdcl⇩W_restart_mset.skip (abs_state S) (abs_state T)›
by (induction rule: skip.cases)
(auto intro!: cdcl⇩W_restart_mset.skip_rule
simp: clauses_def cdcl⇩W_restart_mset.clauses_def cdcl⇩W_restart_mset_state
true_annots_true_cls_def_iff_negation_in_model abs_state_def
in_negate_trial_iff)
lemma resolve_resolve:
‹resolve S T ⟹ cdcl⇩W_restart_mset.resolve (abs_state S) (abs_state T)›
by (induction rule: resolve.cases)
(auto intro!: cdcl⇩W_restart_mset.resolve_rule
simp: clauses_def cdcl⇩W_restart_mset.clauses_def cdcl⇩W_restart_mset_state
true_annots_true_cls_def_iff_negation_in_model abs_state_def
in_negate_trial_iff)
lemma backtrack_backtrack:
‹obacktrack S T ⟹ cdcl⇩W_restart_mset.backtrack (abs_state S) (abs_state T)›
proof (induction rule: obacktrack.cases)
case (obacktrack_rule L D K M1 M2 D' i T)
have H: ‹set_mset (init_clss S) ∪ set_mset (learned_clss S)
⊆ set_mset (init_clss S) ∪ set_mset (conflicting_clss S) ∪ set_mset (learned_clss S)›
by auto
have [simp]: ‹cdcl⇩W_restart_mset.reduce_trail_to M1
(trail S, init_clss S + conflicting_clss S, add_mset D (learned_clss S), None) =
(M1, init_clss S + conflicting_clss S, add_mset D (learned_clss S), None)› for D
using obacktrack_rule by (auto simp add: cdcl⇩W_restart_mset_reduce_trail_to
cdcl⇩W_restart_mset_state)
show ?case
using obacktrack_rule
by (auto intro!: cdcl⇩W_restart_mset.backtrack.intros
simp: cdcl⇩W_restart_mset_state abs_state_def clauses_def cdcl⇩W_restart_mset.clauses_def
ac_simps)
qed
lemma ocdcl⇩W_o_all_rules_induct[consumes 1, case_names decide backtrack skip resolve]:
fixes S T :: 'st
assumes
"ocdcl⇩W_o S T" and
"⋀T. decide S T ⟹ P S T" and
"⋀T. obacktrack 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: ocdcl⇩W_o.induct) (auto simp: cdcl_bnb_bj.simps)
lemma cdcl⇩W_o_cdcl⇩W_o:
‹ocdcl⇩W_o S S' ⟹ cdcl⇩W_restart_mset.cdcl⇩W_o (abs_state S) (abs_state S')›
apply (induction rule: ocdcl⇩W_o_all_rules_induct)
apply (simp add: cdcl⇩W_restart_mset.cdcl⇩W_o.simps decide_decide; fail)
apply (blast dest: backtrack_backtrack)
apply (blast dest: skip_skip)
by (blast dest: resolve_resolve)
lemma cdcl_bnb_stgy_all_struct_inv:
assumes ‹cdcl_bnb S T› and ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using assms
proof (induction rule: cdcl_bnb.cases)
case (cdcl_conflict S')
then show ?case
by (blast dest: conflict_conflict cdcl⇩W_restart_mset.cdcl⇩W_stgy.intros
intro: cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)
next
case (cdcl_propagate S')
then show ?case
by (blast dest: propagate_propagate cdcl⇩W_restart_mset.cdcl⇩W_stgy.intros
intro: cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W_all_struct_inv)
next
case (cdcl_improve S')
then show ?case
using improve_cdcl⇩W_all_struct_inv by blast
next
case (cdcl_conflict_opt S')
then show ?case
using conflict_opt_cdcl⇩W_all_struct_inv by blast
next
case (cdcl_other' S')
then show ?case
by (meson cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_inv cdcl⇩W_restart_mset.other cdcl⇩W_o_cdcl⇩W_o)
qed
lemma rtranclp_cdcl_bnb_stgy_all_struct_inv:
assumes ‹cdcl_bnb⇧*⇧* S T› and ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using assms by induction (auto dest: cdcl_bnb_stgy_all_struct_inv)
definition cdcl_bnb_struct_invs :: ‹'st ⇒ bool› where
‹cdcl_bnb_struct_invs S ⟷
atms_of_mm (conflicting_clss S) ⊆ atms_of_mm (init_clss S)›
lemma cdcl_bnb_cdcl_bnb_struct_invs:
‹cdcl_bnb S T ⟹ cdcl_bnb_struct_invs S ⟹ cdcl_bnb_struct_invs T›
using atms_of_conflicting_clss[of ‹update_weight_information _ S›] apply -
by (induction rule: cdcl_bnb.induct)
(force simp: improvep.simps conflict.simps propagate.simps
conflict_opt.simps ocdcl⇩W_o.simps obacktrack.simps skip.simps resolve.simps
cdcl_bnb_bj.simps decide.simps cdcl_bnb_struct_invs_def)+
lemma rtranclp_cdcl_bnb_cdcl_bnb_struct_invs:
‹cdcl_bnb⇧*⇧* S T ⟹ cdcl_bnb_struct_invs S ⟹ cdcl_bnb_struct_invs T›
by (induction rule: rtranclp_induct) (auto dest: cdcl_bnb_cdcl_bnb_struct_invs)
lemma cdcl_bnb_stgy_cdcl_bnb: ‹cdcl_bnb_stgy S T ⟹ cdcl_bnb S T›
by (auto simp: cdcl_bnb_stgy.simps intro: cdcl_bnb.intros)
lemma rtranclp_cdcl_bnb_stgy_cdcl_bnb: ‹cdcl_bnb_stgy⇧*⇧* S T ⟹ cdcl_bnb⇧*⇧* S T›
by (induction rule: rtranclp_induct)
(auto dest: cdcl_bnb_stgy_cdcl_bnb)
text ‹The following does ∗‹not› hold, because we cannot guarantee the absence of conflict of
smaller level after \<^term>‹improve› and \<^term>‹conflict_opt›.›
lemma cdcl_bnb_all_stgy_inv:
assumes ‹cdcl_bnb S T› and ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant (abs_state S)›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant (abs_state T)›
oops
lemma skip_conflict_is_false_with_level:
assumes ‹skip S T› and
struct_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
confl_inv:‹conflict_is_false_with_level S›
shows ‹conflict_is_false_with_level T›
using assms
proof induction
case (skip_rule L C' M D T) note tr_S = this(1) and D = this(2) and T = this(5)
have conflicting: ‹cdcl⇩W_conflicting S› and
lev: "cdcl⇩W_M_level_inv S"
using struct_inv unfolding cdcl⇩W_conflicting_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
obtain La where
"La ∈# D" and
"get_level (Propagated L C' # M) La = backtrack_lvl S"
using skip_rule 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
qed
lemma propagate_conflict_is_false_with_level:
assumes ‹propagate S T› and
struct_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
confl_inv:‹conflict_is_false_with_level S›
shows ‹conflict_is_false_with_level T›
using assms by (induction rule: propagate.induct) auto
lemma cdcl⇩W_o_conflict_is_false_with_level:
assumes ‹cdcl⇩W_o S T› and
struct_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
confl_inv: ‹conflict_is_false_with_level S›
shows ‹conflict_is_false_with_level T›
apply (rule cdcl⇩W_o_conflict_is_false_with_level_inv[of S T])
subgoal using assms by auto
subgoal using struct_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
subgoal using assms by auto
subgoal using struct_inv unfolding distinct_cdcl⇩W_state_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
subgoal using struct_inv unfolding cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
done
lemma cdcl⇩W_o_no_smaller_confl:
assumes ‹cdcl⇩W_o S T› and
struct_inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
confl_inv: ‹no_smaller_confl S› and
lev: ‹conflict_is_false_with_level S› and
n_s: ‹no_confl_prop_impr S›
shows ‹no_smaller_confl T›
apply (rule cdcl⇩W_o_no_smaller_confl_inv[of S T])
subgoal using assms by (auto dest!:cdcl⇩W_o_cdcl⇩W_o)[]
subgoal using n_s by auto
subgoal using struct_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
subgoal using lev by fast
subgoal using confl_inv unfolding distinct_cdcl⇩W_state_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
cdcl⇩W_restart_mset.no_smaller_confl_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state clauses_def)
done
declare cdcl⇩W_restart_mset.conflict_is_false_with_level_def [simp del]
lemma improve_conflict_is_false_with_level:
assumes ‹improvep S T› and ‹conflict_is_false_with_level S›
shows ‹conflict_is_false_with_level T›
using assms
proof induction
case (improve_rule T)
then show ?case
by (auto simp: cdcl⇩W_restart_mset.conflict_is_false_with_level_def
abs_state_def cdcl⇩W_restart_mset_state in_negate_trial_iff Bex_def negate_ann_lits_empty_iff
intro!: exI[of _ ‹-lit_of (hd M)›])
qed
declare conflict_is_false_with_level_def[simp del]
lemma trail_trail [simp]:
‹CDCL_W_Abstract_State.trail (abs_state S) = trail S›
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
lemma [simp]:
‹CDCL_W_Abstract_State.trail (cdcl⇩W_restart_mset.reduce_trail_to M (abs_state S)) =
trail (reduce_trail_to M S)›
by (auto simp: trail_reduce_trail_to_drop
cdcl⇩W_restart_mset.trail_reduce_trail_to_drop)
lemma [simp]:
‹CDCL_W_Abstract_State.trail (cdcl⇩W_restart_mset.reduce_trail_to M (abs_state S)) =
trail (reduce_trail_to M S)›
by (auto simp: trail_reduce_trail_to_drop
cdcl⇩W_restart_mset.trail_reduce_trail_to_drop)
lemma cdcl⇩W_M_level_inv_cdcl⇩W_M_level_inv[iff]:
‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S) = cdcl⇩W_M_level_inv S›
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset_state)
lemma obacktrack_state_eq_compatible:
assumes
bt: "obacktrack S T" and
SS': "S ∼ S'" and
TT': "T ∼ T'"
shows "obacktrack 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 + conflicting_clss 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 obacktrackE) force
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 obacktrack_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 ocdcl⇩W_o_no_smaller_confl_inv:
fixes S S' :: "'st"
assumes
"ocdcl⇩W_o S S'" and
n_s: "no_step conflict S" and
lev: "cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state 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: ocdcl⇩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 "obacktrack S ?S'"
using obacktrack_rule[OF backtrack.hyps(1-8) T] obacktrack_state_eq_compatible[of S T S] T
by force
then have ‹cdcl_bnb S ?S'›
by (auto dest!: cdcl_bnb_bj.intros ocdcl⇩W_o.intros intro: cdcl_bnb.intros)
then have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state ?S')›
using cdcl_bnb_stgy_all_struct_inv[of S, OF _ lev] by fast
then have "cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state ?S')"
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def)
then have "no_dup (Propagated L D # M1)"
using decomp lev unfolding cdcl⇩W_restart_mset.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 cdcl_bnb_stgy_no_smaller_confl:
assumes ‹cdcl_bnb_stgy S T› and
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
‹no_smaller_confl S› and
‹conflict_is_false_with_level S›
shows ‹no_smaller_confl T›
using assms
proof (induction rule: cdcl_bnb_stgy.cases)
case (cdcl_bnb_conflict S')
then show ?case
using conflict_no_smaller_confl_inv by blast
next
case (cdcl_bnb_propagate S')
then show ?case
using propagate_no_smaller_confl_inv by blast
next
case (cdcl_bnb_improve S')
then show ?case
by (auto simp: no_smaller_confl_def improvep.simps)
next
case (cdcl_bnb_conflict_opt S')
then show ?case
by (auto simp: no_smaller_confl_def conflict_opt.simps)
next
case (cdcl_bnb_other' S')
show ?case
apply (rule ocdcl⇩W_o_no_smaller_confl_inv)
using cdcl_bnb_other' by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def)
qed
lemma ocdcl⇩W_o_conflict_is_false_with_level_inv:
assumes
"ocdcl⇩W_o S S'" and
lev: "cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)" and
confl_inv: "conflict_is_false_with_level S"
shows "conflict_is_false_with_level S'"
using assms(1,2)
proof (induct rule: ocdcl⇩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 ‹resolve S T›
using resolve.intros[of S L C D T] resolve
by auto
then have ‹cdcl⇩W_restart_mset.resolve (abs_state S) (abs_state T)›
by (simp add: resolve_resolve)
moreover have ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (abs_state S)›
using confl_inv
by (auto simp: cdcl⇩W_restart_mset.conflict_is_false_with_level_def
conflict_is_false_with_level_def abs_state_def cdcl⇩W_restart_mset_state)
ultimately have ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (abs_state T)›
using cdcl⇩W_restart_mset.cdcl⇩W_o_conflict_is_false_with_level_inv[of ‹abs_state S› ‹abs_state T›]
lev confl_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by (auto dest!: cdcl⇩W_restart_mset.cdcl⇩W_o.intros
cdcl⇩W_restart_mset.cdcl⇩W_bj.intros)
then show ‹?case›
by (auto simp: cdcl⇩W_restart_mset.conflict_is_false_with_level_def
conflict_is_false_with_level_def abs_state_def cdcl⇩W_restart_mset_state)
next
case (skip L C' M D T) note tr_S = this(1) and D = this(2) and T = this(5)
have ‹skip S T›
using skip.intros[of S L C' M D T] skip
by auto
then have ‹cdcl⇩W_restart_mset.skip (abs_state S) (abs_state T)›
by (simp add: skip_skip)
moreover have ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (abs_state S)›
using confl_inv
by (auto simp: cdcl⇩W_restart_mset.conflict_is_false_with_level_def
conflict_is_false_with_level_def abs_state_def cdcl⇩W_restart_mset_state)
ultimately have ‹cdcl⇩W_restart_mset.conflict_is_false_with_level (abs_state T)›
using cdcl⇩W_restart_mset.cdcl⇩W_o_conflict_is_false_with_level_inv[of ‹abs_state S› ‹abs_state T›]
lev confl_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by (auto dest!: cdcl⇩W_restart_mset.cdcl⇩W_o.intros
cdcl⇩W_restart_mset.cdcl⇩W_bj.intros)
then show ‹?case›
by (auto simp: cdcl⇩W_restart_mset.conflict_is_false_with_level_def
conflict_is_false_with_level_def abs_state_def cdcl⇩W_restart_mset_state)
next
case backtrack
then show ?case
by (auto split: if_split_asm simp: cdcl⇩W_M_level_inv_decomp lev conflict_is_false_with_level_def)
qed (auto simp: conflict_is_false_with_level_def)
lemma cdcl_bnb_stgy_conflict_is_false_with_level:
assumes ‹cdcl_bnb_stgy S T› and
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
‹no_smaller_confl S› and
‹conflict_is_false_with_level S›
shows ‹conflict_is_false_with_level T›
using assms
proof (induction rule: cdcl_bnb_stgy.cases)
case (cdcl_bnb_conflict S')
then show ?case
using conflict_conflict_is_false_with_level
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def)
next
case (cdcl_bnb_propagate S')
then show ?case
using propagate_conflict_is_false_with_level
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def)
next
case (cdcl_bnb_improve S')
then show ?case
using improve_conflict_is_false_with_level by blast
next
case (cdcl_bnb_conflict_opt S')
then show ?case
using conflict_opt_no_smaller_conflict(2) by blast
next
case (cdcl_bnb_other' S')
show ?case
apply (rule ocdcl⇩W_o_conflict_is_false_with_level_inv)
using cdcl_bnb_other' by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def)
qed
lemma decided_cons_eq_append_decide_cons: ‹Decided L # MM = M' @ Decided K # M ⟷
(M' ≠ [] ∧ hd M' = Decided L ∧ MM = tl M' @ Decided K # M) ∨
(M' = [] ∧ L = K ∧ MM = M)›
by (cases M') auto
lemma either_all_false_or_earliest_decomposition:
shows ‹(∀K K'. L = K' @ K ⟶ ¬P K) ∨
(∃L' L''. L = L'' @ L' ∧ P L' ∧ (∀K K'. L' = K' @ K ⟶ K' ≠ [] ⟶ ¬P K))›
apply (induction L)
subgoal by auto
subgoal for a
by (metis append_Cons append_Nil list.sel(3) tl_append2)
done
lemma trail_is_improving_Ex_improve:
assumes confl: ‹conflicting S = None› and
imp: ‹is_improving (trail S) M' S›
shows ‹Ex (improvep S)›
using assms
by (auto simp: improvep.simps intro!: exI)
definition cdcl_bnb_stgy_inv :: "'st ⇒ bool" where
‹cdcl_bnb_stgy_inv S ⟷ conflict_is_false_with_level S ∧ no_smaller_confl S›
lemma cdcl_bnb_stgy_invD:
shows ‹cdcl_bnb_stgy_inv S ⟷ cdcl⇩W_stgy_invariant S›
unfolding cdcl⇩W_stgy_invariant_def cdcl_bnb_stgy_inv_def
by auto
lemma cdcl_bnb_stgy_stgy_inv:
‹cdcl_bnb_stgy S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
cdcl_bnb_stgy_inv S ⟹ cdcl_bnb_stgy_inv T›
using cdcl⇩W_stgy_cdcl⇩W_stgy_invariant[of S T]
cdcl_bnb_stgy_conflict_is_false_with_level cdcl_bnb_stgy_no_smaller_confl
unfolding cdcl_bnb_stgy_inv_def
by blast
lemma rtranclp_cdcl_bnb_stgy_stgy_inv:
‹cdcl_bnb_stgy⇧*⇧* S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
cdcl_bnb_stgy_inv S ⟹ cdcl_bnb_stgy_inv T›
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for T U
using cdcl_bnb_stgy_stgy_inv rtranclp_cdcl_bnb_stgy_all_struct_inv
rtranclp_cdcl_bnb_stgy_cdcl_bnb by blast
done
lemma learned_clss_learned_clss[simp]:
‹CDCL_W_Abstract_State.learned_clss (abs_state S) = learned_clss S›
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
lemma state_eq_init_clss_abs_state[state_simp, simp]:
‹S ∼ T ⟹ CDCL_W_Abstract_State.init_clss (abs_state S) = CDCL_W_Abstract_State.init_clss (abs_state T)›
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
lemma
init_clss_abs_state_update_conflicting[simp]:
‹CDCL_W_Abstract_State.init_clss (abs_state (update_conflicting (Some D) S)) =
CDCL_W_Abstract_State.init_clss (abs_state S)› and
init_clss_abs_state_cons_trail[simp]:
‹CDCL_W_Abstract_State.init_clss (abs_state (cons_trail K S)) =
CDCL_W_Abstract_State.init_clss (abs_state S)›
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
lemma cdcl_bnb_cdcl⇩W_learned_clauses_entailed_by_init:
assumes
‹cdcl_bnb S T› and
entailed: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (abs_state S)› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (abs_state T)›
using assms(1)
proof (induction rule: cdcl_bnb.cases)
case (cdcl_conflict S')
then show ?case
using entailed
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
elim!: conflictE)
next
case (cdcl_propagate S')
then show ?case
using entailed
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
elim!: propagateE)
next
case (cdcl_improve S')
moreover have ‹set_mset (CDCL_W_Abstract_State.init_clss (abs_state S)) ⊆
set_mset (CDCL_W_Abstract_State.init_clss (abs_state (update_weight_information M' S)))›
if ‹is_improving M M' S› for M M'
using that conflicting_clss_update_weight_information_mono[OF all_struct]
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
ultimately show ?case
using entailed
by (fastforce simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
elim!: improveE intro: true_clss_clss_subsetI)
next
case (cdcl_other' S') note T = this(1) and o = this(2)
show ?case
apply (rule cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed[of ‹abs_state S›])
subgoal
using o unfolding T by (blast dest: cdcl⇩W_o_cdcl⇩W_o cdcl⇩W_restart_mset.other)
subgoal using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast
subgoal using entailed by fast
done
next
case (cdcl_conflict_opt S')
then show ?case
using entailed
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
elim!: conflict_optE)
qed
lemma rtranclp_cdcl_bnb_cdcl⇩W_learned_clauses_entailed_by_init:
assumes
‹cdcl_bnb⇧*⇧* S T› and
entailed: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (abs_state S)› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (abs_state T)›
using assms
by (induction rule: rtranclp_induct)
(auto intro: cdcl_bnb_cdcl⇩W_learned_clauses_entailed_by_init
rtranclp_cdcl_bnb_stgy_all_struct_inv)
lemma atms_of_init_clss_conflicting_clss2[simp]:
‹atms_of_mm (init_clss S) ∪ atms_of_mm (conflicting_clss S) = atms_of_mm (init_clss S)›
using atms_of_conflicting_clss[of S] by blast
lemma no_strange_atm_no_strange_atm[simp]:
‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S) = no_strange_atm S›
using atms_of_conflicting_clss[of S]
unfolding cdcl⇩W_restart_mset.no_strange_atm_def no_strange_atm_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
lemma cdcl⇩W_conflicting_cdcl⇩W_conflicting[simp]:
‹cdcl⇩W_restart_mset.cdcl⇩W_conflicting (abs_state S) = cdcl⇩W_conflicting S›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def cdcl⇩W_conflicting_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
lemma distinct_cdcl⇩W_state_distinct_cdcl⇩W_state:
‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (abs_state S) ⟹ distinct_cdcl⇩W_state S›
unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def distinct_cdcl⇩W_state_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state)
lemma conflicting_abs_state_conflicting[simp]:
‹CDCL_W_Abstract_State.conflicting (abs_state S) = conflicting S› and
clauses_abs_state[simp]:
‹cdcl⇩W_restart_mset.clauses (abs_state S) = clauses S + conflicting_clss S› and
abs_state_tl_trail[simp]:
‹abs_state (tl_trail S) = CDCL_W_Abstract_State.tl_trail (abs_state S)› and
abs_state_add_learned_cls[simp]:
‹abs_state (add_learned_cls C S) = CDCL_W_Abstract_State.add_learned_cls C (abs_state S)› and
abs_state_update_conflicting[simp]:
‹abs_state (update_conflicting D S) = CDCL_W_Abstract_State.update_conflicting D (abs_state S)›
by (auto simp: conflicting.simps abs_state_def cdcl⇩W_restart_mset.clauses_def
init_clss.simps learned_clss.simps clauses_def tl_trail.simps
add_learned_cls.simps update_conflicting.simps)
lemma sim_abs_state_simp: ‹S ∼ T ⟹ abs_state S = abs_state T›
by (auto simp: abs_state_def)
lemma abs_state_cons_trail[simp]:
‹abs_state (cons_trail K S) = CDCL_W_Abstract_State.cons_trail K (abs_state S)› and
abs_state_reduce_trail_to[simp]:
‹abs_state (reduce_trail_to M S) = cdcl⇩W_restart_mset.reduce_trail_to M (abs_state S)›
subgoal by (auto simp: abs_state_def cons_trail.simps)
subgoal by (induction rule: reduce_trail_to_induct)
(auto simp: reduce_trail_to.simps cdcl⇩W_restart_mset.reduce_trail_to.simps)
done
lemma obacktrack_imp_backtrack:
‹obacktrack S T ⟹ cdcl⇩W_restart_mset.backtrack (abs_state S) (abs_state T)›
by (elim obacktrackE, rule_tac D=D and L=L and K=K in cdcl⇩W_restart_mset.backtrack.intros)
(auto elim!: obacktrackE simp: cdcl⇩W_restart_mset.backtrack.simps sim_abs_state_simp)
lemma backtrack_imp_obacktrack:
‹cdcl⇩W_restart_mset.backtrack (abs_state S) T ⟹ Ex (obacktrack S)›
by (elim cdcl⇩W_restart_mset.backtrackE, rule exI,
rule_tac D=D and L=L and K=K in obacktrack.intros)
(auto simp: cdcl⇩W_restart_mset.backtrack.simps obacktrack.simps)
lemma cdcl⇩W_same_weight: ‹cdcl⇩W S U ⟹ weight S = weight U›
by (induction rule: cdcl⇩W.induct)
(auto simp: improvep.simps cdcl⇩W.simps
propagate.simps sim_abs_state_simp abs_state_def cdcl⇩W_restart_mset_state
clauses_def conflict.simps cdcl⇩W_o.simps decide.simps cdcl⇩W_bj.simps
skip.simps resolve.simps backtrack.simps)
lemma ocdcl⇩W_o_same_weight: ‹ocdcl⇩W_o S U ⟹ weight S = weight U›
by (induction rule: ocdcl⇩W_o.induct)
(auto simp: improvep.simps cdcl⇩W.simps cdcl_bnb_bj.simps
propagate.simps sim_abs_state_simp abs_state_def cdcl⇩W_restart_mset_state
clauses_def conflict.simps cdcl⇩W_o.simps decide.simps cdcl⇩W_bj.simps
skip.simps resolve.simps obacktrack.simps)
text ‹This is a proof artefact: it is easier to reason on \<^term>‹improvep› when the set of
initial clauses is fixed (here by \<^term>‹N›). The next theorem shows that the conclusion
is equivalent to not fixing the set of clauses.›
lemma wf_cdcl_bnb:
assumes improve: ‹⋀S T. improvep S T ⟹ init_clss S = N ⟹ (ν (weight T), ν (weight S)) ∈ R› and
wf_R: ‹wf R›
shows ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ∧ cdcl_bnb S T ∧
init_clss S = N}›
(is ‹wf ?A›)
proof -
let ?R = ‹{(T, S). (ν (weight T), ν (weight S)) ∈ R}›
have ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_restart_mset.cdcl⇩W S T}›
by (rule cdcl⇩W_restart_mset.wf_cdcl⇩W)
from wf_if_measure_f[OF this, of abs_state]
have wf: ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ∧
cdcl⇩W_restart_mset.cdcl⇩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: cdcl⇩W_same_weight)
done
moreover have ‹?A ⊆ ?R ∪ ?CDCL›
by (auto dest: cdcl⇩W.intros cdcl⇩W_restart_mset.W_propagate cdcl⇩W_restart_mset.W_other
conflict_conflict propagate_propagate decide_decide improve conflict_opt_conflict
cdcl⇩W_o_cdcl⇩W_o cdcl⇩W_restart_mset.W_conflict W_conflict cdcl⇩W_o.intros cdcl⇩W.intros
cdcl⇩W_o_cdcl⇩W_o
simp: cdcl⇩W_same_weight cdcl_bnb.simps ocdcl⇩W_o_same_weight
elim: conflict_optE)
ultimately show ?thesis
by (rule wf_subset)
qed
corollary wf_cdcl_bnb_fixed_iff:
shows ‹(∀N. wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ∧ cdcl_bnb S T
∧ init_clss S = N}) ⟷
wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ∧ cdcl_bnb S T}›
(is ‹(∀N. wf (?A N)) ⟷ wf ?B›)
proof
assume ‹wf ?B›
then show ‹∀N. wf (?A N)›
by (intro allI, rule wf_subset) auto
next
assume ‹∀N. wf (?A N)›
show ‹wf ?B›
unfolding wf_iff_no_infinite_down_chain
proof
assume ‹∃f. ∀i. (f (Suc i), f i) ∈ ?B›
then obtain f where f: ‹(f (Suc i), f i) ∈ ?B› for i
by blast
then have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state (f n))› for n
by (induction n) auto
with f have st: ‹cdcl_bnb⇧*⇧* (f 0) (f n)› for n
apply (induction n)
subgoal by auto
subgoal by (subst rtranclp_unfold,subst tranclp_unfold_end)
auto
done
let ?N = ‹init_clss (f 0)›
have N: ‹init_clss (f n) = ?N› for n
using st[of n] by (auto dest: rtranclp_cdcl_bnb_no_more_init_clss)
have ‹(f (Suc i), f i) ∈ ?A ?N› for i
using f N by auto
with ‹∀N. wf (?A N)› show False
unfolding wf_iff_no_infinite_down_chain by blast
qed
qed
text ‹The following is a slightly more restricted version of the theorem, because it makes it possible
to add some specific invariant, which can be useful when the proof of the decreasing is complicated.
›
lemma wf_cdcl_bnb_with_additional_inv:
assumes improve: ‹⋀S T. improvep S T ⟹ P S ⟹ init_clss S = N ⟹ (ν (weight T), ν (weight S)) ∈ R› and
wf_R: ‹wf R› and
‹⋀S T. cdcl_bnb S T ⟹ P S ⟹ init_clss S = N ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹ P T›
shows ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ∧ cdcl_bnb S T ∧ P S ∧
init_clss S = N}›
(is ‹wf ?A›)
proof -
let ?R = ‹{(T, S). (ν (weight T), ν (weight S)) ∈ R}›
have ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv S ∧ cdcl⇩W_restart_mset.cdcl⇩W S T}›
by (rule cdcl⇩W_restart_mset.wf_cdcl⇩W)
from wf_if_measure_f[OF this, of abs_state]
have wf: ‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ∧
cdcl⇩W_restart_mset.cdcl⇩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: cdcl⇩W_same_weight)
done
moreover have ‹?A ⊆ ?R ∪ ?CDCL›
using assms(3) cdcl_bnb.intros(3)
by (auto dest: cdcl⇩W.intros cdcl⇩W_restart_mset.W_propagate cdcl⇩W_restart_mset.W_other
conflict_conflict propagate_propagate decide_decide improve conflict_opt_conflict
cdcl⇩W_o_cdcl⇩W_o cdcl⇩W_restart_mset.W_conflict W_conflict cdcl⇩W_o.intros cdcl⇩W.intros
cdcl⇩W_o_cdcl⇩W_o
simp: cdcl⇩W_same_weight cdcl_bnb.simps ocdcl⇩W_o_same_weight
elim: conflict_optE)
ultimately show ?thesis
by (rule wf_subset)
qed
lemma conflict_is_false_with_level_abs_iff:
‹cdcl⇩W_restart_mset.conflict_is_false_with_level (abs_state S) ⟷
conflict_is_false_with_level S›
by (auto simp: cdcl⇩W_restart_mset.conflict_is_false_with_level_def
conflict_is_false_with_level_def)
lemma decide_abs_state_decide:
‹cdcl⇩W_restart_mset.decide (abs_state S) T ⟹ cdcl_bnb_struct_invs S ⟹ Ex(decide S)›
apply (cases rule: cdcl⇩W_restart_mset.decide.cases, assumption)
subgoal for L
apply (rule exI)
apply (rule decide.intros[of _ L])
by (auto simp: cdcl_bnb_struct_invs_def abs_state_def cdcl⇩W_restart_mset_state)
done
lemma cdcl_bnb_no_conflicting_clss_cdcl⇩W:
assumes ‹cdcl_bnb S T› and ‹conflicting_clss T = {#}›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W (abs_state S) (abs_state T) ∧ conflicting_clss S = {#}›
using assms
by (auto simp: cdcl_bnb.simps conflict_opt.simps improvep.simps ocdcl⇩W_o.simps
cdcl_bnb_bj.simps
dest: conflict_conflict propagate_propagate decide_decide skip_skip resolve_resolve
backtrack_backtrack
intro: cdcl⇩W_restart_mset.W_conflict cdcl⇩W_restart_mset.W_propagate cdcl⇩W_restart_mset.W_other
dest: conflicting_clss_update_weight_information_in
elim: conflictE propagateE decideE skipE resolveE improveE obacktrackE)
lemma rtranclp_cdcl_bnb_no_conflicting_clss_cdcl⇩W:
assumes ‹cdcl_bnb⇧*⇧* S T› and ‹conflicting_clss T = {#}›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* (abs_state S) (abs_state T) ∧ conflicting_clss S = {#}›
using assms
by (induction rule: rtranclp_induct)
(fastforce dest: cdcl_bnb_no_conflicting_clss_cdcl⇩W)+
lemma conflict_abs_ex_conflict_no_conflicting:
assumes ‹cdcl⇩W_restart_mset.conflict (abs_state S) T› and ‹conflicting_clss S = {#}›
shows ‹∃T. conflict S T›
using assms by (auto simp: conflict.simps cdcl⇩W_restart_mset.conflict.simps abs_state_def
cdcl⇩W_restart_mset_state clauses_def cdcl⇩W_restart_mset.clauses_def)
lemma propagate_abs_ex_propagate_no_conflicting:
assumes ‹cdcl⇩W_restart_mset.propagate (abs_state S) T› and ‹conflicting_clss S = {#}›
shows ‹∃T. propagate S T›
using assms by (auto simp: propagate.simps cdcl⇩W_restart_mset.propagate.simps abs_state_def
cdcl⇩W_restart_mset_state clauses_def cdcl⇩W_restart_mset.clauses_def)
lemma cdcl_bnb_stgy_no_conflicting_clss_cdcl⇩W_stgy:
assumes ‹cdcl_bnb_stgy S T› and ‹conflicting_clss T = {#}›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy (abs_state S) (abs_state T)›
proof -
have ‹conflicting_clss S = {#}›
using cdcl_bnb_no_conflicting_clss_cdcl⇩W[of S T] assms
by (auto dest: cdcl_bnb_stgy_cdcl_bnb)
then show ?thesis
using assms
by (auto 7 5 simp: cdcl_bnb_stgy.simps conflict_opt.simps ocdcl⇩W_o.simps
cdcl_bnb_bj.simps
dest: conflict_conflict propagate_propagate decide_decide skip_skip resolve_resolve
backtrack_backtrack
dest: cdcl⇩W_restart_mset.cdcl⇩W_stgy.intros cdcl⇩W_restart_mset.cdcl⇩W_o.intros
dest: conflicting_clss_update_weight_information_in
conflict_abs_ex_conflict_no_conflicting
propagate_abs_ex_propagate_no_conflicting
intro: cdcl⇩W_restart_mset.cdcl⇩W_stgy.intros(3)
elim: improveE)
qed
lemma rtranclp_cdcl_bnb_stgy_no_conflicting_clss_cdcl⇩W_stgy:
assumes ‹cdcl_bnb_stgy⇧*⇧* S T› and ‹conflicting_clss T = {#}›
shows ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* (abs_state S) (abs_state T)›
using assms apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for T U
using cdcl_bnb_no_conflicting_clss_cdcl⇩W[of T U, OF cdcl_bnb_stgy_cdcl_bnb]
by (auto dest: cdcl_bnb_stgy_no_conflicting_clss_cdcl⇩W_stgy)
done
context
assumes can_always_improve:
‹⋀S. trail S ⊨asm clauses S ⟹ no_step conflict_opt S ⟹
conflicting S = None ⟹
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
total_over_m (lits_of_l (trail S)) (set_mset (clauses S)) ⟹ Ex (improvep S)›
begin
text ‹The following theorems states a non-obvious (and slightly subtle) property: The fact that there
is no conflicting cannot be shown without additional assumption. However, the assumption that every
model leads to an improvements implies that we end up with a conflict.›
lemma no_step_cdcl_bnb_cdcl⇩W:
assumes
ns: ‹no_step cdcl_bnb S› and
struct_invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹no_step cdcl⇩W_restart_mset.cdcl⇩W (abs_state S)›
proof -
have ns_confl: ‹no_step skip S› ‹no_step resolve S› ‹no_step obacktrack S› and
ns_nc: ‹no_step conflict S› ‹no_step propagate S› ‹no_step improvep S› ‹no_step conflict_opt S›
‹no_step decide S›
using ns
by (auto simp: cdcl_bnb.simps ocdcl⇩W_o.simps cdcl_bnb_bj.simps)
have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)›
using struct_invs unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
have False if st: ‹∃T. cdcl⇩W_restart_mset.cdcl⇩W (abs_state S) T›
proof (cases ‹conflicting S = None›)
case True
have ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
using ns_nc True apply - apply (rule ccontr)
by (force simp: decide.simps total_over_m_def total_over_set_def
Decided_Propagated_in_iff_in_lits_of_l)
then have tot: ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))›
using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: total_over_set_atm_of total_over_m_def clauses_def
abs_state_def init_clss.simps learned_clss.simps trail.simps)
then have ‹trail S ⊨asm clauses S›
using ns_nc True unfolding true_annots_def apply -
apply clarify
subgoal for C
using all_variables_defined_not_imply_cnot[of C ‹trail S›]
by (fastforce simp: conflict.simps total_over_set_atm_of
dest: multi_member_split)
done
from can_always_improve[OF this] have ‹False›
using ns_nc True struct_invs tot by blast
then show ‹?thesis›
by blast
next
case False
have nss: ‹no_step cdcl⇩W_restart_mset.skip (abs_state S)›
‹no_step cdcl⇩W_restart_mset.resolve (abs_state S)›
‹no_step cdcl⇩W_restart_mset.backtrack (abs_state S)›
using ns_confl by (force simp: cdcl⇩W_restart_mset.skip.simps skip.simps
cdcl⇩W_restart_mset.resolve.simps resolve.simps
dest: backtrack_imp_obacktrack)+
then show ‹?thesis›
using that False by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W.simps
cdcl⇩W_restart_mset.propagate.simps cdcl⇩W_restart_mset.conflict.simps
cdcl⇩W_restart_mset.cdcl⇩W_o.simps cdcl⇩W_restart_mset.decide.simps
cdcl⇩W_restart_mset.cdcl⇩W_bj.simps)
qed
then show ‹?thesis› by blast
qed
lemma no_step_cdcl_bnb_stgy:
assumes
n_s: ‹no_step cdcl_bnb S› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
stgy_inv: ‹cdcl_bnb_stgy_inv S›
shows ‹conflicting S = None ∨ conflicting S = Some {#}›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain D where ‹conflicting S = Some D› and ‹D ≠ {#}›
by auto
moreover have ‹no_step cdcl⇩W_restart_mset.cdcl⇩W_stgy (abs_state S)›
using no_step_cdcl_bnb_cdcl⇩W[OF n_s all_struct]
cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W by blast
moreover have le: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (abs_state S)›
using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast
ultimately show False
using cdcl⇩W_restart_mset.conflicting_no_false_can_do_step[of ‹abs_state S›] all_struct stgy_inv le
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl_bnb_stgy_inv_def
by (force dest: distinct_cdcl⇩W_state_distinct_cdcl⇩W_state
simp: conflict_is_false_with_level_abs_iff)
qed
lemma no_step_cdcl_bnb_stgy_empty_conflict:
assumes
n_s: ‹no_step cdcl_bnb S› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
stgy_inv: ‹cdcl_bnb_stgy_inv S›
shows ‹conflicting S = Some {#}›
proof (rule ccontr)
assume H: ‹¬ ?thesis›
have all_struct': ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
by (simp add: all_struct)
have le: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (abs_state S)›
using all_struct
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl_bnb_stgy_inv_def
by auto
have ‹conflicting S = None ∨ conflicting S = Some {#}›
using no_step_cdcl_bnb_stgy[OF n_s all_struct' stgy_inv] .
then have confl: ‹conflicting S = None›
using H by blast
have ‹no_step cdcl⇩W_restart_mset.cdcl⇩W_stgy (abs_state S)›
using no_step_cdcl_bnb_cdcl⇩W[OF n_s all_struct]
cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W by blast
then have entail: ‹trail S ⊨asm clauses S›
using confl cdcl⇩W_restart_mset.cdcl⇩W_stgy_final_state_conclusive2[of ‹abs_state S›]
all_struct stgy_inv le
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl_bnb_stgy_inv_def
by (auto simp: conflict_is_false_with_level_abs_iff)
have ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))›
using cdcl⇩W_restart_mset.no_step_cdcl⇩W_total[OF no_step_cdcl_bnb_cdcl⇩W, of S] all_struct n_s confl
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by auto
with can_always_improve entail confl all_struct
show ‹False›
using n_s by (auto simp: cdcl_bnb.simps)
qed
lemma full_cdcl_bnb_stgy_no_conflicting_clss_unsat:
assumes
full: ‹full cdcl_bnb_stgy S T› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
stgy_inv: ‹cdcl_bnb_stgy_inv S› and
ent_init: ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (abs_state S)› and
[simp]: ‹conflicting_clss T = {#}›
shows ‹unsatisfiable (set_mset (init_clss S))›
proof -
have ns: "no_step cdcl_bnb_stgy T" and
st: "cdcl_bnb_stgy⇧*⇧* S T" and
st': "cdcl_bnb⇧*⇧* S T" and
ns': ‹no_step cdcl_bnb T›
using full unfolding full_def apply (blast dest: rtranclp_cdcl_bnb_stgy_cdcl_bnb)+
using full unfolding full_def
by (metis cdcl_bnb.simps cdcl_bnb_conflict cdcl_bnb_conflict_opt cdcl_bnb_improve
cdcl_bnb_other' cdcl_bnb_propagate no_confl_prop_impr.elims(3))
have struct_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
have [simp]: ‹conflicting_clss S = {#}›
using rtranclp_cdcl_bnb_no_conflicting_clss_cdcl⇩W[OF st'] by auto
have ‹cdcl⇩W_restart_mset.cdcl⇩W_stgy⇧*⇧* (abs_state S) (abs_state T)›
using rtranclp_cdcl_bnb_stgy_no_conflicting_clss_cdcl⇩W_stgy[OF st] by auto
then have ‹full cdcl⇩W_restart_mset.cdcl⇩W_stgy (abs_state S) (abs_state T)›
using no_step_cdcl_bnb_cdcl⇩W[OF ns' struct_T] unfolding full_def
by (auto dest: cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W)
moreover have ‹cdcl⇩W_restart_mset.no_smaller_confl (state_butlast S)›
using stgy_inv ent_init
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def conflict_is_false_with_level_abs_iff
cdcl_bnb_stgy_inv_def conflict_is_false_with_level_abs_iff
cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state cdcl_bnb_stgy_inv_def
no_smaller_confl_def cdcl⇩W_restart_mset.no_smaller_confl_def clauses_def
cdcl⇩W_restart_mset.clauses_def)
ultimately have "conflicting T = Some {#} ∧ unsatisfiable (set_mset (init_clss S))
∨ conflicting T = None ∧ trail T ⊨asm init_clss S"
using cdcl⇩W_restart_mset.full_cdcl⇩W_stgy_inv_normal_form[of ‹abs_state S› ‹abs_state T›] all_struct
stgy_inv ent_init
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def conflict_is_false_with_level_abs_iff
cdcl_bnb_stgy_inv_def conflict_is_false_with_level_abs_iff
cdcl⇩W_restart_mset.cdcl⇩W_stgy_invariant_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state cdcl_bnb_stgy_inv_def)
moreover have ‹cdcl_bnb_stgy_inv T›
using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
ultimately show ‹?thesis›
using no_step_cdcl_bnb_stgy_empty_conflict[OF ns' struct_T] by auto
qed
lemma ocdcl⇩W_o_no_smaller_propa:
assumes ‹ocdcl⇩W_o S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
smaller_propa: ‹no_smaller_propa S› and
n_s: ‹no_confl_prop_impr S›
shows ‹no_smaller_propa T›
using assms(1)
proof (cases)
case decide
show ?thesis
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"]
smaller_propa decide
by (auto simp: no_smaller_propa_def elim!: rulesE)
then show False
using n_s unfolding no_confl_prop_impr.simps by blast
qed
next
case bj
then show ?thesis
proof cases
case skip
then show ?thesis
using assms no_smaller_propa_tl[of S T]
by (auto simp: cdcl_bnb_bj.simps ocdcl⇩W_o.simps obacktrack.simps
resolve.simps
elim!: rulesE)
next
case resolve
then show ?thesis
using assms no_smaller_propa_tl[of S T]
by (auto simp: cdcl_bnb_bj.simps ocdcl⇩W_o.simps obacktrack.simps
resolve.simps
elim!: rulesE)
next
case backtrack
have inv_T: "cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)"
using cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W_all_struct_inv inv assms(1)
using cdcl_bnb_stgy_all_struct_inv cdcl_other' by blast
obtain D D' :: "'v clause" and K L :: "'v literal" and
M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat where
"conflicting S = Some (add_mset L D)" and
decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
"get_level (trail S) L = backtrack_lvl S" and
"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 backtrack by (auto elim!: obacktrackE)
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 lev_inv: "cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)"
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by auto
then have lev_inv_T: "cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state T)"
using inv_T unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by auto
have n_d: "no_dup (trail S)"
using lev_inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def trail.simps)
have n_d_T: "no_dup (trail T)"
using lev_inv_T unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def trail.simps)
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 backtrack 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 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 "M1 ⊨as CNot D'"
using inv_T tr_T unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (force simp: abs_state_def trail.simps conflicting.simps)
then have "get_maximum_level M1 D' = i"
using T i n_d D_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
qed
lemma ocdcl⇩W_no_smaller_propa:
assumes ‹cdcl_bnb_stgy S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
smaller_propa: ‹no_smaller_propa S› and
n_s: ‹no_confl_prop_impr S›
shows ‹no_smaller_propa T›
using assms
apply (cases)
subgoal by (auto)
subgoal by (auto)
subgoal by (auto elim!: improveE simp: no_smaller_propa_def)
subgoal by (auto elim!: conflict_optE simp: no_smaller_propa_def)
subgoal using ocdcl⇩W_o_no_smaller_propa by fast
done
text ‹Unfortunately, we cannot reuse the proof we have alrealy done.›
lemma ocdcl⇩W_no_relearning:
assumes ‹cdcl_bnb_stgy S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
smaller_propa: ‹no_smaller_propa S› and
n_s: ‹no_confl_prop_impr S› and
dist: ‹distinct_mset (clauses S)›
shows ‹distinct_mset (clauses T)›
using assms(1)
proof cases
case cdcl_bnb_conflict
then show ?thesis using dist by (auto elim: rulesE)
next
case cdcl_bnb_propagate
then show ?thesis using dist by (auto elim: rulesE)
next
case cdcl_bnb_improve
then show ?thesis using dist by (auto elim: improveE)
next
case cdcl_bnb_conflict_opt
then show ?thesis using dist by (auto elim: conflict_optE)
next
case cdcl_bnb_other'
then show ?thesis
proof cases
case decide
then show ?thesis using dist by (auto elim: rulesE)
next
case bj
then show ?thesis
proof cases
case skip
then show ?thesis using dist by (auto elim: rulesE)
next
case resolve
then show ?thesis using dist by (auto elim: rulesE)
next
case backtrack
have smaller_propa: ‹⋀M K M' D L.
trail S = M' @ Decided K # M ⟹
D + {#L#} ∈# clauses S ⟹ undefined_lit M L ⟹ ¬ M ⊨as CNot D›
using smaller_propa unfolding no_smaller_propa_def by fast
have inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using inv
using cdcl⇩W_restart_mset.cdcl⇩W_stgy_cdcl⇩W_all_struct_inv inv assms(1)
using cdcl_bnb_stgy_all_struct_inv cdcl_other' backtrack ocdcl⇩W_o.intros
cdcl_bnb_bj.intros
by blast
then have n_d: ‹no_dup (trail T)› and
ent: ‹⋀L mark a b.
a @ Propagated L mark # b = trail T ⟹
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto simp: abs_state_def trail.simps)
show ?thesis
proof (rule ccontr)
assume H: ‹¬?thesis›
obtain D D' :: "'v clause" and K L :: "'v literal" and
M1 M2 :: "('v, 'v clause) ann_lit list" and i :: nat where
"conflicting S = Some (add_mset L D)" and
decomp: "(Decided K # M1, M2) ∈ set (get_all_ann_decomposition (trail S))" and
"get_level (trail S) L = backtrack_lvl S" and
"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 backtrack by (auto elim!: obacktrackE)
from H T dist have LD': ‹add_mset L D' ∈# clauses S›
by auto
have ‹¬M1 ⊨as CNot D'›
using get_all_ann_decomposition_exists_prepend[OF decomp] apply (elim exE)
by (rule smaller_propa[of ‹_ @ M2› K M1 D' L])
(use n_d T decomp LD' in auto)
moreover have ‹M1 ⊨as CNot D'›
using ent[of ‹[]› L ‹add_mset L D'› M1] T decomp by auto
ultimately show False
..
qed
qed
qed
qed
lemma full_cdcl_bnb_stgy_unsat:
assumes
st: ‹full cdcl_bnb_stgy S T› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
opt_struct: ‹cdcl_bnb_struct_invs S› and
stgy_inv: ‹cdcl_bnb_stgy_inv S›
shows
‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
proof -
have ns: ‹no_step cdcl_bnb_stgy T› and
st: ‹cdcl_bnb_stgy⇧*⇧* S T› and
st': ‹cdcl_bnb⇧*⇧* S T›
using st unfolding full_def by (auto intro: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
have ns': ‹no_step cdcl_bnb T›
by (meson cdcl_bnb.cases cdcl_bnb_stgy.simps no_confl_prop_impr.elims(3) ns)
have struct_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
have stgy_T: ‹cdcl_bnb_stgy_inv T›
using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
have confl: ‹conflicting T = Some {#}›
using no_step_cdcl_bnb_stgy_empty_conflict[OF ns' struct_T stgy_T] .
have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (abs_state T)› and
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state T)›
using struct_T unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
then have ent': ‹set_mset (clauses T + conflicting_clss T) ⊨p {#}›
using confl unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by auto
show ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
proof
assume ‹satisfiable (set_mset (clauses T + conflicting_clss T))›
then obtain I where
ent'': ‹I ⊨sm clauses T + conflicting_clss T› and
tot: ‹total_over_m I (set_mset (clauses T + conflicting_clss T))› and
‹consistent_interp I›
unfolding satisfiable_def
by blast
then show ‹False›
using ent'
unfolding true_clss_cls_def by auto
qed
qed
end
lemma cdcl_bnb_reasons_in_clauses:
‹cdcl_bnb S T ⟹ reasons_in_clauses S ⟹ reasons_in_clauses T›
by (auto simp: cdcl_bnb.simps reasons_in_clauses_def ocdcl⇩W_o.simps
cdcl_bnb_bj.simps get_all_mark_of_propagated_tl_proped
elim!: rulesE improveE conflict_optE obacktrackE
dest!: in_set_tlD
dest!: get_all_ann_decomposition_exists_prepend)
end
subsubsection ‹OCDCL›
text ‹
The following datatype is equivalent to \<^typ>‹'a option›. Howover, it has the opposite
ordering. Therefore, I decided to use a different type instead of have a second order
which conflicts with 🗏‹~~/src/HOL/Library/Option_ord.thy›.
›
datatype 'a optimal_model = Not_Found | is_found: Found (the_optimal: 'a)
instantiation optimal_model :: (ord) ord
begin
fun less_optimal_model :: ‹'a :: ord optimal_model ⇒ 'a optimal_model ⇒ bool› where
‹less_optimal_model Not_Found _ = False›
| ‹less_optimal_model (Found _) Not_Found ⟷ True›
| ‹less_optimal_model (Found a) (Found b) ⟷ a < b›
fun less_eq_optimal_model :: ‹'a :: ord optimal_model ⇒ 'a optimal_model ⇒ bool› where
‹less_eq_optimal_model Not_Found Not_Found = True›
| ‹less_eq_optimal_model Not_Found (Found _) = False›
| ‹less_eq_optimal_model (Found _) Not_Found ⟷ True›
| ‹less_eq_optimal_model (Found a) (Found b) ⟷ a ≤ b›
instance
by standard
end
instance optimal_model :: (preorder) preorder
apply standard
subgoal for a b
by (cases a; cases b) (auto simp: less_le_not_le)
subgoal for a
by (cases a) auto
subgoal for a b c
by (cases a; cases b; cases c) (auto dest: order_trans)
done
instance optimal_model :: (order) order
apply standard
subgoal for a b
by (cases a; cases b) (auto simp: less_le_not_le)
done
instance optimal_model :: (linorder) linorder
apply standard
subgoal for a b
by (cases a; cases b) (auto simp: less_le_not_le)
done
instantiation optimal_model :: (wellorder) wellorder
begin
lemma wf_less_optimal_model: "wf {(M :: 'a optimal_model, N). M < N}"
proof -
have 1: ‹{(M :: 'a optimal_model, N). M < N} =
map_prod Found Found ` {(M :: 'a, N). M < N} ∪
{(a, b). a ≠ Not_Found ∧ b = Not_Found}› (is ‹?A = ?B ∪ ?C›)
apply (auto simp: image_iff)
apply (case_tac a; case_tac b)
apply auto
apply (case_tac a)
apply auto
done
have [simp]: ‹inj Found›
by (auto simp:inj_on_def)
have ‹wf ?B›
by (rule wf_map_prod_image) (auto intro: wf)
moreover have ‹wf ?C›
by (rule wfI_pf) auto
ultimately show ‹wf (?A)›
unfolding 1
by (rule wf_Un) (auto)
qed
instance by standard (metis CollectI split_conv wf_def wf_less_optimal_model)
end
text ‹This locales includes only the assumption we make on the weight function.›
locale ocdcl_weight =
fixes
ρ :: ‹'v clause ⇒ 'a :: {linorder}›
assumes
ρ_mono: ‹distinct_mset B ⟹ A ⊆# B ⟹ ρ A ≤ ρ B›
begin
lemma ρ_empty_simp[simp]:
assumes ‹consistent_interp (set_mset A)› ‹distinct_mset A›
shows ‹ρ A ≥ ρ {#}› ‹¬ρ A < ρ {#}› ‹ρ A ≤ ρ {#} ⟷ ρ A = ρ {#}›
using ρ_mono[of A ‹{#}›] assms
by auto
abbreviation ρ' :: ‹'v clause option ⇒ 'a optimal_model› where
‹ρ' w ≡ (case w of None ⇒ Not_Found | Some w ⇒ Found (ρ w))›
definition is_improving_int
:: "('v literal, 'v literal, 'b) annotated_lits ⇒ ('v literal, 'v literal, 'b) annotated_lits ⇒ 'v clauses ⇒
'v clause option ⇒ bool"
where
‹is_improving_int M M' N w ⟷ Found (ρ (lit_of `# mset M')) < ρ' w ∧
M' ⊨asm N ∧ no_dup M' ∧
lit_of `# mset M' ∈ simple_clss (atms_of_mm N) ∧
total_over_m (lits_of_l M') (set_mset N) ∧
(∀M'. total_over_m (lits_of_l M') (set_mset N) ⟶ mset M ⊆# mset M' ⟶
lit_of `# mset M' ∈ simple_clss (atms_of_mm N) ⟶
ρ (lit_of `# mset M') = ρ (lit_of `# mset M))›
definition too_heavy_clauses
:: ‹'v clauses ⇒ 'v clause option ⇒ 'v clauses›
where
‹too_heavy_clauses M w =
{#pNeg C | C ∈# mset_set (simple_clss (atms_of_mm M)). ρ' w ≤ Found (ρ C)#}›
definition conflicting_clauses
:: ‹'v clauses ⇒ 'v clause option ⇒ 'v clauses›
where
‹conflicting_clauses N w =
{#C ∈# mset_set (simple_clss (atms_of_mm N)). too_heavy_clauses N w ⊨pm C#}›
lemma too_heavy_clauses_conflicting_clauses:
‹C ∈# too_heavy_clauses M w ⟹ C ∈# conflicting_clauses M w›
by (auto simp: conflicting_clauses_def too_heavy_clauses_def simple_clss_finite)
lemma too_heavy_clauses_contains_itself:
‹M ∈ simple_clss (atms_of_mm N) ⟹ pNeg M ∈# too_heavy_clauses N (Some M)›
by (auto simp: too_heavy_clauses_def simple_clss_finite)
lemma too_heavy_clause_None[simp]: ‹too_heavy_clauses M None = {#}›
by (auto simp: too_heavy_clauses_def)
lemma atms_of_mm_too_heavy_clauses_le:
‹atms_of_mm (too_heavy_clauses M I) ⊆ atms_of_mm M›
by (auto simp: too_heavy_clauses_def atms_of_ms_def
simple_clss_finite dest: simple_clssE)
lemma
atms_too_heavy_clauses_None:
‹atms_of_mm (too_heavy_clauses M None) = {}› and
atms_too_heavy_clauses_Some:
‹atms_of w ⊆ atms_of_mm M ⟹ distinct_mset w ⟹ ¬tautology w ⟹
atms_of_mm (too_heavy_clauses M (Some w)) = atms_of_mm M›
proof -
show ‹atms_of_mm (too_heavy_clauses M None) = {}›
by (auto simp: too_heavy_clauses_def)
assume atms: ‹atms_of w ⊆ atms_of_mm M› and
dist: ‹distinct_mset w› and
taut: ‹¬tautology w›
have ‹atms_of_mm (too_heavy_clauses M (Some w)) ⊆ atms_of_mm M›
by (auto simp: too_heavy_clauses_def atms_of_ms_def simple_clss_finite)
(auto simp: simple_clss_def)
let ?w = ‹w + Neg `# {#x ∈# mset_set (atms_of_mm M). x ∉ atms_of w#}›
have [simp]: ‹inj_on Neg A› for A
by (auto simp: inj_on_def)
have [simp]: ‹distinct_mset (uminus `# w)›
by (subst distinct_image_mset_inj)
(auto simp: dist inj_on_def)
have dist: ‹distinct_mset ?w›
using dist
by (auto simp: distinct_mset_add distinct_image_mset_inj distinct_mset_mset_set uminus_lit_swap
disjunct_not_in dest: multi_member_split)
moreover have not_tauto: ‹¬tautology ?w›
by (auto simp: tautology_union taut uminus_lit_swap dest: multi_member_split)
ultimately have ‹?w ∈ (simple_clss (atms_of_mm M))›
using atms by (auto simp: simple_clss_def)
moreover have ‹ρ ?w ≥ ρ w›
by (rule ρ_mono) (use dist not_tauto in ‹auto simp: consistent_interp_tuatology_mset_set tautology_decomp›)
ultimately have ‹pNeg ?w ∈# too_heavy_clauses M (Some w)›
by (auto simp: too_heavy_clauses_def simple_clss_finite)
then have ‹atms_of_mm M ⊆ atms_of_mm (too_heavy_clauses M (Some w))›
by (auto dest!: multi_member_split)
then show ‹atms_of_mm (too_heavy_clauses M (Some w)) = atms_of_mm M›
using ‹atms_of_mm (too_heavy_clauses M (Some w)) ⊆ atms_of_mm M› by blast
qed
lemma entails_too_heavy_clauses_too_heavy_clauses:
assumes
‹consistent_interp I› and
tot: ‹total_over_m I (set_mset (too_heavy_clauses M w))› and
‹I ⊨m too_heavy_clauses M w› and
w: ‹w ≠ None ⟹ atms_of (the w) ⊆ atms_of_mm M›
‹w ≠ None ⟹ ¬tautology (the w)›
‹w ≠ None ⟹ distinct_mset (the w)›
shows ‹I ⊨m conflicting_clauses M w›
proof (cases w)
case None
have [simp]: ‹{x ∈ simple_clss (atms_of_mm M). tautology x} = {}›
by (auto dest: simple_clssE)
show ?thesis
using None by (auto simp: conflicting_clauses_def true_clss_cls_tautology_iff
simple_clss_finite)
next
case w': (Some w')
have ‹x ∈# mset_set (simple_clss (atms_of_mm M)) ⟹ total_over_set I (atms_of x)› for x
using tot w atms_too_heavy_clauses_Some[of w' M] unfolding w'
by (auto simp: total_over_m_def simple_clss_finite total_over_set_alt_def
dest!: simple_clssE)
then show ?thesis
using assms
by (subst true_cls_mset_def)
(auto simp: conflicting_clauses_def true_clss_cls_def
dest!: spec[of _ I])
qed
lemma not_entailed_too_heavy_clauses_ge:
‹C ∈ simple_clss (atms_of_mm N) ⟹ ¬ too_heavy_clauses N w ⊨pm pNeg C ⟹ ¬Found (ρ C) ≥ ρ' w›
using true_clss_cls_in[of ‹pNeg C› ‹set_mset (too_heavy_clauses N w)›]
too_heavy_clauses_contains_itself
by (auto simp: too_heavy_clauses_def simple_clss_finite
image_iff)
lemma pNeg_simple_clss_iff[simp]:
‹pNeg C ∈ simple_clss N ⟷ C ∈ simple_clss N›
by (auto simp: simple_clss_def)
lemma conflicting_clss_incl_init_clauses:
‹atms_of_mm (conflicting_clauses N w) ⊆ atms_of_mm (N)›
unfolding conflicting_clauses_def
apply (auto simp: simple_clss_finite)
by (auto simp: simple_clss_def atms_of_ms_def split: if_splits)
lemma distinct_mset_mset_conflicting_clss2: ‹distinct_mset_mset (conflicting_clauses N w)›
unfolding conflicting_clauses_def distinct_mset_set_def
apply (auto simp: simple_clss_finite)
by (auto simp: simple_clss_def)
lemma too_heavy_clauses_mono:
‹ρ a > ρ (lit_of `# mset M) ⟹ too_heavy_clauses N (Some a) ⊆#
too_heavy_clauses N (Some (lit_of `# mset M))›
by (auto simp: too_heavy_clauses_def multiset_filter_mono2
intro!: multiset_filter_mono image_mset_subseteq_mono)
lemma is_improving_conflicting_clss_update_weight_information: ‹is_improving_int M M' N w ⟹
conflicting_clauses N w ⊆# conflicting_clauses N (Some (lit_of `# mset M'))›
using too_heavy_clauses_mono[of M' ‹the w› ‹N›]
by (cases ‹w›)
(auto simp: is_improving_int_def conflicting_clauses_def
simp: multiset_filter_mono2
intro!: image_mset_subseteq_mono
intro: true_clss_cls_subset
dest: simple_clssE)
lemma conflicting_clss_update_weight_information_in2:
assumes ‹is_improving_int M M' N w›
shows ‹negate_ann_lits M' ∈# conflicting_clauses N (Some (lit_of `# mset M'))›
using assms apply (auto simp: simple_clss_finite
conflicting_clauses_def is_improving_int_def)
by (auto simp: is_improving_int_def conflicting_clauses_def
simp: multiset_filter_mono2 simple_clss_def lits_of_def
negate_ann_lits_pNeg_lit_of image_iff dest: total_over_m_atms_incl
intro!: true_clss_cls_in too_heavy_clauses_contains_itself)
lemma atms_of_init_clss_conflicting_clauses'[simp]:
‹atms_of_mm N ∪ atms_of_mm (conflicting_clauses N S) = atms_of_mm N›
using conflicting_clss_incl_init_clauses[of N] by blast
lemma entails_too_heavy_clauses_if_le:
assumes
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm N› and
le: ‹Found (ρ I) < ρ' (Some M')›
shows
‹set_mset I ⊨m too_heavy_clauses N (Some M')›
proof -
show ‹set_mset I ⊨m too_heavy_clauses N (Some M')›
unfolding true_cls_mset_def
proof
fix C
assume ‹C ∈# too_heavy_clauses N (Some M')›
then obtain x where
[simp]: ‹C = pNeg x› and
x: ‹x ∈ simple_clss (atms_of_mm N)› and
we: ‹ρ M' ≤ ρ x›
unfolding too_heavy_clauses_def
by (auto simp: simple_clss_finite)
then have ‹x ≠ I›
using le
by auto
then have ‹set_mset x ≠ set_mset I›
using distinct_set_mset_eq_iff[of x I] x dist
by (auto simp: simple_clss_def)
then have ‹∃a. ((a ∈# x ∧ a ∉# I) ∨ (a ∈# I ∧ a ∉# x))›
by auto
moreover have not_incl: ‹¬set_mset x ⊆ set_mset I›
using ρ_mono[of I ‹x›] we le distinct_set_mset_eq_iff[of x I] simple_clssE[OF x]
dist cons
by auto
moreover have ‹x ≠ {#}›
using we le cons dist not_incl
by auto
ultimately obtain L where
L_x: ‹L ∈# x› and
‹L ∉# I›
by auto
moreover have ‹atms_of x ⊆ atms_of I›
using simple_clssE[OF x] tot
atm_iff_pos_or_neg_lit[of a I] atm_iff_pos_or_neg_lit[of a x]
by (auto dest!: multi_member_split)
ultimately have ‹-L ∈# I›
using tot simple_clssE[OF x] atm_of_notin_atms_of_iff
by auto
then show ‹set_mset I ⊨ C›
using L_x by (auto simp: simple_clss_finite pNeg_def dest!: multi_member_split)
qed
qed
lemma entails_conflicting_clauses_if_le:
fixes M''
defines ‹M' ≡ lit_of `# mset M''›
assumes
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm N› and
le: ‹Found (ρ I) < ρ' (Some M')› and
‹is_improving_int M M'' N w›
shows
‹set_mset I ⊨m conflicting_clauses N (Some (lit_of `# mset M''))›
proof -
show ?thesis
apply (rule entails_too_heavy_clauses_too_heavy_clauses)
subgoal using cons by auto
subgoal
using assms unfolding is_improving_int_def
by (auto simp: total_over_m_alt_def M'_def atms_of_def
atms_too_heavy_clauses_Some eq_commute[of _ ‹atms_of_mm N›]
lit_in_set_iff_atm
dest: multi_member_split
dest!: simple_clssE)
subgoal
using entails_too_heavy_clauses_if_le[OF assms(2-5)]
by (auto simp: M'_def)
subgoal
using assms unfolding is_improving_int_def
by (auto simp: M'_def lits_of_def image_image
dest!: simple_clssE)
subgoal
using assms unfolding is_improving_int_def
by (auto simp: M'_def lits_of_def image_image
dest!: simple_clssE)
subgoal
using assms unfolding is_improving_int_def
by (auto simp: M'_def lits_of_def image_image
dest!: simple_clssE)
done
qed
end
text ‹This is one of the version of the weight functions used by Christoph Weidenbach.›
locale ocdcl_weight_WB =
fixes
ν :: ‹'v literal ⇒ nat›
begin
definition ρ :: ‹'v clause ⇒ nat› where
‹ρ M = (∑A ∈# M. ν A)›
sublocale ocdcl_weight ρ
by (unfold_locales)
(auto simp: ρ_def sum_image_mset_mono)
end
locale conflict_driven_clause_learning⇩W_optimal_weight =
conflict_driven_clause_learning⇩W
state_eq
state
trail init_clss learned_clss conflicting
cons_trail tl_trail add_learned_cls remove_cls
update_conflicting
init_state +
ocdcl_weight ρ
for
state_eq :: "'st ⇒ 'st ⇒ bool" (infix "∼" 50) and
state :: "'st ⇒ ('v, 'v clause) ann_lits × 'v clauses × 'v clauses × 'v clause option ×
'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" and
ρ :: ‹'v clause ⇒ 'a :: {linorder}› +
fixes
update_additional_info :: ‹'v clause option × 'b ⇒ 'st ⇒ 'st›
assumes
update_additional_info:
‹state S = (M, N, U, C, K) ⟹ state (update_additional_info K' S) = (M, N, U, C, K')› and
weight_init_state:
‹⋀N :: 'v clauses. fst (additional_info (init_state N)) = None›
begin
thm conflicting_clss_incl_init_clauses
definition update_weight_information :: ‹('v, 'v clause) ann_lits ⇒ 'st ⇒ 'st› where
‹update_weight_information M S =
update_additional_info (Some (lit_of `# mset M), snd (additional_info S)) S›
lemma
trail_update_additional_info[simp]: ‹trail (update_additional_info w S) = trail S› and
init_clss_update_additional_info[simp]:
‹init_clss (update_additional_info w S) = init_clss S› and
learned_clss_update_additional_info[simp]:
‹learned_clss (update_additional_info w S) = learned_clss S› and
backtrack_lvl_update_additional_info[simp]:
‹backtrack_lvl (update_additional_info w S) = backtrack_lvl S› and
conflicting_update_additional_info[simp]:
‹conflicting (update_additional_info w S) = conflicting S› and
clauses_update_additional_info[simp]:
‹clauses (update_additional_info w S) = clauses S›
using update_additional_info[of S] unfolding clauses_def
by (subst (asm) state_prop; subst (asm) state_prop; auto; fail)+
lemma
trail_update_weight_information[simp]:
‹trail (update_weight_information w S) = trail S› and
init_clss_update_weight_information[simp]:
‹init_clss (update_weight_information w S) = init_clss S› and
learned_clss_update_weight_information[simp]:
‹learned_clss (update_weight_information w S) = learned_clss S› and
backtrack_lvl_update_weight_information[simp]:
‹backtrack_lvl (update_weight_information w S) = backtrack_lvl S› and
conflicting_update_weight_information[simp]:
‹conflicting (update_weight_information w S) = conflicting S› and
clauses_update_weight_information[simp]:
‹clauses (update_weight_information w S) = clauses S›
using update_additional_info[of S] unfolding update_weight_information_def by auto
definition weight where
‹weight S = fst (additional_info S)›
lemma
additional_info_update_additional_info[simp]:
"additional_info (update_additional_info w S) = w"
unfolding additional_info_def using update_additional_info[of S]
by (cases ‹state S›; auto; fail)+
lemma
weight_cons_trail2[simp]: ‹weight (cons_trail L S) = weight S› and
clss_tl_trail2[simp]: "weight (tl_trail S) = weight S" and
weight_add_learned_cls_unfolded:
"weight (add_learned_cls U S) = weight S"
and
weight_update_conflicting2[simp]: "weight (update_conflicting D S) = weight S" and
weight_remove_cls2[simp]:
"weight (remove_cls C S) = weight S" and
weight_add_learned_cls2[simp]:
"weight (add_learned_cls C S) = weight S" and
weight_update_weight_information2[simp]:
"weight (update_weight_information M S) = Some (lit_of `# mset M)"
by (auto simp: update_weight_information_def weight_def)
sublocale conflict_driven_clause_learning⇩W
where
state_eq = state_eq and
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state
by unfold_locales
sublocale conflict_driven_clause_learning_with_adding_init_clause_cost⇩W_no_state
where
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state and
weight = weight and
update_weight_information = update_weight_information and
is_improving_int = is_improving_int and
conflicting_clauses = conflicting_clauses
by unfold_locales
lemma state_additional_info':
‹state S = (trail S, init_clss S, learned_clss S, conflicting S, weight S, additional_info' S)›
unfolding additional_info'_def by (cases ‹state S›; auto simp: state_prop weight_def)
lemma state_update_weight_information:
‹state S = (M, N, U, C, w, other) ⟹
∃w'. state (update_weight_information T S) = (M, N, U, C, w', other)›
unfolding update_weight_information_def by (cases ‹state S›; auto simp: state_prop weight_def)
lemma atms_of_init_clss_conflicting_clauses[simp]:
‹atms_of_mm (init_clss S) ∪ atms_of_mm (conflicting_clss S) = atms_of_mm (init_clss S)›
using conflicting_clss_incl_init_clauses[of ‹(init_clss S)›] unfolding conflicting_clss_def by blast
lemma lit_of_trail_in_simple_clss: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def abs_state_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: simple_clss_def cdcl⇩W_restart_mset_state atms_of_def pNeg_def lits_of_def
dest: no_dup_not_tautology no_dup_distinct)
lemma pNeg_lit_of_trail_in_simple_clss: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
pNeg (lit_of `# mset (trail S)) ∈ simple_clss (atms_of_mm (init_clss S))›
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def abs_state_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: simple_clss_def cdcl⇩W_restart_mset_state atms_of_def pNeg_def lits_of_def
dest: no_dup_not_tautology_uminus no_dup_distinct_uminus)
lemma conflict_clss_update_weight_no_alien:
‹atms_of_mm (conflicting_clss (update_weight_information M S))
⊆ atms_of_mm (init_clss S)›
by (auto simp: conflicting_clss_def conflicting_clauses_def atms_of_ms_def
cdcl⇩W_restart_mset_state simple_clss_finite
dest: simple_clssE)
sublocale state⇩W_no_state
where
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state
by unfold_locales
sublocale state⇩W_no_state
where
state_eq = state_eq and
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state
by unfold_locales
sublocale conflict_driven_clause_learning⇩W
where
state_eq = state_eq and
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state
by unfold_locales
lemma is_improving_conflicting_clss_update_weight_information': ‹is_improving M M' S ⟹
conflicting_clss S ⊆# conflicting_clss (update_weight_information M' S)›
using is_improving_conflicting_clss_update_weight_information[of M M' ‹init_clss S› ‹weight S›]
unfolding conflicting_clss_def
by auto
lemma conflicting_clss_update_weight_information_in2':
assumes ‹is_improving M M' S›
shows ‹negate_ann_lits M' ∈# conflicting_clss (update_weight_information M' S)›
using conflicting_clss_update_weight_information_in2[of M M' ‹init_clss S› ‹weight S›] assms
unfolding conflicting_clss_def
by auto
sublocale conflict_driven_clause_learning_with_adding_init_clause_cost⇩W_ops
where
state = state and
trail = trail and
init_clss = init_clss and
learned_clss = learned_clss and
conflicting = conflicting and
cons_trail = cons_trail and
tl_trail = tl_trail and
add_learned_cls = add_learned_cls and
remove_cls = remove_cls and
update_conflicting = update_conflicting and
init_state = init_state and
weight = weight and
update_weight_information = update_weight_information and
is_improving_int = is_improving_int and
conflicting_clauses = conflicting_clauses
apply unfold_locales
subgoal by (rule state_additional_info')
subgoal by (rule state_update_weight_information)
subgoal unfolding conflicting_clss_def by (rule conflicting_clss_incl_init_clauses)
subgoal unfolding conflicting_clss_def by (rule distinct_mset_mset_conflicting_clss2)
subgoal by (rule is_improving_conflicting_clss_update_weight_information')
subgoal by (rule conflicting_clss_update_weight_information_in2'; assumption)
done
lemma wf_cdcl_bnb_fixed:
‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ∧ cdcl_bnb S T
∧ init_clss S = N}›
apply (rule wf_cdcl_bnb[of N id ‹{(I', I). I' ≠ None ∧
(the I') ∈ simple_clss (atms_of_mm N) ∧ (ρ' I', ρ' I) ∈ {(j, i). j < i}}›])
subgoal for S T
by (cases ‹weight S›; cases ‹weight T›)
(auto simp: improvep.simps is_improving_int_def split: enat.splits)
subgoal
apply (rule wf_finite_segments)
subgoal by (auto simp: irrefl_def)
subgoal
apply (auto simp: irrefl_def trans_def intro: less_trans[of ‹Found _› ‹Found _›])
apply (rule less_trans[of ‹Found _› ‹Found _›])
apply auto
done
subgoal for x
by (subgoal_tac ‹{y. (y, x)
∈ {(I', I).
I' ≠ None ∧
the I' ∈ simple_clss (atms_of_mm N) ∧
(ρ' I', ρ' I) ∈ {(j, i). j < i}}} =
Some ` {y. (y, x)
∈ {(I', I).
I' ∈ simple_clss (atms_of_mm N) ∧
(ρ' (Some I'), ρ' I) ∈ {(j, i). j < i}}}›)
(auto simp: finite_image_iff
intro: finite_subset[OF _ simple_clss_finite[of ‹atms_of_mm N›]])
done
done
lemma wf_cdcl_bnb2:
‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)
∧ cdcl_bnb S T}›
by (subst wf_cdcl_bnb_fixed_iff[symmetric]) (intro allI, rule wf_cdcl_bnb_fixed)
lemma can_always_improve:
assumes
ent: ‹trail S ⊨asm clauses S› and
total: ‹total_over_m (lits_of_l (trail S)) (set_mset (clauses S))› and
n_s: ‹no_step conflict_opt S› and
confl: ‹conflicting S = None› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹Ex (improvep S)›
proof -
have H: ‹(lit_of `# mset (trail S)) ∈# mset_set (simple_clss (atms_of_mm (init_clss S)))›
‹(lit_of `# mset (trail S)) ∈ simple_clss (atms_of_mm (init_clss S))›
‹no_dup (trail S)›
apply (subst finite_set_mset_mset_set[OF simple_clss_finite])
using all_struct by (auto simp: simple_clss_def cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
no_strange_atm_def atms_of_def lits_of_def image_image
cdcl⇩W_M_level_inv_def clauses_def
dest: no_dup_not_tautology no_dup_distinct)
then have le: ‹Found (ρ (lit_of `# mset (trail S))) < ρ' (weight S)›
using n_s confl total
by (auto simp: conflict_opt.simps conflicting_clss_def lits_of_def
conflicting_clauses_def clauses_def negate_ann_lits_pNeg_lit_of image_iff
simple_clss_finite subset_iff
dest!: spec[of _ ‹(lit_of `# mset (trail S))›]
dest: not_entailed_too_heavy_clauses_ge)
have tr: ‹trail S ⊨asm init_clss S›
using ent by (auto simp: clauses_def)
have tot': ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
using total all_struct by (auto simp: total_over_m_def total_over_set_def
cdcl⇩W_all_struct_inv_def clauses_def
no_strange_atm_def)
have M': ‹ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))›
if ‹total_over_m (lits_of_l M') (set_mset (init_clss S))› and
incl: ‹mset (trail S) ⊆# mset M'› and
‹lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S))›
for M'
proof -
have [simp]: ‹lits_of_l M' = set_mset (lit_of `# mset M')›
by (auto simp: lits_of_def)
obtain A where A: ‹mset M' = A + mset (trail S)›
using incl by (auto simp: mset_subset_eq_exists_conv)
have M': ‹lits_of_l M' = lit_of ` set_mset A ∪ lits_of_l (trail S)›
unfolding lits_of_def
by (metis A image_Un set_mset_mset set_mset_union)
have ‹mset M' = mset (trail S)›
using that tot' total unfolding A total_over_m_alt_def
apply (case_tac A)
apply (auto simp: A simple_clss_def distinct_mset_add M' image_Un
tautology_union mset_inter_empty_set_mset atms_of_def atms_of_s_def
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set image_image
tautology_add_mset)
by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
lits_of_def subsetCE)
then show ?thesis
using total by auto
qed
have ‹is_improving (trail S) (trail S) S›
if ‹Found (ρ (lit_of `# mset (trail S))) < ρ' (weight S)›
using that total H confl tr tot' M' unfolding is_improving_int_def lits_of_def
by fast
then show ‹Ex (improvep S)›
using improvep.intros[of S ‹trail S› ‹update_weight_information (trail S) S›] total H confl le
by fast
qed
lemma no_step_cdcl_bnb_stgy_empty_conflict2:
assumes
n_s: ‹no_step cdcl_bnb S› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
stgy_inv: ‹cdcl_bnb_stgy_inv S›
shows ‹conflicting S = Some {#}›
by (rule no_step_cdcl_bnb_stgy_empty_conflict[OF can_always_improve assms])
lemma cdcl_bnb_larger_still_larger:
assumes
‹cdcl_bnb S T›
shows ‹ρ' (weight S) ≥ ρ' (weight T)›
using assms apply (cases rule: cdcl_bnb.cases)
by (auto simp: conflict.simps decide.simps propagate.simps improvep.simps is_improving_int_def
conflict_opt.simps ocdcl⇩W_o.simps cdcl_bnb_bj.simps skip.simps resolve.simps
obacktrack.simps)
lemma obacktrack_model_still_model:
assumes
‹obacktrack S T› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
ent: ‹set_mset I ⊨sm clauses S› ‹set_mset I ⊨sm conflicting_clss S› and
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (init_clss S)› and
opt_struct: ‹cdcl_bnb_struct_invs S› and
le: ‹Found (ρ I) < ρ' (weight T)›
shows
‹set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm conflicting_clss T›
using assms(1)
proof (cases rule: obacktrack.cases)
case (obacktrack_rule L D K M1 M2 D' i) note confl = this(1) and DD' = this(7) and
clss_L_D' = this(8) and T = this(9)
have H: ‹total_over_m I (set_mset (clauses S + conflicting_clss S) ∪ {add_mset L D'}) ⟹
consistent_interp I ⟹
I ⊨sm clauses S + conflicting_clss S ⟹ I ⊨ add_mset L D'› for I
using clss_L_D'
unfolding true_clss_cls_def
by blast
have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)›
using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have ‹total_over_m (set_mset I) (set_mset (init_clss S))›
using tot[symmetric]
by (auto simp: total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit)
then have 1: ‹total_over_m (set_mset I) (set_mset (clauses S + conflicting_clss S) ∪
{add_mset L D'})›
using alien T confl tot DD' opt_struct
unfolding cdcl⇩W_restart_mset.no_strange_atm_def total_over_m_def total_over_set_def
apply (auto simp: cdcl⇩W_restart_mset_state abs_state_def atms_of_def clauses_def
cdcl_bnb_struct_invs_def dest: multi_member_split)
by blast
have 2: ‹set_mset I ⊨sm conflicting_clss S›
using tot cons ent(2) by auto
have ‹set_mset I ⊨ add_mset L D'›
using H[OF 1 cons] 2 ent by auto
then show ?thesis
using ent obacktrack_rule 2 by auto
qed
lemma entails_conflicting_clauses_if_le':
fixes M''
defines ‹M' ≡ lit_of `# mset M''›
assumes
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (init_clss S)› and
le: ‹Found (ρ I) < ρ' (Some M')› and
‹is_improving M M'' S› and
‹N = init_clss S›
shows
‹set_mset I ⊨m conflicting_clauses N (weight (update_weight_information M'' S))›
using entails_conflicting_clauses_if_le[OF assms(2-6)[unfolded M'_def]] assms(7)
unfolding conflicting_clss_def
by auto
lemma improve_model_still_model:
assumes
‹improvep S T› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
ent: ‹set_mset I ⊨sm clauses S› ‹set_mset I ⊨sm conflicting_clss S› and
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (init_clss S)› and
opt_struct: ‹cdcl_bnb_struct_invs S› and
le: ‹Found (ρ I) < ρ' (weight T)›
shows
‹set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm conflicting_clss T›
using assms(1)
proof (cases rule: improvep.cases)
case (improve_rule M') note imp = this(1) and confl = this(2) and T = this(3)
have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
using all_struct unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
then have atm_trail: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
using alien by (auto simp: no_strange_atm_def lits_of_def atms_of_def)
have dist2: ‹distinct_mset (lit_of `# mset (trail S))› and
taut2: ‹¬ tautology (lit_of `# mset (trail S))›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto dest: no_dup_distinct no_dup_not_tautology)
have tot2: ‹total_over_m (set_mset I) (set_mset (init_clss S))›
using tot[symmetric]
by (auto simp: total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit)
have atm_trail: ‹atms_of (lit_of `# mset M') ⊆ atms_of_mm (init_clss S)› and
dist2: ‹distinct_mset (lit_of `# mset M')› and
taut2: ‹¬ tautology (lit_of `# mset M')›
using imp by (auto simp: no_strange_atm_def lits_of_def atms_of_def is_improving_int_def
simple_clss_def)
have tot2: ‹total_over_m (set_mset I) (set_mset (init_clss S))›
using tot[symmetric]
by (auto simp: total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit)
have
‹set_mset I ⊨m conflicting_clauses (init_clss S) (weight (update_weight_information M' S))›
apply (rule entails_conflicting_clauses_if_le'[unfolded conflicting_clss_def])
using T dist cons tot le imp by (auto intro!: )
then have ‹set_mset I ⊨m conflicting_clss (update_weight_information M' S)›
by (auto simp: update_weight_information_def conflicting_clss_def)
then show ?thesis
using ent improve_rule T by auto
qed
lemma cdcl_bnb_still_model:
assumes
‹cdcl_bnb S T› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
ent: ‹set_mset I ⊨sm clauses S› ‹set_mset I ⊨sm conflicting_clss S› and
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (init_clss S)› and
opt_struct: ‹cdcl_bnb_struct_invs S›
shows
‹(set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm conflicting_clss T) ∨ Found (ρ I) ≥ ρ' (weight T)›
using assms
proof (cases rule: cdcl_bnb.cases)
case cdcl_conflict
then show ?thesis
using ent by (auto simp: conflict.simps)
next
case cdcl_propagate
then show ?thesis
using ent by (auto simp: propagate.simps)
next
case cdcl_conflict_opt
then show ?thesis
using ent by (auto simp: conflict_opt.simps)
next
case cdcl_improve
from improve_model_still_model[OF this all_struct ent dist cons tot opt_struct]
show ?thesis
by (auto simp: improvep.simps)
next
case cdcl_other'
then show ?thesis
proof (induction rule: ocdcl⇩W_o_all_rules_induct)
case (decide T)
then show ?case
using ent by (auto simp: decide.simps)
next
case (skip T)
then show ?case
using ent by (auto simp: skip.simps)
next
case (resolve T)
then show ?case
using ent by (auto simp: resolve.simps)
next
case (backtrack T)
from obacktrack_model_still_model[OF this all_struct ent dist cons tot opt_struct]
show ?case
by auto
qed
qed
lemma rtranclp_cdcl_bnb_still_model:
assumes
st: ‹cdcl_bnb⇧*⇧* S T› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
ent: ‹(set_mset I ⊨sm clauses S ∧ set_mset I ⊨sm conflicting_clss S) ∨ Found (ρ I) ≥ ρ' (weight S)› and
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (init_clss S)› and
opt_struct: ‹cdcl_bnb_struct_invs S›
shows
‹(set_mset I ⊨sm clauses T ∧ set_mset I ⊨sm conflicting_clss T) ∨ Found (ρ I) ≥ ρ' (weight T)›
using st
proof (induction rule: rtranclp_induct)
case base
then show ?case
using ent by auto
next
case (step T U) note star = this(1) and st = this(2) and IH = this(3)
have 1: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF star all_struct] .
have 2: ‹cdcl_bnb_struct_invs T›
using rtranclp_cdcl_bnb_cdcl_bnb_struct_invs[OF star opt_struct] .
have 3: ‹atms_of I = atms_of_mm (init_clss T)›
using tot rtranclp_cdcl_bnb_no_more_init_clss[OF star] by auto
show ?case
using cdcl_bnb_still_model[OF st 1 _ _ dist cons 3 2] IH
cdcl_bnb_larger_still_larger[OF st]
by auto
qed
lemma full_cdcl_bnb_stgy_larger_or_equal_weight:
assumes
st: ‹full cdcl_bnb_stgy S T› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
ent: ‹(set_mset I ⊨sm clauses S ∧ set_mset I ⊨sm conflicting_clss S) ∨ Found (ρ I) ≥ ρ' (weight S)› and
dist: ‹distinct_mset I› and
cons: ‹consistent_interp (set_mset I)› and
tot: ‹atms_of I = atms_of_mm (init_clss S)› and
opt_struct: ‹cdcl_bnb_struct_invs S› and
stgy_inv: ‹cdcl_bnb_stgy_inv S›
shows
‹Found (ρ I) ≥ ρ' (weight T)› and
‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
proof -
have ns: ‹no_step cdcl_bnb_stgy T› and
st: ‹cdcl_bnb_stgy⇧*⇧* S T› and
st': ‹cdcl_bnb⇧*⇧* S T›
using st unfolding full_def by (auto intro: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
have ns': ‹no_step cdcl_bnb T›
by (meson cdcl_bnb.cases cdcl_bnb_stgy.simps no_confl_prop_impr.elims(3) ns)
have struct_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
have stgy_T: ‹cdcl_bnb_stgy_inv T›
using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
have confl: ‹conflicting T = Some {#}›
using no_step_cdcl_bnb_stgy_empty_conflict2[OF ns' struct_T stgy_T] .
have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (abs_state T)› and
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state T)›
using struct_T unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
then have ent': ‹set_mset (clauses T + conflicting_clss T) ⊨p {#}›
using confl unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by auto
have atms_eq: ‹atms_of I ∪ atms_of_mm (conflicting_clss T) = atms_of_mm (init_clss T)›
using tot[symmetric] atms_of_conflicting_clss[of T] alien
unfolding rtranclp_cdcl_bnb_no_more_init_clss[OF st'] cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: clauses_def total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit
abs_state_def cdcl⇩W_restart_mset_state)
have ‹¬ (set_mset I ⊨sm clauses T + conflicting_clss T)›
proof
assume ent'': ‹set_mset I ⊨sm clauses T + conflicting_clss T›
moreover have ‹total_over_m (set_mset I) (set_mset (clauses T + conflicting_clss T))›
using tot[symmetric] atms_of_conflicting_clss[of T] alien
unfolding rtranclp_cdcl_bnb_no_more_init_clss[OF st'] cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: clauses_def total_over_m_def total_over_set_def atm_iff_pos_or_neg_lit
abs_state_def cdcl⇩W_restart_mset_state atms_eq)
then show ‹False›
using ent' cons ent''
unfolding true_clss_cls_def by auto
qed
then show ‹ρ' (weight T) ≤ Found (ρ I)›
using rtranclp_cdcl_bnb_still_model[OF st' all_struct ent dist cons tot opt_struct]
by auto
show ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
proof
assume ‹satisfiable (set_mset (clauses T + conflicting_clss T))›
then obtain I where
ent'': ‹I ⊨sm clauses T + conflicting_clss T› and
tot: ‹total_over_m I (set_mset (clauses T + conflicting_clss T))› and
‹consistent_interp I›
unfolding satisfiable_def
by blast
then show ‹False›
using ent' cons ent''
unfolding true_clss_cls_def by auto
qed
qed
lemma full_cdcl_bnb_stgy_unsat2:
assumes
st: ‹full cdcl_bnb_stgy S T› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
opt_struct: ‹cdcl_bnb_struct_invs S› and
stgy_inv: ‹cdcl_bnb_stgy_inv S›
shows
‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
proof -
have ns: ‹no_step cdcl_bnb_stgy T› and
st: ‹cdcl_bnb_stgy⇧*⇧* S T› and
st': ‹cdcl_bnb⇧*⇧* S T›
using st unfolding full_def by (auto intro: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
have ns': ‹no_step cdcl_bnb T›
by (meson cdcl_bnb.cases cdcl_bnb_stgy.simps no_confl_prop_impr.elims(3) ns)
have struct_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using rtranclp_cdcl_bnb_stgy_all_struct_inv[OF st' all_struct] .
have stgy_T: ‹cdcl_bnb_stgy_inv T›
using rtranclp_cdcl_bnb_stgy_stgy_inv[OF st all_struct stgy_inv] .
have confl: ‹conflicting T = Some {#}›
using no_step_cdcl_bnb_stgy_empty_conflict2[OF ns' struct_T stgy_T] .
have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clause (abs_state T)› and
alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state T)›
using struct_T unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def by fast+
then have ent': ‹set_mset (clauses T + conflicting_clss T) ⊨p {#}›
using confl unfolding cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by auto
show ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
proof
assume ‹satisfiable (set_mset (clauses T + conflicting_clss T))›
then obtain I where
ent'': ‹I ⊨sm clauses T + conflicting_clss T› and
tot: ‹total_over_m I (set_mset (clauses T + conflicting_clss T))› and
‹consistent_interp I›
unfolding satisfiable_def
by blast
then show ‹False›
using ent'
unfolding true_clss_cls_def by auto
qed
qed
lemma weight_init_state2[simp]: ‹weight (init_state S) = None› and
conflicting_clss_init_state[simp]:
‹conflicting_clss (init_state N) = {#}›
unfolding weight_def conflicting_clss_def conflicting_clauses_def
by (auto simp: weight_init_state true_clss_cls_tautology_iff simple_clss_finite
filter_mset_empty_conv mset_set_empty_iff dest: simple_clssE)
text ‹First part of \cwref{theo:prop:cdclmmcorrect}{Theorem 2.15.6}›
lemma full_cdcl_bnb_stgy_no_conflicting_clause_unsat:
assumes
st: ‹full cdcl_bnb_stgy S T› and
all_struct: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
opt_struct: ‹cdcl_bnb_struct_invs S› and
stgy_inv: ‹cdcl_bnb_stgy_inv S› and
[simp]: ‹weight T = None› and
ent: ‹cdcl⇩W_learned_clauses_entailed_by_init S›
shows ‹unsatisfiable (set_mset (init_clss S))›
proof -
have ‹cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init (abs_state S)› and
‹conflicting_clss T = {#}›
using ent
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_learned_clauses_entailed_by_init_def
cdcl⇩W_learned_clauses_entailed_by_init_def abs_state_def cdcl⇩W_restart_mset_state
conflicting_clss_def conflicting_clauses_def true_clss_cls_tautology_iff simple_clss_finite
filter_mset_empty_conv mset_set_empty_iff dest: simple_clssE)
then show ?thesis
using full_cdcl_bnb_stgy_no_conflicting_clss_unsat[OF _ st all_struct
stgy_inv] by (auto simp: can_always_improve)
qed
definition annotation_is_model where
‹annotation_is_model S ⟷
(weight S ≠ None ⟶ (set_mset (the (weight S)) ⊨sm init_clss S ∧
consistent_interp (set_mset (the (weight S))) ∧
atms_of (the (weight S)) ⊆ atms_of_mm (init_clss S) ∧
total_over_m (set_mset (the (weight S))) (set_mset (init_clss S)) ∧
distinct_mset (the (weight S))))›
lemma cdcl_bnb_annotation_is_model:
assumes
‹cdcl_bnb S T› and
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
‹annotation_is_model S›
shows ‹annotation_is_model T›
proof -
have [simp]: ‹atms_of (lit_of `# mset M) = atm_of ` lit_of ` set M› for M
by (auto simp: atms_of_def)
have ‹consistent_interp (lits_of_l (trail S)) ∧
atm_of ` (lits_of_l (trail S)) ⊆ atms_of_mm (init_clss S) ∧
distinct_mset (lit_of `# mset (trail S))›
using assms(2) by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
abs_state_def cdcl⇩W_restart_mset_state cdcl⇩W_restart_mset.no_strange_atm_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
dest: no_dup_distinct)
with assms(1,3)
show ?thesis
apply (cases rule: cdcl_bnb.cases)
subgoal
by (auto simp: conflict.simps annotation_is_model_def)
subgoal
by (auto simp: propagate.simps annotation_is_model_def)
subgoal
by (force simp: annotation_is_model_def true_annots_true_cls lits_of_def
improvep.simps is_improving_int_def image_Un image_image simple_clss_def
consistent_interp_tuatology_mset_set
dest!: consistent_interp_unionD intro: distinct_mset_union2)
subgoal
by (auto simp: annotation_is_model_def conflict_opt.simps)
subgoal
by (auto simp: annotation_is_model_def
ocdcl⇩W_o.simps cdcl_bnb_bj.simps obacktrack.simps
skip.simps resolve.simps decide.simps)
done
qed
lemma rtranclp_cdcl_bnb_annotation_is_model:
‹cdcl_bnb⇧*⇧* S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
annotation_is_model S ⟹ annotation_is_model T›
by (induction rule: rtranclp_induct)
(auto simp: cdcl_bnb_annotation_is_model rtranclp_cdcl_bnb_stgy_all_struct_inv)
text ‹\cwref{theo:prop:cdclmmcorrect}{Theorem 2.15.6}›
theorem full_cdcl_bnb_stgy_no_conflicting_clause_from_init_state:
assumes
st: ‹full cdcl_bnb_stgy (init_state N) T› and
dist: ‹distinct_mset_mset N›
shows
‹weight T = None ⟹ unsatisfiable (set_mset N)› and
‹weight T ≠ None ⟹ consistent_interp (set_mset (the (weight T))) ∧
atms_of (the (weight T)) ⊆ atms_of_mm N ∧ set_mset (the (weight T)) ⊨sm N ∧
total_over_m (set_mset (the (weight T))) (set_mset N) ∧
distinct_mset (the (weight T))› and
‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm N ⟹
set_mset I ⊨sm N ⟹ Found (ρ I) ≥ ρ' (weight T)›
proof -
let ?S = ‹init_state N›
have ‹distinct_mset C› if ‹C ∈# N› for C
using dist that by (auto simp: distinct_mset_set_def dest: multi_member_split)
then have dist: ‹distinct_mset_mset N›
by (auto simp: distinct_mset_set_def)
then have [simp]: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv ([], N, {#}, None)›
unfolding init_state.simps[symmetric]
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def)
moreover have [iff]: ‹cdcl_bnb_struct_invs ?S›
by (auto simp: cdcl_bnb_struct_invs_def)
moreover have [simp]: ‹cdcl_bnb_stgy_inv ?S›
by (auto simp: cdcl_bnb_stgy_inv_def conflict_is_false_with_level_def)
moreover have ent: ‹cdcl⇩W_learned_clauses_entailed_by_init ?S›
by (auto simp: cdcl⇩W_learned_clauses_entailed_by_init_def)
moreover have [simp]: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state (init_state N))›
unfolding CDCL_W_Abstract_State.init_state.simps abs_state_def
by auto
ultimately show ‹weight T = None ⟹ unsatisfiable (set_mset N)›
using full_cdcl_bnb_stgy_no_conflicting_clause_unsat[OF st]
by auto
have ‹annotation_is_model ?S›
by (auto simp: annotation_is_model_def)
then have ‹annotation_is_model T›
using rtranclp_cdcl_bnb_annotation_is_model[of ?S T] st
unfolding full_def by (auto dest: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
moreover have ‹init_clss T = N›
using rtranclp_cdcl_bnb_no_more_init_clss[of ?S T] st
unfolding full_def by (auto dest: rtranclp_cdcl_bnb_stgy_cdcl_bnb)
ultimately show ‹weight T ≠ None ⟹ consistent_interp (set_mset (the (weight T))) ∧
atms_of (the (weight T)) ⊆ atms_of_mm N ∧ set_mset (the (weight T)) ⊨sm N ∧
total_over_m (set_mset (the (weight T))) (set_mset N) ∧
distinct_mset (the (weight T))›
by (auto simp: annotation_is_model_def)
show ‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm N ⟹
set_mset I ⊨sm N ⟹ Found (ρ I) ≥ ρ' (weight T)›
using full_cdcl_bnb_stgy_larger_or_equal_weight[of ?S T I] st unfolding full_def
by auto
qed
lemma pruned_clause_in_conflicting_clss:
assumes
ge: ‹⋀M'. total_over_m (set_mset (mset (M @ M'))) (set_mset (init_clss S)) ⟹
distinct_mset (atm_of `# mset (M @ M')) ⟹
consistent_interp (set_mset (mset (M @ M'))) ⟹
Found (ρ (mset (M @ M'))) ≥ ρ' (weight S)› and
atm: ‹atms_of (mset M) ⊆ atms_of_mm (init_clss S)› and
dist: ‹distinct M› and
cons: ‹consistent_interp (set M)›
shows ‹pNeg (mset M) ∈# conflicting_clss S›
proof -
have 0: ‹(pNeg o mset o ((@) M))` {M'.
distinct_mset (atm_of `# mset (M @ M')) ∧ consistent_interp (set_mset (mset (M @ M'))) ∧
atms_of_s (set (M @ M')) ⊆ (atms_of_mm (init_clss S)) ∧
card (atms_of_mm (init_clss S)) = n + card (atms_of (mset (M @ M')))} ⊆
set_mset (conflicting_clss S)› for n
proof (induction n)
case 0
show ?case
proof clarify
fix x :: ‹'v literal multiset› and xa :: ‹'v literal multiset› and
xb :: ‹'v literal list› and xc :: ‹'v literal list›
assume
dist: ‹distinct_mset (atm_of `# mset (M @ xc))› and
cons: ‹consistent_interp (set_mset (mset (M @ xc)))› and
atm': ‹atms_of_s (set (M @ xc)) ⊆ atms_of_mm (init_clss S)› and
0: ‹card (atms_of_mm (init_clss S)) = 0 + card (atms_of (mset (M @ xc)))›
have D[dest]:
‹A ∈ set M ⟹ A ∉ set xc›
‹A ∈ set M ⟹ -A ∉ set xc›
for A
using dist multi_member_split[of A ‹mset M›] multi_member_split[of ‹-A› ‹mset xc›]
multi_member_split[of ‹-A› ‹mset M›] multi_member_split[of ‹A› ‹mset xc›]
by (auto simp: atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set)
have dist2: ‹distinct xc› ‹distinct_mset (atm_of `# mset xc)›
‹distinct_mset (mset M + mset xc)›
using dist distinct_mset_atm_ofD[OF dist]
unfolding mset_append[symmetric] distinct_mset_mset_distinct
by (auto dest: distinct_mset_union2 distinct_mset_atm_ofD)
have eq: ‹card (atms_of_s (set M) ∪ atms_of_s (set xc)) =
card (atms_of_s (set M)) + card (atms_of_s (set xc))›
by (subst card_Un_Int) auto
let ?M = ‹M @ xc›
have H1: ‹atms_of_s (set ?M) = atms_of_mm (init_clss S)›
using eq atm card_mono[OF _ atm'] card_subset_eq[OF _ atm'] 0
by (auto simp: atms_of_s_def image_Un)
moreover have tot2: ‹total_over_m (set ?M) (set_mset (init_clss S))›
using H1
by (auto simp: total_over_m_def total_over_set_def lit_in_set_iff_atm)
moreover have ‹¬tautology (mset ?M)›
using cons unfolding consistent_interp_tautology[symmetric]
by auto
ultimately have ‹mset ?M ∈ simple_clss (atms_of_mm (init_clss S))›
using dist atm cons H1 dist2
by (auto simp: simple_clss_def consistent_interp_tautology atms_of_s_def)
moreover have tot2: ‹total_over_m (set ?M) (set_mset (init_clss S))›
using H1
by (auto simp: total_over_m_def total_over_set_def lit_in_set_iff_atm)
ultimately show ‹(pNeg ∘ mset ∘ (@) M) xc ∈# conflicting_clss S›
using ge[of ‹xc›] dist 0 cons card_mono[OF _ atm] tot2 cons
by (auto simp: conflicting_clss_def too_heavy_clauses_def
simple_clss_finite
intro!: too_heavy_clauses_conflicting_clauses imageI)
qed
next
case (Suc n) note IH = this(1)
let ?H = ‹{M'.
distinct_mset (atm_of `# mset (M @ M')) ∧
consistent_interp (set_mset (mset (M @ M'))) ∧
atms_of_s (set (M @ M')) ⊆ atms_of_mm (init_clss S) ∧
card (atms_of_mm (init_clss S)) = n + card (atms_of (mset (M @ M')))}›
show ?case
proof clarify
fix x :: ‹'v literal multiset› and xa :: ‹'v literal multiset› and
xb :: ‹'v literal list› and xc :: ‹'v literal list›
assume
dist: ‹distinct_mset (atm_of `# mset (M @ xc))› and
cons: ‹consistent_interp (set_mset (mset (M @ xc)))› and
atm': ‹atms_of_s (set (M @ xc)) ⊆ atms_of_mm (init_clss S)› and
0: ‹card (atms_of_mm (init_clss S)) = Suc n + card (atms_of (mset (M @ xc)))›
then obtain a where
a: ‹a ∈ atms_of_mm (init_clss S)› and
a_notin: ‹a ∉ atms_of_s (set (M @ xc))›
by (metis Suc_n_not_le_n add_Suc_shift atms_of_mmltiset atms_of_s_def le_add2
subsetI subset_antisym)
have dist2: ‹distinct xc› ‹distinct_mset (atm_of `# mset xc)›
‹distinct_mset (mset M + mset xc)›
using dist distinct_mset_atm_ofD[OF dist]
unfolding mset_append[symmetric] distinct_mset_mset_distinct
by (auto dest: distinct_mset_union2 distinct_mset_atm_ofD)
let ?xc1 = ‹Pos a # xc›
let ?xc2 = ‹Neg a # xc›
have ‹?xc1 ∈ ?H›
using dist cons atm' 0 dist2 a_notin a
by (auto simp: distinct_mset_add mset_inter_empty_set_mset
lit_in_set_iff_atm card_insert_if)
from set_mp[OF IH imageI[OF this]]
have 1: ‹too_heavy_clauses (init_clss S) (weight S) ⊨pm add_mset (-(Pos a)) (pNeg (mset (M @ xc)))›
unfolding conflicting_clss_def unfolding conflicting_clauses_def
by (auto simp: pNeg_simps)
have ‹?xc2 ∈ ?H›
using dist cons atm' 0 dist2 a_notin a
by (auto simp: distinct_mset_add mset_inter_empty_set_mset
lit_in_set_iff_atm card_insert_if)
from set_mp[OF IH imageI[OF this]]
have 2: ‹too_heavy_clauses (init_clss S) (weight S) ⊨pm add_mset (Pos a) (pNeg (mset (M @ xc)))›
unfolding conflicting_clss_def unfolding conflicting_clauses_def
by (auto simp: pNeg_simps)
have ‹¬tautology (mset (M @ xc))›
using cons unfolding consistent_interp_tautology[symmetric]
by auto
then have ‹¬tautology (pNeg (mset M) + pNeg (mset xc))›
unfolding mset_append[symmetric] pNeg_simps[symmetric]
by (auto simp del: mset_append)
then have ‹pNeg (mset M) + pNeg (mset xc) ∈ simple_clss (atms_of_mm (init_clss S))›
using atm' dist2
by (auto simp: simple_clss_def atms_of_s_def
simp flip: pNeg_simps)
then show ‹(pNeg ∘ mset ∘ (@) M) xc ∈# conflicting_clss S›
using true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[OF 1 2] apply -
unfolding conflicting_clss_def conflicting_clauses_def
by (subst (asm) true_clss_cls_remdups_mset[symmetric])
(auto simp: simple_clss_finite pNeg_simps intro: true_clss_cls_cong_set_mset
simp del: true_clss_cls_remdups_mset)
qed
qed
have ‹[] ∈ {M'.
distinct_mset (atm_of `# mset (M @ M')) ∧
consistent_interp (set_mset (mset (M @ M'))) ∧
atms_of_s (set (M @ M')) ⊆ atms_of_mm (init_clss S) ∧
card (atms_of_mm (init_clss S)) =
card (atms_of_mm (init_clss S)) - card (atms_of (mset M)) +
card (atms_of (mset (M @ M')))}›
using card_mono[OF _ assms(2)] assms by (auto dest: card_mono distinct_consistent_distinct_atm)
from set_mp[OF 0 imageI[OF this]]
show ‹pNeg (mset M) ∈# conflicting_clss S›
by auto
qed
subsubsection ‹Alternative versions›
subsubsection ‹Calculus with simple Improve rule›
text ‹To make sure that the paper version of the correct, we restrict the previous calculus to exactly
the rules that are on paper.›
inductive pruning :: ‹'st ⇒ 'st ⇒ bool› where
pruning_rule:
‹pruning S T›
if
‹⋀M'. total_over_m (set_mset (mset (map lit_of (trail S) @ M'))) (set_mset (init_clss S)) ⟹
distinct_mset (atm_of `# mset (map lit_of (trail S) @ M')) ⟹
consistent_interp (set_mset (mset (map lit_of (trail S) @ M'))) ⟹
ρ' (weight S) ≤ Found (ρ (mset (map lit_of (trail S) @ M')))›
‹conflicting S = None›
‹T ∼ update_conflicting (Some (negate_ann_lits (trail S))) S›
inductive oconflict_opt :: "'st ⇒ 'st ⇒ bool" for S T :: 'st where
oconflict_opt_rule:
‹oconflict_opt S T›
if
‹Found (ρ (lit_of `# mset (trail S))) ≥ ρ' (weight S)›
‹conflicting S = None›
‹T ∼ update_conflicting (Some (negate_ann_lits (trail S))) S›
inductive improve :: "'st ⇒ 'st ⇒ bool" for S T :: 'st where
improve_rule:
‹improve S T›
if
‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
‹Found (ρ (lit_of `# mset (trail S))) < ρ' (weight S)›
‹trail S ⊨asm init_clss S›
‹conflicting S = None›
‹T ∼ update_weight_information (trail S) S›
text ‹This is the basic version of the calculus:›
inductive ocdcl⇩w :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
ocdcl_conflict: "conflict S S' ⟹ ocdcl⇩w S S'" |
ocdcl_propagate: "propagate S S' ⟹ ocdcl⇩w S S'" |
ocdcl_improve: "improve S S' ⟹ ocdcl⇩w S S'" |
ocdcl_conflict_opt: "oconflict_opt S S' ⟹ ocdcl⇩w S S'" |
ocdcl_other': "ocdcl⇩W_o S S' ⟹ ocdcl⇩w S S'" |
ocdcl_pruning: "pruning S S' ⟹ ocdcl⇩w S S'"
inductive ocdcl⇩w_stgy :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
ocdcl⇩w_conflict: "conflict S S' ⟹ ocdcl⇩w_stgy S S'" |
ocdcl⇩w_propagate: "propagate S S' ⟹ ocdcl⇩w_stgy S S'" |
ocdcl⇩w_improve: "improve S S' ⟹ ocdcl⇩w_stgy S S'" |
ocdcl⇩w_conflict_opt: "conflict_opt S S' ⟹ ocdcl⇩w_stgy S S'" |
ocdcl⇩w_other': "ocdcl⇩W_o S S' ⟹ no_confl_prop_impr S ⟹ ocdcl⇩w_stgy S S'"
lemma pruning_conflict_opt:
assumes ocdcl_pruning: ‹pruning S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹conflict_opt S T›
proof -
have le:
‹⋀M'. total_over_m (set_mset (mset (map lit_of (trail S) @ M')))
(set_mset (init_clss S)) ⟹
distinct_mset (atm_of `# mset (map lit_of (trail S) @ M')) ⟹
consistent_interp (set_mset (mset (map lit_of (trail S) @ M'))) ⟹
ρ' (weight S) ≤ Found (ρ (mset (map lit_of (trail S) @ M')))›
using ocdcl_pruning by (auto simp: pruning.simps)
have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have incl: ‹atms_of (mset (map lit_of (trail S))) ⊆ atms_of_mm (init_clss S)›
using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
have dist: ‹distinct (map lit_of (trail S))› and
cons: ‹consistent_interp (set (map lit_of (trail S)))›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
dest: no_dup_map_lit_of)
have ‹negate_ann_lits (trail S) ∈# conflicting_clss S›
unfolding negate_ann_lits_pNeg_lit_of comp_def mset_map[symmetric]
apply (rule pruned_clause_in_conflicting_clss)
subgoal using le by fast
subgoal using incl by fast
subgoal using dist by fast
subgoal using cons by fast
done
then show ‹conflict_opt S T›
apply (rule conflict_opt.intros)
subgoal using ocdcl_pruning by (auto simp: pruning.simps)
subgoal using ocdcl_pruning by (auto simp: pruning.simps)
done
qed
lemma ocdcl_conflict_opt_conflict_opt:
assumes ocdcl_pruning: ‹oconflict_opt S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹conflict_opt S T›
proof -
have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have incl: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
have dist: ‹distinct_mset (lit_of `# mset (trail S))› and
cons: ‹consistent_interp (set (map lit_of (trail S)))› and
tauto: ‹¬tautology (lit_of `# mset (trail S))›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
dest: no_dup_map_lit_of no_dup_distinct no_dup_not_tautology)
have ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
using dist incl tauto by (auto simp: simple_clss_def)
then have simple: ‹(lit_of `# mset (trail S))
∈ {a. a ∈# mset_set (simple_clss (atms_of_mm (init_clss S))) ∧
ρ' (weight S) ≤ Found (ρ a)}›
using ocdcl_pruning by (auto simp: simple_clss_finite oconflict_opt.simps)
have ‹negate_ann_lits (trail S) ∈# conflicting_clss S›
unfolding negate_ann_lits_pNeg_lit_of comp_def conflicting_clss_def
by (rule too_heavy_clauses_conflicting_clauses)
(use simple in ‹auto simp: too_heavy_clauses_def oconflict_opt.simps›)
then show ‹conflict_opt S T›
apply (rule conflict_opt.intros)
subgoal using ocdcl_pruning by (auto simp: oconflict_opt.simps)
subgoal using ocdcl_pruning by (auto simp: oconflict_opt.simps)
done
qed
lemma improve_improvep:
assumes imp: ‹improve S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹improvep S T›
proof -
have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have incl: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
have dist: ‹distinct_mset (lit_of `# mset (trail S))› and
cons: ‹consistent_interp (set (map lit_of (trail S)))› and
tauto: ‹¬tautology (lit_of `# mset (trail S))› and
nd: ‹no_dup (trail S)›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
dest: no_dup_map_lit_of no_dup_distinct no_dup_not_tautology)
have ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
using dist incl tauto by (auto simp: simple_clss_def)
have tot': ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))› and
confl: ‹conflicting S = None› and
T: ‹T ∼ update_weight_information (trail S) S›
using imp nd by (auto simp: is_improving_int_def improve.simps)
have M': ‹ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))›
if ‹total_over_m (lits_of_l M') (set_mset (init_clss S))› and
incl: ‹mset (trail S) ⊆# mset M'› and
‹lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S))›
for M'
proof -
have [simp]: ‹lits_of_l M' = set_mset (lit_of `# mset M')›
by (auto simp: lits_of_def)
obtain A where A: ‹mset M' = A + mset (trail S)›
using incl by (auto simp: mset_subset_eq_exists_conv)
have M': ‹lits_of_l M' = lit_of ` set_mset A ∪ lits_of_l (trail S)›
unfolding lits_of_def
by (metis A image_Un set_mset_mset set_mset_union)
have ‹mset M' = mset (trail S)›
using that tot' unfolding A total_over_m_alt_def
apply (case_tac A)
apply (auto simp: A simple_clss_def distinct_mset_add M' image_Un
tautology_union mset_inter_empty_set_mset atms_of_def atms_of_s_def
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set image_image
tautology_add_mset)
by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
lits_of_def subsetCE)
then show ?thesis
by auto
qed
have ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
using tauto dist incl by (auto simp: simple_clss_def)
then have improving: ‹is_improving (trail S) (trail S) S› and
‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
using imp nd by (auto simp: is_improving_int_def improve.simps intro: M')
show ‹improvep S T›
by (rule improvep.intros[OF improving confl T])
qed
lemma ocdcl⇩w_cdcl_bnb:
assumes ‹ocdcl⇩w S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl_bnb S T›
using assms by (cases) (auto intro: cdcl_bnb.intros dest: pruning_conflict_opt
ocdcl_conflict_opt_conflict_opt improve_improvep)
lemma ocdcl⇩w_stgy_cdcl_bnb_stgy:
assumes ‹ocdcl⇩w_stgy S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl_bnb_stgy S T›
using assms by (cases)
(auto intro: cdcl_bnb_stgy.intros dest: pruning_conflict_opt improve_improvep)
lemma rtranclp_ocdcl⇩w_stgy_rtranclp_cdcl_bnb_stgy:
assumes ‹ocdcl⇩w_stgy⇧*⇧* S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl_bnb_stgy⇧*⇧* S T›
using assms
by (induction rule: rtranclp_induct)
(auto dest: rtranclp_cdcl_bnb_stgy_all_struct_inv[OF rtranclp_cdcl_bnb_stgy_cdcl_bnb]
ocdcl⇩w_stgy_cdcl_bnb_stgy)
lemma no_step_ocdcl⇩w_no_step_cdcl_bnb:
assumes ‹no_step ocdcl⇩w S› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹no_step cdcl_bnb S›
proof -
have
nsc: ‹no_step conflict S› and
nsp: ‹no_step propagate S› and
nsi: ‹no_step improve S› and
nsco: ‹no_step oconflict_opt S› and
nso: ‹no_step ocdcl⇩W_o S›and
nspr: ‹no_step pruning S›
using assms(1) by (auto simp: cdcl_bnb.simps ocdcl⇩w.simps)
have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have incl: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
have dist: ‹distinct_mset (lit_of `# mset (trail S))› and
cons: ‹consistent_interp (set (map lit_of (trail S)))› and
tauto: ‹¬tautology (lit_of `# mset (trail S))› and
n_d: ‹no_dup (trail S)›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
dest: no_dup_map_lit_of no_dup_distinct no_dup_not_tautology)
have nsip: False if imp: ‹improvep S S'› for S'
proof -
obtain M' where
[simp]: ‹conflicting S = None› and
is_improving:
‹⋀M'. total_over_m (lits_of_l M') (set_mset (init_clss S)) ⟶
mset (trail S) ⊆# mset M' ⟶
lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S)) ⟶
ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))› and
S': ‹S' ∼ update_weight_information M' S›
using imp by (auto simp: improvep.simps is_improving_int_def)
have 1: ‹¬ ρ' (weight S) ≤ Found (ρ (lit_of `# mset (trail S)))›
using nsco
by (auto simp: is_improving_int_def oconflict_opt.simps)
have 2: ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain A where
‹A ∈ atms_of_mm (init_clss S)› and
‹A ∉ atms_of_s (lits_of_l (trail S))›
by (auto simp: total_over_m_def total_over_set_def)
then show ‹False›
using decide_rule[of S ‹Pos A›, OF _ _ _ state_eq_ref] nso
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l ocdcl⇩W_o.simps)
qed
have 3: ‹trail S ⊨asm init_clss S›
unfolding true_annots_def
proof clarify
fix C
assume C: ‹C ∈# init_clss S›
have ‹total_over_m (lits_of_l (trail S)) {C}›
using 2 C by (auto dest!: multi_member_split)
moreover have ‹¬ trail S ⊨as CNot C›
using C nsc conflict_rule[of S C, OF _ _ _ state_eq_ref]
by (auto simp: clauses_def dest!: multi_member_split)
ultimately show ‹trail S ⊨a C›
using total_not_CNot[of ‹lits_of_l (trail S)› C] unfolding true_annots_true_cls true_annot_def
by auto
qed
have 4: ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
using tauto cons incl dist by (auto simp: simple_clss_def)
have ‹improve S (update_weight_information (trail S) S)›
by (rule improve.intros[OF 2 _ 3]) (use 1 2 in auto)
then show False
using nsi by auto
qed
moreover have False if ‹conflict_opt S S'› for S'
proof -
have [simp]: ‹conflicting S = None›
using that by (auto simp: conflict_opt.simps)
have 1: ‹¬ ρ' (weight S) ≤ Found (ρ (lit_of `# mset (trail S)))›
using nsco
by (auto simp: is_improving_int_def oconflict_opt.simps)
have 2: ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain A where
‹A ∈ atms_of_mm (init_clss S)› and
‹A ∉ atms_of_s (lits_of_l (trail S))›
by (auto simp: total_over_m_def total_over_set_def)
then show ‹False›
using decide_rule[of S ‹Pos A›, OF _ _ _ state_eq_ref] nso
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l ocdcl⇩W_o.simps)
qed
have 3: ‹trail S ⊨asm init_clss S›
unfolding true_annots_def
proof clarify
fix C
assume C: ‹C ∈# init_clss S›
have ‹total_over_m (lits_of_l (trail S)) {C}›
using 2 C by (auto dest!: multi_member_split)
moreover have ‹¬ trail S ⊨as CNot C›
using C nsc conflict_rule[of S C, OF _ _ _ state_eq_ref]
by (auto simp: clauses_def dest!: multi_member_split)
ultimately show ‹trail S ⊨a C›
using total_not_CNot[of ‹lits_of_l (trail S)› C] unfolding true_annots_true_cls true_annot_def
by auto
qed
have 4: ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
using tauto cons incl dist by (auto simp: simple_clss_def)
have [intro]: ‹ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))›
if
‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))› and
‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)› and
‹no_dup (trail S)› and
‹total_over_m (lits_of_l M') (set_mset (init_clss S))› and
incl: ‹mset (trail S) ⊆# mset M'› and
‹lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S))›
for M' :: ‹('v literal, 'v literal, 'v literal multiset) annotated_lit list›
proof -
have [simp]: ‹lits_of_l M' = set_mset (lit_of `# mset M')›
by (auto simp: lits_of_def)
obtain A where A: ‹mset M' = A + mset (trail S)›
using incl by (auto simp: mset_subset_eq_exists_conv)
have M': ‹lits_of_l M' = lit_of ` set_mset A ∪ lits_of_l (trail S)›
unfolding lits_of_def
by (metis A image_Un set_mset_mset set_mset_union)
have ‹mset M' = mset (trail S)›
using that 2 unfolding A total_over_m_alt_def
apply (case_tac A)
apply (auto simp: A simple_clss_def distinct_mset_add M' image_Un
tautology_union mset_inter_empty_set_mset atms_of_def atms_of_s_def
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set image_image
tautology_add_mset)
by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
lits_of_def subsetCE)
then show ?thesis
using 2 by auto
qed
have imp: ‹is_improving (trail S) (trail S) S›
using 1 2 3 4 incl n_d unfolding is_improving_int_def
by (auto simp: oconflict_opt.simps)
show ‹False›
using trail_is_improving_Ex_improve[of S, OF _ imp] nsip
by auto
qed
ultimately show ?thesis
using nsc nsp nsi nsco nso nsp nspr
by (auto simp: cdcl_bnb.simps)
qed
lemma all_struct_init_state_distinct_iff:
‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state (init_state N)) ⟷
distinct_mset_mset N›
unfolding init_state.simps[symmetric]
by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
cdcl⇩W_restart_mset.no_strange_atm_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
abs_state_def cdcl⇩W_restart_mset_state)
lemma no_step_ocdcl⇩w_stgy_no_step_cdcl_bnb_stgy:
assumes ‹no_step ocdcl⇩w_stgy S› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹no_step cdcl_bnb_stgy S›
using assms no_step_ocdcl⇩w_no_step_cdcl_bnb[of S]
by (auto simp: ocdcl⇩w_stgy.simps ocdcl⇩w.simps cdcl_bnb.simps cdcl_bnb_stgy.simps
dest: ocdcl_conflict_opt_conflict_opt pruning_conflict_opt)
lemma full_ocdcl⇩w_stgy_full_cdcl_bnb_stgy:
assumes ‹full ocdcl⇩w_stgy S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹full cdcl_bnb_stgy S T›
using assms rtranclp_ocdcl⇩w_stgy_rtranclp_cdcl_bnb_stgy[of S T]
no_step_ocdcl⇩w_stgy_no_step_cdcl_bnb_stgy[of T]
unfolding full_def
by (auto dest: rtranclp_cdcl_bnb_stgy_all_struct_inv[OF rtranclp_cdcl_bnb_stgy_cdcl_bnb])
corollary full_ocdcl⇩w_stgy_no_conflicting_clause_from_init_state:
assumes
st: ‹full ocdcl⇩w_stgy (init_state N) T› and
dist: ‹distinct_mset_mset N›
shows
‹weight T = None ⟹ unsatisfiable (set_mset N)› and
‹weight T ≠ None ⟹ model_on (set_mset (the (weight T))) N ∧ set_mset (the (weight T)) ⊨sm N ∧
distinct_mset (the (weight T))› and
‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm N ⟹
set_mset I ⊨sm N ⟹ Found (ρ I) ≥ ρ' (weight T)›
using full_cdcl_bnb_stgy_no_conflicting_clause_from_init_state[of N T,
OF full_ocdcl⇩w_stgy_full_cdcl_bnb_stgy[OF st] dist] dist
by (auto simp: all_struct_init_state_distinct_iff model_on_def
dest: multi_member_split)
lemma wf_ocdcl⇩w:
‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)
∧ ocdcl⇩w S T}›
by (rule wf_subset[OF wf_cdcl_bnb2]) (auto dest: ocdcl⇩w_cdcl_bnb)
subsubsection ‹Calculus with generalised Improve rule›
text ‹Now a version with the more general improve rule:›
inductive ocdcl⇩w_p :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
ocdcl_conflict: "conflict S S' ⟹ ocdcl⇩w_p S S'" |
ocdcl_propagate: "propagate S S' ⟹ ocdcl⇩w_p S S'" |
ocdcl_improve: "improvep S S' ⟹ ocdcl⇩w_p S S'" |
ocdcl_conflict_opt: "oconflict_opt S S' ⟹ ocdcl⇩w_p S S'" |
ocdcl_other': "ocdcl⇩W_o S S' ⟹ ocdcl⇩w_p S S'" |
ocdcl_pruning: "pruning S S' ⟹ ocdcl⇩w_p S S'"
inductive ocdcl⇩w_p_stgy :: ‹'st ⇒ 'st ⇒ bool› for S :: 'st where
ocdcl⇩w_p_conflict: "conflict S S' ⟹ ocdcl⇩w_p_stgy S S'" |
ocdcl⇩w_p_propagate: "propagate S S' ⟹ ocdcl⇩w_p_stgy S S'" |
ocdcl⇩w_p_improve: "improvep S S' ⟹ ocdcl⇩w_p_stgy S S'" |
ocdcl⇩w_p_conflict_opt: "conflict_opt S S' ⟹ ocdcl⇩w_p_stgy S S'"|
ocdcl⇩w_p_pruning: "pruning S S' ⟹ ocdcl⇩w_p_stgy S S'" |
ocdcl⇩w_p_other': "ocdcl⇩W_o S S' ⟹ no_confl_prop_impr S ⟹ ocdcl⇩w_p_stgy S S'"
lemma ocdcl⇩w_p_cdcl_bnb:
assumes ‹ocdcl⇩w_p S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl_bnb S T›
using assms by (cases) (auto intro: cdcl_bnb.intros dest: pruning_conflict_opt
ocdcl_conflict_opt_conflict_opt)
lemma ocdcl⇩w_p_stgy_cdcl_bnb_stgy:
assumes ‹ocdcl⇩w_p_stgy S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl_bnb_stgy S T›
using assms by (cases) (auto intro: cdcl_bnb_stgy.intros dest: pruning_conflict_opt)
lemma rtranclp_ocdcl⇩w_p_stgy_rtranclp_cdcl_bnb_stgy:
assumes ‹ocdcl⇩w_p_stgy⇧*⇧* S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹cdcl_bnb_stgy⇧*⇧* S T›
using assms
by (induction rule: rtranclp_induct)
(auto dest: rtranclp_cdcl_bnb_stgy_all_struct_inv[OF rtranclp_cdcl_bnb_stgy_cdcl_bnb]
ocdcl⇩w_p_stgy_cdcl_bnb_stgy)
lemma no_step_ocdcl⇩w_p_no_step_cdcl_bnb:
assumes ‹no_step ocdcl⇩w_p S› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹no_step cdcl_bnb S›
proof -
have
nsc: ‹no_step conflict S› and
nsp: ‹no_step propagate S› and
nsi: ‹no_step improvep S› and
nsco: ‹no_step oconflict_opt S› and
nso: ‹no_step ocdcl⇩W_o S›and
nspr: ‹no_step pruning S›
using assms(1) by (auto simp: cdcl_bnb.simps ocdcl⇩w_p.simps)
have alien: ‹cdcl⇩W_restart_mset.no_strange_atm (abs_state S)› and
lev: ‹cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv (abs_state S)›
using inv unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
by fast+
have incl: ‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)›
using alien unfolding cdcl⇩W_restart_mset.no_strange_atm_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def)
have dist: ‹distinct_mset (lit_of `# mset (trail S))› and
cons: ‹consistent_interp (set (map lit_of (trail S)))› and
tauto: ‹¬tautology (lit_of `# mset (trail S))› and
n_d: ‹no_dup (trail S)›
using lev unfolding cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by (auto simp: abs_state_def cdcl⇩W_restart_mset_state lits_of_def image_image atms_of_def
dest: no_dup_map_lit_of no_dup_distinct no_dup_not_tautology)
have False if ‹conflict_opt S S'› for S'
proof -
have [simp]: ‹conflicting S = None›
using that by (auto simp: conflict_opt.simps)
have 1: ‹¬ ρ' (weight S) ≤ Found (ρ (lit_of `# mset (trail S)))›
using nsco
by (auto simp: is_improving_int_def oconflict_opt.simps)
have 2: ‹total_over_m (lits_of_l (trail S)) (set_mset (init_clss S))›
proof (rule ccontr)
assume ‹¬ ?thesis›
then obtain A where
‹A ∈ atms_of_mm (init_clss S)› and
‹A ∉ atms_of_s (lits_of_l (trail S))›
by (auto simp: total_over_m_def total_over_set_def)
then show ‹False›
using decide_rule[of S ‹Pos A›, OF _ _ _ state_eq_ref] nso
by (auto simp: Decided_Propagated_in_iff_in_lits_of_l ocdcl⇩W_o.simps)
qed
have 3: ‹trail S ⊨asm init_clss S›
unfolding true_annots_def
proof clarify
fix C
assume C: ‹C ∈# init_clss S›
have ‹total_over_m (lits_of_l (trail S)) {C}›
using 2 C by (auto dest!: multi_member_split)
moreover have ‹¬ trail S ⊨as CNot C›
using C nsc conflict_rule[of S C, OF _ _ _ state_eq_ref]
by (auto simp: clauses_def dest!: multi_member_split)
ultimately show ‹trail S ⊨a C›
using total_not_CNot[of ‹lits_of_l (trail S)› C] unfolding true_annots_true_cls true_annot_def
by auto
qed
have 4: ‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))›
using tauto cons incl dist by (auto simp: simple_clss_def)
have [intro]: ‹ρ (lit_of `# mset M') = ρ (lit_of `# mset (trail S))›
if
‹lit_of `# mset (trail S) ∈ simple_clss (atms_of_mm (init_clss S))› and
‹atms_of (lit_of `# mset (trail S)) ⊆ atms_of_mm (init_clss S)› and
‹no_dup (trail S)› and
‹total_over_m (lits_of_l M') (set_mset (init_clss S))› and
incl: ‹mset (trail S) ⊆# mset M'› and
‹lit_of `# mset M' ∈ simple_clss (atms_of_mm (init_clss S))›
for M' :: ‹('v literal, 'v literal, 'v literal multiset) annotated_lit list›
proof -
have [simp]: ‹lits_of_l M' = set_mset (lit_of `# mset M')›
by (auto simp: lits_of_def)
obtain A where A: ‹mset M' = A + mset (trail S)›
using incl by (auto simp: mset_subset_eq_exists_conv)
have M': ‹lits_of_l M' = lit_of ` set_mset A ∪ lits_of_l (trail S)›
unfolding lits_of_def
by (metis A image_Un set_mset_mset set_mset_union)
have ‹mset M' = mset (trail S)›
using that 2 unfolding A total_over_m_alt_def
apply (case_tac A)
apply (auto simp: A simple_clss_def distinct_mset_add M' image_Un
tautology_union mset_inter_empty_set_mset atms_of_def atms_of_s_def
atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set image_image
tautology_add_mset)
by (metis (no_types, lifting) atm_of_in_atm_of_set_iff_in_set_or_uminus_in_set
lits_of_def subsetCE)
then show ?thesis
using 2 by auto
qed
have imp: ‹is_improving (trail S) (trail S) S›
using 1 2 3 4 incl n_d unfolding is_improving_int_def
by (auto simp: oconflict_opt.simps)
show ‹False›
using trail_is_improving_Ex_improve[of S, OF _ imp] nsi by auto
qed
then show ?thesis
using nsc nsp nsi nsco nso nsp nspr
by (auto simp: cdcl_bnb.simps)
qed
lemma no_step_ocdcl⇩w_p_stgy_no_step_cdcl_bnb_stgy:
assumes ‹no_step ocdcl⇩w_p_stgy S› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹no_step cdcl_bnb_stgy S›
using assms no_step_ocdcl⇩w_p_no_step_cdcl_bnb[of S]
by (auto simp: ocdcl⇩w_p_stgy.simps ocdcl⇩w_p.simps
cdcl_bnb.simps cdcl_bnb_stgy.simps)
lemma full_ocdcl⇩w_p_stgy_full_cdcl_bnb_stgy:
assumes ‹full ocdcl⇩w_p_stgy S T› and
inv: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹full cdcl_bnb_stgy S T›
using assms rtranclp_ocdcl⇩w_p_stgy_rtranclp_cdcl_bnb_stgy[of S T]
no_step_ocdcl⇩w_p_stgy_no_step_cdcl_bnb_stgy[of T]
unfolding full_def
by (auto dest: rtranclp_cdcl_bnb_stgy_all_struct_inv[OF rtranclp_cdcl_bnb_stgy_cdcl_bnb])
corollary full_ocdcl⇩w_p_stgy_no_conflicting_clause_from_init_state:
assumes
st: ‹full ocdcl⇩w_p_stgy (init_state N) T› and
dist: ‹distinct_mset_mset N›
shows
‹weight T = None ⟹ unsatisfiable (set_mset N)› and
‹weight T ≠ None ⟹ model_on (set_mset (the (weight T))) N ∧ set_mset (the (weight T)) ⊨sm N ∧
distinct_mset (the (weight T))› and
‹distinct_mset I ⟹ consistent_interp (set_mset I) ⟹ atms_of I = atms_of_mm N ⟹
set_mset I ⊨sm N ⟹ Found (ρ I) ≥ ρ' (weight T)›
using full_cdcl_bnb_stgy_no_conflicting_clause_from_init_state[of N T,
OF full_ocdcl⇩w_p_stgy_full_cdcl_bnb_stgy[OF st] dist] dist
by (auto simp: all_struct_init_state_distinct_iff model_on_def
dest: multi_member_split)
lemma cdcl_bnb_stgy_no_smaller_propa:
‹cdcl_bnb_stgy S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
no_smaller_propa S ⟹ no_smaller_propa T›
apply (induction rule: cdcl_bnb_stgy.induct)
subgoal
by (auto simp: no_smaller_propa_def propagated_cons_eq_append_decide_cons
conflict.simps propagate.simps improvep.simps conflict_opt.simps
ocdcl⇩W_o.simps no_smaller_propa_tl cdcl_bnb_bj.simps
elim!: rulesE)
subgoal
by (auto simp: no_smaller_propa_def propagated_cons_eq_append_decide_cons
conflict.simps propagate.simps improvep.simps conflict_opt.simps
ocdcl⇩W_o.simps no_smaller_propa_tl cdcl_bnb_bj.simps
elim!: rulesE)
subgoal
by (auto simp: no_smaller_propa_def propagated_cons_eq_append_decide_cons
conflict.simps propagate.simps improvep.simps conflict_opt.simps
ocdcl⇩W_o.simps no_smaller_propa_tl cdcl_bnb_bj.simps
elim!: rulesE)
subgoal
by (auto simp: no_smaller_propa_def propagated_cons_eq_append_decide_cons
conflict.simps propagate.simps improvep.simps conflict_opt.simps
ocdcl⇩W_o.simps no_smaller_propa_tl cdcl_bnb_bj.simps
elim!: rulesE)
subgoal for T
apply (cases rule: ocdcl⇩W_o.cases, assumption; thin_tac ‹ocdcl⇩W_o S T›)
subgoal
using decide_no_smaller_step[of S T]
unfolding no_confl_prop_impr.simps
by auto
subgoal
apply (cases rule: cdcl_bnb_bj.cases, assumption; thin_tac ‹cdcl_bnb_bj S T›)
subgoal
using no_smaller_propa_tl[of S T]
by (auto elim: rulesE)
subgoal
using no_smaller_propa_tl[of S T]
by (auto elim: rulesE)
subgoal
using backtrackg_no_smaller_propa[OF obacktrack_backtrackg, of S T]
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by (auto elim: obacktrackE)
done
done
done
lemma rtranclp_cdcl_bnb_stgy_no_smaller_propa:
‹cdcl_bnb_stgy⇧*⇧* S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
no_smaller_propa S ⟹ no_smaller_propa T›
by (induction rule: rtranclp_induct)
(use rtranclp_cdcl_bnb_stgy_all_struct_inv
rtranclp_cdcl_bnb_stgy_cdcl_bnb in ‹force intro: cdcl_bnb_stgy_no_smaller_propa›)+
lemma wf_ocdcl⇩w_p:
‹wf {(T, S). cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)
∧ ocdcl⇩w_p S T}›
by (rule wf_subset[OF wf_cdcl_bnb2]) (auto dest: ocdcl⇩w_p_cdcl_bnb)
end
end