Riot+SATで数独ソルバー

以前、ブラウザ内で動くSATソルバーを使ってパズルのソルバーを作っていましたが、じつは表示＆入力部分を作るほうが圧倒的に面倒だということもあって、しばらく放置していました。最近知ったRiotを使えば、このあたりの複雑性もなんとかなりそうだと思ったので、アルゴリズム自体に悩むことがほぼない数独で試作してみました（https://jkr2255.github.io/js_puzzle_solvers/sudoku.html）。

入力＆表示部分

今までは、「内部的な盤面データ」と「表示」を連動させる処理にてこずっていたのですが、Riotを使えば、内部用のデータを書き換えるだけで、あとは.updateすれば表示は適宜書き換えてくれます。マス目自体は<table>で適宜CSSをかけて表現しています。

ビルド方法

JavaScriptのビルドシステムをbrowserify+rakeで組んでいたのですが、Riotを加えるにあたってどうしようかなと悩みました。riotifyという手も考えたのですが、コマンドラインコンパイラのriotに-mというオプションがあって、コンパイルを行うと以下のようなコードを吐きます。

riot-m.js

(function(tagger) {
  if (typeof define === 'function' && define.amd) {
    define(function(require, exports, module) { tagger(require('riot'), require, exports, module)})
  } else if (typeof module !== 'undefined' && typeof module.exports !== 'undefined') {
    tagger(require('riot'), require, exports, module)
  } else {
    tagger(window.riot)
  }
})(function(riot, require, exports, module) {
riot.tag2('tag-name', 'html', 'css', function(opts) {
 // 略
});
});

UMD的な形となっていて、「非同期RequireJS」「CommonJS（NodeやBrowserify）」「Riotを<script>で読み込んだブラウザ環境」のいずれにも対応できます。Riotコンパイラでここまで生成して、あとはBrowserifyに投げる、という形を取りました。

なお、この形でコンパイルされると、require()しても何も返ってきません。依存関係を明示するためにrequire()だけ書いて、返り値は使わない、というちょっと見慣れない書き方となりました。

アルゴリズム

数独ならそれ専門にアルゴリズムを考えてもそこまで手間はかからないのですが、SATソルバーに丸投げすれば、本当に「数独の条件そのまま」を起こすだけで終わりです。あとは何も考えなくてもSATソルバーがすべて処理していきます。

なお、「全体で81個」ということが決まれば明らかだと、「同じ列に2個以下」など一部の条件を省略していたところ、ソルバーに3秒くらいかかってしまいました。サボらずに全部条件を開くと、数十ミリ秒まで高速化しました。

改良したい点

• 表出の数字と、ソルバーが埋めていった数字の区別
• 別解がある場合に、一意に決まる場所だけ埋めていく機能