Improving Backtrack Search for SAT by Means of Redundancy
Laure Brisoux, Éric Grégoire, Lakhdar Saïs · 1999
Abstract. In this paper, a new heuristic that can be grafted to many of the most ecient branching strategies for Davis and Putnam procedures for SAT is described. This heuristic gives a higher weight to clauses that have been shown unsatisable at some previous steps of the search pro-cess. It is shown ecient for many classes of SAT instances, in particular structured ones. 1