4 ms·
You're looking for a mixed integer programming solver. Although the problem is NP-hard, in practice, state of the art MIP solvers run much faster than brute fo
by anderskaseorg 7y ago
You're looking for a mixed integer programming solver. Although the problem is NP-hard, in practice, state of the art MIP solvers run much faster than brute force search in most non-pathological cases.
- ampdepolymerase 7y agoAre SMT solvers insufficient?
- Hercuros 7y agoMixed integer programming is a more specialized task than SMT solving, therefore an MIP implementation is likely to be more optimized for the task, even if you might be able to use an SMT solver to solve the same problem. Moreover, SMT solvers are focused on finding some solution to some constraints, whereas MIP solvers are focused on finding the best solution to the constraints according to some linear objective. Finally, an SMT solver is basically a SAT solver combined with a theory solver for reasoning about integers, etc. If the problem can be expressed just as a conjunction of constraints (i.e, it has no interesting propositional structure), then you don’t really need the SAT solver part and can just use a specialized theory solver (optimizer, in this case) directly.