4 ms·
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) he
by 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 agoIt 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.