Re:Modern SAT solvers: fast, neat and underused
by wenc on Sunday September 29, 2019 @03:32PM
(#21109169)
Depends on the problem
Cbc [1] is modern, free and is competitive for most non-complex problems like timetabling (say less than 100k variables). (Cbc is much better than GNU Linear Programming Kit -- GLPK -- which uses outdated algorithms and is not competitive). Cbc can also be called from Excel via OpenSolver.
Scip [2] is the most performant "non-commercial" solver, but is only free for non-commercial uses. Commercial uses require licensing.
As for writing MIPs, this FICO MIP formulation guide [3] is extremely well written. Modeling MIPs is something of an art, and this doc captures most of the common formulations.
Cbc [1] is modern, free and is competitive for most non-complex problems like timetabling (say less than 100k variables). (Cbc is much better than GNU Linear Programming Kit -- GLPK -- which uses outdated algorithms and is not competitive). Cbc can also be called from Excel via OpenSolver.
Scip [2] is the most performant "non-commercial" solver, but is only free for non-commercial uses. Commercial uses require licensing.
As for writing MIPs, this FICO MIP formulation guide [3] is extremely well written. Modeling MIPs is something of an art, and this doc captures most of the common formulations.
[1] https://github.com/coin-or/Cbc
[2] https://scip.zib.de/
[3] https://www.fico.com/en/resource-download-file/3217