When I've tried using SAT (or SMT) solvers I've had issues with scalability. The solution times, even if they didn't increase exponentially, tended to go up as some higher polynomial (like, cubic) in the size of the initial problems I was trying them on.
My experience is they respond yes/no very quickly for lots of problems, but as the problem approaches "probably narrowly solvable" the runtime goes exponential.
