LoginSignup
1
1

More than 1 year has passed since last update.

ジグソー数独(Sudoku Jigsaw)を色々なソルバー(prolog, minizinc, clingo)で解く

Last updated at Posted at 2021-11-13

こちらも書いたので参考まで。

ジグソー数独は縦1列と横1行に入る数字が全て異なる様にする。またマスの各色に入る数字も全て異なる様にする。

問題例と

その解答

SWI-Prolog

制約論理プログラミングについてはここを参照。
http://www.nct9.ne.jp/m_hiroi/prolog/clp.html

SWI-Prologのインストール

MacでHomebrewな人はSWI-Prologを下の様にインストールできる。
Homebrewがまだ入ってない方はこちら https://brew.sh/index_ja

brew install swi-prolog

プログラム

下のprologコードをファイルjigsaw_sudoku.plにする

jigsaw_sudoku.pl
#!/usr/bin/env swipl

:- initialization(main, main).

% e.g. Shell command:
%  ./jigsaw_sudoku.pl 2 jigsaw_sudoku_data.pl
main(Argv) :-
   argv(2,Argv,A,Data),
   consult(Data),
   term_to_atom(T,A),
   problem(T, Rows, Colors),
   sudoku(Rows, Colors), maplist(portray_clause, Rows).

% 引数
argv(1,[X],X).
argv(2,[X,Y],X,Y).

:- use_module(library(clpfd)).

sudoku(Rows, Colors) :-
   length(Rows, 9),                                  %制約: 行は9行
   maplist(same_length(Rows), Rows),                 %制約: 全ての行は同じ長さ
   append(Rows, Rows1d), Rows1d ins 1..9,            % 1次元配列に均す
   maplist(all_distinct, Rows),                      %制約: 行は全て異なる
   transpose(Rows, Columns),
   maplist(all_distinct, Columns),                   %制約: 列は全て異なる
   append(Colors, Colors1d),                         % 色も1次元配列に均す
   Color = [a,b,c,d,e,f,g,h,i],                      % 色名定義a~i
   forall(member(X, Colors1d), member(X, Color)),    %制約: 色名はa~i
   Blankl = [[],[],[],[],[],[],[],[],[]],
   zip(Colors1d, Rows1d, Ts),                        % 数字1d配列と色1d配列をジップしタプル配列にする
   foldl(grplist, Ts, Blankl, Cll),                  % 色ごとにグループ分けをする
   maplist(all_distinct, Cll).                       %制約: 色内は全て異なる

% 色を配列に振り分け
grplist((G, V), [La,Lb,Lc,Ld,Le,Lf,Lg,Lh,Li], L) :-
   G = a -> L = [[V|La],Lb,Lc,Ld,Le,Lf,Lg,Lh,Li];
   G = b -> L = [La,[V|Lb],Lc,Ld,Le,Lf,Lg,Lh,Li];
   G = c -> L = [La,Lb,[V|Lc],Ld,Le,Lf,Lg,Lh,Li];
   G = d -> L = [La,Lb,Lc,[V|Ld],Le,Lf,Lg,Lh,Li];
   G = e -> L = [La,Lb,Lc,Ld,[V|Le],Lf,Lg,Lh,Li];
   G = f -> L = [La,Lb,Lc,Ld,Le,[V|Lf],Lg,Lh,Li];
   G = g -> L = [La,Lb,Lc,Ld,Le,Lf,[V|Lg],Lh,Li];
   G = h -> L = [La,Lb,Lc,Ld,Le,Lf,Lg,[V|Lh],Li];
   G = i -> L = [La,Lb,Lc,Ld,Le,Lf,Lg,Lh,[V|Li]];
   fail.

% 色名と数字をタプルにした配列を作る
zip([X|Xs], [Y|Ys], [(X,Y)|Zs]) :- zip(Xs,Ys,Zs).
zip([X], [Y], [(X,Y)]).
zip(_, [], _) :- fail.
zip([], _, _) :- fail.

パーミッションを実行可能にしておく

chmod +x jigsaw_sudoku.pl

問題は下の様にファイルjigsaw_sudoku_data.plに書く
マスの色をグループと呼んでいて、a~iのアルファベットで表している

jigsaw_sudoku_data.pl

problem(1,
   [[3,_,_,_,_,_,_,_,4],
    [_,_,2,_,6,_,1,_,_],
    [_,1,_,9,_,8,_,2,_],
    [_,_,5,_,_,_,6,_,_],
    [_,2,_,_,_,_,_,1,_],
    [_,_,9,_,_,_,8,_,_],
    [_,8,_,3,_,4,_,6,_],
    [_,_,4,_,1,_,9,_,_],
    [5,_,_,_,_,_,_,_,7]],

   [[a,a,a,b,c,c,c,c,c],
    [a,a,a,b,b,b,c,c,c],
    [a,d,d,d,d,b,b,b,c],
    [a,a,d,e,e,e,e,b,b],
    [d,d,d,d,e,f,f,f,f],
    [g,g,e,e,e,e,f,i,i],
    [h,g,g,g,f,f,f,f,i],
    [h,h,h,g,g,g,i,i,i],
    [h,h,h,h,h,g,i,i,i]]).

problem(2,
   [[_,9,_,_,5,4,_,8,1],
    [_,_,_,6,_,_,4,_,_],
    [9,_,_,_,2,_,_,_,_],
    [5,_,_,4,6,_,_,_,_],
    [3,2,_,_,_,9,_,6,_],
    [_,_,_,1,_,_,_,5,7],
    [6,_,_,_,_,_,_,_,4],
    [1,_,3,_,_,_,_,2,_],
    [7,_,_,_,4,_,_,9,3]],

   [[a,b,b,b,b,b,c,c,c],
    [a,d,d,b,b,b,c,c,c],
    [a,d,d,b,c,c,c,e,e],
    [a,d,d,d,f,e,e,e,e],
    [a,d,f,f,f,e,g,g,g],
    [a,d,f,f,f,e,g,g,g],
    [a,h,h,h,f,e,g,g,g],
    [a,h,h,h,f,i,i,i,i],
    [a,h,h,h,i,i,i,i,i]]).

シェルで実行。第1引数で問題の番号を選択し、第2引数は問題のファイル

./jigsaw_sudoku.pl 1 jigsaw_sudoku_data.pl

結果

[3, 5, 8, 1, 9, 6, 2, 7, 4].
[4, 9, 2, 5, 6, 7, 1, 3, 8].
[6, 1, 3, 9, 7, 8, 4, 2, 5].
[1, 7, 5, 8, 4, 2, 6, 9, 3].
[8, 2, 6, 4, 5, 3, 7, 1, 9].
[2, 4, 9, 7, 3, 1, 8, 5, 6].
[9, 8, 7, 3, 2, 4, 5, 6, 1].
[7, 3, 4, 6, 1, 5, 9, 8, 2].
[5, 6, 1, 2, 8, 9, 3, 4, 7].

MiniZinc

制約モデリング言語です
https://www.minizinc.org/

チュートリアルを訳してみました。
MiniZincチュートリアル1
MiniZincチュートリアル2
MiniZincチュートリアル3
MiniZincチュートリアル4
MiniZincチュートリアル5
MiniZincチュートリアル6
MiniZincチュートリアル7

インストール

ここからインストーラを取ってくる
https://www.minizinc.org/software.html

MacでHomebrewな人は brew install minizinc でインストールしたくなるだろうが、
ソルバーの設定が出来ずに私は詰んだので、素直にインストーラーを使う方が良い。

プログラム

下のコードをファイル jigsaw_sudoku.mzn にする

jigsaw_sudoku.mzn
include "alldifferent.mzn";

int: N = 9;
int: digs = ceil(log(10.0,int2float(N))); % digits for output

set of int: PuzzleRange = 1..N;

array[1..N,1..N] of 0..N: problem; %% initial board 0 = empty
array[1..N,1..N] of var PuzzleRange: puzzle;

enum ColorId = {a,b,c,d,e,f,g,h,i};
array[1..N,1..N] of ColorId: colors;

% fill initial board
constraint forall(k,l in PuzzleRange) (
    if problem[k,l] > 0 then puzzle[k,l] = problem[k,l] else true endif );

% All different in rows 
constraint forall(k in PuzzleRange) (
    alldifferent( [ puzzle[k,l] | l in PuzzleRange ]) ); 

% All different in columns.
constraint forall(l in PuzzleRange) (
    alldifferent( [ puzzle[k,l] | k in PuzzleRange ]) );

% All different in colors
constraint forall(m in ColorId) (
    alldifferent( [ puzzle[k,l] | k,l in PuzzleRange where m == colors[k,l] ] ) );

solve satisfy;

output  [ show_int(digs, puzzle[k,l]) ++ " " ++ 
         if l == N then
             if k != N then "\n" else "" endif
	     else "" endif  
         | k,l in PuzzleRange ] ++ ["\n"];

問題を下の様にファイル jigsaw_sudoku1.dzn に書く

jigsaw_sudoku1.dzn
problem=[|
3,0,0,0,0,0,0,0,4|
0,0,2,0,6,0,1,0,0|
0,1,0,9,0,8,0,2,0|
0,0,5,0,0,0,6,0,0|
0,2,0,0,0,0,0,1,0|
0,0,9,0,0,0,8,0,0|
0,8,0,3,0,4,0,6,0|
0,0,4,0,1,0,9,0,0|
5,0,0,0,0,0,0,0,7|];

colors = [|
a,a,a,b,c,c,c,c,c|
a,a,a,b,b,b,c,c,c|
a,d,d,d,d,b,b,b,c|
a,a,d,e,e,e,e,b,b|
d,d,d,d,e,f,f,f,f|
g,g,e,e,e,e,f,i,i|
h,g,g,g,f,f,f,f,i|
h,h,h,g,g,g,i,i,i|
h,h,h,h,h,g,i,i,i|];

シェルで実行

minizinc --solver gecode -a jigsaw_sudoku.mzn jigsaw_sudoku1.dzn

結果

3 5 8 1 9 6 2 7 4
4 9 2 5 6 7 1 3 8
6 1 3 9 7 8 4 2 5
1 7 5 8 4 2 6 9 3
8 2 6 4 5 3 7 1 9
2 4 9 7 3 1 8 5 6
9 8 7 3 2 4 5 6 1
7 3 4 6 1 5 9 8 2
5 6 1 2 8 9 3 4 7
----------
==========

Clingo

Clingoについてはこの辺を参照

チュートリアルとか

プログラム

下の通り

jignump_enc.lp
num(1..9). color(a;b;c;d;e;f;g;h;i).

% 行I, 列Jが1から9の整数であるとき、マスm(I, J, N)を満たす1から9の整数Nはただ一つある
% 早い話が1つのマスには1つの数字しか入らず、それは1〜9のいずれかである。
{m(I, J, N) : num(N)} = 1 :- num(I), num(J).

% 1つのマスには1つの色定義文字"a~i"しか入らない。
{o(I, J, C) : color(C)} = 1 :- num(I), num(J).

% 一つの行に同じ数字は無い
N1 != N2 :- m(I, J1, N1), m(I, J2, N2), J1 != J2.
% 一つの列に同じ数字は無い
N1 != N2 :- m(I1, J, N1), m(I2, J, N2), I1 != I2.

% 同一マスかどうか
samepos(I1,J1,I2,J2) :- I1 == I2, J1 == J2, num(I1), num(I2), num(J1), num(J2).

% 同じ色oに同じ数字は無い
N1 != N2 :- m(I1, J1, N1), m(I2, J2, N2), 
            o(I1, J1, P),  o(I2, J2, P), not samepos(I1, J2, I2, J2).

#show m/3.

問題定義は下の通りなのだが、だいぶ読みづらいし書きづらい。
clingoは配列とかリストとか無さそうなので仕方ない。
綺麗な書き方ができるのなら教えて欲しいです。

jignum_prob.lp
m(1,1,3).                                                                       m(1,9,4).
                    m(2,3,2).           m(2,5,6).           m(2,7,1).                    
          m(3,2,1).           m(3,4,9).           m(3,6,8).           m(3,8,2).          
                    m(4,3,5).                               m(4,7,6).                    
          m(5,2,2).                                                   m(5,8,1).          
                    m(6,3,9).                               m(6,7,8).                    
          m(7,2,8).           m(7,4,3).           m(7,6,4).           m(7,8,6).          
                    m(8,3,4).           m(8,5,1).           m(8,7,9).                    
m(9,1,5).                                                                       m(9,9,7).

o(1,1,a). o(1,2,a). o(1,3,a). o(1,4,b). o(1,5,c). o(1,6,c). o(1,7,c). o(1,8,c). o(1,9,c).
o(2,1,a). o(2,2,a). o(2,3,a). o(2,4,b). o(2,5,b). o(2,6,b). o(2,7,c). o(2,8,c). o(2,9,c).
o(3,1,a). o(3,2,d). o(3,3,d). o(3,4,d). o(3,5,d). o(3,6,b). o(3,7,b). o(3,8,b). o(3,9,c).
o(4,1,a). o(4,2,a). o(4,3,d). o(4,4,e). o(4,5,e). o(4,6,e). o(4,7,e). o(4,8,b). o(4,9,b).
o(5,1,d). o(5,2,d). o(5,3,d). o(5,4,d). o(5,5,e). o(5,6,f). o(5,7,f). o(5,8,f). o(5,9,f).
o(6,1,g). o(6,2,g). o(6,3,e). o(6,4,e). o(6,5,e). o(6,6,e). o(6,7,f). o(6,8,i). o(6,9,i).
o(7,1,h). o(7,2,g). o(7,3,g). o(7,4,g). o(7,5,f). o(7,6,f). o(7,7,f). o(7,8,f). o(7,9,i).
o(8,1,h). o(8,2,h). o(8,3,h). o(8,4,g). o(8,5,g). o(8,6,g). o(8,7,i). o(8,8,i). o(8,9,i).
o(9,1,h). o(9,2,h). o(9,3,h). o(9,4,h). o(9,5,h). o(9,6,g). o(9,7,i). o(9,8,i). o(9,9,i).

問題を毎回上のをいじるのはだるいので、下の様にシンプルに記述して、上のフォーマットにgawkで変換する事にした。

numbers
_ 9 _ _ 5 4 _ 8 1
_ _ _ 6 _ _ 4 _ _
9 _ _ _ 2 _ _ _ _
5 _ _ 4 6 _ _ _ _
3 2 _ _ _ 9 _ 6 _
_ _ _ 1 _ _ _ 5 7
6 _ _ _ _ _ _ _ 4
1 _ 3 _ _ _ _ 2 _
7 _ _ _ 4 _ _ 9 3

colors
a b b b b b c c c
a d d b b b c c c
a d d b c c c f f
a d d d e f f f f
a d e e e f g g g
a d e e e f g g g
a h h h e f g g g
a h h h e i i i i
a h h h i i i i i

gawkのインストール。Macでbrewな人は下の通り。

brew install gawk

変換するgawkプログラムは下の通り。

jigcon.awk
#!/usr/bin/env gawk -f

BEGIN {
  start = 0;
  color = 0;
  row = 0;
}

/^numbers/ {start = NR; color = 0;}
/^colors/ {start = NR; color = 1;}

/^[1-9_a-i] / {
  if (0 < start && start < NR && NR <= start + 9) {
    if (NF != 9) {printf "s=%s,NF=%d,列数は9にすること!\n", $0, NF > "/dev/stderr"}
    row = NR - start;
    for (col = 1; col <= 9; col++ ) {
      x = $(col);
      if (color) {
        if (x !~ /[a-i]/) {printf "x=%d,ブロック文字はa~iにすること!\n", x > "/dev/stderr"}
      }else{
        if (x !~ /[_1-9]/) {printf "x=%d,数字は1~9,不明数は_にすること!\n", x > "/dev/stderr"}
      }
      delim = col < 9 ? " " : "\n";
      if (!color && x ~ /[1-9]/) {
        printf "m(%d,%d,%d).%s", row, col, x, delim;
      }else if (color && x ~ /[a-i]/) {
        printf "o(%d,%d,%s).%s", row, col, x, delim;
      }else{
        printf "         %s", delim;
      }
    }
  }else{
    printf "\n";
    start = 0;
  }
}
END {
}

パーミッションを実行にしておく。

chmod +x jigcon.awk

ところで下の様に、普通に実行すると

clingo jignump_enc.lp jignum_prob.lp

こんな風に出て、

clingo version 5.5.0
Reading from jignump_enc.lp ...
Solving...
Answer: 1
m(1,1,3) m(1,9,4) m(2,3,2) m(2,5,6) m(2,7,1) m(3,2,1) m(3,4,9) m(3,6,8) m(3,8,2) m(4,3,5) m(4,7,6) m(5,2,2) m(5,8,1) m(6,3,9) m(6,7,8) m(7,2,8) m(7,4,3) m(7,6,4) m(7,8,6) m(8,3,4) m(8,5,1) m(8,7,9) m(9,1,5) m(9,9,7) m(8,2,3) m(3,3,3) m(6,5,3) m(5,6,3) m(9,7,3) m(2,8,3) m(4,9,3) m(4,1,1) m(9,3,1) m(6,6,1) m(7,9,1) m(6,1,2) m(9,4,2) m(7,5,2) m(4,6,2) m(8,9,2) m(2,1,4) m(6,2,4) m(5,4,4) m(4,5,4) m(3,7,4) m(9,8,4) m(2,4,5) m(5,5,5) m(8,6,5) m(7,7,5) m(6,8,5) m(3,9,5) m(3,1,6) m(9,2,6) m(5,3,6) m(8,4,6) m(6,9,6) m(4,2,7) m(8,1,7) m(7,3,7) m(6,4,7) m(3,5,7) m(2,6,7) m(5,7,7) m(5,1,8) m(4,4,8) m(9,5,8) m(8,8,8) m(2,9,8) m(2,2,9) m(7,1,9) m(9,6,9) m(4,8,9) m(5,9,9) m(1,2,5) m(1,3,8) m(1,4,1) m(1,5,9) m(1,6,6) m(1,7,2) m(1,8,7)
SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.226s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.224s

これもまた、読みにくいので、出力もgawkで成形して見やすくする。
下が出力を成形するプログラム。

jigout.awk
#!/usr/bin/env gawk -f

function printrow(a){
  len = length(a);
  for (i = 1; i <= len; i++) {
    delim = i == len ? "\n" : " ";
    printf "%d%s", a[i], delim;
  }
}

BEGIN {
}
{
  if ( $0 ~ /^m\([1-9],[1-9],[1-9]\).+m\([1-9],[1-9],[1-9]\)$/ ) {
    split($0, arr, " ");
    for (i = 1; i <= length(arr); i++) {
      match(arr[i], /m\(([1-9]),([1-9]),([1-9])\)/, a);
      switch(a[1]){
        case 1: r1[a[2]] = a[3]; break
        case 2: r2[a[2]] = a[3]; break
        case 3: r3[a[2]] = a[3]; break
        case 4: r4[a[2]] = a[3]; break
        case 5: r5[a[2]] = a[3]; break
        case 6: r6[a[2]] = a[3]; break
        case 7: r7[a[2]] = a[3]; break
        case 8: r8[a[2]] = a[3]; break
        case 9: r9[a[2]] = a[3]; break
        default: print "Error" > "/dev/stderr"; break
      }
    }
  }
}
END {
  printrow(r1);
  printrow(r2);
  printrow(r3);
  printrow(r4);
  printrow(r5);
  printrow(r6);
  printrow(r7);
  printrow(r8);
  printrow(r9);
}

問題をファイルに書く

jignum2.prob
numbers
3 _ _ _ _ _ _ _ 4
_ _ 2 _ 6 _ 1 _ _
_ 1 _ 9 _ 8 _ 2 _
_ _ 5 _ _ _ 6 _ _
_ 2 _ _ _ _ _ 1 _
_ _ 9 _ _ _ 8 _ _
_ 8 _ 3 _ 4 _ 6 _
_ _ 4 _ 1 _ 9 _ _
5 _ _ _ _ _ _ _ 7

colors
a a a b c c c c c
a a a b b b c c c
a d d d d b b b c
a a d e e e e b b
d d d d e f f f f
g g e e e e f i i
h g g g f f f f i
h h h g g g i i i
h h h h h g i i i

シェルで実行

cat jignum2.prob | ./jigcon.awk >! /tmp/temp.lp \
&& clingo jignump_enc.lp /tmp/temp.lp | ./jigout.awk ; rm -f /tmp/temp.lp

結果

3 5 8 1 9 6 2 7 4
4 9 2 5 6 7 1 3 8
6 1 3 9 7 8 4 2 5
1 7 5 8 4 2 6 9 3
8 2 6 4 5 3 7 1 9
2 4 9 7 3 1 8 5 6
9 8 7 3 2 4 5 6 1
7 3 4 6 1 5 9 8 2
5 6 1 2 8 9 3 4 7
1
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
1
1