I wrote a Z3 solver that finds maximal packings, below are the resulting boards, shown with uppercase/lowercase only for visual contrast of light/dark squares (case does not indicate color).
1. 62 pieces, 2 kings
R n N n B n N n
p Q r P b P n P
P r . p Q p . p
p N n P n P n P
Q n B p R p B n
p P b Q b R b P
K n B r N q B p
n N q K n N r N
FEN (no compression):
RNNNBNNN/PQRPBPNP/PR.PQP.P/PNNPNPNP/QNBPRPBN/PPBQBRBP/KNBRNQBP/NNQKNNRN
2. 62 pieces, 2 kings; Black king not in check
N b N b N q R n
p P q P p P p R
N . N r N . Q n
p Q r N p B p N
N b P q P r P n
n N k N r B p Q
K p P p P b P n
b R b N q B n N
FEN:
NBNBNQRN/PPQPPPPR/N.NRN.QN/PQRNPBPN/NBPQPRPN/NNKNRBPQ/KPPPPBPN/BRBNQBNN
3. 62 pieces, 2 kings; White not immediately stalemated
N n Q r N b B n
p N b P n P q P
P q B p N r B p
p N r Q n P k P
P n P p N p B .
q N b K r P . P
P p P p Q p R n
r N b N n B n N
FEN:
NNQRNBBN/PNBPNPQP/PQBPNRBP/PNRQNPKP/PNPPNPB./QNBKRP.P/PPPPQPRN/RNBNNBNN
4. 63 pieces, exactly 1 king
N b R q K n N n
p P p P b P n P
N r N n B p Q p
p P p N r P n P
B . Q b B r N p
p P p N q P r P
N q N r B p N p
r N b N b N n N
FEN:
NBRQKNNN/PPPPBPNP/NRNNBPQP/PPPNRPNP/B.QBBRNP/PPPNQPRP/NQNRBPNP/RNBNBNNN
5. 64 pieces, 0 kings
N n N n N n Q n
p P p P p B p B
B b Q b R b P n
p P p P p R p Q
B n R n N n P n
p R p Q p B p B
P n P b P q P r
n N n R n N n N
FEN:
NNNNNNQN/PPPPPBPB/BBQBRBPN/PPPPPRPQ/BNRNNNPN/PRPQPBPB/PNPBPQPR/NNNRNNNN
This is a completely full board with no kings.
from z3 import *
import time
def solve_minimal(target, n_kings, mode="plain"):
s, B = Solver(), [Int(f'x{i}') for i in range(64)]
dist = lambda i, j: (abs(i//8 - j//8), abs(i%8 - j%8))
def attacks(src_idx, dst_idx):
dr, dc = dist(src_idx, dst_idx)
p = B[src_idx]
return Or(
And(p == 4, dr*dc == 0), # R
And(p == 3, dr == dc), # B
And(p == 5, Or(dr*dc == 0, dr == dc)), # Q
And(p == 2, dr*dc == 2), # N
And(p == 1, dr == 1, dc == 1), # P (symmetric)
And(p == 6, dr < 2, dc < 2, dr + dc > 0) # K
)
# Domains
s.add([And(x >= 0, x <= 6) for x in B]) # 0:., 1:P, 2:N, 3:B, 4:R, 5:Q, 6:K
# No pawns on back ranks
s.add([B[i] != 1 for i in list(range(8)) + list(range(56, 64))])
# Same-type non-attacking (air rule)
for i in range(64):
for j in range(i+1, 64):
s.add(Implies(B[i] == B[j], Not(attacks(i, j))))
# Counts
s.add(Sum([If(x > 0, 1, 0) for x in B]) == target)
s.add(Sum([If(x == 6, 1, 0) for x in B]) == n_kings)
# Mode: “safe_black” == every king not attacked by any piece (no colors here)
if mode == "safe_black":
for i in range(64):
s.add(Implies(
B[i] == 6,
And([Not(attacks(j, i)) for j in range(64) if j != i])
))
# Mode: “active_white” == there exists a king with at least one safe adjacent square
if mode == "active_white":
safe_king_exists = []
for i in range(64):
neighbors = []
for j in range(64):
dr, dc = dist(i, j)
if dr <= 1 and dc <= 1 and (dr + dc) > 0:
# j empty and not attacked by any piece
safe_j = And(
B[j] == 0,
And([Not(attacks(k, j)) for k in range(64) if k != j])
)
neighbors.append(safe_j)
if neighbors:
# i is a king AND it has a safe neighbor
safe_king_exists.append(And(B[i] == 6, Or(neighbors)))
s.add(Or(safe_king_exists))
print(f"Solving {target} pieces ({mode})...")
t0 = time.time()
if s.check() == sat:
m = s.model()
print(f"Found in {time.time()-t0:.2f}s")
sym = ".PNBRQK"
for r in range(8):
row = [m[B[r*8+c]].as_long() for c in range(8)]
print(" ".join(sym[x] if (r+c)%2==0 else sym[x].lower()
for c, x in enumerate(row)))
else:
print("Unsat")
if __name__ == "__main__":
solve_minimal(62, 2, "plain") # Scenario 1
solve_minimal(62, 2, "safe_black") # Scenario 2
solve_minimal(62, 2, "active_white") # Scenario 3
solve_minimal(63, 1, "plain") # Scenario 4
solve_minimal(64, 0, "plain") # Scenario 5
