Generating Z3/Python code with Claude

(832) 422-8646

Contact

I’ve written a couple posts lately on getting an LLM to generate code to solve chess problems. The first used Claude to generate Prolog and the second used ChatGPT to generate Prolog. This post will use Claude to generate Z3/Python code.

The puzzle is one I’ve written about before:

Place all the pieces—king, queen, two bishops, two knights, and two rooks—on a 6 × 5 chessboard, with the requirement that the two bishops be on opposite colored squares and no piece is attacking another.

Incidentally, it’s common for "piece" to exclude pawns, as above. But then what do you call all the things on a chessboard? You might call them "chess pieces," in which case a pawn is a "chess piece" but not a "piece." One convention is to use "chessmen" or simply "men" to include pieces and pawns.

This was the prompt I used.

Write Z3/Python code to find all solutions to the following chess puzzle.

Place all the pieces—king, queen, two bishops, two knights, and two rooks—on a 6 × 5 chessboard, with the requirement that the two bishops be on opposite colored squares and no piece is attacking another.

The code found 192 = 8 × 24 solutions. The factor of 8 comes from 23 ways of swapping the pairs of bishops, knights, and rooks. The script reports

Total raw solutions: 192<br>Unique solutions (deduplicating piece-pair swaps): 24

── Solution 1 ──<br>0 1 2 3 4<br>0 . K . . N<br>1 . . . . B<br>2 . . R . .<br>3 Q . . . .<br>4 . . . R .<br>5 . B . . N<br>King: (0,1)<br>Queen: (3,0)<br>Bishop1: (5,1) [light]<br>Bishop2: (1,4) [dark]<br>Knight1: (5,4)<br>Knight2: (0,4)<br>Rook1: (4,3)<br>Rook2: (2,2)

── Solution 2 ──<br>0 1 2 3 4<br>0 N . . K .<br>1 B . . . .<br>2 . . R . .<br>3 . . . . Q<br>4 . R . . .<br>5 N . . B .<br>King: (0,3)<br>Queen: (3,4)<br>Bishop1: (5,3) [light]<br>Bishop2: (1,0) [dark]<br>Knight1: (5,0)<br>Knight2: (0,0)<br>Rook1: (4,1)<br>Rook2: (2,2)

...

── Solution 24 ──<br>0 1 2 3 4<br>0 B . . B .<br>1 N . . . .<br>2 . . . . Q<br>3 . . R . .<br>4 . R . . .<br>5 N . . K .<br>King: (5,3)<br>Queen: (2,4)<br>Bishop1: (0,0) [light]<br>Bishop2: (0,3) [dark]<br>Knight1: (5,0)<br>Knight2: (1,0)<br>Rook1: (3,2)<br>Rook2: (4,1)

Here’s the code.

"""<br>Chess Puzzle Solver using Z3<br>Place king, queen, 2 bishops, 2 knights, 2 rooks on a 6×5 board<br>such that:<br>- The two bishops are on opposite-colored squares<br>- No piece attacks any other piece<br>"""

from z3 import (<br>Int, Solver, Or, And, Not, Distinct, If,<br>sat, ForAll, Implies<br>import itertools

ROWS = 6<br>COLS = 5<br>TOTAL_CELLS = ROWS * COLS # 30

PIECES = ["king", "queen", "bishop1", "bishop2", "knight1", "knight2", "rook1", "rook2"]<br>N = len(PIECES) # 8 pieces

def cell(r, c):<br>return r * COLS + c

def pos_to_rc(pos):<br>return pos // COLS, pos % COLS

def color(r, c):<br>"""Square color: 0=light, 1=dark"""<br>return (r + c) % 2

def attacks_king(r1, c1, r2, c2):<br>return max(abs(r1 - r2), abs(c1 - c2)) == 1

def attacks_queen(r1, c1, r2, c2):<br>return (r1 == r2 or c1 == c2 or<br>abs(r1 - r2) == abs(c1 - c2))

def attacks_bishop(r1, c1, r2, c2):<br>return abs(r1 - r2) == abs(c1 - c2)

def attacks_rook(r1, c1, r2, c2):<br>return r1 == r2 or c1 == c2

def attacks_knight(r1, c1, r2, c2):<br>dr, dc = abs(r1 - r2), abs(c1 - c2)<br>return (dr == 1 and dc == 2) or (dr == 2 and dc == 1)

# Map piece index to its attack function<br>ATTACK_FN = {<br>0: attacks_king,<br>1: attacks_queen,<br>2: attacks_bishop,<br>3: attacks_bishop,<br>4: attacks_knight,<br>5: attacks_knight,<br>6: attacks_rook,<br>7: attacks_rook,

def solve_all():<br>solutions = []

# Each piece gets an integer position in [0, TOTAL_CELLS)<br>pos = [Int(f"pos_{p}") for p in PIECES]

s = Solver()

# All positions in valid range<br>for p in pos:<br>s.add(p >= 0, p<br>Related post : Lessons Learned With the Z3 SAT/SMT Solver

Leave a Reply<br>Your email address will not be published. Required fields are marked *<br>Comment *<br>Name *

Email *

Website

Search for:

John D. Cook, PhD

My colleagues and I have decades of consulting experience helping companies solve complex problems involving data privacy, applied math, and statistics.

Let’s talk. We look forward to exploring the opportunity to help your company too.