Un problème SAT est un problème de décision décrit par une série d'équations logiques. Un projet ROMEO débuté en 2007 avait pour vocation la résolution de tels problèmes de manière efficace sur une architecture parallèle. Quelques années plus tart, le projet s'est concrétisé avec une thèse (soutenue par Pascal Vander-Swalmen en décembre 2009), une collaboration avec l'Université de Picardie Jules-Vernes, un site web dédié ainsi qu'un logiciel disponible en téléchargement sur
Pascal Vander-Swalmen, qui a préparé sa thèse en co-direction entre Reims et Amiens, vient de publier son environnement parallèle de résolution de problèmes logiques (SAT). P. Vander-Swalmen a développé MTSS (Multi Threaded Sat Solver) sur les serveurs ROMEO2.
RDV sur http://www.parallel-sat.net pour toute information complémentaire.
The aim of this website is to provide a place where all the people interested in parallel SAT could find solvers, tools and informations. Everybody can help to extend and fill this website, just see the section called "Contacts" in the menu.
Le problème SAT :
SAT is an NP-complete problem. Parallelism will not change that, but parallelism can offer better performances to solve SAT formulas. Furthermore, today, multi-core architectures are in almost all new computers all around the world. From 2 to 8 cores, it is very easy to access such a computer. Some people think that future computers will contain many kinds of processors. Everyone knows SAT is very important for industrial applications, it has to be solved quickly and designing parallel SAT solvers is a new way to extract power from new hardwares.
Le logiciel :
MTSS is a Multi-Threaded SAT Solver. It is designed for shared memory computers. The most interesting feature for the SAT community is the parallelization of existing SAT solvers. It introduces the rich / poor approach which is a general framework in which one a lot of SAT implementations can be parallelized. And MTSS introduces also the new parallel object called the guiding tree, which is an object used in parallel to distribute and balance the workload in the system
