3 ms·

Automated Configuration and Selection of SAT Solvers [pdf]

41 points by luu 5y ago

jjoonathan 5y ago
I wonder... could this help the anaconda sat solver that increasingly seems to get stuck on even modest package lists these days? Solving Environment | \ - / |
- sacado2 5y ago
  This is probably a bit overkill for that kind of problems. In Anaconda, the problem is probably that the instance isn't described optimally. In real life (that is, unless you make it up and artificially find the worse possible example), package configuration / management is not considered a "hard" SAT problem (but an "industrial" one, i.e, still NP-complete, but solvable in a reasonable amount of time in practice). "Hard" problems are those you don't expect to solve in a few minutes on a desktop (or laptop) computer.
maweki 5y ago
If you've been to a SAT conference in recent years you know that they're basically on the hunt for hard instances, ie instances that are hard for any (known) heuristic. So far, from what I've gathered, this hunt has not been very fruitful. Guesstimating or even feedback-controlled-cobfiguration/selection of the suitable solvers and heuristics could bring us leaps and bounds. Encoding techniques you can usually look up. But selecting the solver and heuristics needs years of real life experience. This automated approach could make SAT solving an order of magnitude faster for "the uninitiated".
- thesz 5y ago
  It is not hard to find hard instances. Encode SHA256 in SAT, for one example. As for heuristics, etc, I strongly prefer approach that stems from observations valid for any problem. One such example is SDCL - Satisfaction Driven Clause Learning [1]. [1] https://publik.tuwien.ac.at/showentry.php?ID=266903&lang=6 https://publik.tuwien.ac.at/showentry.php?ID=266903&lang=6 They found a way to constrain search that needs selection - e.g., propagation has stopped and solver needs to select. This approach helps to solve pigeonhole problems much faster and is applicable outside of pigeonhole problems.

41 points by luu 5y ago

I wonder... could this help the anaconda sat solver that increasingly seems to get stuck on even modest package lists these days? Solving Environment | \ - / |

sacado2 5y ago
This is probably a bit overkill for that kind of problems. In Anaconda, the problem is probably that the instance isn't described optimally. In real life (that is, unless you make it up and artificially find the worse possible example), package configuration / management is not considered a "hard" SAT problem (but an "industrial" one, i.e, still NP-complete, but solvable in a reasonable amount of time in practice). "Hard" problems are those you don't expect to solve in a few minutes on a desktop (or laptop) computer.

maweki 5y ago

If you've been to a SAT conference in recent years you know that they're basically on the hunt for hard instances, ie instances that are hard for any (known) heuristic. So far, from what I've gathered, this hunt has not been very fruitful. Guesstimating or even feedback-controlled-cobfiguration/selection of the suitable solvers and heuristics could bring us leaps and bounds. Encoding techniques you can usually look up. But selecting the solver and heuristics needs years of real life experience. This automated approach could make SAT solving an order of magnitude faster for "the uninitiated".

thesz 5y ago
It is not hard to find hard instances. Encode SHA256 in SAT, for one example. As for heuristics, etc, I strongly prefer approach that stems from observations valid for any problem. One such example is SDCL - Satisfaction Driven Clause Learning [1]. [1] https://publik.tuwien.ac.at/showentry.php?ID=266903&lang=6 https://publik.tuwien.ac.at/showentry.php?ID=266903&lang=6 They found a way to constrain search that needs selection - e.g., propagation has stopped and solver needs to select. This approach helps to solve pigeonhole problems much faster and is applicable outside of pigeonhole problems.