I wanted to mention Z3, which is one of the most user friendly yet advanced solvers I know. It's actually an SMT solver, so can solve a few more things than only SAT problems.
Yeah, I've been using z3 for a couple of projects and it is an absolute pleasure.
One of my projects involves I'm.entiong part of the JVMs execution in Z3 constraints and we have been able to prove stuff about program equivalence this way which is exciting.
Once the problems get big enough we will need to find clever ways of shaping Z3s search path, maybe by writing a theory, but for now it works for anything we have thrown at it.
Hard constraints are constraints that cannot be violated for the allocation to be valid (i.e.: to be a solution).
Soft constraints are constraints that incur some cost/penalty when violated.
Then the problem objective changes from "find an allocation that is a solution" (SAT) to "find the minimal cost solution (if one exists)" (Weighted SAT / Constraint Optimization).
For instance:
- SAT problem (a,b are binary):
Hard constraint: a = b
Solutions: a=0,b=0 and a=1,b=1
- Constraint optimization:
Hard constraint: a = b
Soft constraint: cost(a,b) = a+b
Optimal solution: a=0,b=0 with cost 0. The allocation a=1,b=1 is a solution because it fulfills the hard constraints, but it is not optimal because it's cost (2) is larger than the cost of another solution (0).
