Comment by naet
2 days ago
I actually wrote a backtracking solution to the LinkedIn queens game a while ago (and the tango game).
I know nothing about SMT or SAT and I imagine they might be faster, but the backtracking appears to solve just as instantaneously when you push the button.
Might be cool to learn a bit about SMT or SAT. Not sure how broadly applicable they are but I've seen people use them to solve some difficult advent of code problems if nothing else.
Definite broad applicability.
NP-complete are the hardest problems in NP. Cook in 1971 proved SAT to be in NP-complete. In the worst case for any other problem in NP, we can quickly (i.e., in polynomial time) convert instances of that problem into instances of SAT. In other words, we can use SAT to solve any problem in NP.
It turns out there are many problems in NP-complete. The fast conversion applies among them too, so in some sense, problems in NP-complete are all the same because we can use them all to solve instances of each other. However, for some of those problem instances the best known algorithm is to try all possible inputs, which requires exponential time (very, very slow for even modestly large inputs).
Lots of research has been and continues to be poured into SAT because any gains automatically yield improvements to everything else in NP-complete and the rest of NP. Using a SAT solver allows you to hitch a ride more or less for free on the results of all that research. Each incremental improvement to SAT solvers benefits programs that use them.
As the author noted, forming SAT instances by hand can be a pain. SMT or SAT Modulo Theories is sort of a high-level language that “compiles down” to SAT. Expressing problems with SMT is more natural and reduces the burden of converting your problem to SMT and SMT solutions back to your problem domain.