15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'03)
Eliminating Redundancies in SAT Search Trees
Sacramento, California, USA
November 03-November 05
ISBN: 0-7695-2038-3
Conflict analysis is a powerful paradigm of backtrack search algorithms, in particular for solving satisfiability problems arising from practical applications. Accordingly, most recent Boolean satisfiability solvers implement forms of conflict analysis, at least to some extent. In this paper, a branching criterion initially introduced by Purdom is revisited and extended. Contrary to the author?s a priori analysis, it is shown very efficient from a practical point of view in that it allows search trees in SAT solving to be pruned in a significant way while obeying an interesting time and space trade-off. More precisely, we show that redundancies during the search process can be avoided without adding new constraints explicitly. Moreover, the technique can be used not only to prune branches in the search tree, but also to derive implied literals. Extensive experimental results illustrate the feasibility and practical interest of this approach.
Index Terms:
SAT, Davis and Putnam?s algorithm, Boolean search and satisfiability
Citation:
Richard Ostrowski, Bertrand Mazure, Lakhdar Saïs, Éric Grégoire, "Eliminating Redundancies in SAT Search Trees," ictai, pp.100, 15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'03), 2003