Block Party
A Jane Street puzzle: fill each region of a 9×9 irregularly-partitioned grid with the numbers 1 through N (where N is the region size), such that for every cell containing K, the nearest matching K (taxicab distance) is exactly K cells away.
Z3 solves the puzzle directly: one integer variable per cell, range and region-distinct constraints, plus a disjunction over the four directions and all possible values. Full Python model and the solved grid are in the PDF.