The state of the art solvers are the proprietary ones like Gurobi, FICO, Cplex, Mosek, etc. A major contributor to the proprietary "sauce" is in the heuristics they use. For example, all solvers will have a "presolve" phase which attempts to eliminate redundant constraints/variables. There may be some ML they are using behind the scenes to derive these heuristics, I'm not sure, although I know it is a major research area.
Otherwise, the basic underlying algorithms are all the same, as in the textbook: branch-and-bound and so on.
I tried it with a certain conceptual problem in computer algebra (which I’ve had dismal results on GPT o1-preview and o1-mini… sort of a private benchmark) and it spent 2 minutes arguing with itself about what a Python function was called.
I think this is a criticism about the general Python ecosystem, but the article has nothing to do with what other package authors do or security vulnerabilities etc. It converts SAT to “dependency resolution” by creating a bunch of dummy packages and dependencies that map back to the SAT instance. And it’s definitely just for fun, I highly doubt it’s useful except as an exercise in NP-complete reductions :)
