トップ «前の日記(2010-04-17) 最新 次の日記(2010-04-23)» 月表示 編集

日々の流転


2010-04-21 [長年日記]

λ. GLPKで数独を解く

去年はいろんなソルバやモデルファインダーを使って数独を解いて遊んでいて、最後にやったのが、丁度一年前の記事の「ASPで数独を解く」。 一年ぶりにまたふとやってみたくなったので、今度はフリーの線形計画法ソルバの GLPK (GNU Linear Programming Kit) を使ってやってみた。

まずは問題の構造を記述したファイル SudokuGLPK.mod:

set Number := 1..9;

param Data{Number, Number, Number} binary default 0;

var Ans{Number, Number, Number} binary;
s.t. GIVEN{x in Number, y in Number, n in Number}: Data[x,y,n] <= Ans[x,y,n];
s.t. FILLED{x in Number, y in Number}: sum{n in Number} Ans[x,y,n] = 1;
s.t. COL{n in Number, x in Number}: sum{y in Number} Ans[x,y,n] = 1;
s.t. ROW{n in Number, y in Number}: sum{x in Number} Ans[x,y,n] = 1;
s.t. BLOCK{n in Number, x0 in 0..2, y0 in 0..2}:
      sum{x1 in 1..3, y1 in 1..3} Ans[3*x0+x1, 3*y0+y1, n] = 1;

「座標(x,y)の数がnであること」をAns[x,y,n]が1であることで表現して、その組み合わせに関する条件を算術的に表現している。 やっている事自体はSATで解く場合と大して変わらないんだけど、結構直観的に書けて良かった。

次に、具体的な問題のデータを記述したファイル SudokuGLPK.dat:

param Data := 
  1 1 1 1
  1 4 2 1
  1 7 3 1
  2 2 2 1
  2 5 3 1
  2 8 4 1
  3 3 3 1
  3 6 4 1
  3 9 5 1
  4 1 6 1
  4 4 4 1
  4 7 5 1
  5 2 7 1
  5 5 5 1
  5 8 6 1
  6 3 8 1
  6 6 6 1
  6 9 7 1
  7 1 8 1
  7 4 9 1
  7 7 7 1
  8 2 9 1
  8 5 1 1
  8 8 8 1
  9 3 1 1
  9 6 2 1
  9 9 4 1;

このファイルは配列Dataに対する値の割り当てを表していて、「a b c 1」という行は Data[a,b,c] が 1 であることを表している。

これで glpsol.exe -m SudokuGLPK.mod -d SudokuGLPK.dat -o ans.txt と実行すると、ans.txtのようなファイルが得られる。 このファイルの途中を見ると、以下のような感じで配列Ansに対する値の割り当てが得られる。 たとえば、Ans[1,2,4]のActivityが1なので、座標(1,2)の数が4であることが分かる。

…
   No. Column name       Activity     Lower bound   Upper bound
------ ------------    ------------- ------------- -------------
     1 Ans[1,1,1]   *              1             0             1 
     2 Ans[1,1,2]   *              0             0             1 
     3 Ans[1,1,3]   *              0             0             1 
     4 Ans[1,1,4]   *              0             0             1 
     5 Ans[1,1,5]   *              0             0             1 
…
    13 Ans[1,2,4]   *              1             0             1 
…

参考