Chess puzzle by Martin Gardner: Place a queen, king, bishop, rook, and knight on a 4 by 4 chessboard so that no pieces is attacking any other.

smalln.py

from z3 import *
from itertools import combinations

# === Parameters ===
N = 4  # Board size
solver = Solver()

# === Helper functions ===
def z3_abs(x):
    return If(x >= 0, x, -x)

def not_same_square(p1, p2):
    r1, c1 = p1
    r2, c2 = p2
    return Or(r1 != r2, c1 != c2)

# === Piece positions ===
pieces = {
    "queen":  (Int("q_row"), Int("q_col")),
    "king":   (Int("k_row"), Int("k_col")),
    "bishop": (Int("b_row"), Int("b_col")),
    "rook":   (Int("r_row"), Int("r_col")),
    "knight": (Int("n_row"), Int("n_col")),
}

# === Attack rules ===
def knight_does_not_attack(p1, p2):
    r1, c1 = p1
    r2, c2 = p2
    return Not(Or(
        And(z3_abs(r1 - r2) == 2, z3_abs(c1 - c2) == 1),
        And(z3_abs(r1 - r2) == 1, z3_abs(c1 - c2) == 2)
    ))

def bishop_does_not_attack(p1, p2):
    r1, c1 = p1
    r2, c2 = p2
    return z3_abs(r1 - r2) != z3_abs(c1 - c2)

def rook_does_not_attack(p1, p2):
    r1, c1 = p1
    r2, c2 = p2
    return Not(Or(r1 == r2, c1 == c2))

def queen_does_not_attack(p1, p2):
    r1, c1 = p1
    r2, c2 = p2
    return Not(Or(
        r1 == r2,
        c1 == c2,
        z3_abs(r1 - r2) == z3_abs(c1 - c2)
    ))

def king_does_not_attack(p1, p2):
    r1, c1 = p1
    r2, c2 = p2
    return Or(
        z3_abs(r1 - r2) > 1,
        z3_abs(c1 - c2) > 1
    )

attack_rules = {
    "knight": knight_does_not_attack,
    "bishop": bishop_does_not_attack,
    "rook":   rook_does_not_attack,
    "queen":  queen_does_not_attack,
    "king":   king_does_not_attack,
}

# === Constraints ===

# === Constraints ===
# 1. Board bounds
for r, c in pieces.values():
    solver.add(And(0 <= r, r < N))
    solver.add(And(0 <= c, c < N))

# 2. No overlapping pieces (using Distinct)
solver.add(Distinct([r * N + c for (r, c) in pieces.values()]))

# 3. No attacking constraints (only check each pair once)
for (name1, p1), (name2, p2) in combinations(pieces.items(), 2):
    rule1 = attack_rules[name1]
    rule2 = attack_rules[name2]
    solver.add(rule1(p1, p2))
    # Optional: Add rule2(p2, p1) if needed (but usually redundant)

# === Solve and display ===
# === Enumerate all solutions ===
solutions = []
while solver.check() == sat:
    model = solver.model()

    # Extract concrete positions
    placement = {}
    for name, (r_var, c_var) in pieces.items():
        r = model[r_var].as_long()
        c = model[c_var].as_long()
        placement[name] = (r, c)
        # Optional: print(name, (r, c))

    solutions.append(placement)

    # Block this exact solution
    block = []
    for name, (r_var, c_var) in pieces.items():
        r = model[r_var]
        c = model[c_var]
        r_val, c_val = placement[name]
        block.append(Or(r != r_val, c != c_val))
    solver.add(Or(block))

# === Display all solutions ===
print(f"\n✅ Found {len(solutions)} solution(s):\n")

for i, placement in enumerate(solutions):
    board = [["." for _ in range(N)] for _ in range(N)]
    for name, (r, c) in placement.items():
        display_letter = "N" if name == "knight" else name[0].upper()
        board[r][c] = display_letter

    print(f"Solution {i+1}:\n")
    for row in board:
        print(" ".join(row))
    print()

solution.txt

✅ Found 1 solution(s):

Solution 1:

. . . K
Q . . .
. . . N
. R . B