3 ms·

Are SMT solvers insufficient?

• Hercuros 7y ago
  Mixed 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.