彼女(SATソルバ)を実装しました

はじめに

この記事は IPFactory Advent Calendar 2020 の11日目の分です．

WIPです．とりあえず途中だけど公開はしておきます．

昨日はmorioka12によるセキュリティ視点からのJWT入門でした．

明日はy0d3nによる WordPressをハックしてみる です．

WebSec勢に挟まれていますが，自分のスタイルを貫きます．

経緯

彼女の紹介をする前に，経緯を書きたいと思います．

アドカレに書くネタが思いつかなかった時，去年の IPFactory Advent Calendar 2019 を読んでいると，前後編に渡るナンプレをPythonで解くを書いたpycysが一番記事数が多いのがわかります．

今年の弊サークルのメンバーは調子が悪いのか，あまり埋まりが良くなかったので自分が最多となってしまっています．

せっかくなので自分もナンプレを解いて記事を書こうと決めました．

しかし，実はナンプレなんて人力でもほぼ解いた事はありませんでした．

そんな中，いらないリポジトリを消そうと自分のGitHubを周回していると，SATソルバを実装しようとしてREADMEだけ書いてあるリポジトリを見つけした．

ナンプレ(数独)は充足可能性問題であることが一般的に知られており，それは即ち彼女に解いてもらえるという事です．

というわけで，ここからは私が実装した彼女について説明します．

Simple SAT Solver by Rust

SATソルバをRustで実装してみました．

リポジトリはここ

リポジトリを作ったのはセキュキャンの最中で，「実践・難読化バイナリ解析（前編・後編）」の講義を受けた際，

今まで知らなかったSATソルバの使い道を知り，「せっかくだから実装したい」と勢いだけでリポジトリまで作ったものの，コードは一切書いていませんでした．

SAT Solverとは

そもそも「SATソルバとは何か」

この説明については，自分は論理学的な知識に乏しいので，先にわかりやすい資料を共有しておきます．

以上の資料を読めば，「数独が充足可能性問題である」点も理解できると思います．

一応，自分の言葉でも説明しておくと

SATソルバとは，その名の通り充足可能性問題(SAT)を解いてくれるプログラムです．

先程のバイナリ解析の中での用法を例に説明すると，

例えばa, b, c, d, eというbool型の変数があるとき，

if (a || b) && c && (d || e) && !b {

の様な条件式を満たす変数の組み合わせが存在するのか教えてくれます．

難読化されたバイナリの中では，「実際には絶対に通る事のない分岐」が埋め込まれている事があり，その判断の為にSATソルバが使われるという事です．

今回実装した彼女はDIMACS CNFというフォーマットで充足可能性問題を受け取り，satisfiableかそうでないか，もしsatisfiableであればどんな組み合わせの場合かを教えてくれます．いい彼女を作りました．

DIMACS CNF

DIMACS CNFは，(a || b) && c && (d || e) && !bのような論理式(これは既にCNF(連言標準形)というフォーマットを満たしています．CNFについてはちょっと説明が長くなるし論理学的な話なので省きます)を記述する方法で，

a OR bの様な，ANDで区切られた節毎に記述し，0で区切ります．

各命題変数を数字で記述し，論理否定する場合は-を付けます．

こんな感じ

c test (x1 ∨ z2) ∧ x3 ∧ (x4 ∨ x5) ∧ ¬x2
p cnf 5 4
1 2 0
3 0
4 5 0
-2 0

cで始まる行はコメントで，pはproblemのp．problemにはスペース区切りで

を記述します．

実装

SATソルバの実装難易度はそのアルゴリズムに依存すると考えています．

全探索を実装するだけでもSATソルバとしては機能します．

しかし，変数が増えると当然時間が増えるので，やはり世の中にあるSATソルバは他のアルゴリズムを採用しているものがほとんどです．

例えばDPLLとか，CDCLとか．

さて，コードを書き始めたのは水曜日．「アドベントカレンダーの12/24の枠を譲ってくれないか」とwa1m3im先輩に言われた後です．

彼女がいる人のクリスマスイブの予定を奪えるとなれば，これ程嬉しい事は無いので急いで実装を進めました．

とりあえず動くものを作るという方針のもと，全探索で実装しました．

全探索するコード書いた時，「これ天才じゃね?」って実装したんですが，これはいわゆる「bit全探索」というアルゴリズムだったらしく，「う〜ん，アルゴリズムの知識」って感じでした．う〜ん．

DIMACS CNFのパースはdimacs使うと一瞬でできます．ありがてぇ．おかげで合計150行くらいで実装できた．

挙動

彼女の挙動を説明します．

例として，先程の例で書いた(a || b) && c && (d || e) && !bという式をDIMACS CNFのフォーマットに落とし込んだファイルを与えます．

c test (x1 ∨ z2) ∧ x3 ∧ (x4 ∨ x5) ∧ ¬x2
p cnf 5 4
1 2 0
3 0
4 5 0
-2 0

彼女はこのファイルを受け取ると，

This is satisfiable when 1, -2, 3, 4, -5,
This is satisfiable when 1, -2, 3, -4, 5,
This is satisfiable when 1, -2, 3, 4, 5,

みたいな出力をしてくれます．可愛い．

今のところ彼女は親切心から充足する条件を全て列挙してくれていますが，SATソルバとしてはその必要は無く，一でも見つければその時点で終了しても構いません．

強化

彼女を作るだけなら以上で満たせています．

しかし，せっかく作った彼女です．もっと可愛くしたい．

今の彼女の問題点を説明するのは憚られるので，こちらを見て下さい．

要は遅い．

ユーフォ見て泣きながら勢いだけでガーッと書いたので，設計が雑すぎて，この上にDPLLを実装し辛い気がします．

一回彼女と別れて新しく作り直そうと思うので，WIPって訳です．

DPLL

DPLLとはどういうアルゴリズムかというと，命題論理式に対していくつかのルールを再帰的に適用していき，命題変数や節を削減していくものです．

One Literal Rule

あるリテラルL一つしか含まない節がある時はそのリテラルを充足し，他の節の否定リテラル¬Lを削除していく．

上の操作を再帰的に繰り返す．

例えば，

c (a ∨ b) ∧ (a ∨ ¬c) ∧ (c) ∧ (¬b ∨ c)
p cnf 3 4
1 2 0
1 -3 0
3 0
-2 3 0

のような充足可能性問題を解く時，

最初に3 0の節を見ると3は真に確定する．

すると，同じく3を含む-2 3 0の節は充足するので考慮する必要がなくなる．

そして，-3を含む1 -3 0の節からは-3を削除でき，1 0に変化する．

するとその節はリテラルを一つしか持たないので同じ規則が適用でき，1は真に確定する．

再帰的に適用していくと，この問題は1, 3が真であれば2に関係なく常に充足することがわかる．

Pure Literal Rule

問題中に，否定か肯定の一方しか現れないリテラルがあれば，そのリテラルを含む節を削除できる．

例えば，

c (a ∨ b) ∧ (a ∨ ¬c) ∧ (c) ∧ (¬b ∨ c)
p cnf 3 4
1 2 0
1 -3 0
3 0
-2 3 0

先程と同じ充足可能性問題を解く時，

1は真の一方しか現れない．

即ち，1を真と仮定した時，他の節への影響は無いので1を真と確定してもよい．

よって，1を含む節は削除できる．

Spliting Rule

上二つのルールを適用しても節を減らせなかった時はこのルールを適用する．

真偽両方含むリテラルについて，真の場合と偽の場合に分割する．

2つに分けた上で，さらに他のルールを適用していく．

これらの繰り返しによって，充足可能性問題を解いていく

数独を彼女に解かせる

数独をSATソルバで解く方法については，SAT ソルバで数独を解く方法を参照してください．

例にならって，簡単のため4x4にしましょう．

4^3で64変数です．

しかし，今の彼女は全探索しているのでいつまでかかるかわかったもんじゃありません．

彼女が解いている間に別の彼女を実装するので，そちらの用意ができたら今の彼女は用無しです．

WIP

現在実装中です．ユーフォに集中したいので遅れます．