NO_WAIT

主にプログラミング

ラテン方格と数独をSAT Solverで生成 (JavaScript logic-solver)

ラテン方格と数独をSAT Solverライブラリを使用してJavaScriptで生成してみました。 生成結果を表示する簡単な画面も作成しました。

例: ラテン方格 1
f:id:shinaisan:20171126145726p:plain

例: 数独 2
f:id:shinaisan:20171126145759p:plain

ラテン方格と数独は充足可能性問題(Boolean satisfiability problem, SAT) 3 として表現でき、SAT Solverを利用して解くことができます。

JavaScriptを使用したかったため、ここでは logic-solver4 ライブラリを選択しました。

詳細に入る前に、作成したプログラムの核心部分を示します。 雰囲気はつかめるのではと思います。

// solver: an instance of Logic.Solver where Logic is the logic-solver module.
// vars: a multi-dimensional (n x n x n) array of variable names.
// range: a utility function to make an array of integers from 1 to n.
function latinSquare(solver, vars) {
  const n = vars.length;
  range(n).forEach((i) => {
    range(n).forEach((j) => {
      solver.require(Logic.exactlyOne(range(n).map((k) => (vars[k][i][j]))));
      solver.require(Logic.exactlyOne(range(n).map((k) => (vars[i][k][j]))));
      solver.require(Logic.exactlyOne(range(n).map((k) => (vars[i][j][k]))));
    });
  });
}

function sudoku(solver, vars) {
  const n = vars.length;
  const m = Math.floor(Math.sqrt(n));
  latinSquare(solver, vars);
  range(m).forEach((i) => {
    range(m).forEach((j) => {
      range(n).forEach((k) => {
        solver.require(Logic.exactlyOne(
          range(n).map((l) => (
            vars[m*i + Math.floor(l/m)][m*j + (l%m)][k]
          ))));
      });
    });
  });
}

ソース

動作方法

動作には Node.js が必要です。下記手順でサーバーを起動します。

# Correct the following placeholders REPO and THE_DIR_OF_CLONED_REPO.
git clone $REPO
cd $THE_DIR_OF_CLONED_REPO
yarn install
yarn run start

サーバーが起動したらWebブラウザからアクセスできます。 デフォルトではポート3000を使用します。

ラテン方格のデモ(sat-latin-square)はサイズ入力用フォームを表示します。 サイズを2から6まで入力してSolveボタンを押すと、計算が開始され、 結果がフォーム下に表示されます。 解が多くなると、ブラウザが重くなるので、 表示数は制限してあります。

数独のデモ(sat-sudoku-solver)は左右に2つのグリッドを表示します。 左側には数字の初期配置を入力します。 Solveボタンを押すと右側に解の1つを(あれば)表示します。

logic-solver使用部詳細

logic-solverモジュールをLogicとして使用します。

const Logic = require('logic-solver');

論理式を構築する前に部品を用意しておきます。 range関数を数値0からn-1を配列にして返すよう定義します。 問題のサイズn回分の繰り返しが多いため、多用されます。

続いて変数名を生成する関数genVarsも定義しておきます。 これは3つの添字(r, c, s)でアクセスされる多次元配列を返します。 それぞれ行、列、記号(数字)を示すインデックスとなります。 問題のサイズをnとおくと、 次元は n x n x n となります。 (r, c)はラテン方格の1区画を指します。 つまり genVars('v', n)[r][c][s] がtrueとなるときは、その1区画に記号sが入ることを示します。

function genVars(prefix, size) {
  return range(size).map((i) => (
    range(size).map((j) => (
      range(size).map((k) => (
        [prefix, i.toString(), j.toString(), k.toString()].join('_')
      ))
    ))
  ));
}

ラテン方格を表す論理式を構築する関数latinSquareを定義します。 ラテン方格は n x n の表に n 個の異なる記号を並べたものです。 下記の論理積として表現します。

  • 各記号は各列に1回だけ使用される。
  • 各記号は各行に1回だけ使用される。
  • 表中の各区画には1つの記号が使用される。

関数exactlyOneが上の各条件を記述するのに使えます。 これは与えられた変数のうち1つだけがtrueとなることを要請する 論理式を返します。 solverインスタンスrequireメソッドに論理式を与えていくことで、 目的の論理式に新たな条件を論理積で結合していきます。

// vars = genVars('v', n)
function latinSquare(solver, vars) {
  const n = vars.length;
  range(n).forEach((i) => {
    range(n).forEach((j) => {
      solver.require(Logic.exactlyOne(range(n).map((k) => (vars[k][i][j]))));
      solver.require(Logic.exactlyOne(range(n).map((k) => (vars[i][k][j]))));
      solver.require(Logic.exactlyOne(range(n).map((k) => (vars[i][j][k]))));
    });
  });
}

数独は、ラテン方格の条件をもとに、 次の条件を追加して表します。

  • サイズm x m のブロックがn個あり(m x m = n)、それぞれについて各記号が1回だけ使用される。
function sudoku(solver, vars) {
  const n = vars.length;
  const m = Math.floor(Math.sqrt(n));
  latinSquare(solver, vars);
  range(m).forEach((i) => {
    range(m).forEach((j) => {
      range(n).forEach((k) => {
        solver.require(Logic.exactlyOne(
          range(n).map((l) => (
            vars[m*i + Math.floor(l/m)][m*j + (l%m)][k]
          ))));
      });
    });
  });
}

問題を解くには、例えば数独の場合次のようなコードとなります。

    const n = 9;
    const solver = new Logic.Solver();
    sudoku(solver, genVars('v', n));
    const solution = solver.solve();

解がない場合、solutionnullとなります。 この事実を利用して、solve()メソッドを nullが返るまで繰り返し、 すべての解を得ることができます。

変数への真理値の割り当てはsolution.getMap()により得られます。 このメソッドは、変数名をキー、真理値を対応する値とする辞書を返します。

所感

複雑そうに見えたラテン方格や数独があっさり記述できてしまい、 SAT Solverを遊び以外の用途で使用してみたいという 動機付けになりました。

興味深い技術であり、アルゴリズムなどの詳細も 調査するとなかなか奥が深そうです。 深入りする時間が取れそうにありませんが…

参考

英語版記事