Approaches to Parallel SAT Solving

This lecture presents a full overview of parallelism in SAT. After a presentation of the classical divide-and-conquer approach, the talk introduces the more recent parallel portfolios algorithms. The theoretical and practical performances of these techniques are analysed, and in the second part of the lecture two recent improvements are detailed. The first one leverages conflict-clause sharing through various strategies used to dynamically balance between the communication overhead and the quality of the shared clauses. The second one considers the important question of adding determinism to a parallel portfolio. We present for the first time an innovative synchronizing strategy able to add determinism while preserving the performance level of a parallel SAT portfolio.

Youssef Hamadi,Microsoft Research, Cambridge, UK

Youssef Hamadi leads the Constraint Reasoning Group in Microsoft Research Cambridge. He is also the founder and co-director of the Microsoft-CNRS chair Optimisation for Sustainable Development, at École Polytechnique. His current research considers the design of complex systems based on multiple formalisms feed by different information channels which plan ahead and perform smart decisions. This work is set at the intersection of Optimization and Artificial Intelligence. Currently, his focus is on Autonomous Search, Parallel Search, and Propositional Satisfiability, with applications to software-verification, Automated Planning and business intelligence.