4 ms·
As cool as Z3 is, I wish it didn't become so incredibly slow once soft constraints are introduced. I guess it's inevitable to an extent...
by ris 8y ago
As cool as Z3 is, I wish it didn't become so incredibly slow once soft constraints are introduced. I guess it's inevitable to an extent...
- OscarCunningham 8y agoWhat are soft constraints?
- kilburn 8y agoHard 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).
- OscarCunningham 8y agoInteresting. Thanks!
- tomp 8y agoLooks like you want to integrate a SAT/SMT solver with a convex optimisation engine :)