All pieces on a 6 by 5 board

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 2³ ways of swapping the pairs of bishops, knights, and rooks. The script reports

Total raw solutions: 192Unique solutions (deduplicating piece-pair swaps): 24 Solution 1 0 1 2 3 40 . K . . N1 . . . . B2 . . 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 40 N . . K .1 B . . . .2 . . R . .3 . . . . Q4 . 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 40 B . . B .1 N . . . .2 . . . . Q3 . . 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 Z3Place king, queen, 2 bishops, 2 knights, 2 rooks on a 6*5 boardsuch 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 itertoolsROWS = 6COLS = 5TOTAL_CELLS = ROWS * COLS # 30PIECES = ["king", "queen", "bishop1", "bishop2", "knight1", "knight2", "rook1", "rook2"]N = len(PIECES) # 8 piecesdef cell(r, c): return r * COLS + cdef pos_to_rc(pos): return pos // COLS, pos % COLSdef color(r, c): """Square color: 0=light, 1=dark""" return (r + c) % 2def attacks_king(r1, c1, r2, c2): return max(abs(r1 - r2), abs(c1 - c2)) == 1def 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 == c2def 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)# Map piece index to its attack functionATTACK_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 = [] # Each piece gets an integer position in [0, TOTAL_CELLS) pos = [Int(f"pos_{p}") for p in PIECES] s = Solver() # All positions in valid range for p in pos: s.add(p >= 0, p < TOTAL_CELLS) # All pieces on distinct squares s.add(Distinct(*pos)) # Bishops on opposite colors # bishop1 = pos[2], bishop2 = pos[3] # color of pos = ((pos // COLS) + (pos % COLS)) % 2 b1_color = (pos[2] / COLS + pos[2] % COLS) % 2 # Z3 integer arithmetic b2_color = (pos[3] / COLS + pos[3] % COLS) % 2 # Z3 doesn't do Python //; use integer division carefully # We'll encode opposite colors: sum of colors == 1 # color(pos) = (row + col) % 2 = (pos//COLS + pos%COLS) % 2 # For Z3 int vars, use: (pos / COLS + pos % COLS) % 2 s.add((pos[2] / COLS + pos[2] % COLS) % 2 != (pos[3] / COLS + pos[3] % COLS) % 2) # No piece attacks another # We enumerate all (i,j) pairs and for each possible (pos_i, pos_j) assignment, # assert that those pieces don't attack each other. # Since positions are Z3 vars, we use a constraint table approach: # For each pair (i,j), add constraints over all concrete (r1,c1,r2,c2) combos. # Pre-build attack lookup tables for each piece-type pair # This avoids slow Z3 symbolic reasoning over large disjunctions. # We'll encode: for all concrete assignments, if pos[i]==cell(r1,c1) and pos[j]==cell(r2,c2), # then piece i must not attack piece j. # Equivalently: NOT (pos[i]==cell(r1,c1) AND pos[j]==cell(r2,c2)) for all attacking pairs. # For efficiency, we build a set of "forbidden (cell_i, cell_j)" pairs per piece pair. 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 # i attacks j or j attacks i if fn_i(r1, c1, r2, c2) or fn_j(r2, c2, r1, c1): forbidden.append((cell(r1, c1), cell(r2, c2))) if forbidden: # Add: NOT (pos[i] == ci AND pos[j] == cj) for each forbidden pair s.add(And([ Not(And(pos[i] == ci, pos[j] == cj)) for ci, cj in forbidden ])) # Enumerate all solutions 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 # Block this solution (and symmetric duplicates via blocking exact assignment) 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 solutionsdef 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() # Deduplicate by canonical form 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

The post All pieces on a 6 by 5 board first appeared on John D. Cook.