Aspects parallèles des problèmes de satisfaisabilité
Pascal Vander-Swalmen · HAL (Le Centre pour la Communication Scientifique Directe) · 2009
In spite of its computational complexity, the SATisfiability problem is a great and competitive approach to solve a wide range of problems. This leads to have a strong demand for high-performance SAT-solving tools in industry. Over the years, many different approaches and optimizations have been developed to tackle the problem more efficiently while being unaware of the actual trend in processor development which is from single-core to multi-core CPUs. This thesis presents a new kind of parallel algorithm with a strong collaborative approach where a rich thread is in charge of the search-tree evaluation and where a set of poor threads yield partial or global, logical or heuristics information to simplify the rich task. To become this solver real and efficient, we extended the guiding path notion to the guiding tree notion. The entire search-tree is shared in the main memory and each processor can work on it at the same time. This new solver is named MTSS for Multi-Threaded SAT Solver. In addition, we implemented a task for rich and poor threads which can execute an external SAT solver with or without lemma exchange policy. This permits to parallelize all kind of solvers (dedicated to industrial or random formulas). This new framework facilitates the future parallel SAT solving implementation approaches. Some examples and experimentations with and without lemma exchange strategies parallelizing external solvers are presented, as well as some benchmarks on MTSS itself. Sometimes, speedups are super linear.