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.
It sounds like you are trying to solve a partial maxsat problem. Partial maxsat uses two sets of clauses, hard and soft clauses. The hard clauses must be satisfied and the soft clauses are "nice to haves." The goal for the solver is to satisfy all the hard clauses and as many as the soft clauses as possible.
Its not perfect, but optimization problems are usually solved with SAT as follows: Suppose you have some X that you want to maximize. You encode a constraint X>=5, and see if there is a solution to that. If there is, you try with X>=6.
You continue until you can not find a solution or get unsat.
In your case, X would be the number of "nice to have constraints" that are satisfied. It would be simpler to formulate the these conditions in some SMT language, rather than in SAT directly.
>if you want particular properties of your answer that are "nice to haves" but not required, it is hard to encode
what I like about Reduced Ordered Binary Decision Diagrams (ROBDD) is that they can also tell you how many solutions there are, so you first encode the mandatory requirements, and if there are plenty of solutions, you can try adding requirements for the next-most-desired properties, or give up on a certain property by keeping an eye on the number of solutions.
