Library · Short Excursions · Logic puzzles and solvers
Solving the LinkedIn Queens Puzzle with Z3
LinkedIn's Queens puzzle: place one queen per row, column, and colour region of an n×n board, with the additional constraint that no two queens touch, not even diagonally.
The classical n-queens formulation is extended with a per-colour-region constraint (exactly one queen per region). Each cell is a 0/1 variable; diagonal adjacency is forbidden via implication. Full Python code and a colour-aware visualisation for two example puzzles are in the PDF.