Theory CDCL_W_BnB
theory CDCL_W_BnB
imports CDCL.CDCL_W_Abstract_State
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›
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_bnb⇩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)›
text ‹While it would more be natural to add an sublocale with the extended version clause set,
this actually causes a loop in the hierarchy structure (although with different parameters).
Therefore, adding theorems (e.g. defining an inductive predicate) causes a loop.
›
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_bnb⇩W_ops =
conflict_driven_clause_learning_with_adding_init_clause_bnb⇩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
paragraph ‹Conversion to CDCL›
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')
paragraph ‹Overall simplification on states›
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')+
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
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 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 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 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 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)
paragraph ‹CDCL with branch-and-bound›
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]
by (induction rule: conflict_opt.cases)
(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 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)
lemma cdcl_bnb_stgy_cdcl⇩W_or_improve:
assumes ‹cdcl_bnb S T› and ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹(λS T. cdcl⇩W_restart_mset.cdcl⇩W (abs_state S) (abs_state T) ∨ improvep S T) S T›
using assms
apply (induction rule: cdcl_bnb.cases)
apply (auto dest!: propagate_propagate conflict_conflict
intro: cdcl⇩W_restart_mset.cdcl⇩W.intros simp add: cdcl⇩W_restart_mset.W_conflict conflict_opt_conflict
cdcl⇩W_o_cdcl⇩W_o cdcl⇩W_restart_mset.W_other)
done
lemma rtranclp_cdcl_bnb_stgy_cdcl⇩W_or_improve:
assumes ‹rtranclp cdcl_bnb S T› and ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)›
shows ‹(λS T. cdcl⇩W_restart_mset.cdcl⇩W (abs_state S) (abs_state T) ∨ improvep S T)⇧*⇧* S T›
using assms
apply (induction rule: rtranclp_induct)
subgoal by auto
subgoal for T U
using cdcl_bnb_stgy_cdcl⇩W_or_improve[of T U] rtranclp_cdcl_bnb_stgy_all_struct_inv[of S T]
by (smt rtranclp_unfold tranclp_unfold_end)
done
lemma eq_diff_subset_iff: ‹A = B + (A -B) ⟷ B ⊆# A›
by (metis mset_subset_eq_add_left subset_mset.add_diff_inverse)
lemma cdcl_bnb_conflicting_clss_mono:
‹cdcl_bnb S T ⟹ cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S) ⟹
conflicting_clss S ⊆# conflicting_clss T›
by (auto simp: cdcl_bnb.simps ocdcl⇩W_o.simps improvep.simps cdcl_bnb_bj.simps
obacktrack.simps conflict_opt.simps conflicting_clss_update_weight_information_mono elim!: rulesE)
lemma cdcl_or_improve_cdclD:
assumes ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
‹cdcl_bnb S T›
shows ‹∃N.
cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* (trail S, init_clss S + N, learned_clss S, conflicting S) (abs_state T) ∧
CDCL_W_Abstract_State.init_clss (abs_state T) = init_clss S + N›
proof -
have inv_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using assms(1) assms(2) cdcl_bnb_stgy_all_struct_inv by blast
consider
‹improvep S T› |
‹cdcl⇩W_restart_mset.cdcl⇩W (abs_state S) (abs_state T)›
using cdcl_bnb_stgy_cdcl⇩W_or_improve[of S T] assms by blast
then show ?thesis
proof cases
case 1
then show ?thesis
using assms cdcl_bnb_stgy_cdcl⇩W_or_improve[of S T]
unfolding abs_state_def cdcl_bnb_no_more_init_clss[of S T, OF assms(2)]
by (auto simp: improvep.simps cdcl⇩W_restart_mset_state eq_diff_subset_iff)
next
case 2
let ?S' = ‹(trail S, init_clss S + (conflicting_clss S) + (conflicting_clss T - conflicting_clss S),
learned_clss S, conflicting S)›
let ?S'' = ‹(trail S, init_clss S + conflicting_clss T, learned_clss S, conflicting S)›
let ?T' = ‹(trail T, init_clss T + (conflicting_clss T) + (conflicting_clss T - conflicting_clss S),
learned_clss T, conflicting T)›
have subs: ‹conflicting_clss S ⊆# conflicting_clss T›
using cdcl_bnb_conflicting_clss_mono[of S T] assms by fast
then have H[simp]: ‹set_mset (conflicting_clss T + (conflicting_clss T -
conflicting_clss S)) = set_mset (conflicting_clss T)›
apply (auto simp flip: multiset_diff_union_assoc[OF subs])
apply (subst (asm) multiset_diff_union_assoc[OF subs] set_mset_union)+
apply (auto dest: in_diffD)
apply (subst multiset_diff_union_assoc[OF subs] set_mset_union)+
apply (auto dest: in_diffD)
done
have [simp]: ‹set_mset (init_clss T + conflicting_clss T + conflicting_clss T -
conflicting_clss S) = set_mset (init_clss T + conflicting_clss T)›
by (subst multiset_diff_union_assoc, (rule subs))
(simp only: H ac_simps, subst set_mset_union, subst H, simp)
have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv ?T'›
by (rule cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_clauses_cong[OF inv_T])
(auto simp: cdcl⇩W_restart_mset_state eq_diff_subset_iff abs_state_def subs)
then have ‹cdcl⇩W_restart_mset.cdcl⇩W ?S' ?T'›
using 2 cdcl⇩W_restart_mset.cdcl⇩W_enlarge_clauses[of ‹abs_state S› ‹abs_state T› ?S' ‹conflicting_clss T - conflicting_clss S› ‹{#}›]
by (auto simp: cdcl⇩W_restart_mset_state abs_state_def subs)
then have ‹cdcl⇩W_restart_mset.cdcl⇩W ?S'' (abs_state T)›
using cdcl⇩W_restart_mset.cdcl⇩W_clauses_cong[of ‹?S'› ?T' ?S'']
cdcl⇩W_restart_mset.cdcl⇩W_learnel_clss_mono[of ‹?S'› ?T']
cdcl⇩W_restart_mset.cdcl⇩W_restart_init_clss[OF cdcl⇩W_restart_mset.cdcl⇩W_cdcl⇩W_restart, of ‹?S'› ?T']
unfolding abs_state_def cdcl_bnb_no_more_init_clss[of S T, OF assms(2)]
by (auto simp: cdcl⇩W_restart_mset_state abs_state_def subs)
then show ?thesis
by (auto intro!: exI[of _ ‹conflicting_clss T›] simp: abs_state_def init_clss.simps
cdcl_bnb_no_more_init_clss[of S T, OF assms(2)])
qed
qed
lemma rtranclp_cdcl_or_improve_cdclD:
assumes ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state S)› and
‹cdcl_bnb⇧*⇧* S T›
shows ‹∃N.
cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* (trail S, init_clss S + N, learned_clss S, conflicting S) (abs_state T) ∧
CDCL_W_Abstract_State.init_clss (abs_state T) = init_clss S + N›
using assms(2,1)
proof (induction rule: rtranclp_induct)
case base
then show ?case by (auto intro!: exI[of _ ‹{#}›] simp: abs_state_def init_clss.simps)
next
case (step T U)
then obtain N where
st: ‹cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* (trail S, init_clss S + N, learned_clss S, conflicting S)
(abs_state T)› and
eq: ‹CDCL_W_Abstract_State.init_clss (abs_state T) = init_clss S + N›
by auto
obtain N' where
st': ‹cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* (trail T, init_clss T + N', learned_clss T, conflicting T)
(abs_state U)› and
eq': ‹CDCL_W_Abstract_State.init_clss (abs_state U) = init_clss T + N'›
using cdcl_or_improve_cdclD[of T U] rtranclp_cdcl_bnb_stgy_all_struct_inv[of S T] step
by (auto simp: cdcl⇩W_restart_mset_state)
have inv_T: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state T)›
using rtranclp_cdcl_bnb_stgy_all_struct_inv step.hyps(1) step.prems by blast
have [simp]: ‹init_clss S = init_clss T› ‹init_clss T = init_clss U›
using rtranclp_cdcl_bnb_no_more_init_clss[OF step(1)] cdcl_bnb_no_more_init_clss[OF step(2)]
by fast+
then have ‹N ⊆# N'›
using eq eq' inv_T cdcl_bnb_conflicting_clss_mono[of T U] step
by (auto simp: abs_state_def init_clss.simps)
let ?S = ‹(trail S, init_clss S + N, learned_clss S, conflicting S)›
let ?S' = ‹(trail S, (init_clss S + N) + (N' - N), learned_clss S, conflicting S)›
let ?T' = ‹(trail T, init_clss T + (conflicting_clss T) + (N' - N), learned_clss T, conflicting T)›
have ‹cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* ?S' ?T'›
using st eq cdcl⇩W_restart_mset.rtranclp_cdcl⇩W_enlarge_clauses[of ?S' ?S ‹N' - N› ‹{#}› ‹abs_state T›]
by (auto simp: cdcl⇩W_restart_mset_state abs_state_def)
moreover have ‹init_clss T + (conflicting_clss T) + (N' - N) = init_clss T + N'›
using eq eq' ‹N ⊆# N'›
by (auto simp: abs_state_def init_clss.simps)
ultimately have
‹cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧* (trail S, init_clss S + N', learned_clss S, conflicting S)
(abs_state U)›
using eq' st' ‹N ⊆# N'› unfolding abs_state_def
by auto
then show ?case
using eq' st' by (auto intro!: exI[of _ N'])
qed
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
by induction (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)›])
declare conflict_is_false_with_level_def[simp del]
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_other' S')
show ?case
by (rule ocdcl⇩W_o_no_smaller_confl_inv)
(use cdcl_bnb_other' in ‹auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def›)
qed (auto intro: conflict_no_smaller_confl_inv propagate_no_smaller_confl_inv;
auto simp: no_smaller_confl_def improvep.simps conflict_opt.simps)+
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 ‹cdcl⇩W_restart_mset.skip (abs_state S) (abs_state T)›
using skip.intros[of S L C' M D T] skip 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 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 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 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 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
then show ‹unsatisfiable (set_mset (clauses T + conflicting_clss T))›
unfolding true_clss_cls_def satisfiable_def by auto
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 get_all_ann_decomposition_exists_prepend)
lemma cdcl_bnb_pow2_n_learned_clauses:
assumes ‹distinct_mset_mset N›
‹cdcl_bnb⇧*⇧* (init_state N) T›
shows ‹size (learned_clss T) ≤ 2 ^ (card (atms_of_mm N))›
proof -
have H: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (abs_state (init_state N))›
using assms apply (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.cdcl⇩W_learned_clause_def
cdcl⇩W_restart_mset.reasons_in_clauses_def)
using assms by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
distinct_mset_mset_conflicting_clss
cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def abs_state_def init_clss.simps)
then obtain Na where Na: ‹ cdcl⇩W_restart_mset.cdcl⇩W⇧*⇧*
(trail (init_state N), init_clss (init_state N) + Na,
learned_clss (init_state N), conflicting (init_state N))
(abs_state T) ∧
CDCL_W_Abstract_State.init_clss (abs_state T) = init_clss (init_state N) + Na›
using rtranclp_cdcl_or_improve_cdclD[OF H assms(2)] by auto
moreover have ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv ([], N + Na, {#}, None)›
using assms Na rtranclp_cdcl_bnb_no_more_init_clss[OF assms(2)]
apply (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.cdcl⇩W_learned_clause_def
cdcl⇩W_restart_mset.reasons_in_clauses_def)
using assms by (auto simp: cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def cdcl⇩W_restart_mset_state
distinct_mset_mset_conflicting_clss 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.distinct_cdcl⇩W_state_def abs_state_def init_clss.simps)
ultimately show ?thesis
using rtranclp_cdcl_bnb_no_more_init_clss[OF assms(2)]
cdcl⇩W_restart_mset.cdcl_pow2_n_learned_clauses2[of ‹N + Na› ‹abs_state T›]
by (auto simp: init_state.simps abs_state_def cdcl⇩W_restart_mset_state)
qed
end
end