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
Unique solutions (deduplicating piece-pair swaps): 24
── Solution 1 ──
0 1 2 3 4
0 . K . . N
1 . . . . B
2 . . R . .
3 Q . . . .
4 . . . R .
5 . B . . N
King: (0,1)
Queen: (3,0)
Bishop1: (5,1) [light]
Bishop2: (1,4) [dark]
Knight1: (5,4)
Knight2: (0,4)
Rook1: (4,3)
Rook2: (2,2)
── Solution 2 ──
0 1 2 3 4
0 N . . K .
1 B . . . .
2 . . R . .
3 . . . . Q
4 . R . . .
5 N . . B .
King: (0,3)
Queen: (3,4)
Bishop1: (5,3) [light]
Bishop2: (1,0) [dark]
Knight1: (5,0)
Knight2: (0,0)
Rook1: (4,1)
Rook2: (2,2)
...
── Solution 24 ──
0 1 2 3 4
0 B . . B .
1 N . . . .
2 . . . . Q
3 . . R . .
4 . R . . .
5 N . . K .
King: (5,3)
Queen: (2,4)
Bishop1: (0,0) [light]
Bishop2: (0,3) [dark]
Knight1: (5,0)
Knight2: (1,0)
Rook1: (3,2)
Rook2: (4,1)
Here’s the code.
"""
Chess Puzzle Solver using Z3
Place king, queen, 2 bishops, 2 knights, 2 rooks on a 6×5 board
such that:
- The two bishops are on opposite-colored squares
- No piece attacks any other piece
"""
from z3 import (
Int, Solver, Or, And, Not, Distinct, If,
sat, ForAll, Implies
)
import itertools
ROWS = 6
COLS = 5
TOTAL_CELLS = ROWS * COLS # 30
PIECES = ["king", "queen", "bishop1", "bishop2", "knight1", "knight2", "rook1", "rook2"]
N = len(PIECES) # 8 pieces
def cell(r, c):
return r * COLS + c
def pos_to_rc(pos):
return pos // COLS, pos % COLS
def color(r, c):
"""Square color: 0=light, 1=dark"""
return (r + c) % 2
def attacks_king(r1, c1, r2, c2):
return max(abs(r1 - r2), abs(c1 - c2)) == 1
def attacks_queen(r1, c1, r2, c2):
return (r1 == r2 or c1 == c2 or
abs(r1 - r2) == abs(c1 - c2))
def attacks_bishop(r1, c1, r2, c2):
return abs(r1 - r2) == abs(c1 - c2)
def attacks_rook(r1, c1, r2, c2):
return r1 == r2 or c1 == c2
def attacks_knight(r1, c1, r2, c2):
dr, dc = abs(r1 - r2), abs(c1 - c2)
return (dr == 1 and dc == 2) or (dr == 2 and dc == 1)
ATTACK_FN = {
0: attacks_king,
1: attacks_queen,
2: attacks_bishop,
3: attacks_bishop,
4: attacks_knight,
5: attacks_knight,
6: attacks_rook,
7: attacks_rook,
}
def solve_all():
solutions = []
pos = [Int(f"pos_{p}") for p in PIECES]
s = Solver()
for p in pos:
s.add(p >= 0, p < TOTAL_CELLS)
s.add(Distinct(*pos))
b1_color = (pos[2] / COLS + pos[2] % COLS) % 2 # Z3 integer arithmetic
b2_color = (pos[3] / COLS + pos[3] % COLS) % 2
s.add((pos[2] / COLS + pos[2] % COLS) % 2 != (pos[3] / COLS + pos[3] % COLS) % 2)
for i, j in itertools.combinations(range(N), 2):
fn_i = ATTACK_FN[i]
fn_j = ATTACK_FN[j]
forbidden = []
for r1, c1 in itertools.product(range(ROWS), range(COLS)):
for r2, c2 in itertools.product(range(ROWS), range(COLS)):
if (r1, c1) == (r2, c2):
continue
if fn_i(r1, c1, r2, c2) or fn_j(r2, c2, r1, c1):
forbidden.append((cell(r1, c1), cell(r2, c2)))
if forbidden:
s.add(And([
Not(And(pos[i] == ci, pos[j] == cj))
for ci, cj in forbidden
]))
solution_count = 0
while s.check() == sat:
m = s.model()
sol = [m[pos[k]].as_long() for k in range(N)]
solutions.append(sol)
solution_count += 1
s.add(Or([pos[k] != sol[k] for k in range(N)]))
if solution_count % 10 == 0:
print(f" Found {solution_count} solutions so far...")
return solutions
def print_board(sol):
board = [["." for _ in range(COLS)] for _ in range(ROWS)]
symbols = ["K", "Q", "B", "B", "N", "N", "R", "R"]
for k, p in enumerate(sol):
r, c = pos_to_rc(p)
board[r][c] = symbols[k]
print(" " + " ".join(str(c) for c in range(COLS)))
for r in range(ROWS):
print(f"{r} " + " ".join(board[r]))
def canonicalize(sol):
"""
Produce a canonical form to deduplicate solutions where
bishop1/bishop2, knight1/knight2, rook1/rook2 are interchangeable.
Returns a frozenset-based key.
"""
king_pos = sol[0]
queen_pos = sol[1]
bishops = tuple(sorted([sol[2], sol[3]]))
knights = tuple(sorted([sol[4], sol[5]]))
rooks = tuple(sorted([sol[6], sol[7]]))
return (king_pos, queen_pos, bishops, knights, rooks)
def main():
print("Solving chess puzzle on 6×5 board...")
print("Pieces: King, Queen, 2 Bishops (opposite colors), 2 Knights, 2 Rooks")
print("Constraint: No piece attacks another\n")
solutions = solve_all()
seen = {}
for sol in solutions:
key = canonicalize(sol)
if key not in seen:
seen[key] = sol
unique = list(seen.values())
print(f"\nTotal raw solutions: {len(solutions)}")
print(f"Unique solutions (deduplicating piece-pair swaps): {len(unique)}\n")
for idx, sol in enumerate(unique, 1):
print(f"── Solution {idx} ──")
print_board(sol)
labels = ["King", "Queen", "Bishop1", "Bishop2", "Knight1", "Knight2", "Rook1", "Rook2"]
for k, p in enumerate(sol):
r, c = pos_to_rc(p)
col_name = "light" if color(r, c) == 0 else "dark"
sq = f"({r},{c})"
extra = f" [{col_name}]" if "Bishop" in labels[k] else ""
print(f" {labels[k]}: {sq}{extra}")
print()
if __name__ == "__main__":
main()
Related post: Lessons Learned With the Z3 SAT/SMT Solver