この記事では、AIモデルClaudeを用いて、6×5のチェス盤上にキング、クイーン、ビショップ2、ナイト2、ルーク2を配置し、どの駒も互いを攻撃しないようにするパズルを解くためのZ3/Pythonコードを生成する方法を紹介しています。

過去の投稿では、ClaudeとChatGPTでPrologコードを生成しましたが、今回はZ3/Pythonに挑戦します。

パズルの条件は以下の通りです：

• 6×5のチェス盤に、キング、クイーン、ビショップ2、ナイト2、ルーク2を配置する。
• 2つのビショップは必ず異なる色のマスに配置する。
• どの駒も他の駒を攻撃しないようにする。

生成されたコードは192個の解を見つけました。これは、ビショップ、ナイト、ルークのペアの入れ替えによる8通りの組み合わせと、ユニークな配置24通りから構成されます。

記事では、これらの解の例と、パズルを解くためのZ3/Pythonコード全体も公開されています。

関連投稿として、「Z3 SAT/SMTソルバーで学んだこと」も紹介されています。