バトルシップおもしろいよね
タイトルの通り、Sugar利用によるSATソルバーで、ペンシルパズルであるバトルシップを解くための記事です。
SAT ソルバーと Sugar については下の記事参照:
(いやたぶんググった方がいいと思うけど...)
ルール確認
バトルシップのルールは次の通りです (パズル同人誌「トケタ?」より引用):
1. 盤面のマスに沿って指定された艦をすべて配置します。波のマス上に艦が重なることはありません。
2. 盤面の外の数字は、その列で艦の入るマスの数を表します。
3. 異なる艦の入ったマスはタテヨコナナメに接しません。
なお、基本的に艦は幅 1 の長方形で、加えて端が丸みをおびていて、向きが分かる形状になっています。ただし今回は議論を分かりやすくするために、艦は単に長方形だと思ってください。なので、問題には艦影 (= 艦を構成するパーツ) の表出がないものとします。
また使用する艦は、おおむね
・1*1 が 4 個
・1*2 が 3 個
・1*3 が 2 個
・1*4 が 1 個
というように「1*k が b+1-k 個」というセットが多いです。これをサイズ b の 標準艦隊 (standard fleet) とよぶことにします。上の例はサイズ 4 ですね。なお、盤面サイズとの兼ね合いで、b = (3,) 4, 5 となることが多いです。
以下では、この標準艦隊を用いる問題を考えます。
取った作戦
バトルシップはいわゆる配置系のパズルです。なので「各マスについて艦が占有するかどうかを決める問題」と捉えることができます。よって、マスに対応する変数 x[i][j] を用意し、占有するなら 1, しないなら 0 とします。各マスについて、0 か 1 かのどちらかを決定したいわけですね。
では、与えられたヒントを制約の式に落とし込むことを考えましょう。まず、波のヒント (= 艦を置かない場所) や外周の表出は、この変数 x を使ってかんたんに表せます。なのであとは、「標準艦隊の配置をどのように表現するか」がカギになります。
今回取った作戦では、「艦がすべて幅 1 の長方形である」という事実を用いて、
作戦 A :幅 1 の長方形にどう限定するか
作戦 B :その上で、どうやって長さをうまくカウントするか
と問題を分割して考えます。
まず作戦 A について。バトルシップの初級手筋として「艦影どうしはナナメに接しない」というのがあります。
逆に、「艦影どうしはナナメに接しない」というルールを追加した上で、いくつかのマスに艦影を配置することを考えましょう。すると実は、艦影の連結成分 (= 艦) は自動的に、すべて幅 1 の長方形になります。
この事実を用いれば、作戦 A はクリアできます。すなわち、やるべきことは「ナナメの 2 マスの両方に艦影が入ることはない」という制約を書くだけです!
というわけで、あとは作戦 B を考えるのみです。長さのカウントをするには、艦影たちの連結性を調べる必要があります。そこで、一般に連結性を SAT に落とし込むときに使うのと同じように、根付き木を使用します。
といっても今回は、さっきのナナメ制約によって木の形状がほとんど決まっています。つまり、出てくる木はまっすぐなものしかありません。よって長さのカウントはかなり楽にできます。
具体的には、根の変数は用意せず、カウントのための変数 z[i][j] のみ用意します。値の範囲は 0 以上 b 以下 ( b は標準艦隊のサイズだった) としておきます。数字は、0 なら艦が無いことを表し、0 以外だと「左または上から数えた順番」を表すことにします。具体的には、次の図のような感じになります:
すると、この z[i][j] のみたすべき制約は、
・x[i][j] = 0 (艦影がない) ならば、 z[i][j] = 0
・x[i][j] = 1 (艦影がある) ならば、z[i][j] = z[i-1][j] + z[i][j-1] + 1
とかんたんな条件式で書けます。艦は向きがタテヨコありますが、足し算だといっしょに扱えるのがポイントです。
あとは、盤面全体で z[i][j] のうち 1, 2, ... , b が何個あるかカウントすれば、使用艦の制約を書き下せます。例として b = 3 (図のケース) ならば、1, 2, 3がそれぞれ 6, 3, 1 個あればよいですね。
これで無事、ルールを定式化できました!
なお唯一解チェックはいつもの通り、出てきた解を除外すればよいです。
実際に作ってみた
実際に実装し、トケタの問題や落ちていた問題を回してみたところ、ほとんどの問題を一瞬で解いてしまいました!一番かかったのはトケタ 4 の座談会問題 (10*10, b = 5) ですが、それも 15 秒程度で解けました (解自体は 3 秒 → 唯一解チェックに 15 秒)。サイズでいえば、Puzzle Picnic に 12*12, b = 5 の星 5 の作品がありましたが、これも瞬殺です。超優秀!
性能が良かった理由を考察しておきます。
・連結性を見たのに、実質的には変数が増えていません。たしかに変数 z を加えたものの、 x を決めてしまえばただちに確定します (というかただちに確定するような作戦を取ったのがえらい!)。よって、本質的には二値の変数がマスの個数しかないので、SAT ソルバーくんも安心して探索できた気がします。
・そもそも定式化の時点で、すでに手筋としてナナメ禁を入れているのも、大きいかもしれませんね。
さらなる発展
まず、今回省いた艦影自体の表出ですが、これは z[i][j] への制約として比較的すぐに表せそうです。たとえば艦の端の U 字形 だと、「自分が z > 0 なこと」および「上下 (左右) が正かどうか」を制約として入れればよいです。他の形でも同様ですね。なのですぐに実装できそうです (めんどうではあるので、あとでやる...)
パズルそのものについて。バトルシップは、どうしても試行錯誤が必要なパートが出てきがちです。なので唯一解チェックには相当役立つと思います。また、試行錯誤だけの闇問も生成できるかも...!
ぜひ公開して使えるようにしたいのですが、まだぱずりんくで公開されていないのと、情報の知識に乏しいことから、良い感じに公開できません。どうしたもんか... 一応ファイルだけなら公開できるかもです (これもまたあとで...)。
変種対応について。 Weighted ならできそうですが、カウント方法を変える必要がありりそうです。具体的には、艦影が自分の長さを把握できるようにしないといけません。今のままだと左や上の艦影はできてないですよね。これをどう扱うか。別のカウント方法か、実質無の変数を追加するか、、、
右下からカウントして足したら (艦のサイズ+1) になるというウルトラ C を思いつきましたが、さすがに効率落ちるかなぁ...
最後に、他の配置系パズルについて。
上でもちらっと言いましたが、配置系パズルは単一配置であれば SAT ソルバーくんとものすごく相性がいいです。しかしペントミノプレースのように複数配置のものは、配置するものを管理する必要があり、SAT ではなかなか表現が難しいのではないかと予想しています。
今回のバトルシップではうまく配置を管理できましたが、かなり艦の特殊性を利用しています。なので「じゃあペントミノだとどうするの?」ってなったらわりとお手上げです。つまり、配置したものがどの種類かを判定するのがかなり大変だと思います。今回みたいな作戦がうまく使えないのかなぁ。
なお、ペントミノ系で言うと、分割系ではあるのですがファイブセルズがまだマシかなと思ってます。これはペントミノの種類は無視できるためです。まあそもそも分割系が闇っぽいのでなんとも言えないですけどね...
というわけで以上です。とりあえず、完全版を作ること、別のカウント方法を考えてみること、それらを公開すること、などが残りの作業ですかね。気が向いたらやります。あとは、他のペンパも思いつきしだい実装できたらいいな。
視聴者プレゼント
ここまで読んでくださったみなさんのために、特別にバトルシップの問題を用意しました!
ぜひ解いてみてね!