• PhD Student:
  • Nicolas Szczepanski
  • Funding : Artois, Région HdF
  • PhD defended on :
  • Dec 12, 2017 • faculté des sciences

This thesis deals with propositional satisfiability ( SAT ) in a massively parallel setting. The SAT problem is widely used for solving several combinatorial problems (e.g. formal verification of hardware and software, bioinformatics, cryptography, planning, scheduling, etc.). The first contribution of this thesis concerns the design of efficient algorithms based on the approaches « portfolio » and « divide and conquer ». Secondly, an adaptation of several parallel programming models including hybrid (parallel and distributed computing) to SAT is proposed. This work has led to several contributions to international conferences and highly competitive distributed SAT solvers.

Keywords: SAT, SAT solvers, parallel, distributed computing, hybrid programming models