Block Party 4
A Jane Street variant of Block Party on a 10×10 grid: fill each region with 1 through N, but with a cleaner taxicab constraint expressed as two implication clauses per cell.
The 10×10 variant factors the K-distance rule into a “no cell with value K closer than K” constraint and a “at least one cell with value K at exactly K” constraint, both over all cells. Z3 solves. Full model in the PDF.