Modern SAT solvers: fast, neat and underused

Re:Modern SAT solvers: fast, neat and underused by salty_biscuits on Sunday September 29, 2019 @01:08AM (#21105222)

... only a small subset know about MIP solvers

And an even smaller subset are willing to pay to use gurobi or cplex. It would be so nice if the open source alternatives had competitive performance!

[ Parent | on HN ]

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.

[1] https://github.com/coin-or/Cbc

[2] https://scip.zib.de/

[3] https://www.fico.com/en/resource-download-file/3217

[ Parent | on HN ]

Re:Modern SAT solvers: fast, neat and underused by nurettin on Sunday September 29, 2019 @07:49AM (#21106497)

In your experience, does google's or-tools library have any chance in comparison?

[ Parent | on HN ]

Re:Modern SAT solvers: fast, neat and underused by disjhshava on Sunday September 29, 2019 @06:55PM (#21110143)

I didn't benchmark it and can't give a speed comparison, but I had success solving a pretty big optimization problem with GLOP, which I beleive uses or-tools.

[ Parent | on HN ]