Theory CDCL_Conflict_Minimisation
theory CDCL_Conflict_Minimisation
imports
Watched_Literals_Watch_List
More_Sepref.WB_More_Refinement
More_Sepref.WB_More_Refinement_List "List-Index.List_Index"
begin
chapter ‹Conflict Minimisation›
text ‹We implement the conflict minimisation as presented by Sörensson and Biere
(``Minimizing Learned Clauses''').
We refer to the paper for further details, but the general idea is to produce a series of resolution
steps such that eventually (i.e., after enough resolution steps) no new literals has been introduced
in the conflict clause.
The resolution steps are only done with the reasons of the of literals
appearing in the trail. Hence these steps are terminating: we are ``shortening'' the trail we have
to consider with each resolution step. Remark that the shortening refers to the length of the trail
we have to consider, not the levels.
The concrete proof was harder than we initially expected. Our first proof try was to certify the
resolution steps. While this worked out, adding caching on top of that turned to be rather hard,
since it is not obvious how to add resolution steps in the middle of the current proof if the
literal has already been removed (basically we would have to prove termination and confluence of the
rewriting system).
Therefore, we worked instead directly on the entailment of the literals of the conflict clause
(up to the point in the trail we currently considering, which is also the termination measure).
The previous try is still present in our formalisation (see \<^term>‹minimize_conflict_support›, which
we however only use for the termination proof).
The algorithm presented above does not distinguish between literals propagated at the same level:
we cannot reuse information about failures to cut branches. There is a variant of the algorithm
presented above that is able to do so (Van Gelder, ``Improved Conflict-Clause Minimization
Leads to Improved Propositional Proof Traces''). The algorithm is however more complicated and has
only be implemented in very few solvers (at least lingeling and cadical) and is especially not part
of glucose nor cryptominisat. Therefore, we have decided to not implement it: It is probably not
worth it and requires some additional data structures.
›
declare cdcl⇩W_restart_mset_state[simp]
type_synonym out_learned = ‹nat clause_l›
text ‹The data structure contains the (unique) literal of highest at position one. This is useful
since this is what we want to have at the end (propagation clause) and we can skip the first
literal when minimising the clause.
›
definition out_learned :: ‹(nat, nat) ann_lits ⇒ nat clause option ⇒ out_learned ⇒ bool› where
‹out_learned M D out ⟷
out ≠ [] ∧
(D = None ⟶ length out = 1) ∧
(D ≠ None ⟶ mset (tl out) = filter_mset (λL. get_level M L < count_decided M) (the D))›
definition out_learned_confl :: ‹(nat, nat) ann_lits ⇒ nat clause option ⇒ out_learned ⇒ bool› where
‹out_learned_confl M D out ⟷
out ≠ [] ∧ (D ≠ None ∧ mset out = the D)›
lemma out_learned_Cons_None[simp]:
‹out_learned (L # aa) None ao ⟷ out_learned aa None ao›
by (auto simp: out_learned_def)
lemma out_learned_tl_None[simp]:
‹out_learned (tl aa) None ao ⟷ out_learned aa None ao›
by (auto simp: out_learned_def)
definition index_in_trail :: ‹('v, 'a) ann_lits ⇒ 'v literal ⇒ nat› where
‹index_in_trail M L = index (map (atm_of o lit_of) (rev M)) (atm_of L)›
lemma Propagated_in_trail_entailed:
assumes
invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, N, U, D)› and
in_trail: ‹Propagated L C ∈ set M›
shows
‹M ⊨as CNot (remove1_mset L C)› and ‹L ∈# C› and ‹N + U ⊨pm C› and
‹K ∈# remove1_mset L C ⟹ index_in_trail M K < index_in_trail M L› and
‹¬tautology C› and ‹distinct_mset C›
proof -
obtain M2 M1 where
M: ‹M = M2 @ Propagated L C # M1›
using split_list[OF in_trail] by metis
have ‹a @ Propagated L mark # b = trail (M, N, U, D) ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› and
dist: ‹cdcl⇩W_restart_mset.distinct_cdcl⇩W_state (M, N, U, D)›
for L mark a b
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by fast+
then have L_E: ‹L ∈# C› and M1_E: ‹M1 ⊨as CNot (remove1_mset L C)›
unfolding M by force+
then have M_E: ‹M ⊨as CNot (remove1_mset L C)›
unfolding M by (simp add: true_annots_append_l)
show ‹M ⊨as CNot (remove1_mset L C)› and ‹L ∈# C›
using L_E M_E by fast+
have ‹set (get_all_mark_of_propagated (trail (M, N, U, D)))
⊆ set_mset (cdcl⇩W_restart_mset.clauses (M, N, U, D))›
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_learned_clause_alt_def
by fast
then have ‹C ∈# N + U›
using in_trail cdcl⇩W_restart_mset.in_get_all_mark_of_propagated_in_trail[of C M]
by (auto simp: clauses_def)
then show ‹N + U ⊨pm C› by auto
have n_d: ‹no_dup M›
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by auto
show ‹index_in_trail M K < index_in_trail M L› if K_C: ‹K ∈# remove1_mset L C›
proof -
have
KL: ‹atm_of K ≠ atm_of L› and
uK_M1: ‹-K ∈ lits_of_l M1› and
L: ‹L ∉ lit_of ` (set M2 ∪ set M1)› ‹-L ∉ lit_of ` (set M2 ∪ set M1)›
using M1_E K_C n_d unfolding M true_annots_true_cls_def_iff_negation_in_model
by (auto dest!: multi_member_split simp: atm_of_eq_atm_of lits_of_def uminus_lit_swap
Decided_Propagated_in_iff_in_lits_of_l)
have L_M1: ‹atm_of L ∉ (atm_of ∘ lit_of) ` set M1›
using L by (auto simp: image_Un atm_of_eq_atm_of)
have K_M1: ‹atm_of K ∈ (atm_of ∘ lit_of) ` set M1›
using uK_M1 by (auto simp: lits_of_def image_image comp_def uminus_lit_swap)
show ?thesis
using KL L_M1 K_M1 unfolding index_in_trail_def M by (auto simp: index_append)
qed
have ‹¬tautology(remove1_mset L C)›
by (rule consistent_CNot_not_tautology[of ‹lits_of_l M1›])
(use n_d M1_E in ‹auto dest: distinct_consistent_interp no_dup_appendD
simp: true_annots_true_cls M›)
then show ‹¬tautology C›
using multi_member_split[OF L_E] M1_E n_d
by (auto simp: tautology_add_mset true_annots_true_cls_def_iff_negation_in_model M
dest!: multi_member_split in_lits_of_l_defined_litD)
show ‹distinct_mset (C)›
using dist ‹C ∈# N + U› unfolding cdcl⇩W_restart_mset.distinct_cdcl⇩W_state_def
by (auto dest: multi_member_split)
qed
text ‹This predicate corresponds to one resolution step.›
inductive minimize_conflict_support :: ‹('v, 'v clause) ann_lits ⇒ 'v clause ⇒ 'v clause ⇒ bool›
for M where
resolve_propa:
‹minimize_conflict_support M (add_mset (-L) C) (C + remove1_mset L E)›
if ‹Propagated L E ∈ set M› |
remdups: ‹minimize_conflict_support M (add_mset L C) C›
lemma index_in_trail_uminus[simp]: ‹index_in_trail M (-L) = index_in_trail M L›
by (auto simp: index_in_trail_def)
text ‹This is the termination argument of the conflict minimisation: the multiset of the levels
decreases (for the multiset ordering).›
definition minimize_conflict_support_mes :: ‹('v, 'v clause) ann_lits ⇒ 'v clause ⇒ nat multiset›
where
‹minimize_conflict_support_mes M C = index_in_trail M `# C›
context
fixes M :: ‹('v, 'v clause) ann_lits› and N U :: ‹'v clauses› and
D :: ‹'v clause option›
assumes invs: ‹cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv (M, N, U, D)›
begin
private lemma
no_dup: ‹no_dup M› and
consistent: ‹consistent_interp (lits_of_l M)›
using invs unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_M_level_inv_def
by simp_all
lemma minimize_conflict_support_entailed_trail:
assumes ‹minimize_conflict_support M C E› and ‹M ⊨as CNot C›
shows ‹M ⊨as CNot E›
using assms
proof (induction rule: minimize_conflict_support.induct)
case (resolve_propa L E C) note in_trail = this(1) and M_C = this(2)
then show ?case
using Propagated_in_trail_entailed[OF invs in_trail] by (auto dest!: multi_member_split)
next
case (remdups L C)
then show ?case
by auto
qed
lemma rtranclp_minimize_conflict_support_entailed_trail:
assumes ‹(minimize_conflict_support M)⇧*⇧* C E› and ‹M ⊨as CNot C›
shows ‹M ⊨as CNot E›
using assms apply (induction rule: rtranclp_induct)
subgoal by fast
subgoal using minimize_conflict_support_entailed_trail by fast
done
lemma minimize_conflict_support_mes:
assumes ‹minimize_conflict_support M C E›
shows ‹minimize_conflict_support_mes M E < minimize_conflict_support_mes M C›
using assms unfolding minimize_conflict_support_mes_def
proof (induction rule: minimize_conflict_support.induct)
case (resolve_propa L E C) note in_trail = this
let ?f = ‹λxa. index (map (λa. atm_of (lit_of a)) (rev M)) xa›
have ‹?f (atm_of x) < ?f (atm_of L)› if x: ‹x ∈# remove1_mset L E› for x
proof -
obtain M2 M1 where
M: ‹M = M2 @ Propagated L E # M1›
using split_list[OF in_trail] by metis
have ‹a @ Propagated L mark # b = trail (M, N, U, D) ⟶
b ⊨as CNot (remove1_mset L mark) ∧ L ∈# mark› for L mark a b
using invs
unfolding cdcl⇩W_restart_mset.cdcl⇩W_all_struct_inv_def
cdcl⇩W_restart_mset.cdcl⇩W_conflicting_def
by fast
then have L_E: ‹L ∈# E› and M_E: ‹M1 ⊨as CNot (remove1_mset L E)›
unfolding M by force+
then have ‹-x ∈ lits_of_l M1›
using x unfolding true_annots_true_cls_def_iff_negation_in_model by auto
then have ‹?f (atm_of x) < length M1›
using no_dup
by (auto simp: M lits_of_def index_append Decided_Propagated_in_iff_in_lits_of_l
uminus_lit_swap)
moreover have ‹?f (atm_of L) = length M1›
using no_dup unfolding M by (auto simp: index_append Decided_Propagated_in_iff_in_lits_of_l
atm_of_eq_atm_of lits_of_def)
ultimately show ?thesis by auto
qed
then show ?case by (auto simp: comp_def index_in_trail_def)
next
case (remdups L C)
then show ?case by auto
qed
lemma wf_minimize_conflict_support:
shows ‹wf {(C', C). minimize_conflict_support M C C'}›
apply (rule wf_if_measure_in_wf[of ‹{(C', C). C' < C}› _ ‹minimize_conflict_support_mes M›])
subgoal using wf .
subgoal using minimize_conflict_support_mes by auto
done
end
lemma conflict_minimize_step:
assumes
‹NU ⊨p add_mset L C› and
‹NU ⊨p add_mset (-L) D› and
‹⋀K'. K' ∈# C ⟹ NU ⊨p add_mset (-K') D›
shows ‹NU ⊨p D›
proof -
have ‹NU ⊨p D + C›
using assms(1,2) true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or by blast
then show ?thesis
using assms(3)
proof (induction C)
case empty
then show ?case
using true_clss_cls_in true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or by fastforce
next
case (add x C) note IH =this(1) and NU_DC = this(2) and entailed = this(3)
have ‹NU ⊨p D + C + D›
using entailed[of x] NU_DC
true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[of NU ‹-x› ‹D + C› D]
by auto
then have ‹NU ⊨p D + C›
by (smt (verit) total_over_m_sum total_over_m_union true_cls_union true_clss_cls_def)
from IH[OF this] entailed show ?case by auto
qed
qed
text ‹This function filters the clause by the levels up the level of the given literal. This is
the part the conflict clause that is considered when testing if the given literal is redundant.›
definition filter_to_poslev where
‹filter_to_poslev M L D = filter_mset (λK. index_in_trail M K < index_in_trail M L) D›
lemma filter_to_poslev_uminus[simp]:
‹filter_to_poslev M (-L) D = filter_to_poslev M L D›
by (auto simp: filter_to_poslev_def)
lemma filter_to_poslev_empty[simp]:
‹filter_to_poslev M L {#} = {#}›
by (auto simp: filter_to_poslev_def)
lemma filter_to_poslev_mono:
‹index_in_trail M K' ≤ index_in_trail M L ⟹
filter_to_poslev M K' D ⊆# filter_to_poslev M L D›
unfolding filter_to_poslev_def
by (auto simp: multiset_filter_mono2)
lemma filter_to_poslev_mono_entailement:
‹index_in_trail M K' ≤ index_in_trail M L ⟹
NU ⊨p filter_to_poslev M K' D ⟹ NU ⊨p filter_to_poslev M L D›
by (metis (full_types) filter_to_poslev_mono subset_mset.le_iff_add true_clss_cls_mono_r)
lemma filter_to_poslev_mono_entailement_add_mset:
‹index_in_trail M K' ≤ index_in_trail M L ⟹
NU ⊨p add_mset J (filter_to_poslev M K' D) ⟹ NU ⊨p add_mset J (filter_to_poslev M L D)›
by (metis filter_to_poslev_mono mset_subset_eq_add_mset_cancel subset_mset.le_iff_add
true_clss_cls_mono_r)
lemma conflict_minimize_intermediate_step:
assumes
‹NU ⊨p add_mset L C› and
K'_C: ‹⋀K'. K' ∈# C ⟹ NU ⊨p add_mset (-K') D ∨ K' ∈# D›
shows ‹NU ⊨p add_mset L D›
proof -
have ‹NU ⊨p add_mset L C + D›
using assms(1) true_clss_cls_mono_r by blast
then show ?thesis
using assms(2)
proof (induction C)
case empty
then show ?case
using true_clss_cls_in true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or by fastforce
next
case (add x C) note IH =this(1) and NU_DC = this(2) and entailed = this(3)
have 1: ‹NU ⊨p add_mset x (add_mset L (D + C))›
using NU_DC by (auto simp: add_mset_commute ac_simps)
moreover have 2: ‹remdups_mset (add_mset L (D + C + D)) = remdups_mset (add_mset L (C + D))›
by (auto simp: remdups_mset_def)
moreover have 3: ‹remdups_mset (D + C + D) = remdups_mset (D + C)›
by (auto simp: remdups_mset_def)
moreover have ‹x ∈# D ⟹ NU ⊨p add_mset L (D + C + D)›
using 1
apply (subst (asm) true_clss_cls_remdups_mset[symmetric])
apply (subst true_clss_cls_remdups_mset[symmetric])
by (auto simp: 2 3)
ultimately have ‹NU ⊨p add_mset L (D + C + D)›
using entailed[of x] NU_DC
true_clss_cls_or_true_clss_cls_or_not_true_clss_cls_or[of NU ‹-x› ‹add_mset L D + C› D]
by auto
moreover have ‹remdups_mset (D + (C + D)) = remdups_mset (D + C)›
by (auto simp: remdups_mset_def)
ultimately have ‹NU ⊨p add_mset L C + D›
apply (subst true_clss_cls_remdups_mset[symmetric])
apply (subst (asm) true_clss_cls_remdups_mset[symmetric])
by (auto simp add: 3 2 add.commute simp del: true_clss_cls_remdups_mset)
from IH[OF this] entailed show ?case by auto
qed
qed
lemma conflict_minimize_intermediate_step_filter_to_poslev:
assumes
lev_K_L: ‹⋀K'. K' ∈# C ⟹ index_in_trail M K' < index_in_trail M L› and
NU_LC: ‹NU ⊨p add_mset L C› and
K'_C: ‹⋀K'. K' ∈# C ⟹ NU ⊨p add_mset (-K') (filter_to_poslev M L D) ∨
K' ∈# filter_to_poslev M L D›
shows ‹NU ⊨p add_mset L (filter_to_poslev M L D)›
proof -
have C_entailed: ‹K' ∈# C ⟹ NU ⊨p add_mset (-K') (filter_to_poslev M L D) ∨
K' ∈# filter_to_poslev M L D› for K'
using filter_to_poslev_mono[of M K' L D] lev_K_L[of K'] K'_C[of K']
true_clss_cls_mono_r[of _ ‹ add_mset (- K') (filter_to_poslev M K' D)› ]
by (auto simp: mset_subset_eq_exists_conv)
show ?thesis
using conflict_minimize_intermediate_step[OF NU_LC C_entailed] by fast
qed