as a SAT solver's preprocessor
Vivification がなんなのか、日本語で探しても出てこないので以下の論文をまとめてみた。 （最新の話かと思っていたけど2008年とは。。。）
- C. Piette, Y. Hamadi, and L. Saïs, "Vivifying propositional clausal formulae,” Front. Artif. Intell. Appl., vol. 178, pp. 525–529, 2008.
Splr でいうところの processor が節数に対する制約内での網羅的な変数除去と節包摂(clause subsumption)とを実行するのに対し、vivification は（その節に「対応」する割り当てを仮定して）propagateを行った結果を用いて節の包摂方針を決めるというもの。 節長を減らす方向でのみ置換するので、（節数の増加と引き換えに）不要な複雑さの導入を抑えることができるらしい。 効果は1割程度のようである。
ちなみに 'vivify' は論文では'shorten existing clauses'の意味で使われているが、辞書で引くと：
verb: enliven or animate: outings vivify learning for children.
とのこと。ぼやけていた制約の強化ということで、日本語になっているビビッドからも想像できる感じなんだろう。
cover image: https://images.unsplash.com/photo-1506884403171-cdb32baec15f
アルゴリズム（上記論文より引用）
- 6行目で $c$ を $\Sigma$ から削除して、30行目で戻している。しかし $\Sigma$ に対する伝播は行わないので、30行目まで残しておいても構わない。
- 20行目の解釈： 節 $c$ が存在しない $\Sigma_b$ において、リテラル $l$ に対して決定による割当てを行うと矛盾した（11行目）。しかし、学習節 $c_l$ は節 $c$ に含まれないなら（16行目）。これは矛盾は別の節集合によって生じたことを意味する。従ってこの節は冗長かもしれない。もし学習節 $c_l$ が節 $c$ より小さいなら（17行目）、これは節 $c$ より強い制約であるので $\Sigma_b$ に追加する。そして節 $c$ 自身も $\Sigma_b$ に戻した上で、節 $c$ に対する検査を終了させる（矛盾節を含む式と学習節を含む式とは充足可能性において等価である（矛盾の回避は割当て列に関する枝刈であって論理式の等価変換であることには違いない））。そうでないなら（19行目）、つまり節 $c$ （に含まれるリテラル集合）は今回の矛盾とは関係ないが今回の矛盾によって吸収できるとは言い切れない場合には、節 $c$ に含まれていたリテラル集合 $c_b$ を $\Sigma_b$ に追加し（代わりに $c$ を削除し）て節 $c$ に対する処理を終了する（より強い制約に置き換えている？？）。
- $\exists i \in {1, \cdots, n-1}; s.t.; \Sigma\backslash{c} \cup {\neg l_1, \cdots, \neg l_i} \models_{UP} \bot$
In this case, we have $\Sigma\backslash{c} \models_{UP} c'$ with $c' = (l_1 \vee \cdots \vee l_i)$. This new clause $c'$ strictly subsumes $c$. Hence, the original clause can be substituted by the new deduced one. Obviously, $c'$ is not necessarily minimally redundant modulo UP. Indeed, another ordering on the literals ${l_1, l_2, \cdots, l_i}$ might lead to an even shorter sub-clause. Thanks to a conflict analysis, the deduced sub-clause $c'$ could be shortened again leading to an even smaller sub-clause. Indeed, a new clause η can be generated by a complete traversal of the implication graph associated to $\Sigma$ and to the assignments of the literals ${\neg l_1, \cdots, \neg l_i}$. The complete traversal of the implication graph ensure that the clause η contains only literals from $c'$. Thereby, η is a sub-clause of $(l_1 \vee \cdots \vee l_i)$.
- 23, 27行目の型が合わないんだけどなあ。念のためもう一本読んでおいた方がよさそうだ。
- $A \leftarrow A \cup B$ は
A.push(B);ではなくif !A.contains(&B) { A.push(B); }であることに注意。
もう少し説明を加えるとこういう感じ。
while 不動点になるまで
for sigma中の全ての節cに対して
現在のsigmaのコピーをenvとする
cb.clear();
shortened = false;
while !shortened && c != cb // == until shorten || c == cb { .. }
c\cbから適当にリテラルlを選ぶ
cbにlを追加する
!lを割当て伝播させる
if 矛盾しているなら
その学習節をclとする
if 学習節clが元々の節cを包摂するなら
clをsigmaに追加; shortened = true;
else
if cよりclの方が節長が短いなら
clをsigmaに追加; cb = c; // これは終了条件, cは後でsigmaに追加される
if c != cb // ここがわからない
cbをsigmaに追加; shortened = true;
else
if cの残りに含まれるリテラルlsの中で、env中に含まれるものがあるなら
if cの残りがls以外のリテラルを含んでいたら
cbにlsだけを追加した節を sigma に追加; shortened = true;
if cの残りに含まれるリテラルlsの中で、env中にその反リテラルが含まれるものがあるなら
cからリテラルlsを除いてsigma に追加; shortened = true;
if shorted
sigma.remove(c);
change = true;
Splr実装案
これを何も考えずにRustで書いてみるとこんな感じだろうか。 Splr だと単位節は cdb に入れられないので CNF というよりも(asg, cdb) を持ち回るとした方が現実的かも。
/// Vivification of a given CNF formula, returning a vivified CNF formula
/// Note: `remove` used here is a non-destructive function (`Fn<T>([T]) -> Vec<T>`).
fn vivify(mut sigma: (AssginStack, ClauseDB)) {
let mut env: (AssignStack, ClauseDB);
let mut change: bool = true;
let mut shortened: bool = true;
let mut cb: Vec<Lit> = Vec::new();
let mut ci: usize;
while change {
change = false;
ci = 0;
while ci < sigma.len() {
let mut c = &mut sigma[ci];
let c_len = c.len();
ci += 1;
env = sigma.clone();
env.remove_clause(ci);
cb.clear();
shortened = false;
while !shortened && c != cb {
let cx = c.remove_items(cb);
l = select_literal(cx);
cb.push(l); // cb = cb ∪ {l};
env.add_assignment(!l); // Σb ← (Σb ∪ {¬l})
if let Some(ls) = env.propagate() { // ⊥ ∈ UP(Σb)
let learnt = conflict_analyze(); // returns a learnt clause
if learnt.iter().all(|l| c.includes(l)) { // cl ⊂ c
sigma.new_clause(learnt); // Σ ← Σ ∪ {cl}
shortened = true;
} else {
if learnt.len() == c_len {
sigma.new_clause(learnt); // Σ ← Σ ∪ {cl}
cb = c;
}
if c != cb {
sigma.new_clause(cb); // Σ ← Σ ∪ {cb}
shortened = true;
}
}
} else {
if let Some(ls) = cx.iter().find(|l| env.contains(l)) { // ∃(ls ∈ (c\cb))
if 1 < cx.len() { // (c\cb) /= {ls}
sigma.new_clause(cb.push(ls)); // Σ ← Σ ∪ {cb ∪ {ls}} ;
shortened = true;
}
}
if let Some(ls) = cx.iter().find(|l| env.contains(!l)) { // ∃(¬ls ∈ (c\cb))
sigma.new_clause(c.remove(ls)); // Σ ← Σ ∪ {c\{ls}}
shortened = true;
}
}
if shortened {
sigma.kill(c);
change = true;
}
}
}
}
// return sigma;
}
2020-06-23
AssignStack や ClauseDB のコピーはコストが大きいので $\Sigma$ だけで対応したい。
- $\Sigma$ と
envの違いは$l$の割り当てをもつかどうか。これは割り当てをキャンセルできればいいはず。 - 内側のwhile文中で $\Sigma$ に対して節や割り当てを追加しているので、これを遅延させる。
assign,conflict_analysis,cancel_untilを呼び出すので変数および節の活性度が影響を受ける。どうしたものか。
fn vivify(mut sigma: (AssginStack, ClauseDB)) {
let mut change: bool = true;
while change {
change = false;
let mut ci: usize = 0;
let mut clauses: Vec<Vec<Lit>> = Vec::new();
while ci < sigma.len() {
let mut c = &mut sigma[ci];
let c_lits = c.lits.clone();
let c_len = c.len();
let dl = sigma.decision_level();
i += 1;
sigma.remove_clause(ci);
let mut cb: Vec<Lit> = Vec::new();
let mut shortened = false;
while !shortened && c != cb {
let cx = c.remove_items(cb);
l = select_literal(cx);
cb.push(l); // cb = cb ∪ {l};
sigma.assign_by_decision(!l); // Σb ← (Σb ∪ {¬l})
if let Some(ls) = sigma.propagate() { // ⊥ ∈ UP(Σb)
let learnt = conflict_analyze(); // returns a learnt clause
if learnt.iter().all(|l| c.includes(l)) { // cl ⊂ c
clauses.push(learnt); // MODIFIED: Σ ← Σ ∪ {cl}
shortened = true;
} else {
if learnt.len() == c_len {
clauses.push(learnt); // MODIFIED: Σ ← Σ ∪ {cl}
cb = c;
}
if c != cb {
clauses.push(cb); // MODIFIED: Σ ← Σ ∪ {cb}
shortened = true;
}
}
} else {
if let Some(ls) = cx.iter().find(|l| sigma.contains(l)) { // ∃(ls ∈ (c\cb))
if 1 < cx.len() { // (c\cb) /= {ls}
clauses.push(cb.push(ls)); // MODIFIED: Σ ← Σ ∪ {cb ∪ {ls}} ;
shortened = true;
}
}
if let Some(ls) = cx.iter().find(|l| sigma.contains(!l)) { // ∃(¬ls ∈ (c\cb))
clauses.push(c.remove(ls)); // MODIFIED: Σ ← Σ ∪ {c\{ls}}
shortened = true;
}
}
if !shortened {
sigma.new_clause(c_lits);
} else {
change = true;
}
sigma.cancel_until(dl);
}
for c in &clauses {
if c.len() == 1 {
sigma.new_assignment(c[0]);
} else {
sigma.new_clause(c);
}
}
}
}
}
これでどうだろうか。実装してみなくては。
こうしてみると、統計的ソルバの手法みたい。
2020-06-24
めちゃくちゃ重い！ vivifyに10000秒くらい掛かりそうだ。 節に含まれるリテラル全てに対して伝播検査をしているのだから当然ではある。 とりあえず先頭のリテラルだけの伝播にしてみたのだが、それでも論外。 propagateで矛盾が検出されたときの依存グラフをキャッシュに残すようにするとどうだろうか。。。
conflict_analyzeのカスタムバージョンが必要 -- TODO- cidが GCで変わってしまう -- しかしこれは
shortenedの時にpurgeすればいい。 - purgeされるリテラルが多すぎてヒット率が低いのではないか -- no idea
- 矛盾が発生する場合は結果をキャッシュできるが、そうでない場合は有用ではないのでは -- うーむ
type ConflictDep = HashMap<Lit, (bool, HashSet<ClauseId>, Vec<Lit>)>
impl ConflictDep {
fn clear(&mut self, l: Lit) { ... }
fn put(&mut self, l: Lit, ...) { ... }
fn purge(&mut self, l: Lit) { ... }
}
2020-06-26
もう少し軽いキャッシュを実装してみた。 無矛盾時の処理をサボっても論理的には間違いではないので、一度調べたリテラルの伝播結果をキャッシュすると(assign $\to$ propagate $\to$ cancel_until)の一連の処理が減らせる。 とにかく網羅速度を上げなければ。
2020-06-27
vivificationはpropagateやcancel_untilなど多くの機能を流用しているが、sandbox化しなくていいだろうか。
- 各種計数カウンタは切り離すべき
- 変数活性度は取り込むべき。理由はどうであれ伝播の結果わかった統計情報なのだから。
- ただし変数活性度の計算にはいくつかのカウンタは正しく動いている（更新される）ことが必要なので、計数カウンタを止めたサンドボックスを作るよりもvivify後に増分をキャンセルすることが必要かも。
2020-06-29
アルゴリズムの理解進展。いろいろ突っ込みどころを見つけて、反映したバージョンがこちら。
- 23行目と27行目が同時に成立することはない
- 30行目はwhileの中に入れる必要はない
- キャッシュは意味がない。多くの場合すぐに
breakしているから。
fn vivify(asg: &mut AssignStack, cdb: &mut ClauseDB) {
let mut changed: bool = true;
while changed {
changed = false;
for c in &clauses {
let clits = c.lits.clone();
let mut shortened = false;
let mut new_clause: Vec<Lit> = Vec::new();
cdb.delete_clause(c);
for (i, l) in clits.iter().enumerate() {
asg.assign_by_decision(!*l);
if asg.propagate(cdb) == ⊥ {
let learnt = conflict_analyze_and_learnt(asg, cdb);
if learnt.iter().all(|l| clits.contains(l)) {
new_clause = learnt.clone();
shortened = true;
} else {
if learnt.len() < clits.len() {
asg.cancel_until(asg.root_level);
break;
}
if i < clits.len() - 1 {
new_clause = clits[..=i].to_vec();
shortened = true;
}
}
} else if let Some(ls) = clits[i + 1..].iter().find(|l| asg.assigned(**l) == Some(true)) {
if i < clits.len() - 1 {
new_clause = clits[..=i].to_vec();
new_clause.push(*ls);
shortened = true;
}
} else if let Some(ls) = clits[i + 1..].iter().find(|l| asg.assigned(!**l) == Some(true)) {
new_clause = clits.iter().copied().filter(|l| l != ls).collect::<Vec<_>>();
shortened = true;
}
asg.cancel_until(asg.root_level);
if shortened {
break;
}
}
if shortened {
if new_clause.len() == 1 {
asg.assign_at_rootlevel(new_clause[0]);
} else {
cdb.new_clause(asg, new_clause);
}
changed = true;
} else {
cdb.new_clause(asg, clits);
}
}
}
}
2020-07-01
やはり、vivification中の活性度修正はしない方がよさそうだ。確かに外乱ではある。 そして、短くなった節にはrewardを受け継がせなければ。。。
2020-07-04
cancel_untilを呼び出す場所を間違っていた。今のままだと、新しい節は空節から始まってだんだん長くなっていくのではなく、常に単位節ということになる。正しいように修正したら遅くなった。 まあ確かにヒューリスティックスとして全てのリテラルを確かめるというのはあるかもしれないが、論文通りにすべきではなかろうか。。。
2020-07-05
ベンチマークを実行してみると少しは効果がありました。 しかし、そろそろ新しい論文の方を読んで検討すべき頃合いだろう（もっと早く読めって）。 長さ的にもいい頃合いなので、項を改めて検討を続けることにします。