Hacker News new | ask | show | jobs
by anoncept 1527 days ago
After several years of exploring, my current gotos are:

* Minion for IP for scheduling + edge crossing minimization.

* cvxpy (wrapping ECOS, OSQP, and SCS by default) for convex optimization for making nice geometry.

* Z3 and STP for SAT/SMT for program analysis.

All are FLOSS, which is my main criterion in many situations.

Beyond that, I like minion for its focus on only providing efficiently implementable primitives, cvxpy for the awesome lectures and documentation the folks behind it have produced, and z3 + stp for their use in tools I like, such as klee.

2 comments

I'm curious what kind of person has 3 favorite constraint optimizers. What do you do that has you making use of so many different ones?
Not OP, but I work as a data scientist consultant, so various industries applications require different types of solvers e.g. mining operations optimization, branch location optimization, etc. would often each require a different solver depending on the problem space.
Not OP either, but there are many different aspects to solvers that make them useful in different situations.

For example, I would perhaps not use the same solver for a best-effort problem where I can program strong heuristics, vs a problem that must be optimized and no natural heuristics exist. Sometimes problems have a natural type of formulation, and it is best to use a solver for that type of problem (linear programming, mixed integer programming, SAT, pseudo boolean, constraint programming, ...).

Choosing a solver also very much depends on the deployment situation; how should a model be used and what operational concerns are there.

Doing all sorts of things will introduce you to all sorts of problems; from there, it’s just a matter of habitually looking around to try to see who/what has already worked on whatever problem is currently in front of you.

For example, I first found minion when I was learning about scheduling problems, initially to help a friend who was a Chief Resident on a pediatrics ward and later, to automate the administrative hassle of scheduling incident responders. (I wrote about that a little bit many years ago here if you’re curious: https://mstone.info/posts/scheduling/)

Concurrently with that, while I was working with and supervising security researchers, I spent quite a bit of time implementing various program analyses to answer questions about what certain programs of interest might do, and to find inputs that would make them do interesting things. For this purpose, though, minion is much less immediately relevant than Z3 since the interfaces and research interests of the relevant communities are so different.

Finally, this year, I am focusing on problems that have a more conventionally geometric flavor as opposed to the more discrete search spaces mentioned above. Here, convex optimization is a starting point that cvxpy makes incredibly accessible, especially in combination with Stephen Boyd’s Stanford SEE EE364A lectures (or similar): https://see.stanford.edu/Course/EE364A

Decade+ CISO of Akamai, math bent. http://www.mstone.info/resume/resume.pdf
Yep, that'll do it. :) Thanks!
I'd love to see an answer to this, too. Just to learn a little bit more about the field!
What are you thoughts on GLPK?