Those are small examples but you can scale them up and Z3 can still handle it.
I have no meaningful experience in OR, don’t know how SAT solvers work or how Z3 reduces things to SAT. Yet I was able to use it to attack a really gnarly scheduling problem with hundreds of variables, weird constraints, preferences, etc.
In addition to finding feasible solutions Z3 has an “Optimize” class that can handle soft constraints and objective functions. This is really useful. (I suspect CPLEX/Gurobi would be better at this but Z3 still works well.)
currymj|7 years ago
I have no meaningful experience in OR, don’t know how SAT solvers work or how Z3 reduces things to SAT. Yet I was able to use it to attack a really gnarly scheduling problem with hundreds of variables, weird constraints, preferences, etc.
In addition to finding feasible solutions Z3 has an “Optimize” class that can handle soft constraints and objective functions. This is really useful. (I suspect CPLEX/Gurobi would be better at this but Z3 still works well.)