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