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 23 articles , 1 standard article )

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

1 2 next

  1. Le Frioux, Ludovic; Baarir, Souheib; Sopena, Julien; Kordon, Fabrice: Painless: a framework for parallel SAT solving (2017)
  2. Lindauer, Marius; Hoos, Holger; Leyton-Brown, Kevin; Schaub, Torsten: Automatic construction of parallel portfolios via algorithm configuration (2017)
  3. Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten: SAT race 2015 (2016)
  4. Hamadi, Youssef; Jabbour, Saïd; Saïs, Lakhdar: What we can learn from conflicts in propositional satisfiability (2016)
  5. Amadini, Roberto; Gabbrielli, Maurizio; Mauro, Jacopo: Why CP portfolio solvers are (under)utilized? issues and challenges (2015)
  6. Balyo, Tomáš; Sanders, Peter; Sinz, Carsten: HordeSat: a massively parallel portfolio SAT solver (2015)
  7. Burchard, Jan; Schubert, Tobias; Becker, Bernd: Laissez-faire caching for parallel #SAT solving (2015)
  8. Caniou, Yves; Codognet, Philippe; Richoux, Florian; Diaz, Daniel; Abreu, Salvador: Large-scale parallelism for constraint-based local search: the costas array case study (2015)
  9. Phan, Anh-Dung; Hansen, Michael R.: An approach to multicore parallelism using functional programming: a case study based on Presburger arithmetic (2015)
  10. Audemard, Gilles; Simon, Laurent: Lazy clause exchange policy for parallel SAT solvers (2014)
  11. Angione, Claudio; Occhipinti, Annalisa; Stracquadanio Giovanni; Nicosia, Giuseppe: Bose-Einstein condensation in satisfiability problems (2013)
  12. Belov, Anton; Manthey, Norbert; Marques-Silva, Joao: Parallel MUS extraction (2013)
  13. Hamadi, Youssef; Jabbour, Saïd; Saïs, Lakhdar: Learning from conflicts in propositional satisfiability (2012)
  14. Martins, Ruben; Manquinho, Vasco; Lynce, In^es: An overview of parallel SAT solving (2012)
  15. Hamadi, Youssef; Ringwelski, Georg: Boosting distributed constraint satisfaction (2011) ioport
  16. Hyvärinen, Antti E.J.; Junttila, Tommi; Niemelä, Ilkka: Partitioning search spaces of a randomized search (2011)
  17. Brummayer, Robert; Lonsing, Florian; Biere, Armin: Automated testing and debugging of SAT and QBF solvers (2010)
  18. Diaz, Daniel; Abreu, Salvador; Codognet, Philippe: Parallel constraint-based local search on the Cell/BE multicore architecture (2010)
  19. Hyvärinen, Antti E.J.; Junttila, Tommi; Niemelä, Ilkka: Partitioning SAT instances for distributed solving (2010)
  20. Schulz, Sven; Blochinger, Wolfgang: Parallel SAT solving on peer-to-peer desktop grids (2010) ioport

1 2 next