Gilles Audemard

News

New accepted papers at ECAI'24 and IJCAI'24

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

CoSoCo

A constrained based solver

Written in C++, CoSoCo is a solver that can solve XCSP3 problems. It solves both satisfaction and optimization problems. It supports almost all constraints from XCSP3 core (sum, count, nvalues, regular, table, binpacking...).
CoSoCo would not have taken place without Christophe Lecoutre. I would like to thank him very warmly for his support. Indeed, this is the result of many discussions and most of the contraint propagators come from ACE.

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

XCSP³ and PyCSP³

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.

PyCSP³

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.