以前数独のソルバーを作ったことがあったが、今度はカックロのソルバーを作ってみた。
カックロとは？
カックロは縦横のマスの合計が指定どおりになるように１から９の数値を配置するという、ニコリの定番ペンシルパズル。 また並び内では数値は重複しないという制約がある。
ソルバーの方針
パズルを解くプログラムを作るにはルールを基に解くためのアルゴリズムを考案する必要がある。 しかしパズルの種類ごとにアルゴリズムを考えるのは結構大変。 そこでSATソルバーを使う。
SATソルバー
SATソルバーは真偽値を持つ変数に対して、制約を満たす組合せを解くことができる。 以前の数独を解く際には各マスに対して、１が入るか、２が入るか、…という具合に真偽値の変数を9つ用意して、条件を指定していくという方法だった。 数独ではどの数値が入るかという真偽値の組み合わせで解けるため素のSATソルバーを使えばよかったが、カックロでは数値の合計を扱う必要があるのでそのままだと大変そうだ。
今回はJavaScript/NPMのLogic Solverというモジュールを使ってみた。 このモジュールでは単純な真偽値だけじゃなく、数値・加算、不等式も扱えるのでカックロを解くには好都合。
便利なメソッド群は以下のとおり（抜粋）：
- Nビット数値変数の作成：
variableBits - 定数の作成：
constantBits - 不等式：
lessThanOrEqualやgreaterThanOrEqualなど - 加算：
sum - 数値が等しいかどうか：
equalBits
カックロソルバー
条件は以下の通り：
- 各マスには１から９のどれかが入る
- 並びの合計が指定の値になる
- 並びには同じ数値は入らない
と、ルールをほぼそのまま記述するだけ。 あとは問題のテキストフォーマットの読み込み、並びの列挙、解の表示を作ってやれば出来上がり。
Logic Solverがどう処理しているか？
Logic Solverで真偽値だけじゃなくて数値や加算、不等式なども扱うのはどうやっているのか？ 実際のCPUが論理ゲートから構成されているように、Logic Solverも加算などの高レベルな処理を論理式で構築している （ソース）。
ソルバー自体はMiniSatをEmpscriptenしてJavaScriptで動かしているとのこと。