Parallelization CSP / SAT (Master's Internship)

30 November 2024

Most recent news

(list of all news)

Interview in the Science et Vie Special Issue on AI

(20 October 2025)

I've had the privilege for some time of occasionally answering journalists' questions about the impacts of AI on society, thanks to the Trustworthy AI Chair which has increased the visibility...


AI Act Afternoon by the Trustworthy AI Chair

(06 October 2025)

October 13th: afternoon of presentation and exchanges on the AI Act! **Listen, question and understand the AI Act** - An afternoon of explanations, theoretical insights and applied experience feedback to...


Science & Vie Roundtable — Fête de la Science

(01 October 2025)

On the eve of the official launch of Fête de la Science 2025, and at the offices of the Ministry of Higher Education, I took part in a roundtable organized...


AI Training at Aérocampus

(04 July 2025)

The Aérocampus of Nouvelle Aquitaine is a training center for aeronautical technicians. It's a unique campus where industry plays a major role. Here, airplanes (including a Rafale) and helicopters of...


2025 Agrégation Jury

(23 June 2025)

Since 2022, France has finally established an external computer science agrégation. I remember my own computer science classes in middle school (on PCs with 5"1/4 floppy disks and MO5/TO7 machines)....

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

(Last Modified date: 22 February 2025)
(version française)
This page was translated using AI tools (Deepl, GPT, ...)
(list of all news)