Modern SAT solvers: fast, neat and underused

Re:Modern SAT solvers: fast, neat and underused by shaklee3 on Sunday May 19, 2019 @12:52PM (#19954191)

Yes, yes, yes. I've made this comment a few times on here but tools like MIP solvers are vastly unknown since they didn't take on a sexy name when they started out. However, they can outperform most heuristic based algorithms, and even solve some of the largest problems. It's how the NFL makes their schedules oh, and you can imagine how complicated that is.

[ Parent | on HN ]

Re:Modern SAT solvers: fast, neat and underused by new4thaccount on Sunday May 19, 2019 @10:31PM (#19957086)

Fun fact. Most power grids in the developed world are run off of some of the largest MILP and LP problems. We're talking about millions of constraints to commit units and hundreds of thousands to dispatch them. These run around the clock 24/7.

I've only recently learned about SAT type solvers as MILP/LP problems are very fast and globally optimal, unlike things like A* or Genetic Algorithms. I think GA's are cool because you can write one in less than 1/2 page of Python, where MIP solvers are usually large black-box C codesets (Ex: GLPK, CPLEX, GUROBI, XPRESS, Open-Solver).

[ Parent | on HN ]

Re:Modern SAT solvers: fast, neat and underused by jvanderbot on Monday May 20, 2019 @07:27PM (#19966301)

GA does not belong anywhere near real problems. They are toy solutions with zero guarantees.

Fun to code though!

[ Parent | on HN ]

Re:Modern SAT solvers: fast, neat and underused by new4thaccount on Wednesday May 22, 2019 @06:33AM (#19979687)

Sadly, I've mostly come to the same conclusion in that I at least need a MIP Gap to tell me how far I am from the optimal solution.

My only issue with LP and MILP solvers is scalibility. You have none! Multicore doesn't really seem to help any.

[ Parent | on HN ]