Parallelization CSP / SAT (Master's Internship)

30 November 2024

Most recent news

(list of all news)

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


Launch of the Institutional Diploma in AI

(13 February 2025)

The institutional diploma "Experts in AI" has just been established, right after the AI summit in Paris (ahead of schedule!). This program was proposed thanks to the impetus of the...


Page on the AI Convention

(09 February 2025)

After months of preliminary work, we are officially launching the recruitment of students for the student citizen convention that will take place at the Bordeaux Métropole premises on the weekend...


AI in Initial Training

(30 January 2025)

AI and Training: From University to the Professional World With Juliette MATTIOLI, Expert Fellow in AI at Thalès, we had the pleasure of presenting, in two hours, the challenges of...


AI & Training

(24 January 2025)

As part of a series of meetings and conferences organized by France Travail (with more than 400 visitors in total), at the premises of Bordeaux Métropole, I had the pleasure,...

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)