Start February 2025
SAT, Logic, Constraint Programming, Parallelization
Location: LaBRI, Laboratoire Bordelais de Recherche en Informatique, Talence, France
(This Master’s internship is funded by the Google Award 2024)
Description of the proposed master’s project
The resolution of the SAT problem (Satisfiability of a logical formula in propositional logic) has seen considerable progress in recent years, despite a near theoretical impossibility (SAT is the archetype of NP-Complete problems). These advances, notably illustrated by the performance of the Glucose SAT solver [1] co-developed at LaBRI, have faced challenges in recent years due to new architectural models of machines. It is indeed difficult to fully exploit the parallel, even massively parallel, architectures of recent machines.
This internship aims to revisit current methods of work-sharing for SAT solvers, specifically focusing on SAT formulas derived from problems initially expressed as constraints, which may present particular structures, or where higher-level methods can help analyze. The study is limited to a single machine with shared memory, excluding cloud computing. Recent approaches to massive parallelization of SAT exploit various paradigms of search space separation, among which “Cube and Conquer” [2]. This method involves dividing the main problem into thousands, or even hundreds of thousands, of smaller sub-problems, which are then distributed based on the availability of computing cores.
In this internship, we propose to study how the calculations already performed on the cores can be used to more precisely select the next sub-problem to solve.
The objective of this Master’s internship is to propose measures to share the work for the practical resolution of the SAT problem.
[1] The Glucose SAT Solver, Gilles Audemard, Laurent Simon, IJAIT’s Volume No.27, Issue No. 01.2018
[2] Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads, Heule, M.J.H., Kullmann, O., Wieringa, S., Biere, A., HVC 2011. Lecture Notes in Computer Science, vol 7261.
(The post announcing the Google Award).
Candidate
The candidate should have strong knowledge in Programming.
Contact: Laurent Simon