Résolution séquentielle et parallèle du problème de la satisfiabilité propositionnelle
- PhD Student:
- Long Guo
- Advisor :
- Lakhdar Saïs
- Co-Supervisor :
- Saïd Jabbour
- Funding : MSR
- PhD defended on :
- Jul 8, 2013
In this thesis, we deal with the sequential and parallel resolution of the problem SAT. Despite of its complexity, the resolution of SAT problem is an excellent and competitive approach for solving the combinatorial problems such as the formal verification of hardware and software, the cryptography, the planning and the bioinfomatics.
Several contribution are made in this thesis. The first contribution aims to find the compromise of diversification and intensification in the solver of type portfolio. In our second contribution, we propose to dynamically adjust the configuration of a core in a portfolio parallel sat solver when it is determined that another core performs similar work. In the third contribution, we improve the strategy of reduction of the base of learnt clauses, we construct a portfolio strategy of reduction in parallel solver.
Finally, we present a new approach named “Virtual Control” which is to distribute the additional constraints to each core in a parallel solver and verify their consistency during search.