Sciweavers

ICTAI
2003
IEEE

Eliminating Redundancies in SAT Search Trees

13 years 9 months ago
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 satisfiability solvers implement forms of conflict analysis, at least to some extent. In this paper, a branching criterion initially introduced by Purdom [16] is revisited and extended. Contrary to his 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.
Richard Ostrowski, Bertrand Mazure, Lakhdar Sais,
Added 04 Jul 2010
Updated 04 Jul 2010
Type Conference
Year 2003
Where ICTAI
Authors Richard Ostrowski, Bertrand Mazure, Lakhdar Sais, Éric Grégoire
Comments (0)