Youssef Hamadi,

C – Microsoft Research


Clause sharing is key to the performance of parallel SAT solvers. However, without limitation, sharing clauses might lead to an exponential blow up in communication or to the sharing of irrelevant clauses. This talk presents two innovative policies to dynamically adjust the size of shared clauses between any pair of processing units. The first approach controls the overall number of exchanged clauses whereas the second additionally exploits the relevance quality of shared clauses.


Date: 2011-Feb-28     Time: 16:00:00     Room: 336

For more information: