ManySAT

ManySAT: a parallel SAT solver. 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.


References in zbMATH (referenced in 36 articles , 1 standard article )

Showing results 1 to 20 of 36.
Sorted by year (citations)

1 2 next

  1. Roh, Dongyoung; Koo, Bonwook; Jung, Younghoon; Jeong, Il Woong; Lee, Dong-Geon; Kwon, Daesung; Kim, Woo-Hwan: Revised version of block cipher CHAM (2020)
  2. Vallade, Vincent; Le Frioux, Ludovic; Baarir, Souheib; Sopena, Julien; Ganesh, Vijay; Kordon, Fabrice: Community and LBD-based clause sharing policy for parallel SAT solving (2020)
  3. Zaikin, Oleg; Kochemazov, Stepan: Black-box optimization in an extended search space for SAT solving (2019)
  4. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  5. Gent, Ian P.; Miguel, Ian; Nightingale, Peter; McCreesh, Ciaran; Prosser, Patrick; Moore, Neil C. A.; Unsworth, Chris: A review of literature on parallel constraint solving (2018)
  6. Liang, Jia Hui; Oh, Chanseok; Mathew, Minu; Thomas, Ciza; Li, Chunxiao; Ganesh, Vijay: Machine learning-based restart policy for CDCL SAT solvers (2018)
  7. Marques-Silva, Joao; Malik, Sharad: Propositional SAT solving (2018)
  8. Adelshin, A. V.; Kuchin, A. K.: Analysis of (L)-structure of polyhedron in the partial MAX SAT problem (2017)
  9. Audemard, Gilles; Lagniez, Jean-Marie; Szczepanski, Nicolas; Tabary, Sébastien: A distributed version of Syrup (2017)
  10. Le Frioux, Ludovic; Baarir, Souheib; Sopena, Julien; Kordon, Fabrice: Painless: a framework for parallel SAT solving (2017)
  11. Lindauer, Marius; Hoos, Holger; Leyton-Brown, Kevin; Schaub, Torsten: Automatic construction of parallel portfolios via algorithm configuration (2017)
  12. Nejati, Saeed; Newsham, Zack; Scott, Joseph; Liang, Jia Hui; Gebotys, Catherine; Poupart, Pascal; Ganesh, Vijay: A propagation rate based splitting heuristic for divide-and-conquer solvers (2017)
  13. Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten: SAT race 2015 (2016)
  14. Hamadi, Youssef; Jabbour, Saïd; Saïs, Lakhdar: What we can learn from conflicts in propositional satisfiability (2016)
  15. Loveland, Donald; Sabharwal, Ashish; Selman, Bart: DPLL: the core of modern satisfiability solvers (2016)
  16. Adel’shin, A. V.; Kolokolov, A. A.: Analysis and solution of discrete optimization problems with logical constraints on the base of (L)-partition approach (2015)
  17. Amadini, Roberto; Gabbrielli, Maurizio; Mauro, Jacopo: Why CP portfolio solvers are (under)utilized? issues and challenges (2015)
  18. Balyo, Tomáš; Sanders, Peter; Sinz, Carsten: HordeSat: a massively parallel portfolio SAT solver (2015)
  19. Burchard, Jan; Schubert, Tobias; Becker, Bernd: Laissez-faire caching for parallel #SAT solving (2015)
  20. Caniou, Yves; Codognet, Philippe; Richoux, Florian; Diaz, Daniel; Abreu, Salvador: Large-scale parallelism for constraint-based local search: the costas array case study (2015)

1 2 next