A Distributed Version of Syrup
Autor: | Jean-Marie Lagniez, Sébastien Tabary, Gilles Audemard, Nicolas Szczepanski |
---|---|
Přispěvatelé: | Centre de Recherche en Informatique de Lens (CRIL), Université d'Artois (UA)-Centre National de la Recherche Scientifique (CNRS), DELORME, Fabien |
Jazyk: | angličtina |
Rok vydání: | 2017 |
Předmět: |
060201 languages & linguistics
[INFO.INFO-AI] Computer Science [cs]/Artificial Intelligence [cs.AI] Distributed Computing Environment Computer science 06 humanities and the arts 02 engineering and technology Parallel computing Solver [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI] Range (mathematics) Shared memory 0602 languages and literature 0202 electrical engineering electronic engineering information engineering Programming paradigm Portfolio 020201 artificial intelligence & image processing Boolean satisfiability problem ComputingMilieux_MISCELLANEOUS |
Zdroj: | 20th International Conference on Theory and Applications of Satisfiability Testing (SAT'17) 20th International Conference on Theory and Applications of Satisfiability Testing (SAT'17), 2017, Melbourne, Australia. pp.215-232 Theory and Applications of Satisfiability Testing – SAT 2017 ISBN: 9783319662626 SAT |
Popis: | A portfolio SAT solver has to share clauses in order to be efficient. In a distributed environment, such sharing implies additional problems: more information has to be exchanged and communications among solvers can be time consuming. In this paper, we propose a new version of the state-of-the-art SAT solver Syrup that is now able to run on distributed architectures. We analyze and compare different programming models of communication. We show that, using a dedicated approach, it is possible to share many clauses without penalizing the solvers. Experiments conducted on SAT 2016 benchmarks with up to 256 cores show that our solver is very effective and outperforms other approaches. This opens a broad range of possibilities to boost parallel solvers needing to share many data. |
Databáze: | OpenAIRE |
Externí odkaz: |