loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Richard Ostrowski, Université déArtois
Bertrand Mazure, Université déArtois
Lakhdar Saïs, Université déArtois
Éric Grégoire, Université déArtois
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
Usage of this product signifies your acceptance of the Terms of Use.