Sudoku as a SAT Problem
数独は、9x9 のマスで構成されている。これは、3x3 の箱が 9 つあるとも表せる。マスは数字が入っているものと、そうでないものがある。
数独は、箱、行、列の中に 9 つの数字がそれぞれ 1 回ずつ現れるように埋められると、解けたことになる。
以下のどちらかの性質を持つもののみ、ここでは扱うことにする：
1. ただ1つの解法のみが存在するもの。
2. bruteforce せずに、理詰めで解けるもの。
$ n が平方数であるとき、数独は $ n \times n の大きさに一般化できる。これは NP 完全な問題である。(12)
しかし、先程の性質をもつものは多項式時間で解くことができる。
$ S_{xyz} : \mathbf{P} := x行$ y列の数字が$ zである
すでに assign された箇所はもちろん unit clause として現れる。
それぞれの割り当て、行、列、箱についての制約が SAT 問題に還元するときに考慮される。
最小限の還元でも問題を解くことはできるが、拡張された還元では冗長な制約も加えることになる。
どちらの還元でも、$ \Omicron(n^4)の大きさになる。
冗長な制約は非常に直感的なものであり、したがって拡張された還元は自然に頭の中に浮かんでくるようなものである。
最小の還元
それぞれのマスに最低でも1つの数字が入っている
それぞれの行、列、箱にそれぞれの数字が最高でも1回だけ現れる
より形式的に
1. それぞれのマスに最低でも1つの数字が入っている
$ \bigwedge^9_{x=1}\bigwedge^9_{y=1}\bigvee^9_{z=1} s_{xyz}
そうだね
2. それぞれの数字が高々1回だけ同じ列に現れる
$ \bigwedge^9_{y=1}\bigwedge^9_{z=1}\bigwedge^8_{x=1}\bigwedge^9_{i=x+1} (\lnot s_{xyz} \lor \lnot s_{iyz})
https://gyazo.com/3d3cd377d945427bcff84fa9e599196a
これらの繋がっているもの同士が別々の値であるという制約
$ \frac{1}{2}n(n-1) \cdot n \cdot n つの節が生成される
ある列について、それぞれの値同士が異なることを保証するために必要な不等号の個数 × 数字の種類（$ n） × 列の個数
3. それぞれの数字が最高でも1回だけ同じ行に現れる
$ \bigwedge^9_{x=1}\bigwedge^9_{z=1}\bigwedge^8_{y=1}\bigwedge^9_{i=y+1} (\lnot s_{xyz} \lor \lnot s_{xiz})
https://gyazo.com/d82d224960dcb47b7c99eb5ac3e71618
上のやつと同じ（列と行が逆になっただけ。添字にも注目）
4. それぞれの数字が高々1回だけ同じ箱に現れる
1. $ \bigwedge_{z=1}^9 \bigwedge_{i=0}^2 \bigwedge_{j=0}^2 \bigwedge_{x=1}^3 \bigwedge_{y=1}^3 \bigwedge_{k=y+1}^3 (\lnot s_{(3i+x)(3j+y)z} \lor \lnot s_{(3i+x)(3j+k)z})
4-1 は重複した制約を生成しない。
2. $ \bigwedge_{z=1}^9 \bigwedge_{i=0}^2 \bigwedge_{j=0}^2 \bigwedge_{x=1}^3 \bigwedge_{y=1}^3 \bigwedge_{k=y+1}^3 \bigwedge_{l=1}^3 (\lnot s_{(3i+x)(3j+y)z} \lor \lnot s_{(3i+k)(3j+l)z})
これは 4-1. で生成された制約と被ることがある。
code:duplicate.txt
dame: 211231
dame: 311321
dame: 311331
dame: 321331
dame: 241251
dame: 241261
dame: 341351
dame: 341361
dame: 351361
dame: 271281
dame: 271291
3-2 は重複した制約を生成しない。
code:result.txt
111211
111221
111231
111311
111321
111331
112212
112222
112232
112312
112322
112332
113213
拡張された還元は、それぞれのマスにただ1つの数字が入ることや、それぞれの箱・列・行にそれぞれの数字がただ9つのみ表れることなどの主張を含む。
拡張された還元は最小の還元での制約をすべてと、次のような制約を含む。
1. それぞれのマスには高々1つの数字が入っている
$ \bigwedge^9_{x=1}\bigwedge^9_{y=1}\bigwedge^8_{z=1}\bigwedge^9_{i=z+1} (\lnot s_{xyz} \lor \lnot s_{xyi})
2. それぞれの列には最低でも1回、それぞれの数字が入る
$ \bigwedge^9_{y=1}\bigwedge^9_{z=1}\bigvee^9_{x=1} s_{xyz}
3. それぞれの行には最低でも1回、それぞれの数字が入る
$ \bigwedge^9_{x=1}\bigwedge^9_{z=1}\bigvee^9_{y=1} s_{xyz}
4. それぞれの箱には最低でも1回、それぞれの数字が入る
$ \bigvee_{z=1}^9 \bigwedge_{i=0}^2 \bigwedge_{j=0}^2 \bigwedge_{x=1}^3 \bigwedge_{y=1}^3 s_{(3i+x)(3j+y)z}