Theory LBD
theory LBD
imports IsaSAT_Literals
begin
chapter ‹LBD›
text ‹LBD (literal block distance) or glue is a measure of usefulness of clauses: It is the number
of different levels involved in a clause. This measure has been introduced by Glucose in 2009
(Audemart and Simon).
LBD has also another advantage, explaining why we implemented it even before working on restarts: It
can speed the conflict minimisation. Indeed a literal might be redundant only if there is a literal
of the same level in the conflict.
The LBD data structure is well-suited to do so: We mark every level that appears in the conflict in
a hash-table like data structure.
Remark that we combine the LBD with a MTF scheme.
›
section ‹Types and relations›
type_synonym lbd = ‹bool list›
type_synonym lbd_ref = ‹nat list × nat × nat›
text ‹Beside the actual ``lookup'' table, we also keep the highest level marked so far to unmark
all levels faster (but we currently don't save the LBD and have to iterate over the data structure).
We also handle growing of the structure by hand instead of using a proper hash-table.
›
definition lbd_ref :: ‹(lbd_ref × lbd) set› where
‹lbd_ref = {((lbd, stamp, m), lbd').
length lbd' ≤ Suc (Suc (unat32_max div 2)) ∧
m = length (filter id lbd') ∧
stamp > 0 ∧
length lbd = length lbd' ∧
(∀v ∈ set lbd. v ≤ stamp) ∧
(∀i < length lbd'. lbd' ! i ⟷ lbd ! i = stamp)
}›
section ‹Testing if a level is marked›
definition level_in_lbd :: ‹nat ⇒ lbd ⇒ bool› where
‹level_in_lbd i = (λlbd. i < length lbd ∧ lbd!i)›
definition level_in_lbd_ref :: ‹nat ⇒ lbd_ref ⇒ bool› where
‹level_in_lbd_ref = (λi (lbd, stamp, _). i < length_uint32_nat lbd ∧ lbd!i = stamp)›
lemma level_in_lbd_ref_level_in_lbd:
‹(uncurry (RETURN oo level_in_lbd_ref), uncurry (RETURN oo level_in_lbd)) ∈
nat_rel ×⇩r lbd_ref →⇩f ⟨bool_rel⟩nres_rel›
by (intro frefI nres_relI) (auto simp: level_in_lbd_ref_def level_in_lbd_def lbd_ref_def)
section ‹Marking more levels›
definition list_grow where
‹list_grow xs n x = xs @ replicate (n - length xs) x›
definition lbd_write :: ‹lbd ⇒ nat ⇒ lbd› where
‹lbd_write = (λlbd i.
(if i < length lbd then (lbd[i := True])
else ((list_grow lbd (i + 1) False)[i := True])))›
definition lbd_ref_write :: ‹lbd_ref ⇒ nat ⇒ lbd_ref nres› where
‹lbd_ref_write = (λ(lbd, stamp, n) i. do {
ASSERT(length lbd ≤ unat32_max ∧ n + 1 ≤ unat32_max);
(if i < length_uint32_nat lbd then
let n = if lbd ! i = stamp then n else n+1 in
RETURN (lbd[i := stamp], stamp, n)
else do {
ASSERT(i + 1 ≤ unat32_max);
RETURN ((list_grow lbd (i + 1) 0)[i := stamp], stamp, n + 1)
})
})›
lemma length_list_grow[simp]:
‹length (list_grow xs n a) = max (length xs) n›
by (auto simp: list_grow_def)
lemma list_update_append2: ‹i ≥ length xs ⟹ (xs @ ys)[i := x] = xs @ ys[i - length xs := x]›
by (induction xs arbitrary: i) (auto split: nat.splits)
lemma lbd_ref_write_lbd_write:
‹(uncurry (lbd_ref_write), uncurry (RETURN oo lbd_write)) ∈
[λ(lbd, i). i ≤ Suc (unat32_max div 2)]⇩f
lbd_ref ×⇩f nat_rel → ⟨lbd_ref⟩nres_rel›
unfolding lbd_ref_write_def lbd_write_def
by (intro frefI nres_relI)
(auto simp: level_in_lbd_ref_def level_in_lbd_def lbd_ref_def list_grow_def
nth_append unat32_max_def length_filter_update_true list_update_append2
length_filter_update_false
intro!: ASSERT_leI le_trans[OF length_filter_le]
elim!: in_set_upd_cases)
section ‹Cleaning the marked levels›
definition lbd_emtpy_inv :: ‹nat list ⇒ nat list × nat ⇒ bool› where
‹lbd_emtpy_inv ys = (λ(xs, i). (∀j < i. xs ! j = 0) ∧ i ≤ length xs ∧ length ys = length xs)›
definition lbd_empty_loop_ref where
‹lbd_empty_loop_ref = (λ(xs, _, _). do {
(xs, i) ←
WHILE⇩T⇗lbd_emtpy_inv xs⇖
(λ(xs, i). i < length xs)
(λ(xs, i). do {
ASSERT(i < length xs);
ASSERT(i + 1 < unat32_max);
RETURN (xs[i := 0], i + 1)})
(xs, 0);
RETURN (xs, 1, 0)
})›
definition lbd_empty where
‹lbd_empty xs = RETURN (replicate (length xs) False)›
lemma lbd_empty_loop_ref:
assumes ‹((xs, m, n), ys) ∈ lbd_ref›
shows
‹lbd_empty_loop_ref (xs, m, n) ≤ ⇓ lbd_ref (RETURN (replicate (length ys) False))›
proof -
have le_xs: ‹length xs ≤ unat32_max div 2 + 2›
‹length ys = length xs›
using assms by (auto simp: lbd_ref_def)
have [iff]: ‹(∀j. ¬ j < (b :: nat)) ⟷ b = 0› for b
by auto
have init: ‹lbd_emtpy_inv xs (xs, 0)›
unfolding lbd_emtpy_inv_def
by (auto simp: lbd_ref_def)
have lbd_remove: ‹lbd_emtpy_inv xs (a[b := 0], b + 1)›
if
inv: ‹lbd_emtpy_inv xs s› and
‹case s of (ys, i) ⇒ length ys = length xs› and
cond: ‹case s of (xs, i) ⇒ i < length xs› and
s: ‹s = (a, b)› and
b_le: ‹b < length a›
for s a b
proof -
have 1: ‹a[b := 0] ! j = 0› if ‹j<b› for j
using inv that unfolding lbd_emtpy_inv_def s
by auto
have ‹a[b := 0] ! j = 0› if ‹j<b + 1› for j
using 1[of j] that cond b_le by (cases ‹j = b›) auto
then show ?thesis
using cond inv unfolding lbd_emtpy_inv_def s by auto
qed
have lbd_final: ‹((a, 1, 0), replicate (length ys) False) ∈ lbd_ref›
if
lbd: ‹lbd_emtpy_inv xs s› and
I': ‹case s of (ys, i) ⇒ length ys = length xs› and
cond: ‹¬ (case s of (xs, i) ⇒ i < length xs)› and
s: ‹s = (a, b)›
for s a b
proof -
have 1: ‹a[b := 0] ! j = 0› if ‹j<b› for j
using lbd that unfolding lbd_emtpy_inv_def s
by auto
have [simp]: ‹length a = length xs›
using I' unfolding s by auto
have [dest]: ‹i < length xs ⟹ a ! i = 0› for i
using 1[of i] lbd cond unfolding s lbd_emtpy_inv_def by (cases ‹i < Suc m›) auto
have [simp]: ‹a = replicate (length xs) 0›
unfolding list_eq_iff_nth_eq
apply (intro conjI)
subgoal by simp
subgoal by auto
done
show ?thesis
using le_xs by (auto simp: lbd_ref_def)
qed
show ?thesis
unfolding lbd_empty_loop_ref_def conc_fun_RETURN
apply clarify
apply (refine_vcg WHILEIT_rule_stronger_inv[where R = ‹measure (λ(xs, i). length xs - i)› and
I' = ‹λ(ys, i). length ys = length xs›])
subgoal by auto
subgoal by (rule init)
subgoal by auto
subgoal by auto
subgoal using assms by (auto simp: lbd_ref_def lbd_emtpy_inv_def unat32_max_def)
subgoal by (rule lbd_remove)
subgoal by auto
subgoal by (auto simp: lbd_emtpy_inv_def)
subgoal by (rule lbd_final)
done
qed
definition lbd_empty_cheap_ref where
‹lbd_empty_cheap_ref = (λ(xs, stamp, n). RETURN (xs, stamp + 1, 0))›
lemma lbd_empty_cheap_ref:
assumes ‹((xs, m, n), ys) ∈ lbd_ref›
shows
‹lbd_empty_cheap_ref (xs, m, n) ≤ ⇓ lbd_ref (RETURN (replicate (length ys) False))›
using assms unfolding lbd_empty_cheap_ref_def lbd_ref_def
by (auto simp: filter_empty_conv all_set_conv_nth in_set_conv_nth)
definition lbd_empty_ref :: ‹lbd_ref ⇒ lbd_ref nres› where
‹lbd_empty_ref = (λ(xs, m, n). if m = unat32_max then lbd_empty_loop_ref (xs,m,n)
else lbd_empty_cheap_ref (xs, m, n)) ›
lemma lbd_empty_ref:
assumes ‹((xs, m, n), ys) ∈ lbd_ref›
shows
‹lbd_empty_ref (xs, m, n) ≤ ⇓ lbd_ref (RETURN (replicate (length ys) False))›
using lbd_empty_cheap_ref[OF assms] lbd_empty_loop_ref[OF assms]
by (auto simp: lbd_empty_ref_def)
lemma lbd_empty_ref_lbd_empty:
‹(lbd_empty_ref, lbd_empty) ∈ lbd_ref →⇩f ⟨lbd_ref⟩nres_rel›
apply (intro frefI nres_relI)
apply clarify
subgoal for lbd m lbd'
using lbd_empty_ref[of lbd m]
by (auto simp: lbd_empty_def)
done
definition (in -)empty_lbd :: ‹lbd› where
‹empty_lbd = (replicate 32 False)›
definition empty_lbd_ref :: ‹lbd_ref› where
‹empty_lbd_ref = (replicate 32 0, 1, 0)›
lemma empty_lbd_ref_empty_lbd:
‹(λ_. (RETURN empty_lbd_ref), λ_. (RETURN empty_lbd)) ∈ unit_rel →⇩f ⟨lbd_ref⟩nres_rel›
by (intro frefI nres_relI) (auto simp: empty_lbd_def lbd_ref_def empty_lbd_ref_def
unat32_max_def nth_Cons split: nat.splits)
section ‹Extracting the LBD›
text ‹We do not prove correctness of our algorithm, as we don't care about the actual returned
value (for correctness).›
definition get_LBD :: ‹lbd ⇒ nat nres› where
‹get_LBD lbd = SPEC(λ_. True)›
definition get_LBD_ref :: ‹lbd_ref ⇒ nat nres› where
‹get_LBD_ref = (λ(xs, m, n). RETURN n)›
lemma get_LBD_ref:
‹((lbd, m), lbd') ∈ lbd_ref ⟹ get_LBD_ref (lbd, m) ≤ ⇓ nat_rel (get_LBD lbd')›
unfolding get_LBD_ref_def get_LBD_def
by (auto split:prod.splits)
lemma get_LBD_ref_get_LBD:
‹(get_LBD_ref, get_LBD) ∈ lbd_ref →⇩f ⟨nat_rel⟩nres_rel›
apply (intro frefI nres_relI)
apply clarify
subgoal for lbd m n lbd'
using get_LBD_ref[of lbd]
by (auto simp: lbd_empty_def lbd_ref_def)
done
end