数独+IP+GLPK - 裏紙・メモ帳・忘備録

某友人がCPLEXで数独を解いてみたと聞いて、自分でもやってみた。
01変数を9*9*9=729個使った定式化。たぶん某友人と同じ。
モデリングにはGNU MathProgを使い、ソルバはGLPKを使った。

以下のファイルを書いてから

glpsol -m sudoku.mod -d instance.dat -w result.txt

で最適化実行。
結果をawkで整形すればできあがり。

tail -n 729 result.txt | gawk '{c += $0*++i;};NR%9==0{printf("%d",c);c=0;i=0};NR%81==0{printf("\n")}'

インスタンスの出展はwikipedia:数独。
計算が重ければソルバにCPLEXを使うこともできるけど、
CPLEXに比べて遅いGLPKでも一瞬で解けた。

# sudoku.mod
set I := 0..8;
set J := 0..8;
set K := 1..9;
set B := 0..8;
set Bs{b in B} := setof{y in 0..2, x in 0..2}(y+3*(b div 3),x+3*(b mod 3));

var X{I,J,K} binary;
param known{I,J}, integer;

minimize dummy: sum{i in I,j in J,k in K}X[i,j,k];
s.t. Row{i in I,k in K}: sum{j in J}X[i,j,k] = 1;
     Col{j in J,k in K}: sum{i in I}X[i,j,k] = 1;
     Cell{i in I,j in J}: sum{k in K}X[i,j,k] = 1;
     Block{b in B,k in K}: sum{(i,j) in Bs[b]}X[i,j,k] = 1;
     Known{i in I,j in J,k in K: known[i,j]==k}: X[i,j,k]=1;

# instance.dat
param known
 : 0 1 2 3 4 5 6 7 8 :=
 0 5 3 0 0 7 0 0 0 0
 1 6 0 0 1 9 5 0 0 0
 2 0 9 8 0 0 0 0 6 0
 3 8 0 0 0 6 0 0 0 3
 4 4 0 0 8 0 3 0 0 1
 5 7 0 0 0 2 0 0 0 6
 6 0 6 0 0 0 0 2 8 0
 7 0 0 0 4 1 9 0 0 5
 8 0 0 0 0 8 0 0 7 9;