Yup, had some great success getting solutions to real instances of NP complete problems. Nice thing is that SAT solvers all have basically the same interfaces, you can serialize the problems easily so it is super easy to try lots of solvers out. It's fun to think about problems in terms of SAT, you can build huge logic networks with hundreds of thousands of clauses and solve them in seconds. Solve integer optimizations with binary encodings. cool stuff. Unfortunately, it is super sensitive and hard to control, so if you want particular properties of your answer that are "nice to haves" but not required, it is hard to encode. Some problems will be solved instantly, some will never be solved with any amount of cpu time, so it is hard to have it in the loop of something that needs to always work unless your problems are really well constrained.