June 12, 2025
Solving LinkedIn Queens with SMT
For sure easier than solving it in SAT!
No newsletter next week
I’ll be speaking at Systems Distributed. My talk isn't close to done yet, which is why this newsletter is both late and short.
Solving LinkedIn Queens in SMT
The article Modern SAT solvers: fast, neat and underused claims that SAT solvers are "criminally underused by the industry". A while back on the newsletter I asked "why": how come they're so powerful and yet nobody uses them? Many experts responded saying the reason is that encoding SAT kinda sucked and they rather prefer using tools that compile to SAT.
I was reminded of this when I read Ryan Berger's post on solving “LinkedIn Queens” as a SAT problem.
A quick overview of Queens. You’re presented with an NxN grid divided into N regions, and have to place N queens so that there is exactly one queen in each row, column, and region. While queens can be on the same diagonal, they cannot be adjacently diagonal.
(Important note: Linkedin “Queens” is a variation on the puzzle game Star Battle, which is the same except the number of stars you place in each row/column/region varies per puzzle, and is usually two. This is also why 'queens' don’t capture like chess queens.)
... continue reading