博士

ロボ子、LinkedIn Queensパズルって知ってるか？N×NのグリッドにN個のクイーンを配置するパズルなんじゃ。

ロボ子

はい、博士。各行、列、領域にクイーンが1つずつ配置される必要があって、クイーンは同じ対角線上に配置できるけど、隣接する対角線上には配置できないんですよね。

博士

そうそう！それをRyan Bergerって人がSATソルバーで解いたらしいぞ。例えば「3行目にクイーンが1つ」みたいな性質を、たくさんのブール節で表現するんじゃ。

ロボ子

SATソルバーですか。初めて聞きました。

博士

SATソルバーよりもっと高レベルなSMTソルバーってのもあるんじゃ。ブール変数だけじゃなくて、もっと色々なデータ型を扱えるらしいぞ。

ロボ子

なるほど。記事によると、SATレベルよりもSMTレベルで問題を解決する方が容易なのですね。

博士

その通り！Z3っていうPython APIを使って同じ問題を解くデモを作ったらしいぞ。クイーンの位置をN個の整数としてエンコードするんじゃ。例えば`q_0 = 5`は0行目のクイーンが5列目に配置されているって意味だ。

ロボ子

`IntVector(str, n)`を使ってn個の整数変数を一度に作成できるんですね。そして、`Distinct`制約を使って、すべての整数が異なる値を持つように強制する、と。

博士

そう！各列に最大1つのクイーンしか置けないようにするんじゃ。さらに、各クイーンについて、左下か右下の角にクイーンが存在しないように制約を追加する(`q_3 != q_2 ± 1`)。

ロボ子

領域の制約は手動でコーディングする必要があるんですね。それは少し大変そうですね。

博士

じゃろ？「各領域にクイーンが1つ存在する」っていう制約を、「領域1にクイーンが存在する OR 領域2にクイーンが存在する OR ...」みたいに表現するんじゃ。

ロボ子

SMTソルバーでLinkedIn Queensパズルを正しく解決できたんですね。生のSATソルバーよりも処理速度は遅いと予想されるけど、SMTで問題を解決する方がSATよりも容易、と。

博士

そうそう。領域のエンコードミスを防ぐために、小さなテストとチェックを追加することも重要じゃ。すべてのマスが領域に含まれているか、同じマスが複数の領域に含まれていないかをチェックするんじゃ。

ロボ子

なるほど。領域を出力して、ボードの図と比較して正しいことを確認するのも良いですね。

博士

ロボ子、今日はよく頑張ったのじゃ！最後に一つなぞなぞじゃ！クイーンがたくさんいる国はどこじゃ？

ロボ子

えっと…、女王様（Queen）がたくさんいる国…ですか？

博士

正解は…イギリス（Eek-ギリス）！…つまらんかったかの？

ロボ子

あはは。博士らしいオチですね！