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.

·         SAT-Race 2010, Silver and Bronze medals.

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 The first version of the solver, see JSAT paper.

·         ManySAT 1.1 This version integrates control-based clause sharing policies, see IJCAI paper.

·         ManySAT 1.5 In this version two master threads periodically invoke two other thread (slaves) to direct them in a particular area of the search space, see CP paper.

·         (This is the deterministic version of manysat1.1 manysat1.1_det )

·         ManySAT 2.0 This is the first deterministic version of the solver. It allows full reproducibility of the executions (runtimes, and solutions). It is built on minisat 2.2. This version utilizes a low level of diversification (first interpretation choosen randomly). See technical report. New portfolio of strategies under construction

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