Hacker News Reader

Comment by loeg | Hacker News Reader

In what way? They're useful for toy problems like this but they're very slow on larger problems.

SAT solvers are used daily to generate solutions for problems that have literally millions of variables. So, what you said is just wrong on the face. Yes, some talented people can write custom code that solves specific problems faster than a general purpose solver, particularly for easy special cases of the general problem, but most of the time that results in the programmer recreating the guts of a solver customized to a specific problem. There’s sort of a corollary of Greenspun’s Tenth Rule that every sufficiently complicated program also contains an ad hoc, informally-specified, bug-ridden, slow-implementation of half of a SAT or SMT solver.

I mean right tool for the right job. Plenty of formulations and problems (our job has plenty of arbitrarily hard graph algorithms) that have 90% of the problem just being a very clever reduction with nice structure.

Then the final 10% is either NP hard, or we want to add some DSL flexibility which introduces halting problem issues. Once you lower it enough, then comes the SMT solvers.

Define large. We've written model which solves real business issues in 8K lines of MiniZinc and it wasn't slow.

The conventional wisdom is the larger you make an NP hard problem, the slower is going to get. Irregardless of algorithm.

Reply on news.ycombinator.com