ManySAT: a Parallel SAT Solverhttp://research.microsoft.com/en-us/people/youssefh/image004small.jpg

ManySAT is a portfolio-based parallel SAT solver. Its design benefits from the main weaknesses of modern SAT solvers: their sensitivity to parameter tuning and their lack of robustness. ManySAT uses a portfolio of complementary sequential algorithms obtained through careful variations of the standard DPLL algorithm. Additionally, each sequential algorithm shares clauses to improve the overall performance of the whole system. This contrasts with most of the parallel SAT solvers generally designed using the divide-and-conquer paradigm.

People

·         Youssef Hamadi, http://research.microsoft.com/en-us/people/youssefh/.

·         Said Jabbour, http://www.msr-inria.inria.fr/~jabbour.

·         Lakhdar Sais, http://www.cril.univ-artois.fr/~sais/.

Awards

·         SAT-Race 2008, best parallel SAT solver, gold.

·         SAT-Competition 2009, gold, silver, bronze, parallel track, special prize.

Papers

·         Diversification and intensification in parallel SAT solving, L. Guo, Y. Hamadi, S. Jabbour, and L. Sais, 16th International Conference on Principles and Practices of Constraint Programming (CP), 2010.

·         ManySAT: a Parallel SAT Solver, Y. Hamadi, S. Jabbour, and L. Sais, Int. Journal on Satisfiability, Boolean Modeling and Computation (JSAT), Volume 6, Special Issue on Parallel SAT, Ed. Y. Hamadi, IOS Press, 2009.

·         Control-based Clause Sharing in Parallel SAT Solving, Y. Hamadi, S. Jabbour, and L. Sais, Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), July 2009, Pasadena, USA.

·         ManySAT solver description, Y. Hamadi, S. Jabbour, and L. Sais, MSR-TR-2008-83, May 2008.

Related papers

·         A Concurrent Portfolio Approach to SMT Solving, C. Wintersteiger, Y. Hamadi, and L. de Moura,  Twenty-one International Conference on Computer Verification (CAV'09), June 2009, Grenoble, France.

·         Experiments with Massively Parallel Constraint Solving, L. Bordeaux, Y. Hamadi, and H. Samulowitz, Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), July 2009, Pasadena, USA.

Download

Please send us an email if you use the solver in some research or application.

·         ManySAT 1.0

Known users

·         Massachusetts Institute of Technology, department of Electrical Engineering and Computer Science, USA

·         Stanford University, USA

·         Saint Petersburg, Department of V.A. Steklov, Institute of Mathematics of the Russian Academy of Sciences, Russia

·         IBM Germany Research & Development GmbH, Boeblingen, Germany

·         University of Munich, Germany

·         University of Tuebingen, Germany

·         Washington University in St. Louis, USA

·         Macquarie University, Sydney, Australia

·         Chaio Tung University, Taiwan