ManySAT: a Parallel SAT Solver

By Youssef Hamadi, Saïd Jabbour, Lakhdar Sais. Journal on Satisfiability, Boolean Modeling and Computation, 2009

366 citations recorded by the source corpus.

In this paper, ManySAT a new portfolio-based parallel SAT solver is thoroughly described. The design of ManySAT 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. Experiments on many industrial SAT instances, and the first rank obtained by ManySAT in the parallel track of the 2008 SAT-Race clearly show the potential of our design philosophy.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Computer Networks and Communications

View Paper: https://www.semanticscholar.org/paper/e8da2dc0b6481f30b2b4ffd5bad6b835616e3f37

Citations in the corpus

• Computing (2021, neutral): “The built environment is a term that encompasses the physical spaces we live in with a primary orientation toward the heavier end of infrastructure development such as constructed homes, buildings, roads, water infrastructure, the electrical grid, and so forth.”