フィルマットが好きだ。あるいはフィルマットをSugar制約ソルバーで解く

フィルマットというパズルがあります。ありますが皆さんご存知です？
まいなすよんは永遠の若手ですので、当然ちゃ当然なのですが、私もニコリ本誌で現役の頃を知らないくらいです。とはいうもののニコリのページの紹介がありますので、ご興味の向きはそちらをどうぞ。
そして例題はこちら。小さいですが。

で、答えはこうなります。

今回は、フィルマットをSugar制約ソルバーで解くことを考えたいと思います。

以前、ぼんさんやカーブデータを解いた時は、盤面に番号を振ってそれを変数として探す、という手法をとりましたが、今回はトラディッショナル（？）に盤面の各マスに変数を割り振ります。
以下のような感じ。左側が変数、右側が最終的に答えとなる数字です。

で、天下り的ですが、補助的な変数を導入します。左側が変数、右側が最終的に答えとなる数字なのは同じですが、数字５と６が設定されています。各数字の役割は以下のようになります。
数字３→面積３のブロックに含まれ、その両端になる。
数字４→面積４のブロックに含まれ、その両端になる。
数字５→面積３のブロックに含まれ、その両端にならない。
数字６→面積４のブロックに含まれ、その両端にならない。

本質的には要らないっちゃ要らないんですが、たぶん変数b_xx_yyを導入したほうが見やすいと思うのですよね。Sugar慣れした方には、もうこれで伝わるものは伝わったかと思うのですが、説明を続けます。

まずは変数の定義。

( int a_00_00 1 4 )
  ; 中略
( int a_03_03 1 4 )

( int b_00_00 1 6 )
  ; 中略
( int b_03_03 1 6 )

次に、この２種類の変数の基本的な関係を記述します。x_00_00の位置の関係のみ列挙します。

( => ( = b_00_00 1 ) ( = a_00_00 1 ) )
( => ( = b_00_00 2 ) ( = a_00_00 2 ) )
( => ( = b_00_00 3 ) ( = a_00_00 3 ) )
( => ( = b_00_00 4 ) ( = a_00_00 4 ) )
( => ( = b_00_00 5 ) ( = a_00_00 3 ) )
( => ( = b_00_00 6 ) ( = a_00_00 4 ) )

表出の記述。例題では４つだけなので全部書いてみます。

( = a_00_00 1 )
( = a_00_01 3 )
( = a_02_02 2 )
( = a_00_03 3 )

各マスについて、そのマスに１から４の数字が入った場合について場合分けして、そのマスの上下左右のマスが満たすべき条件を記述します。さらに、３が入る場合と４が入る場合は、それぞれについて端かそうでないかで場合分けします。説明をすっ飛ばして感覚的に書くと、そのマスに１から６の数字が入った場合について場合分けします。

辺や隅の処理は面倒なので、以下では例としてx_01_01のマスについて記述します。辺や隅は条件をとりうる条件を絞るだけですので、適宜読み替えてください。

まずそのマスに１が入る場合。これは簡単です。隣接するマスには１が入らないということをSugarに教えます。

( => ( = b_01_01 1 ) 
 ( and 
  ( != a_01_00 1 ) 
  ( != a_01_02 1 ) 
  ( != a_00_01 1 ) 
  ( != a_02_01 1 )
 ) 
)

次にそのマスに２が入る場合。これも簡単。隣接するマスには２がただひとつだけ入るということをSugarに教えます。

( => ( = b_01_01 2 )
 ( or 
  ( and
   ( = a_01_00 2 ) 
   ( != a_01_02 2 )
   ( != a_00_01 2 )
   ( != a_02_01 2 )
  )
  ( and 
   ( = a_01_02 2 ) 
   ( != a_01_00 2 ) 
   ( != a_00_01 2 ) 
   ( != a_02_01 2 ) 
  )
  ( and 
   ( = a_00_01 2 ) 
   ( != a_01_00 2 ) 
   ( != a_01_02 2 ) 
   ( != a_02_01 2 )
  )
  ( and 
   ( = a_02_01 2 ) 
   ( != a_01_00 2 ) 
   ( != a_01_02 2 ) 
   ( != a_00_01 2 )
  )
 )
)

次にそのマスに３が入る場合。隣接するマスには５がただひとつだけ入り、その５が入るマス以外には３も５も入りません。

( => ( = b_01_01 3 ) 
 ( or 
  ( and 
   ( = b_01_00 5 )
   ( != a_01_02 3 )
   ( != a_00_01 3 )
   ( != a_02_01 3 )
  )
  ( and 
   ( = b_01_02 5 ) 
   ( != a_01_00 3 ) 
   ( != a_00_01 3 ) 
   ( != a_02_01 3 ) 
  )
  ( and 
   ( = b_00_01 5 ) 
   ( != a_01_00 3 ) 
   ( != a_01_02 3 ) 
   ( != a_02_01 3 ) 
  )
  ( and 
   ( = b_02_01 5 )  
   ( != a_01_00 3 ) 
   ( != a_01_02 3 ) 
   ( != a_00_01 3 )
  )
 )
)

変数a_xx_yyと変数b_xx_yyが混在して見にくいと思いますけどすみません。もっと説明うまい人がSugar使いになってくれるといいんですけど。

とはいうものの、泣いてばかりいたってなんとかはなんとかなので、説明を続けます。次はひとつ飛ばしてそのマスに５が入る場合。この時は、「上下にはいずれも３が入り、左右いずれにも３も５も入らない」か、「左右にはいずれも３が入り、上下いずれにも３も５も入らない」が制約となります。以下のとおり。

( => ( = b_01_01 5 )
 ( or 
  ( and 
   ( = 3 b_01_00 ) 
   ( = 3 b_01_02 )  
   ( != 3 a_00_01 ) 
   ( != 3 a_02_01 )
  )
  ( and 
   ( = 3 b_00_01 ) 
   ( = 3 b_02_01 )  
   ( != 3 a_01_00 ) 
   ( != 3 a_01_02 ) 
  )
 ) 
)

４と６の場合は３と５の場合と同様ですね。６に関しては片方が４、片方が６になるので、逆転する場合も記述しなくてはいけません。以下のとおり。

( => ( = b_01_01 4 )
 ( or 
  ( and 
   ( = b_01_00 6 )
   ( != a_01_02 4 )
   ( != a_00_01 4 )
   ( != a_02_01 4 )
  )
  ( and 
   ( = b_01_02 6 )  
   ( != a_01_00 4 ) 
   ( != a_00_01 4 )
   ( != a_02_01 4 )
  )
  ( and 
   ( = b_00_01 6 )
   ( != a_01_00 4 )
   ( != a_01_02 4 ) 
   ( != a_02_01 4 ) 
  )
  ( and 
   ( = b_02_01 6 )
   ( != a_01_00 4 )
   ( != a_01_02 4 )
   ( != a_00_01 4 )
  )
 )
)

( => ( = b_01_01 6 )
 ( or 
  ( and 
   ( = 4 b_01_00 )
   ( = 6 b_01_02 )
   ( != 4 a_00_01 )
   ( != 4 a_02_01 )
  )
  ( and 
   ( = 6 b_01_00 )
   ( = 4 b_01_02 )
   ( != 4 a_00_01 )
   ( != 4 a_02_01 )
  )
  ( and 
   ( = 4 b_00_01 )
   ( = 6 b_02_01 )
   ( != 4 a_01_00 )
   ( != 4 a_01_02 )
  )
  ( and
   ( = 6 b_00_01 )
   ( = 4 b_02_01 )
   ( != 4 a_01_00 )
   ( != 4 a_01_02 )
  )
 )
)

以上で、同じ面積が隣り合わない１ｘｎのブロックを配置する、という制約が記述できました。ここでちょっとした注意として、四隅には５も６も入らないという制約が必要になります。ブロックの端が盤面外に出てしまうような状況を許すからです。こういうの忘れがち。

「境界線が十字にならない」は割と簡単で、２ｘ２のマスを取り出した時、十字いずれかが境界線にならなければいいですね。左上４マスを取り出します。

( or
 ( = a_00_00 a_01_00 )
 ( = a_00_01 a_01_01 )
 ( = a_00_00 a_00_01 )
 ( = a_01_00 a_01_01 )
)

さて、これまでの制約だと、以下のような別解が生じます。

これはルールをすべて記述できていないからで、「数字が二つ以上入るブロックはない」を記述すれば良いです。数字が二つ以上入るブロックが生じるためには、パズルがきちんと成立しているという仮定を置くなら、
・表出で、３にひとマス空いて３が入っている
・表出で、４にひとマス空いて４が入っている
・表出で、４にふたマス空いて４が入っている
という状況ですね。この状況に対し、「数字が二つ以上入るブロックはない」を実現するためには、その「？マス空いて」のところに別の数字が入ればよいということになります。
例題だと、「a_02_00のマスに３が入らない」ということを記述すればいいですね。

( != a_02_00 3)

以上で、全部の制約は記述できたはずなのですが、最後のところが、個人的には見通し悪いなーと思ってしまうわけです。
なんかうまい処理はないかなっと思っていますの。