4 ms·
>>These so-called "SAT solvers" are able to handle industrial-strength problems, involving millions of variables, with relative ease, andthey've had a profound
by bluecalm 11y ago
>>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?
- pcdavid 11y agop2 (https://www.eclipse.org/equinox/p2/ https://www.eclipse.org/equinox/p2/), the provisioning platform used in Eclipse, uses a SAT solver (specifically, http://sat4j.org/ 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.
- ufo 11y agoOne 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 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.