Improving Backtrack Search for SAT by Means of Redundancy

In this paper, a new heuristic that can be grafted to many of the most e cient branching strategies for Davis and Putnam procedures for SAT is described. This heuristic gives a higher weight to clauses that have been shown unsatis able at some previous steps of the search process. It is shown e cient for many classes of SAT instances, in particular structured ones.

• Type: Conference
• Year: 1999
• Where: ISMIS
• Authors: Laure Brisoux, Éric Grégoire, Lakhdar Sais
• Keywords: Artificial Intelligence, Cient Branching Strategies, Heuristic, ISMIS 1999, Particular Structured Ones