Hacker News Reader

Comment by anjc | Hacker News Reader

Why are people ITT talking about reducing problems to SAT? As I understand it, the point of reducing a problem to SAT is because there's a proof that SAT is NP-Complete which in turn would prove that your problem is NP-Complete. But if you have some sort of industrial constraint satisfaction/ASP/scheduling/search/etc problem, you can solve it with whatever methods are available. You don't have to reduce a problem in such and such domain down to a big Boolean formula and solve it via SAT techniques. Am I wrong?

View on HN

SAT (and SMT) solvers are extremely optimized and very expressive.

Writing an encoding from problem P to SAT is usually much simpler and easier to do correctly than writing a dedicated solver for P. SAT solvers are so efficient than very often they will be competitive with dedicated ones.

At the end of the day, you want to solve your high-level problem, not writing a solver, especially when such good solvers are already available.

> As I understand it, the point of reducing a problem to SAT is because there's a proof that SAT is NP-Complete which in turn would prove that your problem is NP-Complete.

That's kind of backwards: reducing any problem in NP (not just NP-complete ones) to SAT is possible and mathematically straightforward because SAT is NP-complete. You do reductions from SAT to other problems in order to show that they are NP-complete (which involves cleverness in working out how to represent propositional logic in e.g. Sudoku).

What happened was that SAT solvers (and the related SMT solvers) got very fast, so fast that often the fastest way to solve a constraint satisfaction problem is to express it in a form one of these general solvers takes as input and then just using the general tool.

Of course the problems being solved are NP hard in general, but in practice, on the kind of problems they're actually given, the solvers can be sufficiently fast.

To prove that a problem is NP complete you have to reduce SAT to that problem, not that problem to SAT.

You can solve combinatorial search problems with whatever method you want, but it can be very hard to beat a SAT solver, because you may have to duplicate all the strategies, engineering, and heuristics that SAT solvers have. If your problem has special structure then it may be worth writing your own solver. Constraint satisfaction problems can often be written with high level constraints that have good constraint propagators (e.g. the alldifferent constraint).

Reading through a couple of other responses in this thread, it seems that converting a problem to be compatible with a SAT solver can sometimes result in unexpected gains in speed? That SAT solvers can sometimes be a better solution to a problem than the general "go to" solutions for a domain, despite it seeming to be inapplicable to such a domain? Maybe?

It's not that they seem inapplicable to some domain: they're applicable to a huge number of domains (basically any kind of constraint satisfaction problem). A lot of people thinks that this generality means that solving SAT problems is difficult, but in reality it means that a huge amount of effort has been invested into SAT solvers, which may outweigh the benefits you can get from a specialized solver.

Reply on news.ycombinator.com