Adaptive Application of SAT Solving Techniques

10 years 11 months ago
Adaptive Application of SAT Solving Techniques
New heuristics and strategies have enabled major advancements in SAT solving in recent years. However, experimentation has shown that there is no winning solution that works in all cases. A degradation of orders of magnitude can be observed if the wrong heuristic is chosen. The problem is that it is impossible to know, in advance, which heuristics are best for a given problem. Consequently, many ideas - those that turn out to be useful for a small subset of the cases, but significantly increase run times on most others - are discarded. We propose the notion of Adaptive Solving as a possible solution to this problem. In our framework, the SAT solver monitors the effectiveness of the search on-the-fly using a Performance Metric. The metric gives a score according to its assessment of the search progress. Based on this score, one or more heuristics are turned on or off. The goal is to use a specific heuristic or strategy when it is advantageous, and turn it off when it is not, before it ...
Ohad Shacham, Karen Yorav
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Authors Ohad Shacham, Karen Yorav
Comments (0)