Seven Challenges in Parallel SAT Solving

  • Youssef Hamadi Microsoft Research, 7 JJ Thomson Avenue, Cambridge CB3 0FB, United Kingdom
  • Christoph Wintersteiger Microsoft Research, 7 JJ Thomson Avenue, Cambridge CB3 0FB, United Kingdom
Keywords: Satisfiability, Parallelism

Abstract

This paper provides a broad overview of the situation in Parallel SAT Solving. A set of challenges to researchers is presented which, we believe, must be met to ensure the practical applicability of Parallel SAT Solvers in the future. All these challenges are described informally, but put into perspective with related research results, and a (subjective) grading of difficulty for each of them is provided.

Author Biographies

Youssef Hamadi, Microsoft Research, 7 JJ Thomson Avenue, Cambridge CB3 0FB, United Kingdom

Youssef Hamadi is a Senior Researcher at Microsoft Research. He holds a doctoral degree in Computer Science from the University of Montpellier in France. His research interests involve the practical resolution of large scale real life problems. His work is set at the intersection of Optimization and Artificial Intelligence. His research considers the design of complex systems based on multiple formalisms fed by different information channels which plan ahead and perform smart decisions. His current focus is on Autonomous Search, Parallel Search, and Propositional Satisfiability, with applications to Environmental Intelligence, Business Intelligence, and Software Verification.

Christoph Wintersteiger, Microsoft Research, 7 JJ Thomson Avenue, Cambridge CB3 0FB, United Kingdom

Christoph M. Wintersteiger is a Researcher at Microsoft Research. He holds an engineering degree in Computer Science from the University of Linz in Austria and a doctoral degree in Computer Science from ETH Zurich, Switzerland. His research is focussed on the investigation and design of automated reasoning techniques and applications thereof, especially in the field of automated software verification. He currently works on parallel and distributed methods for SAT and SMT solving.

Published
2013-06-21
Section
Articles