Eliminating redundancies in SAT search trees

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.