ぼんさんが好きだ。あるいはぼんさんをsugar制約ソルバーで解く

ぼんさんというパズルがあります。
詳しくはニコリのぼんさんの紹介のページをどうぞ。
今回は、ぼんさんをsugar制約ソルバーを使用して解いてみたいと思います。

サンプルはこちら。ちょっとサイズが大きいですが。
20140428191055

答えはこんな。
20140428191054

盤面に以下のように座標を設定します。
20140428191053
各○に対して番号を付けます。各○の移動後の座標を変数として、sugar先生にこれを探してもらうことにします。

手順を先に書いておくと、
1. 変数を定義する。
2. 縦横にまっすぐ移動することを制約に落とす。
3. ある○の移動後の座標に対し、点対称の位置にどれか別の移動後の○が存在する。
4. 各○の移動の軌道上に、他の○の移動前、移動後それぞれの位置が存在しない。
5. 任意の2つの○に対し、その移動の軌道が交差しない。
となります。
4と5を分割したのはその方が見通しがいいかなーと思ったからなのですが、効果的かどうかはちょっと自信がありません。

それではいつものように1.の変数定義です。サンプル問題を変換すると以下のようになります。

( int x00 0 63 )
( int x01 0 63 )
( int x02 0 63 )
( int x03 0 63 )
( int x04 0 63 )
( int x05 0 63 )
( int x06 0 63 )
( int x07 0 63 )

( alldifferent x00 x01 x02 x03 x04 x05 x06 x07 )

番号は座標の若い順に付けています。以下に示すスクリプト内には登場しませんが、「移動前の各○の座標」を示しておきます。

x00の移動前の座標 → y00=3
x01の移動前の座標 → y01=10
x02の移動前の座標 → y02=13
x03の移動前の座標 → y03=32
x04の移動前の座標 → y04=38
x05の移動前の座標 → y05=48
x06の移動前の座標 → y06=56
x07の移動前の座標 → y07=60


次に、2.縦横にまっすぐ進むということを制約に落とします。

( or ( = 3 ( % x00 8 ) ) ( = 0 ( / x00 8 ) ) )
( or ( = 2 ( % x01 8 ) ) ( = 1 ( / x01 8 ) ) )
( or ( = 5 ( % x02 8 ) ) ( = 1 ( / x02 8 ) ) )
( or ( = 0 ( % x03 8 ) ) ( = 4 ( / x03 8 ) ) )
( or ( = 6 ( % x04 8 ) ) ( = 4 ( / x04 8 ) ) )
( or ( = 0 ( % x05 8 ) ) ( = 6 ( / x05 8 ) ) )
( or ( = 0 ( % x06 8 ) ) ( = 7 ( / x06 8 ) ) )
( or ( = 4 ( % x07 8 ) ) ( = 7 ( / x07 8 ) ) )

面倒なので全部書いてしまいましたが、移動距離が明示されている○に関しては移動場所は最大でも上下左右いずれかの4つですね。○00に関してこの制約を記述してみます。盤外に出てしまうような移動はこの時点で削っています。

( or 
 ( = x00 6 )
 ( = x00 27 )
 ( = x00 0 )
)

移動距離が明示されている○に関して、すべて書き並べてください


さて次は、3.ある○の移動後の座標に対し、点対称の位置にどれか別の移動後の○が存在する、を記述します。座標の付け方からこれは簡単です。たとえば○00の場合は以下のようになります。

( or 
 ( = x00 ( - 63 x01 ) )
 ( = x01 ( - 63 x00 ) )
 ( = x00 ( - 63 x02 ) )
 ( = x02 ( - 63 x00 ) )
 ( = x00 ( - 63 x03 ) )
 ( = x03 ( - 63 x00 ) )
 ( = x00 ( - 63 x04 ) )
 ( = x04 ( - 63 x00 ) )
 ( = x00 ( - 63 x05 ) )
 ( = x05 ( - 63 x00 ) )
 ( = x00 ( - 63 x06 ) )
 ( = x06 ( - 63 x00 ) )
 ( = x00 ( - 63 x07 ) )
 ( = x07 ( - 63 x00 ) )
)

考慮している○の移動後の座標が、盤面サイズの半分より大きいか小さいかで場合分けされるのですが、面倒なので全部書き並べてます。
すべての○に対してこの記述を行います。まともにやると、たぶん半分は無駄な記述ですけどそのへんは気にしない方針で。


続いて4. 各○の移動の軌道上に、他の○の移動前、移動後それぞれの位置が存在しない、です。
ある○が、上下左右いずれに移動するかで場合分けします。
左右方向に移動する場合は、軌道上のマスの座標は区間で表現できます。下の図を参考にしてください。
20140428191056
35の位置にある○が左に移動して33の位置に来たとすると、この軌道上のマスは33以上35以下になりますね。スクリプトではこれを逆に表現して、「他の○の始点と終点は33より小さくなるか、35より大きくなる」として記述しています。
x00が右側に移動するとき、その軌道上に他の○の始点および終点が存在しない、を、以下のように書きました。

; move r
( => ( and ( < 3 x00 ) ( > 8 ( - x00 3 ) ) )
 ( and 
  ( or ( < x01 3 ) ( > x01 x00 ) )
  ( or ( < 10 3 ) ( > 10 x00 ) )
  ( or ( < x02 3 ) ( > x02 x00 ) )
  ( or ( < 13 3 ) ( > 13 x00 ) )
  ( or ( < x03 3 ) ( > x03 x00 ) )
  ( or ( < 32 3 ) ( > 32 x00 ) )
  ( or ( < x04 3 ) ( > x04 x00 ) )
  ( or ( < 38 3 ) ( > 38 x00 ) )
  ( or ( < x05 3 ) ( > x05 x00 ) )
  ( or ( < 48 3 ) ( > 48 x00 ) )
  ( or ( < x06 3 ) ( > x06 x00 ) )
  ( or ( < 56 3 ) ( > 56 x00 ) )
  ( or ( < x07 3 ) ( > x07 x00 ) )
  ( or ( < 60 3 ) ( > 60 x00 ) )
 )
)

他の○の始点に関しては固定されているので、あってもなくてもよろしい条件が残っていますが、ま特に気にしない方針で。(再び)

上下方向の移動は、区間から外れるという条件だけでは表現できませんが、区間から外れてしかも縦方向の軌道からも外れる、という制約を加えればOKです。下の図を参照してください。
20140428191057
35の位置から上に移動して11まで動くとします。単純に11と35を両端にして区間を作ると、深緑色を付けた区間になります。そこから、35を含むタテ列を除外するような条件をつければよろしい。

; move u
( => ( and ( > 3 x00 ) ( < 7 ( - 3 x00 ) ) )
 ( and 
  ( or ( > x01 3 ) ( < x01 x00 ) ( != ( % x01 8 ) ( % x00 8 ) ) )
  ( or ( > 10 3 ) ( < 10 x00 ) ( != 2 ( % x00 8 ) ) )
  ( or ( > x02 3 ) ( < x02 x00 ) ( != ( % x02 8 ) ( % x00 8 ) ) )
  ( or ( > 13 3 ) ( < 13 x00 ) ( != 5 ( % x00 8 ) ) )
  ( or ( > x03 3 ) ( < x03 x00 ) ( != ( % x03 8 ) ( % x00 8 ) ) )
  ( or ( > 32 3 ) ( < 32 x00 ) ( != 0 ( % x00 8 ) ) )
  ( or ( > x04 3 ) ( < x04 x00 ) ( != ( % x04 8 ) ( % x00 8 ) ) )
  ( or ( > 38 3 ) ( < 38 x00 ) ( != 6 ( % x00 8 ) ) )
  ( or ( > x05 3 ) ( < x05 x00 ) ( != ( % x05 8 ) ( % x00 8 ) ) )
  ( or ( > 48 3 ) ( < 48 x00 ) ( != 0 ( % x00 8 ) ) )
  ( or ( > x06 3 ) ( < x06 x00 ) ( != ( % x06 8 ) ( % x00 8 ) ) )
  ( or ( > 56 3 ) ( < 56 x00 ) ( != 0 ( % x00 8 ) ) )
  ( or ( > x07 3 ) ( < x07 x00 ) ( != ( % x07 8 ) ( % x00 8 ) ) )
  ( or ( > 60 3 ) ( < 60 x00 ) ( != 4 ( % x00 8 ) ) )
 )
)

さて最後に、5. 任意の2つの○に対し、その移動の軌道が交差しない。を記述します。始点と終点を除いた軌道が重なる、という条件を付けると、その2つの○の位置関係は、次の2パターンに限定されます。
20140428191058

前者を右下がりの関係、後者を左下がりの関係と呼びます。

右下がりの関係について考えます。図のようにAからDと名前を付けます。AとBに関しては、○とマスにともにAとBという名前がついていると思ってください。
20140428191059

右下がりの関係で軌道が交差するとしたら、「Aが右に移動し、かつ、Bが上に移動する」か、あるいは、「Bが左に移動し、Aが下に移動する」という状態しか起きません。前者に関してはAとBがともにCのマスを越えて移動した場合、後者に関してはAとBがともにDのマスを越えて移動した場合に交差が発生します。
前者と後者で場合分けします。都合により、「Aが右に移動する場合」と「Bが左に移動する場合」で場合分けを行います。
「Aが右に移動する」という仮定のもと、下図をご覧ください。
20140428191100

35がA、53がB、37がCに対応します。Aが右に移動する場合、AがCを越えないようにするためには、Aの終点の座標が37以下ならば良いです。これはわかりやすいですね。で、Aが右に移動するという条件なので、53が左か右か下に移動したなら、これらは自動的に交差しないことが確定します。左か右か下に移動するなら、いずれも37以上の座標になります。Bが上に移動したとき37を越えないようにするためには、Bの終点の座標が37以上ならばよいです。
まとめると、右下がりの関係でAが右に移動する場合には、Aの座標がC以下、あるいはBの座標がC以上であるという条件をつければ、交差することはなくなります。(以上以下をわりとラフに使ったので、端の議論がいい加減ですが、適切に汲んでください)

次に「Bが左に移動する」場合。図だけ示します。
20140428191052


もとの問題図で右下がりの関係にあるx00とx02について、この制約を書き下してみます。以下のようになるでしょう。

( => ( and ( < 3 x00 ) ( > 8 ( - x00 3) ) ) 
 ( or ( < x00 5 ) ( > x02 5 ) ) )
( => ( and ( > 13 x02 ) ( > 8 ( - 13 x02 ) ) ) 
 ( or ( < x00 11 ) ( > x02 11 ) ) )

左下がりの関係も同様です。x00とx01の記述だけ書きます。

( => ( and ( > 3 x00 ) ( > 8 ( - 3 x00 ) ) ) 
 ( or ( > x00 2 ) ( > x01 2 ) ) )
( => ( and ( < 10 x01 ) ( > 8 ( - x01 10) ) ) 
 ( or ( < x00 11 ) ( > x01 11 ) ) )


以上で、sugar先生に頑張ってもらうお膳立ては完了したはず。サンプルは私の環境で数秒で解答が返ってきましたが、大きくしたらどうなるんでしょうねえ……
ということで今回はここまで。