About me

I am professor in the Artois University, located in the north of France. My researches focus on satisfiabilty, quantified boolean formulas, SAT based problems and constraint satisfaction problems.


Glucose, our SAT solver

Glucose is a SAT solver based on a particular scoring scheme for the clause learning mechanism, based on the paper Laurent Simon and I wrote at IJCAI'09. Solver's name is a contraction of the concept of "glue clauses", a particular kind of clauses that glucose detects and preserves during search. Glucose is heavily based on Minisat, so please do cite Minisat also if you want to cite Glucose.
Home page of Glucose.


XCSP3

XCSP3 is a XML-based format designed to represent combinatorial constrained problems. It is compact, easy to read and to parse. Importantly, This new format (partly) captures the structure of the problem models, through the possibilities of declaring arrays of variables, and identifying syntactic and semantic groups of constraints. XCSP3 introduces a limited set of basic constraint forms, and allows many variations of them through lifting, restriction, sliding, logical combination and relaxation mechanisms. As a result, XCSP3 encompasses practically all constraints that can be found in major constraint solvers.
The objective of XCSP3 is to ease the effort required to test and compare different algorithms by providing a common test-bed of combinatorial constrained instances.
Home page of XCSP3.


News

glucose 4.1 is out. This version participated to SAT competition 2016. It uses an automated adaptation (tuned by hand) w.r.t. the kind of search the solver is doing during the first 100,000 conflicts (see our 2016 paper about that)

glucose was used to solve the boolean Pythagorean Triples problem producing "the largest math proof ever".

ANR SATAS started in 2016.

Take a look to Ampharos a distributed SAT solver.


Awards

Best papers

Our paper "Impact of Community Structure on SAT Solver Performance" has received the best student paper award at SAT 2014 conference.

Our paper "On freezing and reactivating learnt clauses" has received the best paper award at SAT 2011 conference.


SAT RACE 2015

Glucose 4.0 was ranked first in parallel track and 3rd in incremental track.


SAT Competition 2014

Glucose 3.0 obtained several medals: 2nd in Apppcation certified UNSAT, 3rd in Hard combinatorial certified UNSAT.

PeneLoPe was ranked 2nd in Apppcation parallel track!. This new version is available online.


SAT Challenge 2013

Glucose 2.3 obtained 5 prizes !

PeneLoPe was ranked 3rd in parallel track.


SAT Challenge 2012

Glucose 2.1 was ranked 1st (single engine solver).

PeneLoPe was ranked 2nd in parallel track.


SAT competition 2011

Glucose 2.0 obtained three medals:


SAT competition 2009

Glucose 1.0 obtained two medals