Parallelization CSP / SAT (Master's Internship)

30 November 2024

Most recent news

(list of all news)

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)....


Does AI Still Belong to Digital Science ?

(03 June 2025)

I had the pleasure of opening the AI Day in Nouvelle Aquitaine, organized by AI in Nouvelle Aquitaine. For this occasion, I allowed myself to venture into areas close to...


2025 Graduation Ceremony

(15 March 2025)

Last Saturday was, as every year, the graduation ceremony for the students of ENSEIRB-MATMECA, where I am still the head of the Computer Science department for a few more months....


Weekly Eco Interview on TV7

(20 February 2025)

Last Wednesday, I had the opportunity to answer questions from Stéphanie Lacazze, from Sud Ouest, as part of [Hebdo Éco](https://www.sudouest.fr/lachainetv7/economie/l-hebdo-eco/) on TV7. It’s a local TV channel belonging to the...

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)