Automated Configuration and Selection of SAT Solvers [pdf] | Hacker News Reader

Automated Configuration and Selection of SAT Solvers [pdf]

cs.ubc.ca

41 pointsluu4 comments

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".

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

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.

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

    Solving Environment
    |
    \
    -
    /
    |

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.

Reply on news.ycombinator.com