Reading through a couple of other responses in this thread, it seems that converting a problem to be compatible with a SAT solver can sometimes result in unexpected gains in speed? That SAT solvers can sometimes be a better solution to a problem than the general "go to" solutions for a domain, despite it seeming to be inapplicable to such a domain? Maybe?
It's not that they seem inapplicable to some domain: they're applicable to a huge number of domains (basically any kind of constraint satisfaction problem). A lot of people thinks that this generality means that solving SAT problems is difficult, but in reality it means that a huge amount of effort has been invested into SAT solvers, which may outweigh the benefits you can get from a specialized solver.
