HaifaSat: a SAT solver based on an Abstraction/Refinement model
Roman Gershman, Ofer Strichman · Journal on Satisfiability Boolean Modeling and Computation · 2008
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. W