MiniZinc でお絵描きロジック

はじめに

制約充足問題を解く制約プログラミングの手法が数理最適化かどうか、というのはちょっと微妙なのですが、今話題のChatGPTさんに伺ったところ問題なさそうでしたので投稿することにしました。

私: 制約プログラミングは数理最適化でしょうか。
ChatGPT:

はい、制約プログラミングは数理最適化の分野に属します。
数理最適化とは、ある目的関数を最大化または最小化するような変数の値を求める
問題を解くための方法を指します。制約プログラミングでは、問題を解く上での
変数の値に制約を設けることができるため、数理最適化の問題を解く際に柔軟な
アプローチが可能になります。

ちなみに、このテーマについては

MiniZincとお絵描きロジックをテーマにすることは面白いと思います。MiniZincは
制約プログラミング用のモデリング言語であり、お絵描きロジックは数学的な問題を
図形や絵で解くという方法です。両者を組み合わせることで、より直感的で視覚的に
制約プログラミングの問題を解くことができるかもしれません。また、お絵描き
ロジックは小学校低学年の子どもたちにも楽しんでもらえる内容ですので、幅広い
年齢層の人たちに参加してもらえるかもしれません。

だそうです。(すごくポジティブ)

前提条件

MiniZinc とは

ChatGPT が説明したとおり、「制約プログラミング用のモデリング言語」です。後ほど出てくる具体例を見ると、どんな雰囲気かが分かると思います。

お絵描きロジック

広く知られたパズルなので、パズル自体の説明は省きます。詳しくは Wikipedia で。

お絵描きロジックと正規表現

各行や各列についているヒント (「2 3」のようなもの)をもとにマスを黒く塗りつぶしていく訳ですが、このヒントは容易に正規表現に変換可能です。前述の例は、以下のパターンを表現しています。

　* 白マスが0個以上 (ヒントの数字が始まる前の部分に対応)
　* 黒マスが2個 (ヒントの"2"に対応)
　* 白マスが1個以上 (ヒントの2と3の間に対応)
　* 黒マスが3個 (ヒントの"3"に対応)
　* 白マスが0個以上 (ヒントの数字がすべて終わった後の部分に対応)

これを正規表現で表せば「白*黒{2}白+黒{3}白*」のようになるでしょう。
(*は直前の文字が0個以上続くこと、{数字}は直前の文字が数字と同じ個数だけ続くこと、+は直前の文字が1個以上続くことをそれぞれ表します)
このヒントが$n$行目についていれば、$n$行目はその正規表現にマッチするということになります。(列ついても同様)

MiniZinc で表現する

CSPLIB で見つかるコードでは、正規表現と等価なオートマトンを構築して、それを制約として設定しています。

しかしながら、最近の MiniZinc では Regular制約として以下のようなものが使えるようになっていました。

predicate regular(array [int] of var int: x, string: r)

文字列rとしては先ほどの正規表現が使えるそうです。正規表現をオートマトンに変換すること自体は機械的に可能とはいえ、問題の理解ともモデリングとも全く異なるレイヤの話なので、こちらを使っていきましょう。

また、MiniZinc では添え字が1から始まるため、白(塗りつぶしなし)を1、黒(塗りつぶしあり)を2とするような表現が良いようです。これは最終的な変換先になるオートマトンの遷移行列の添え字に直接利用できる数値の範囲であるためと考えられます。

% 問題となるマス目の大きさを定義するための定数を宣言
int: rows;
int: cols;

% データは *.dzn という別ファイルに分けるのが流儀ですが、
% ここでは同一ファイルに書いています。
rows = 20;
cols = 20;

% ヒントの定数を宣言
array [1..rows] of string: row_rules;
array [1..cols] of string: col_rules;

% データは *.dzn という別ファイルに分けるのが流儀ですが、
% ここでは同一ファイルに書いています。
% このデータは、CSPLib にある nonogram_dragonfly.dzn を
% 正規表現に変換したものです。
% https://www.csplib.org/Problems/prob012/data/nonogram_dragonfly.dzn.html
row_rules =
[
"1* 2{7} 1+ 2{1} 1*",
"1* 2{1} 1+ 2{1} 1+ 2{2} 1*",
"1* 2{2} 1+ 2{1} 1+ 2{2} 1*",
"1* 2{1} 1+ 2{2} 1+ 2{2} 1*",
"1* 2{4} 1+ 2{2} 1+ 2{3} 1*",
"1* 2{3} 1+ 2{1} 1+ 2{4} 1*",
"1* 2{3} 1+ 2{1} 1+ 2{3} 1*",
"1* 2{2} 1+ 2{1} 1+ 2{4} 1*",
"1* 2{2} 1+ 2{9} 1*",
"1* 2{2} 1+ 2{1} 1+ 2{5} 1*",
"1* 2{2} 1+ 2{7} 1*",
"1* 2{14} 1*",
"1* 2{8} 1+ 2{2} 1*",
"1* 2{6} 1+ 2{2} 1+ 2{2} 1*",
"1* 2{2} 1+ 2{8} 1+ 2{1} 1+ 2{3} 1*",
"1* 2{1} 1+ 2{5} 1+ 2{5} 1+ 2{2} 1*",
"1* 2{1} 1+ 2{3} 1+ 2{2} 1+ 2{4} 1+ 2{1} 1*",
"1* 2{3} 1+ 2{1} 1+ 2{2} 1+ 2{4} 1+ 2{1} 1*",
"1* 2{1} 1+ 2{1} 1+ 2{3} 1+ 2{1} 1+ 2{3} 1*",
"1* 2{2} 1+ 2{1} 1+ 2{1} 1+ 2{2} 1*"
];

col_rules =
[
"1* 2{1} 1+ 2{1} 1+ 2{1} 1+ 2{2} 1*",
"1* 2{3} 1+ 2{1} 1+ 2{2} 1+ 2{1} 1+ 2{1} 1*",
"1* 2{1} 1+ 2{4} 1+ 2{2} 1+ 2{1} 1+ 2{1} 1*",
"1* 2{1} 1+ 2{3} 1+ 2{2} 1+ 2{4} 1*",
"1* 2{1} 1+ 2{4} 1+ 2{6} 1+ 2{1} 1*",
"1* 2{1} 1+ 2{11} 1+ 2{1} 1*",
"1* 2{5} 1+ 2{1} 1+ 2{6} 1+ 2{2} 1*",
"1* 2{14} 1*",
"1* 2{7} 1+ 2{2} 1*",
"1* 2{7} 1+ 2{2} 1*",
"1* 2{6} 1+ 2{1} 1+ 2{1} 1*",
"1* 2{9} 1+ 2{2} 1*",
"1* 2{3} 1+ 2{1} 1+ 2{1} 1+ 2{1} 1*",
"1* 2{3} 1+ 2{1} 1+ 2{3} 1*",
"1* 2{2} 1+ 2{1} 1+ 2{3} 1*",
"1* 2{2} 1+ 2{1} 1+ 2{5} 1*",
"1* 2{3} 1+ 2{2} 1+ 2{2} 1*",
"1* 2{3} 1+ 2{3} 1+ 2{2} 1*",
"1* 2{2} 1+ 2{3} 1+ 2{2} 1*",
"1* 2{2} 1+ 2{6} 1*"
];
% 1..2 の範囲をとる変数の、rows x cols の配列 x を宣言します。
% 制約を満たすように x の各要素の値を決定することが問題を解くことになります。
array[1..rows, 1..cols] of var 1..2: x;

include "globals.mzn"; 

constraint
      % 各列、各行に対し、ヒントの正規表現を制約として設定します。
      forall(j in 1..cols) (
        regular([x[i,j] | i in 1..rows], col_rules[j])
      )
      /\
      forall(i in 1..rows) (
        regular([x[i,j] | j in 1..cols], row_rules[i])
      )
;

% 制約充足問題として解きます。
solve satisfy;

% 結果を表示します。
output 
[
  if j = 1 then "\n" else "" endif ++
     if fix(x[i,j]) = 1 then " " else "#" endif
    
  | i in 1..rows, j in 1..cols
] 
++ 
[
  "\n"
];

結果は以下の通りです。
(トンボに見えないこともない...)

#######            #
 #    #           ##
 ##   #          ## 
  #   ##        ##  
####  ##       ###  
  ###  #     ####   
   ### #    ###     
    ## #  ####      
##  #########       
 ##  # #####        
  ## #######        
   ##############   
    ########    ##  
    ###### ##    ## 
 ## ######## #   ###
#  #####   #####  ##
#  ### ##    ####  #
 ###  # ##    #### #
   #  #  ###   # ###
    ##     #   #  ##

おわりに

お絵描きロジックのヒントは正規表現による制約としてとらえられることを説明しました。また、MiniZinc では正規表現をそのまま制約として設定することが可能であるため、お絵描きロジックを解くプログラム(MiniZincのモデル)は非常に簡単に書けることを示しました。

なお、Regular制約自体はお絵描きロジックのためにある訳ではなく、シフト勤務のスケジュール(日勤や夜勤のパターンが必要になる)を作成する時に使われることもあるようです。