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>

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.