DPLL SAT Solver を自作した

というわけで。（どんなわけで）

DPLL アルゴリズムを使った SAT Solver を自作した。

kazuk/pico-sat

DIMACS とかその辺のサポートをしてない非常に素朴な実装。

SAT Solver に対しての入力になる論理式をこねくり回すロジックは現状実装途中の書きかけ。

DPLL アルゴリズム

世の中のSATソルバーの殆どはこのアルゴリズムないし、その改善型を使っているらしいので利用アルゴリズムとして選定した。

• DPLLアルゴリズム

DPLLアルゴリズムの実装は rust で「素朴」に書くぶんには 200LoC以下に収まるサイズで実装できた。VecとHashSetにほぼほぼ必要な物はあるので組み合わせるだけである。

現状実装では再帰を使っているので問題の規模によってはスタックオーバーフローで落ちるだろうし、複数スレッド化したりメモリ利用を抑え込んだり効率的なバックトラックをしようとするとドンドンデカくなるのは容易に想像が付くのであくまで「素朴」な実装での規模感である。

特に工夫のない DPLL SAT Solver なので現状では「なんの工夫もされてないオンボロの性能」のプロファイリングリファレンスとしてしか使えないと思う。

DPLLアルゴリズムには、２点ヒューリスティックな部分があり、そこにどんな方針を立てて実装しているかは以下

• 分割規則の適用時における分割位置の選択

  分割規則の適用時には、分割位置として選択したリテラルがすべて消えるこのため「消えるのが多い方が嬉しいはず」という事で出現回数が最も多い変数を分割位置として選定している。

• 分割規則で分割後に分割で利用した変数を真と仮定した枝と、偽と仮定した枝のどちらを優先して探索するか

  単一の解答が欲しい solve_one では SAT / UNSATどちらにしても「小さい枝を処理した方が答えが早くでるだろう」という事で小さい枝を優先して探索するようにしている。 すべての解答が欲しい solve_all ではどっちにしても両方処理するので真、偽の順で固定している。

論理式の連言標準形への変換

SAT Solver の入力となる論理式は、連言標準形である必要があり、連言標準形は和積標準形のため、式の木構造としては以下のような構造になる必要がある。

- OR
   - AND
      - 変項
      - NOT 変項

この様な論理式を利用するアプリケーションが直接作り出すのは結構厄介なのは目に見えているので、割と普通の論理式の形で入力ができるようにしたい。

現状実装途中なので、方針が変わる可能性はあるが、以下が現状の実装方針。

Not 配下の OR、Not 配下の AND のノードに対してド・モルガンの法則を適用すると OR が Not AND Not の形になり、ANDの上のNot は元々存在した Not と二重否定になり消え Not が一つ下の階層に移動する。これを繰り返し適用すると、最下層に変項ないし、Not変項が配置される。

And 配下に Or がある項に分配法則を適用して、Or 配下に And がある状態に変換し Or-Or , And-And を押しつぶすと CNF になる。

なんでこんなん作ってんの？

一言で言えば「遊び」。

現状幼稚園の息子がもうちょい育ったら、電子工作とかモーター工作の類で一緒にロボットとか作りたいなと思っている。

そうなると、制御をするソフトウェア、ソフトウェア的なドライバといったファームウェア、実際に接続される回路、回路に乗っているIC、ロボットとかならサーボを30度回すとリンク機構介してアームが何センチ動くとかの制御パラメータとか、ソフトウェアの世界に閉じていない依存性解決が必要になる。

そしてそこをちゃんとできないと、息子氏にドヤってできないお父さんになるのだ、父の威厳のためにも絶対に依存性解決したいのだ。

ソフトウェアに閉じた世界では semver とパッケージマネージャで非常に簡単になっているが、ハードウェア回路のバージョンとか物理機構の制御パラメータや、ファームウェアドライバの依存性解決っていうのは電機メーカーや自動車メーカー等の内部には当然に実用可能な仕組みはあるんだろうなーという程度で、個人趣味の電子工作や、子供が遊びでとか、小中学生でも使える物は多分現状では無い。（あったらおしえて）

ロボットパーツを買ってきたらリポジトリにつないでメタデータを取ってきてビルドすると動かせる、それが10代前半の子供にも気楽にできるような何かを作りたい。

そんな感じなので必要を感じたらで性能含めて諸々手を入れていくつもりです。

実装中に当たった問題

「解決はしていないはず」な問題のメモ。

単一スレッドで素朴に実装しているのに結果が不安定

複数の解答のある命題に solve_one を繰り返し実行すると数回に一回別解が返されるという現象を確認している。

よくよくソースを見ても HashSet 等順序保証が無さそうな物が処理順序に影響を与える様にはなっていないし、スレッドによるタイミング依存や動的確保されるメモリアドレスの影響を受けるようなコードを書いていないので完全に謎。

そのままテストに置いておくとテストがオオカミ少年化してしまうので解答が揺れる命題をテストコードに入れるのを避けたため現状でも潜伏していると思う。

他の機能の実装をして腰を据えて向き合おうという気持ちになったら追う。利用コンパイラバージョンと uname -a は以下。

kazuk:~/kazuk.log$ rustc --version
rustc 1.54.0 (a178d0322 2021-07-26)
kazuk:~/kazuk.log$ uname -a
Linux kazuk-ThinkCentre-M75q-1 5.11.0-27-generic #29~20.04.1-Ubuntu SMP Wed Aug 11 15:58:17 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux