Hillel Wayne wrote about solving the LinkedIn Queens problem with SMT in his Computer Things newsletter. This was in turn inspired by Ryan Berger's post Using SAT to Get the World Record on LinkedIn's Queens that solves the same problem using a SAT solver.

Not to be outdone, this post describes how to use MiniZinc to solve the problem in what I think is a more readable and natural expression of the model than either SAT or SMT. As always, YMMV and what is natural and clear to one person is opaque and weird to someone else.

Nmbr9 as a Constraint Programming Challenge, a paper by Mikael Z. Lagerkvist

State Representation and Polyomino Placement for the Game Patchwork, a paper by Mikael Z. Lagerkvist

Monte Carlo Methods for the Game Kingdomino, a paper by Magnus Gedda, Mikael Z. Lagerkvist and Martin Butler