|
Published Articles >> Table of Contents >> Abstract
15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'03)
p. 100
Eliminating Redundancies in SAT Search Trees
Richard Ostrowski, Université d’Artois
Bertrand Mazure, Université d’Artois
Lakhdar Sais, Université d’Artois
Eric Gregoire, Université d’Artois
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TAI.2003.1250176
Send link to a friend
| Abstract |
|
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.
|
 Additional Information
|
Index Terms- SAT, Davis and Putnam’s algorithm, Boolean search and satisfiability
Citation:
Richard Ostrowski, Bertrand Mazure, Lakhdar Sais, Eric Gregoire,
"Eliminating Redundancies in SAT Search Trees,"
ictai,
p. 100,
15th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'03),
2003
|
|
