Theory IsaSAT_Rephase
theory IsaSAT_Rephase
imports IsaSAT_Phasing
begin
chapter ‹Phase Saving›
section ‹Rephasing›
type_synonym phase_save_heur = ‹phase_saver × 64 word × phase_saver × 64 word × phase_saver × 64 word × 64 word × 64 word›
definition phase_save_heur_rel :: ‹nat multiset ⇒ phase_save_heur ⇒ bool› where
‹phase_save_heur_rel 𝒜 = (λ(φ, target_assigned, target, best_assigned, best,
end_of_phase, curr_phase). phase_saving 𝒜 φ ∧
phase_saving 𝒜 target ∧ phase_saving 𝒜 best ∧ length φ = length best ∧
length target = length best)›
definition end_of_rephasing_phase :: ‹phase_save_heur ⇒ 64 word› where
‹end_of_rephasing_phase = (λ(φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase,
length_phase). end_of_phase)›
definition phase_current_rephasing_phase :: ‹phase_save_heur ⇒ 64 word› where
‹phase_current_rephasing_phase =
(λ(φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase, length_phase). curr_phase)›
text ‹
We implement the idea in CaDiCaL of rephasing:
▪ We remember the best model found so far. It is used as base.
▪ We flip the phase saving heuristics between \<^term>‹True›,
\<^term>‹False›, and random.
›
definition rephase_init :: ‹bool ⇒ bool list ⇒ bool list nres› where
‹rephase_init b φ = do {
let n = length φ;
nfoldli [0..<n]
(λ_. True)
(λ a φ. do {
ASSERT(a < length φ);
RETURN (φ[a := b])
})
φ
}›
lemma rephase_init_spec:
‹rephase_init b φ ≤ SPEC(λψ. length ψ = length φ)›
proof -
show ?thesis
unfolding rephase_init_def Let_def
apply (rule nfoldli_rule[where I = ‹λ_ _ ψ. length φ = length ψ›])
apply (auto dest: in_list_in_setD)
done
qed
definition copy_phase :: ‹bool list ⇒ bool list ⇒ bool list nres› where
‹copy_phase φ φ' = do {
ASSERT(length φ = length φ');
let n = length φ';
nfoldli [0..<n]
(λ_. True)
(λ a φ'. do {
ASSERT(a < length φ);
ASSERT(a < length φ');
RETURN (φ'[a := φ!a])
})
φ'
}›
lemma copy_phase_alt_def:
‹copy_phase φ φ' = do {
ASSERT(length φ = length φ');
let n = length φ;
nfoldli [0..<n]
(λ_. True)
(λ a φ'. do {
ASSERT(a < length φ);
ASSERT(a < length φ');
RETURN (φ'[a := φ!a])
})
φ'
}›
unfolding copy_phase_def
by (auto simp: ASSERT_same_eq_conv)
lemma copy_phase_spec:
‹length φ = length φ' ⟹ copy_phase φ φ' ≤ SPEC(λψ. length ψ = length φ)›
unfolding copy_phase_def Let_def
apply (intro ASSERT_leI)
subgoal by auto
apply (rule nfoldli_rule[where I = ‹λ_ _ ψ. length φ = length ψ›])
apply (auto dest: in_list_in_setD)
done
definition rephase_random :: ‹64 word ⇒ bool list ⇒ bool list nres› where
‹rephase_random b φ = do {
let n = length φ;
(_, φ) ← nfoldli [0..<n]
(λ_. True)
(λa (state, φ). do {
ASSERT(a < length φ);
let state = state * 6364136223846793005 + 1442695040888963407;
RETURN (state, φ[a := (state < 2147483648)])
})
(b, φ);
RETURN φ
}›
lemma rephase_random_spec:
‹rephase_random b φ ≤ SPEC(λψ. length ψ = length φ)›
unfolding rephase_random_def Let_def
apply (refine_vcg nfoldli_rule[where I = ‹λ_ _ (_, ψ). length φ = length ψ›])
apply (auto dest: in_list_in_setD)
done
definition rephase_flipped :: ‹bool list ⇒ bool list nres› where
‹rephase_flipped φ = do {
let n = length φ;
(φ) ← nfoldli [0..<n]
(λ_. True)
(λa φ. do {
ASSERT(a < length φ);
let v = φ ! a;
RETURN (φ[a := ¬v])
})
φ;
RETURN φ
}›
lemma rephase_flipped_spec:
‹rephase_flipped φ ≤ SPEC(λψ. length ψ = length φ)›
unfolding rephase_flipped_def Let_def
apply (refine_vcg nfoldli_rule[where I = ‹λ_ _ ψ. length φ = length ψ›])
apply (auto dest: in_list_in_setD)
done
definition reset_target_phase :: ‹phase_save_heur ⇒ phase_save_heur nres› where
‹reset_target_phase = (λ(φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase).
RETURN (φ, 0, target, best_assigned, best, end_of_phase, curr_phase)
)›
definition reset_best_phase :: ‹phase_save_heur ⇒ phase_save_heur nres› where
‹reset_best_phase = (λ(φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase).
RETURN (φ, target_assigned, target, 0, best, end_of_phase, curr_phase)
)›
lemma reset_target_phase_spec:
assumes ‹phase_save_heur_rel 𝒜 φ›
shows ‹reset_target_phase φ ≤ ⇓Id (SPEC(phase_save_heur_rel 𝒜))›
using assms by (cases φ) (auto simp: reset_target_phase_def phase_save_heur_rel_def)
lemma reset_best_phase_spec:
assumes ‹phase_save_heur_rel 𝒜 φ›
shows ‹reset_best_phase φ ≤ ⇓Id (SPEC(phase_save_heur_rel 𝒜))›
using assms by (cases φ) (auto simp: reset_best_phase_def phase_save_heur_rel_def)
definition current_phase_letter :: ‹64 word ⇒ 64 word› where
‹current_phase_letter curr_phase =
(if curr_phase = 0 ∨ curr_phase = 2 ∨ curr_phase = 4 ∨ curr_phase = 6
then 66
else if curr_phase = 1
then 73
else if curr_phase = 3
then 35
else if curr_phase = 5
then 79
else 70)
›
text ‹
The phases are: BOBIBF independantly of the mode of the solver unlike CaDiCaL where this is
independent and kissat where no flipping is used in unsat mode. We schedule in log interval.
In the last phase, we increase the length of the phase in \<^term>‹Θ(log 10 n*log 10 n)›.
›
definition phase_rephase :: ‹64 word ⇒ 64 word ⇒ 64 word ⇒ phase_save_heur ⇒ phase_save_heur nres› where
‹phase_rephase = (λend_of_phase lrephase (b::64 word) (φ, target_assigned, target, best_assigned, best, _, curr_phase,
length_phase).
do {
let rephaselength = (500 :: 64 word);
let target_assigned = (0::64 word);
target ← copy_phase φ target;
if curr_phase = 0 ∨ curr_phase = 2 ∨ curr_phase = 4 ∨ curr_phase = 6
then do {
φ ← copy_phase best φ;
RETURN (φ, target_assigned, target, 0, best, length_phase*rephaselength+end_of_phase, curr_phase + 1, length_phase)
}
else if curr_phase = 1
then do {
φ ← rephase_init True φ;
RETURN (φ, target_assigned, target, best_assigned, best, length_phase*rephaselength+end_of_phase, curr_phase + 1, length_phase)
}
else if curr_phase = 3
then do {
φ ← rephase_random end_of_phase φ;
RETURN (φ, target_assigned, target, best_assigned, best, length_phase*rephaselength+end_of_phase, curr_phase + 1, length_phase)
}
else if curr_phase = 5
then do {
φ ← rephase_init False φ;
RETURN (φ, target_assigned, target, best_assigned, best, length_phase*rephaselength+end_of_phase, curr_phase + 1, length_phase)
}
else do {
φ ← rephase_flipped φ;
let loglength = (if lrephase+10 > 0 then of_nat (word_log2 (lrephase+10)) else 1);
let new_length = (lrephase+1)*loglength*loglength;
RETURN (φ, target_assigned, target, best_assigned, best, new_length*rephaselength+end_of_phase, 0,
new_length)
}
})›
lemma phase_rephase_spec:
assumes ‹phase_save_heur_rel 𝒜 φ›
shows ‹phase_rephase end_of_phase lrephase b φ ≤ ⇓Id (SPEC(phase_save_heur_rel 𝒜))›
proof -
obtain φ' target_assigned target best_assigned best end_of_phase curr_phase where
φ: ‹φ = (φ', target_assigned, target, best_assigned, best, end_of_phase, curr_phase)›
by (cases φ) auto
then have [simp]: ‹length φ' = length best›
using assms by (auto simp: phase_save_heur_rel_def)
show ?thesis
using assms
unfolding phase_rephase_def
by (refine_vcg lhs_step_If rephase_init_spec[THEN order_trans]
copy_phase_spec[THEN order_trans] rephase_random_spec[THEN order_trans]
rephase_flipped_spec[THEN order_trans])
(auto simp: phase_save_heur_rel_def phase_saving_def)
qed
definition phase_save_phase :: ‹64 word ⇒ phase_save_heur ⇒ phase_save_heur nres› where
‹phase_save_phase = (λn (φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase). do {
target ← (if n > target_assigned
then copy_phase φ target else RETURN target);
target_assigned ← (if n > target_assigned
then RETURN n else RETURN target_assigned);
best ← (if n > best_assigned
then copy_phase φ best else RETURN best);
best_assigned ← (if n > best_assigned
then RETURN n else RETURN best_assigned);
RETURN (φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase)
})›
lemma phase_save_phase_spec:
assumes ‹phase_save_heur_rel 𝒜 φ›
shows ‹phase_save_phase n φ ≤ ⇓Id (SPEC(phase_save_heur_rel 𝒜))›
proof -
obtain φ' target_assigned target best_assigned best end_of_phase curr_phase where
φ: ‹φ = (φ', target_assigned, target, best_assigned, best, end_of_phase, curr_phase)›
by (cases φ) auto
then have [simp]: ‹length φ' = length best› ‹length target = length best›
using assms by (auto simp: phase_save_heur_rel_def)
have 1: ‹⇓Id (SPEC(phase_save_heur_rel 𝒜)) ≥
⇓Id((λ(φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase). do {
target ← (if n > target_assigned
then SPEC (λφ'. length φ = length φ') else RETURN target);
target_assigned ← (if n > target_assigned
then RETURN n else RETURN target_assigned);
best ← (if n > best_assigned
then SPEC (λφ'. length φ = length φ') else RETURN best);
best_assigned ← (if n > best_assigned
then RETURN n else RETURN best_assigned);
RETURN (φ', target_assigned, target, best_assigned, best, end_of_phase, curr_phase)
}) φ)›
using assms
by (auto simp: phase_save_heur_rel_def phase_saving_def RES_RETURN_RES φ RES_RES_RETURN_RES)
show ?thesis
unfolding phase_save_phase_def φ
apply (simp only: prod.case)
apply (rule order_trans)
defer
apply (rule 1)
apply (simp only: prod.case φ)
apply (refine_vcg if_mono rephase_init_spec copy_phase_spec rephase_random_spec)
apply (auto simp: phase_rephase_def)
done
qed
definition get_next_phase_pre :: ‹bool ⇒ nat ⇒ phase_save_heur ⇒ bool› where
‹get_next_phase_pre = (λuse_target_phasing L (φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase).
L < length φ ∧ L < length target)›
definition get_next_phase_stats :: ‹bool ⇒ nat ⇒ phase_save_heur ⇒ bool nres› where
‹get_next_phase_stats = (λuse_target_phasing L (φ, target_assigned, target, best_assigned, best, end_of_phase, curr_phase).
if ¬use_target_phasing then do {
ASSERT(L < length φ);
RETURN(φ ! L)
} else do {
ASSERT(L < length target);
RETURN(target ! L)
})›
end