[amelius]

I know that every NP problem can be written as an SMT problem, theoretically speaking. But is that actually practical?

[KirinDave]

The answer to that question is, "Yes, if your SMT solver has strategies that provide good results for the problem in question."

Unless you're implementing solvers or caught up on the particulars of a solver's implementation, the best way to gauge this is to try it.