MSR PhD Scholarship on Parallel SAT Solving

Context and scientific objectives: SAT (decide if a Boolean formula, typically in conjunctive normal form, admits a valuation which makes it true?) is a fundamental problem in complexity theory with very large practical benefits. Modern SAT solvers can now handle propositional satisfiability problems with hundreds of thousands of variables or more. However, many practical instances remain difficult to all the available SAT solvers. Consequently, new approaches are clearly needed to solve these challenging industrial problems. In this context and with the light of the next generation of computer architectures, the design of parallel satisfiability solvers becomes a fundamental issue. The aim of this PhD is to provide new theoretical and practical advances for parallel satisfiability solving.

Laboratory: CRIL - CNRS UMR 8188, Université d’Artois, Lens, France

Supervision:

• Pr. Lakhdar Sais, CRIL, Lens, France
• Dr. Youssef Hamadi, Microsoft Research, Cambridge, UK

Application: please send CV to : sais [at] cril [dot] fr