後日談
先の記事の続きです。まだ読んでない人は、そちらを先にお読みください。
艦を表出させよう
まず、艦影の種類を考慮できるようになりました。これで、艦影の表出した問題も解けます！つまり、普通の艦隊を使う問題なら、テキストで入力さえすれば、どんな問題も半自動で解けます。やったね！！！
技術的には特に難しいところはなく、前の記事では「z の制約として...」とか書いてましたが、普通に x の制約として表せました。おわり。
ちなみに、速度は変わらない (むしろ艦影を表出させると、制約が強いため早くなる？) ようです。
ここから得られる教訓は
・議論を単純化してとりあえず実装してみるのは、よい試み
・面倒なことはだいたい面倒なだけでむずかしくないので、さっさとやろう
でした。ありがとうございました。
得手不得手
かなり強力なソルバーが作れましたが、残念ながら解けないものもあります。
Sugar を使ったソルバー全般に言えることですが、大域手筋を利用したものはハマりやすい印象です。実際、次の問題が 20 分かけても解けませんでした：
有料の冊子でもないので別に公開してもいいだろうということで、バトルシップを公開します。難度はLv.5+。https://t.co/G7oX9iObsn pic.twitter.com/jOkqzwo0s1
— あーく (@ark184) 2019年11月16日
この問題は完全に理詰めで解けるのですが (考えてみよう！)、仕組まれた理詰めの道をSAT ソルバーくんは当然見つけられず、解の海で溺れてしまうようです。純粋にヒントによる制約が減ってしまうのも痛いでしょうね。人間がある程度解いて補助してあげれば、ソルバーくんでも解き切れるかもしれません。
一方、試行錯誤は得意です (これも当然ですが)。
流行に乗って、私の代表作を4枚。ルールは省略。魑魅魍魎。 pic.twitter.com/9u4ddQfo7s
— あーく (@ark184) 2019年3月31日
このツイートにある 1 枚目の問題は 17 秒で解発見＋30秒で唯一解判定、でした。一方、4 枚目の方は 3分ちょっとで解発見＋6 分で唯一解判定、と結構な時間がかかっています(理詰め問)。
まあそれでも、実際に人間が解くことを思えば、圧倒的なスピードといえるでしょう。
織姫も彦星も、望遠鏡で見ればただの星。。。
完全版の公開
一応それなりに完成形を迎えたわけですが、現在どういう形で公開するか、そもそも公開しなくてもいいか、など思案中です。少々おまちください。
闇をおかわり
代わりに問題をいくつか作ったので投げておきますね (Twitterに投稿したもののまとめです)。
難易度はよく分かりません。7638 のはたぶんできる。
もともとソルバーというおもちゃで遊ぶの大好きだったので、自分でおもちゃを作れたのはちょっとうれしいどころか感動してますね。
そういえば
ペンパアドベント B ってまだ全部埋まってないんですね。とくに明日とか...あれ？
