Hacker News Reader

Comment by bluecalm | Hacker News Reader

>>These so-called "SAT solvers" are able to handle industrial-strength problems, involving millions of variables, with relative ease, andthey've had a profound impact on many areas of research such as computer-aided verification.

I would be very interested in hearing of industrial/practical applications of those. Anyone with some experience?

View on HN

One neat example that comes to my mind is how some package managers use SAT solvers to resolve package conversioning conflicts.

I would say that SAT solvers (or SMT solvers, depending on the problem domain) are applicable to almost any kind of problem where the first thing that comes to your mind is implementing a brute-force search using backtracking. SAT solvers implement lots of tricks that are likely to leave naive backtracking algorithms in the dirt (knuth's chapter covers lots of them)

One silly example I like is the time I used a SAT solver to find the solutions for a little Flash puzzle game.

https://github.com/hugomg/hexiom

My favorite part is how I could add some symmetry-breaking predicates to greatly speed up the solver on highly symmetrical problem instances. Those instances are very hard for hand-written algorithms and a SAT solver let me work around the symmetry problems in a highly declarative manner.

p2 (https://www.eclipse.org/equinox/p2/), the provisioning platform used in Eclipse, uses a SAT solver (specifically, http://sat4j.org/) to resolve complex plug-in dependencies (with version range constraints and other OSGi-specific niceties) when you install or update plug-ins in Eclipse.

Reply on news.ycombinator.com