HaifaSat: a SAT solver based on an Abstraction/Refinement model

Abstract

The popular abstraction/refinement model frequently used in verification, can also explain the success of a SAT decision heuristic like Berkmin. According to this model, conflict clauses are abstractions of the clauses from which they were derived. We suggest a clause-based decision heuristic called Clause-Move-To-Front (CMTF), which attempts to follow an abstraction/refinement strategy (based on the resolve-graph) rather than satisfying the clauses in the chronological order in which they were created, as done in Berkmin. We also show a resolution-based score function for choosing the variable from the selected clause and a similar function for choosing the sign. We implemented the suggested heuristics in our SAT solver HaifaSat. Experiments on hundreds of industrial benchmarks demonstrate the superiority of this method comparing to the Berkmin heuristic. HaifaSat won the 3rd place in the industrial-benchmarks category in the SAT competition of 2005, and did not compete or was developed since. We present experimental results with the benchmarks of the 2007 competition that show that it is about 32% slower than RSAT, the winner of 2007. Considering the time difference, it shows that it is rather robust. The abstraction/refinement theoretical model is still relevant, and there is still room for further research on how to exploit it better given a recent result that permits storing and manipulating the resolve graph in the main memory.