All pieces on a 6 by 5 board
The author describes using Claude (an LLM) to generate Z3/Python code that solves a chess puzzle: placing all pieces (king, queen, two rooks, two bishops, two knights) on a 6x5 board. This follows previous posts where Claude and ChatGPT were used to generate Prolog code for similar chess problems.
Background
John D. Cook is a mathematician and software engineer who blogs about applied math, computing, and technical puzzles. This post is part of an informal series testing whether large language models (LLMs) like Claude and ChatGPT can generate correct code for logic puzzles.
The specific puzzle: place all six standard chess pieces (king, queen, two bishops, two rooks, two knights — actually eight pieces, but the "two" for bishops/rooks/knights explains the count) on a 6×5 board without any piece attacking another. This is a classic constraint satisfaction problem.
Z3 is a popular theorem prover / SMT (Satisfiability Modulo Theories) solver from Microsoft Research. It lets you describe logical constraints that a solution must satisfy, and it finds a solution automatically. Z3/Python means Cook prompted Claude to write a Python script that uses the Z3 library to solve the puzzle.
The post describes how well Claude did at generating correct Z3 code from a natural-language description of the puzzle rules, continuing the author's exploration of LLMs as programming assistants for logic problems.