SAT Solver作ってみた - omochan's diary

この記事は
https://adventar.org/calendars/4520
の22日目の記事として書かれました。昨日はRisebbitさんのシークエント計算の自動証明を実装してみたでした。

夏休みなんかノリでSAT Solverを作ったんで、大変だったところとか書いておきます。

SATとは?

論理式充足問題と言います。例えば $(b_1 \rightarrow b_2) \land(b_2 \land (\lnot b_3 \lor \lnot b_1))$ を充足する変数 $b_1, b_2, b_3$ の真偽の割り当ては存在するか?みたいな感じです。この場合なら、 $b_1=false, b_2=true, b_3=true$ が条件を満たしますね。通常はCNF形式という形に変換してから解きます。上の例なら $(\lnot b_1 \lor b_2) \land (b_2) \land (\lnot b_3 \land \lnot b_1)$ となります。このように $\lor$ で結合された"節"を更に $\land$ で結合した形で表されます。全ての論理式がCNFに変換できることは示せます。

SATが解けて何か嬉しいんか?

SATは単純ゆえ高速化の技術が進歩しています。NP完全問題にかかわらず変数の数が10⁵オーダーの問題も解けるというから驚きです。解きたい問題がSATに帰着さえできれば解ける可能性があるということでもあります。実際以下のような問題で成功を収めているようです。

プランニング (SATPLAN, Blackbox) [Kautz+, 1992]
自動テストパターン生成 [Larrabee, 1992]
ジョブショップスケジューリング [Crawford+, 1994]
有界モデル検査 [Biere, 2009]
ソフトウェア検証 (Alloy) [Jackson, 2006]
書換えシステム (AProVE) [J¨urgen+, 2004]
インテル社の i7 プロセッサの検証 [Kaivola+, 2009]
Eclipse のコンポーネント間の依存解析 [Le Berre+, 2009] 
解集合プログラミング (clasp) [Gebser+, 2012]
Linux のパッケージマネージャである DNF の依存性解決
制約充足問題 (Sugar) [Tamura+, 2009]
　▶ オープンショップスケジューリング問題の未解決問題の求解[Tamura+, 2009]
　▶ パッキング配列問題の未解決問題の求解 [則武+, 2013]

まあこういうのは建前でなんかNP完全問題を解いてるってだけで興奮しませんか…?

SATの高速化技術

ベースにCDCLというアルゴリズムがあり、実装技術、経験的に良いとわかっているヒューリスティックスがたくさんあります。その中から実装したものを紹介します。詳しくは参考資料を見てください。

DPLL

簡単に言ってしまえばバックトラックアルゴリズムです。変数の真偽を決めていって、失敗したら真偽値を変えて続行という感じです。ある変数の真偽を固定した時、他の変数の真偽がどれだけ決まるか計算することを単位伝播と呼んだりします。SAT Solverで一番最初に出てきたアルゴリズムであり、CDCLの礎にもなっています。

CDCL

CDCLに関してはとてもわかりやすいスライドがあるのでこちらをご覧ください。

How a CDCL SAT solver works from Masahiro Sakai

簡単に何をやっているか説明していると、DPLLの要領で順番に真偽を決め単位伝播し、矛盾したらその原因となった割り当てを特定し、その割り当ての真偽を反転させたものを新しく追加する感じです。新しく足された節を学習節と呼びます。学習節のおかげで同じような論理式の割り当てをした時に矛盾が早期の段階で起こるようになり、効率的な探索が行えるようになります。

VSIDS

Variable State Independent Decaying Sumの略です。変数に得点をつけておき、得点の高い順番から真偽割り当てを行うようにします。Decayingとあるように、定期的に全変数の得点を割合で減らします。(0.5倍とか)

学習節の削除

CDCLを回すと大量の学習節が生まれます。それらにも序列があって、論理の肝になるやつと、ただただ(速度面で)単位伝播の邪魔になるものもあります。それらを区別するために学習節にも得点をつけ、その得点が低い順から定期的に削除するようにします。得点は真面目にやるとLBD(Literal Blocks Distance)などの方式がありますが、自分の実装ではVSIDSのようなスコアを使っています。実装が楽なんでね。

リスタート

文字通り今までの変数割り当てを解除して最初からやり直すことです。すると探索範囲が変わって今までとは違うタイプの学習節が獲得できるのではないかというアイディアです。

監視リテラル

VSIDS、学習節の削除、リスタートはヒューリスティックですが、これは実装面での改善です。
実は節の中で常に見ておく必要がある変数は2つだけです。2つ真の変数を見ておき、どちらかが偽になったら真の変数を節中で探します。もし2つ見つからなかったら、もうひとつの変数は必ず真である必要があるので真の割り当てをします。2つ見つかったら、監視中ではない方を新たに監視すればいいです。これにより単位伝播の速度がだいぶ改善されます。
これは実装が辛いです。いろんなパターンがあって結構バグりました。資料はたくさん上がってるんですが全てのパターンを網羅できているものは少なかったです。

実測

Minisatという軽実装で実用的なsat solverがあるのでそれと比較しました。

	CNFのタイプ	自作sat	Minisat
case1	数独(変数729個,節3257個)	120.6s	2.942s
case2	変数60個,節937個のUNSAT	10.82s	7.096s
case3	変数41個,節224個のSAT	4.647s	1.376s

変数が3000個とかになると、Minisatでは一瞬、自作satでは永遠に解けないみたいな問題がたくさんありました。

1sあたりのバックトラック回数	Case1	case2	case3
自作sat	$1.731 \times 10^4$	$2.586 \times 10^4$	$8.749 \times 10^4$
Minisat	$1.505 \times 10^5$	$1.345 \times 10^5$	$4.409 \times 10^5$

ちなみにcase1の数独は

9 0 0 0 0 0 1 8 0
0 0 0 4 0 0 0 0 0
7 0 0 0 0 3 0 0 0
0 4 0 1 0 0 0 0 0
0 0 0 0 8 0 0 2 0
0 3 6 0 0 0 0 0 0
0 0 0 0 2 0 0 0 0
0 0 0 6 0 0 0 0 3
0 5 0 0 0 0 4 0 0

をCNFに変換したものを使いました。0が空白マスです。一応難易度:難となっていたので難しいはず?

改善点

バックトラック回数からわかるようになんか遅い。何がボトルネックになっているのかよくわからないが特定する。制作期間中の後半ずっと考えてたんですけどわかりませんでしたね…データ構造が悪いのかな…

リスタート戦略、学習節の得点のヒューリスティックスがあんまり良くない気がするのでそこら辺を改善する。リスタート戦略に関しては実装していない可能性すらある。(!?)(4ヶ月前なので忘れてしまった)

明日はiojjooさんのゲームの話です。楽しみですね。

コード

https://github.com/omosan0627/sat_solver

参考資料

https://www.slideshare.net/sakai/satsmt
http://www-erato.ist.hokudai.ac.jp/docs/seminar/nabeshima.pdf
http://minisat.se/
超自己流！競プロ解説記事の書き方 - Mister雑記 (この記事はここの方法で書かれました)