魔術師見習いのノート

数独

数独は「数字は独身に限る」という名前に由来するペンシルパズルの1つである．

数独のルールはラテン方陣の応用である．ラテン方陣とは，各行と各列にそれぞれ1からnの整数が1回だけ出てくるn×nの行列である．数独はさらに小行列を持つ(必ずしも小行列とは限らないが)．小行列はn個の要素を持ち，1からnの整数を1つずつ含む．

数独のルールは次の4種類から成る．この記事では，nの値を4として説明する．

数独の解は，これらの全てを満たす．

各マス(要素)のルール

• 1つのマスに1から4の整数が入る．
• 各行の各列の各マスには値が1つだけ入る．

各行のルール

各行各のマスには，各値は1度だけ現れる．

各列のルール

各列の各マスには，各値は1度だけ現れる．

小行列のルール

各小行列の各マスには，各値は1度だけ現れる．

結論からいうと，各行と列，小行列のルールと，各マスのルールの後者は，皆似たような記述で表現できる．そこで，各マス(要素)のルールの2つを代表として説明し，残りのルールについては各マスのルールの後者との差異だけを紹介する．まずこのルールを命題を用いていくつかの言語で示す．

• 日本語(自然言語)
• 述語論理
• 命題論理
• 命題論理(CNF)
• 命題論理(DIMACS CNF形式)

日本語(自然言語)の場合

命題には，次のようなものを使用する．

1行目の1列目のマスを考えた時，それを表す命題は次のように表現できる．

1. 1行目の1列目のマスの値は1である．
2. 1行目の1列目のマスの値は2である．
3. 1行目の1列目のマスの値は3である．
4. 1行目の1列目のマスの値は4である．

• "1行目の1列目のマスの値は1"または"1行目の1列目のマスの値は2"または"1行目の1列目のマスの値は3"または"1行目の1列目のマスの値は4"である．

次に，もう1つの各マスのルール「各行の各列の各マスには値が1つだけ入る．」について説明する．そして「各行の各列の各マスには値が1つだけ入る．」というルールは，前述の各命題を参考にすると，次のように記述できる．

• "1行目の1列目のマスの値は1"または"1行目の1列目のマスの値は2"または"1行目の1列目のマスの値は3"または"1行目の1列目のマスの値は4"である．
• "1行目の1列目のマスの値が1"ならば，"1行目の1列目のマスの値は2"か"1行目の1列目のマスの値は3"か"1行目の1列目のマスの値は4"でない．
• "1行目の1列目のマスの値が2"ならば，"1行目の1列目のマスの値は1"か"1行目の1列目のマスの値は3"か"1行目の1列目のマスの値は4"でない．
• "1行目の1列目のマスの値が3"ならば，"1行目の1列目のマスの値は1"か"1行目の1列目のマスの値は2"か"1行目の1列目のマスの値は4"でない．
• "1行目の1列目のマスの値が4"ならば，"1行目の1列目のマスの値は1"か"1行目の1列目のマスの値は2"か"1行目の1列目のマスの値は3"でない．

述語論理の場合 Part.1

前述の日本語で示した表現を今度は述語論理で表現する． ここでは，次のような記号を使用する．

補助記号: ( ) ,
論理記号: ∨ ∧ ¬ ⇒
対象変数: i j k

Cell(i,j,k): i行目のj列目の値がkである．

「1つのマスに1から4の整数が入る．」

Cell(1,1,1)∨Cell(1,1,2)∨Cell(1,1,3)∨Cell(1,1,4)∧

「各マスには整数が1つだけ入る．」

(Cell(1,1,1)⇒¬(Cell(1,1,2)∨Cell(1,1,3)∨Cell(1,1,4)))∧
(Cell(1,1,2)⇒¬(Cell(1,1,1)∨Cell(1,1,3)∨Cell(1,1,4)))∧
(Cell(1,1,3)⇒¬(Cell(1,1,1)∨Cell(1,1,2)∨Cell(1,1,4)))∧
(Cell(1,1,4)⇒¬(Cell(1,1,1)∨Cell(1,1,2)∨Cell(1,1,3)))

命題論理の場合

Cell(1,1,1)，Cell(1,1,2)，Cell(1,1,3)，Cell(1,1,4)をそれぞれa,b,c,dという命題変数とした時，前述の式は次のように記述できる．

「1つのマスに1から4の整数が入る．」

a∨b∨c∨d∧

「各マスには整数が1つだけ入る．」

(a⇒¬(b∨c∨d))∧
(b⇒¬(a∨c∨d))∧
(c⇒¬(a∨b∨d))∧
(d⇒¬(a∨b∨c))

命題論理(CNF)の場合

SATソルバは，CNF式のみを受け付ける．そのため，前述の式をCNF式に変換例を示す．ただし，ここでは「a⇒¬(b∨c∨d)」をCNF式に変換する例だけを紹介する．これは，いくつかのCNF式を論理積で繋いだ式がCNF式であることに起因する．この例に限らず，論理積で結合される各式がそれぞれCNF式に変換できれば，同様のやり方でCNF式に変換できる．

a⇒¬(b∨c∨d)⇔
¬a∨¬(b∨c∨d)⇔
¬a∨(¬b∧¬c∧¬d)⇔
(¬a∨¬b)∧(¬a∨¬c)∧(¬a∨¬d)

命題論理(DIMACS CNF形式)の場合

前述のCNF式をSATソルバが読み取り可能な形式(DIMACS CNF形式)に書き換えると，このようになる．DIMACS CNF形式では，命題変数を絶対値が1以上の整数，論理否定を"-"，論理和をスペースや改行などの区切り，論理積を"0"で表す．DIMACS CNF形式の詳細については，ここでは言及しない．ここで命題変数はaを1，bを2，cを3，dを4で表す．

1 2 3 4 0
-1 -2 0
-1 -3 0
-1 -4 0
-2 -1 0
-2 -3 0
-2 -4 0
-3 -1 0
-3 -2 0
-3 -4 0
-4 -1 0
-4 -2 0
-4 -3 0

述語論理の場合 Part.2

ユーザがルール全てをタイプするのは困難である．そこで，SATソルバに与える入力ファイルを生成するプログラムを作成する．ここでは代表してマスのルールを述語論理で表す．その後，それに対応した入力データを作成するためのRubyプログラムを紹介する．

ここでは，述語記号Cellや主語を表すiとj，kは，前述と同じである．次の式は各マスのルールを表している．

補助記号: , ( ) { }
対象定数: 1 2 3 4
対象変数: i j k k'
述語記号: ∈ Cell = ≠

i∈{1,2,3,4}
j∈{1,2,3,4}
k∈{1,2,3,4}
k'∈{1,2,3,4}

∀i(∀j(∃k(Cell(i,j,k)∧∀k'((k≠k')⇒¬Cell(i,j,k')))))

命題論理(DIMACS CNF形式)式を出力するRubyプログラム

以下に前述で示した述語論理の式を出力するRubyプログラムを紹介する．ちなみにRubyである必要性はない．

s = [1, 2, 3, 4]

for i in s
  for j in s 
    for k in s
      print "#{Cell(i,j,k)} "
    end
  end
end
puts "0"

for i in s
  for j in s
    for k1 in s
      for k2 in s   
        if i != j then
          puts "#{-Cell(i,j,k1)} #{-Cell(i,j,k2)} 0"
        end
      end
    end
  end
end

その他のルール

行や列，小行列の場合も同じような考え方である．以下に，数独の全てのルールを述語論理で示す．なお，述語記号の意味は前述と同じである．ここで，「∃k(Cell(i,j,k)∧∀k'((k≠k')⇒¬Cell(i,j,k'))」を∃!と省略する．

補助記号: , ( ) { } |
対象定数: 1 2 3 4
対象変数: a b i j k l 
関数記号: ∃! + -
述語記号: ∈ Cell ≦ 


i,j,k∈{1,2,3,4}
a,b∈{1,2}
l∈{x∈Z|2a-1≦x≦2a}
c∈{x∈Z|2b-1≦x≦2b}

∀i∀j∃!k Cell(i,j,k)
∀i∀k∃!j Cell(i,j,k)
∀j∀k∃!i Cell(i,j,k)
∀a∀b∀l∀c∃!k Cell(l,c,k)

このように他のルールに関しても同じように記述できる．それゆえ，入力ファイルを生成するためのプログラムも要領は同じである．

非共通ルール

一般的な数独の問題では，いくつかのマスの値が始めから決まっている．これらを命題論理の式で示すのは難しくない．

... ∧
Cell(1,1,1)∧
Cell(4,4,1)

この論理式はCNF式である．それゆえ共通ルールと非共通ルールの両方を満たす論理式もまたCNF式である．

命題変数と命題の相互変換

SATソルバで解法を行うためには，命題と命題変数を対応付ける必要がある．数独の場合，行番号と列番号，マスの値から命題変数へ命題変数から行番号と列番号，マスの値への変換ができれば，それが可能となる．

例えば，Cell(1,1,1)が命題変数1に，Cell(4,4,1)が命題変数61に対応する時(解があれば)，次のようなファイルが出力される．

SAT
1 -2 -3 -4 ... 61 -62 -63 -64 0

その他のパズル

最後に特殊な数独と数独以外のパズルを紹介しているサイトを示す．

• Killer Sudoku
• ニコリ