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

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Ohad Shacham, Karen Yorav
• Keywords: ENTCS 2006, Heuristic, Major Advancements, Small Subset