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.