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.


News

Release 1.0 of PyXAI is out.

Cosoco (my constraint solver) won the third prize on track Fast COP at XCSP23 competition.

Cosoco (my constraint solver) won the first prize on track Fast COP at XCSP22 competition.

I am a member of the AI Chair EXPEKCTATION of the French National Research Agency (ANR). The project started on September 2020.

CP 2018 was in Lille

SAT competition 2017: glucose-syrup is ranked first in parallel track. Glucose also obtains 2 silver medals.

The first release of cosoco, a CSP solver written in C++, is now available. A git/mercurial repository will come shortly.

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.


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.


PyXAI, eXplainable IA in Python.

PyXAI (Python eXplainable AI) is a Python library (version 3.6 or later) allowing to bring formal explanations suited to (regression or classification) tree-based ML models (Decision Trees, Random Forests, Boosted Trees, ...). In contrast to many approaches to XAI (SHAP, LIME, ...), PyXAI algorithms are model-specific. Furthermore, PyXAI algorithms guarantee certain properties about the explanations generated.
Home page of PyXAI.


SAT Heritage

A community-driven effort for archiving, building and running more than thousand SAT solvers


SAT research has a long history of source code and binary releases, thanks to competitions organized every year. However, since every cycle of competitions has its own set of rules and an adhoc way of publishing source code and binaries, compiling or even running any solver may be harder than what it seems. And there has been more than a thousand solvers published so far, some of them released in the early 90's!

This project drives a community-driven effort to archive and to allow easy compilation and running of all SAT solvers that have been released so far.

Thanks to our tool, building (or running) a solver from its source (or from its binary) can be done in one line.

Home page of SAT Heritage.

pFactory

A generic library for designing parallel solvers


pFactory is a parallel library designed to support and facilitate the implementation of parallel solvers in C++. It provides robust implementations of parallel algorithms and allows seamlessly sharing mechanisms, divide-and-conquer or portfolio methods. pFactory is not related to a specific problem and can very easily be incorporated in order to solve any kind of combinatorial problem (SAT, CSP, MAXSAT...).

Home page of pFactory.

XCSP3 and PyCSP3

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.

PyCSP3

PyCSP3 is a Python library that allows us to write models of combinatorial constrained problems in a declarative manner. Currently, with PyCSP3, you can write models of constraint satisfaction and optimization problems. More specifically, you can build models for CSP and COP problems. The website contains mode than 60 jupyter notebooks to discover popular constraints and classical problems.
Home page of PyCSP3.


Awards

Skolem award. In 2023, our paper " A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions" won the skolem award for a CADE paper that has passed the test of time, by being a most influential paper in the field.

CAV award in 2021 for pionnering contributions to the foundations of SMT.


Best papers

Our paper "PyXAI : calculer en Python des explications pour des modèles d'apprentissage supervisé" (in french) won the best demonstration prize in EGC 2023.

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.


XCSP competition 2023

Cosoco (my constraint solver) won the third prize on the track Fast COP, at XCSP23 competition.


XCSP competition 2022

Cosoco (my constraint solver) won the first prize on the track Fast COP, at XCSP22 competition.


SAT Competition 2017

glucose and syrup obtained several medals. First in the parallel track, 2nd in incremental track and also 2nd in agile track.


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