数独を解くということ

数独を効率よく解くアルゴリズムはすでに確立されている。

あらゆる数独パズルを解く
- これを読むだけでどんな数独も、相当効率的に解けるようになる
- 以降元ネタと表記
- 実装はPython 2.5+

数独の問題も公開されている。入力形式はこれらに合わせるのがよい。

Project Euler 簡単50問
フランスの人の作った難しい95問
世界で一番難しい数独 No.1 No.2

私の数独ソルバの特徴

数独を解くプログラムをQiitaに上げるのは手習い以上の意味はない。

JavaScript(ES6+) + Ramda で実装
- Ramdaの関数を駆使し、簡潔さと可読性を重要視
- 80行
アルゴリズムは元ネタを踏襲
- 制約伝播
- 探索（バックトラック）
- ユニットのデータ構造が少し違う

世界一難しい数独でも 1秒もかからずに解ける。

> const q = '85...24..72......9..4.........1.7..23.5...9...4...........8..7..17..........36.4.'
> console.log(search(load(q)).join(''))
859612437723854169164379528986147352375268914241593786432981675617425893598736241
859612437723854169164379528986147352375268914241593786432981675617425893598736241

コード概要

以下、Ramda のインポートを前提とする。

const R = require('ramda')

01. ユニットとピア

1..9 が重複なく収まる部分をユニットと呼ぶ。横に9個、縦に9個、正方形状に9個、合わせて27個のユニットが存在する。

横に相当する9個のユニットは、R.splitEveryを使って生成しよう。

> R.splitEvery(9, R.range(0, 81));
[ [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ],
  [ 9, 10, 11, 12, 13, 14, 15, 16, 17 ],
  [ 18, 19, 20, 21, 22, 23, 24, 25, 26 ],
...

縦に相当するユニットは、9で割った余りでグルーピングして生成。

>  Object.values(R.groupBy(R.flip(R.modulo)(9))(R.range(0, 81)));
[ [ 0, 9, 18, 27, 36, 45, 54, 63, 72 ],
  [ 1, 10, 19, 28, 37, 46, 55, 64, 73 ],
  [ 2, 11, 20, 29, 38, 47, 56, 65, 74 ],
...

正方形状のユニットは、少し力任せにこんな感じで作る。

> const baseBox = n => [n, n+1, n+2, n+9, n+10, n+11, n+18, n+19, n+20];
> [0,3,6,27,30,33,54,57,60].map(baseBox);
[ [ 0, 1, 2, 9, 10, 11, 18, 19, 20 ],
  [ 3, 4, 5, 12, 13, 14, 21, 22, 23 ],
  [ 6, 7, 8, 15, 16, 17, 24, 25, 26 ],
...

以上で計 27個のユニットを作ることができる。

マスの位置を指定した際に、そのマスと同じ数字が入らないマスの集合が定義できる。これをピアと呼ぶ。1マスにつき、ピアの数は20個である。（縦に8個、横に8個、同じBOXで4個）。マスの位置を指定した際にすぐにピア一覧を得れるようにしておくことは有用である。ピアは、ユニットから簡単に生成できる。

> peer[0]
[ 1, 2, 3, 4, 5, 6, 7, 8, 9, 18, 27, 36, 45, 54, 63, 72, 10, 11, 19, 20 ]

ユニットとピアを構成するコード例を示す。

const unit1 = R.splitEvery(9, R.range(0, 81));
const unit2 = Object.values(R.groupBy(R.flip(R.modulo)(9))(R.range(0, 81)));
const baseBox = n => [n, n+1, n+2, n+9, n+10, n+11, n+18, n+19, n+20];
const unit3 = [0,3,6,27,30,33,54,57,60].map(baseBox);
const units = [...unit1, ...unit2, ...unit3];
const peers = R.range(0, 81).map((i) => {
  const myUnits = units.filter(u => u.includes(i));
  return R.uniq(R.flatten(myUnits)).filter(n => n !== i);
});

02. バリュー

数独をやっていれば何となく気づくが、「このマスに入る値の候補」という概念が非常に大事になってくる。これをバリューと呼ぶ。

この概念を使うと、以下のように翻訳ができる。

「ゲームのクリア」⇔ 「全てのマスのバリューが単一の値になる」
「矛盾の発生」⇔「一つ以上のマスのバリューがカラになる」
「値の確定」⇔「確定値以外の値をバリューから消しこむ」
「初期状態（データロード前）」⇔「全てのマスのバリューが 123456789 」

本稿では、バリューとして最大9文字の文字列を使う。全てのマスのバリューは、サイズ81のリストで実装し、values という変数を使う。

const initValues = R.range(0, 81).map(() => '123456789');

03. 代入、消しこみ、制約伝播

「マスに値を代入する(assign) 」という操作は、本質的にはバリューの値の消しこみ(eliminate)である。例えば、マス 12 のバリューが values[12] === '345' という状態であったとして、マス 12の値を 3を代入するということは、3以外の候補をなくす、すなわち、 eliminate(12, 4, values); eliminate(12, 5, values); という操作と同等である。よって以下では、より一般に、バリューの消しこみ操作について考える。

さて、バリューの消しこみは、他のマスのバリューの変化を誘発する。

誘発パターン1 消しこみ ⇒ 値の確定 ⇒ ピアのバリュー消しこみ

消しこみによってバリューが単一値になる場合、値は確定される。値が確定すれば、ピアのバリューを消しこむことができる。この消しこみが、もしかしたら、別のピアの値の確定を引き起こし、さらにその先のピアのバリュー消しこみを誘発するかもしれない。このように値が確定すると、芋づる式に値が確定されることがある。例：「このマスには8は入らないな。3 か 8が候補だから、3に確定。ってことは同じ列にあるこっちのマスには3が入らないな」

誘発パターン2 消しこみ ⇒ ユニット制約による別マスにおける値の確定

消しこみによってマス s に値 val を入れない場合、s を含むユニットのうち、s 以外のどこかのマスが val を引き受けなければならない。もしユニット内に引き受け可能なマスが 1つしかない場合、そのマスの値が val に確定する。「このマスには4は入らないなー、じゃあ縦の列をみて4 が入りそうなマスはあるかなー？一個だけあった！じゃあこのマスが4に確定！」

この辺をコード化するとこのようになる。assign と eliminate が循環的に定義されていてややこしい。

// assign() can fail when contradiction occurs
const assign = (pos, val, values) => {
  if (!values) return false;
  return R.reduce(
    (acc, x) => (acc ? eliminate(pos, x, acc) : R.reduced(false)),
    values,
    values[pos].replace(val, ''), // loop for other candicates.
  );
};
// eliminate() can fail when contradiction occurs
const eliminate = (pos, val, values) => {
  if (!values) return false;
  if (!values[pos].includes(val)) return values; // do nothing when already done.
  let work = R.clone(values);
  work[pos] = work[pos].replace(val, ''); // do eliminate
  if (work[pos].length === 0) return false; // check contradictions.
  // check if something will be triggered.
  if (work[pos].length === 1) { // pattern 1
    const fixed = work[pos];
    for (const peer of peers[pos]) {
      work = eliminate(peer, fixed, work);
      if (!work) return false;
    }
  }
  for (const unit of units) { // pattern 2
    const places = unit.filter(s => work[s].includes(val));
    if (places.length === 0) return false;
    if (places.length !== 1) continue;
    work = assign(places[0], val, work);
    if (!work) return false;
  }
  return work;
};

assign も eliminate も失敗した際には false を返す。失敗するとは、値の代入や消しこみを続けているうちに矛盾（＝どれかのマスのバリューが空になってしまう）が発生した場合である。

04. 初期盤面ロード

初期盤面のロードとは、各マスに値を割り当てるという操作である。したがって前節の議論＝データの代入に帰着させることが出来る。

const load = (str) => {
  let values = R.range(0, 81).map(() => '123456789');
  const parsed = [...str].filter(x => [...'.0123456789'].includes(x));
  assert(parsed.length === 81);
  for (const [i, val] of parsed.entries()) {
    if (val === '0' || val === '.') continue;
    values = assign(i, val, values);
    if (!values) return false;
  }
  return values;
};

05. バックトラック

データロード、それに伴うバリューの変化が一息つくと、あとはバックトラックで解くしかない。バリューの値が小さいマスを選ぶことで成功率をあげる工夫をしながらバックトラックをしよう。

const findMinValuesPosition = (values) => {
  const arr = values.map((val, i) => [i, val.length]).filter(x => x[1] > 1);
  arr.sort((a, b) => a[1] - b[1]);
  return arr[0][0];
};

const search = (values) => {
  if (!values) return false; // failed last time.
  if (R.all(v => v.length === 1)(values)) return values; // solved!
  const pos = findMinValuesPosition(values);
  for (const val of values[pos]) {
    const ret = search(assign(pos, val, values));
    if (ret) return ret;
  }
  return false;
};

コード

sdk.js

const R = require('ramda');
const assert = require('assert');

// construct unit and peers
const unit1 = R.splitEvery(9, R.range(0, 81));
const unit2 = Object.values(R.groupBy(R.flip(R.modulo)(9))(R.range(0, 81)));
const baseBox = n => [n, n+1, n+2, n+9, n+10, n+11, n+18, n+19, n+20];
const unit3 = [0,3,6,27,30,33,54,57,60].map(baseBox);
const units = [...unit1, ...unit2, ...unit3];
const peers = R.range(0, 81).map((i) => {
  const myUnits = units.filter(u => u.includes(i));
  return R.uniq(R.flatten(myUnits)).filter(n => n !== i);
});
// assign() can fail when contradiction occurs
const assign = (pos, val, values) => {
  if (!values) return false;
  return R.reduce(
    (acc, x) => (acc ? eliminate(pos, x, acc) : R.reduced(false)),
    values,
    values[pos].replace(val, ''), // loop for other candicates.
  );
};
// eliminate() can fail when contradiction occurs
const eliminate = (pos, val, values) => {
  if (!values) return false;
  if (!values[pos].includes(val)) return values; // do nothing when already done.
  let work = R.clone(values);
  work[pos] = work[pos].replace(val, ''); // do eliminate
  if (work[pos].length === 0) return false; // check contradictions.
  // check if something will be triggered.
  if (work[pos].length === 1) { // pattern 1
    const fixed = work[pos];
    for (const peer of peers[pos]) {
      work = eliminate(peer, fixed, work);
      if (!work) return false;
    }
  }
  for (const unit of units) { // pattern 2
    const places = unit.filter(s => work[s].includes(val));
    if (places.length === 0) return false;
    if (places.length !== 1) continue;
    work = assign(places[0], val, work);
    if (!work) return false;
  }
  return work;
};
const load = (str) => {
  let values = R.range(0, 81).map(() => '123456789');
  const parsed = [...str].filter(x => [...'.0123456789'].includes(x));
  assert(parsed.length === 81);
  for (const [i, val] of parsed.entries()) {
    if (val === '0' || val === '.') continue;
    values = assign(i, val, values);
    if (!values) return false;
  }
  return values;
};


const findMinValuesPosition = (values) => {
  const arr = values.map((val, i) => [i, val.length]).filter(x => x[1] > 1);
  arr.sort((a, b) => a[1] - b[1]);
  return arr[0][0];
};

const search = (values) => {
  if (!values) return false; // failed last time.
  if (R.all(v => v.length === 1)(values)) return values; // solved!
  const pos = findMinValuesPosition(values);
  for (const val of values[pos]) {
    const ret = search(assign(pos, val, values));
    if (ret) return ret;
  }
  return false;
};

const show = v => R.splitEvery(9, v).join('\n');

module.exports = { load, show, search };

main.js

const { load, search } = require('./sdk.js');
const fs = require('fs');

// solve hardest problem
console.log('solve hardest puzzles');
const hardest = [
  '85...24..72......9..4.........1.7..23.5...9...4...........8..7..17..........36.4.',
  '..53.....8......2..7..1.5..4....53...1..7...6..32...8..6.5....9..4....3......97..',
];
for (const q of hardest) {
  console.log(search(load(q)).join(''));
}

// solve easy problem
console.log('solve easy puzzles');
const easy = fs.readFileSync('easy.txt',{encoding:'utf-8'}).split(/Grid\s\d\d/);
easy.shift(); // first line is not a question.
for (const q of easy) {
  console.log(search(load(q)).join(''));
}

// solve hard problem
console.log('solve hard puzzles');
const hard = fs.readFileSync('hard.txt',{encoding:'utf-8'}).split(/\n/);
hard.pop(); // last line is not a question
for (const q of hard) {
  console.log(search(load(q)).join(''));
}

数独 JavaScript with Ramda