December 12, 2017, 10am, salle des thèses de la faculté Jean Perrin
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