Solving LinkedIn Queens Using Haskell

how would you encode a constraint system where the generator must yield exactly one solution and that solution remains unique under all transformations in the problem’s symmetry group, without relying on post-solution filtering or external isomorphism checks?

Directly modelling the unique solution property would be a quantified problem, essentially it would be "there exists a solution such that it is not the case that there exists a different solution". In principle, you can explode this into an enumeration of all O(n!) placements of queens and saying "either the placement is the same as the solution, or it is not a solution". That significantly increases the model size though.

For the symmetry, LinkedIn Queens generally do not have symmetric boards since that would imply more than one solution.