2 ms·
Is a specialized MIP solver mandatory, or would using a general SMT solver like Z3 usually be good enough?
by logicchains 7y ago
Is a specialized MIP solver mandatory, or would using a general SMT solver like Z3 usually be good enough?
- mattz0rt 7y agoIn my experience SMT solvers tends to be an order of magnitude slower than MIP solvers, even when looking at the exact same constraints. But yes given a small enough problem SMT solvers like Z3 are an excellent choice and provide additional functionality like propositional logic (if A then B else C).
- atak1 7y agoSpecialized is necessary due to business requirements. User requests aren't always "here's a problem + the data, solve this to optimal". Here are other examples: 1. "here's the problem + data, solve it well enough within 10s" 2. "here's the problem + data, solve it well enough with a subset of the data" 3. "here's the problem + data, solve it partially, and then when near real-time updates come in, update solution to take new information into account"