That was always a bit of a red herring, from my understanding. Yes, if you poorly model something into an ad hoc SAT solver, expect slowness.
Which is a bit of the general idea of these being underused. If you can get your problem into a SAT form or three, than feed it to a state of the art solver, it can work amazingly well. But, you will be spending a lot of time moving to and from the SAT formulation.
Which is a bit of the general idea of these being underused. If you can get your problem into a SAT form or three, than feed it to a state of the art solver, it can work amazingly well. But, you will be spending a lot of time moving to and from the SAT formulation.