Introduction
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.
Members
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.
Download
Please send us an email if you use the solver in some research or application (insert mail address here).
- 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.
- ManySAT 1.1_det
- This is the deterministic version of ManySAT 1.1.
- 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