The recommended solution for many NP-hard problems seems to be "just give it to a SAT solver". Are there cases where this isn't a good fit?