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.
· 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/.
· 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.
· 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.
· 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.
Please send us an email if you use the solver in some research or application.
· (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
· 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