The glucose SAT solver
XCSP3 format and PyCSP3 modelisation tool
pFactory, a parallel library.
Ampharos, a distributed SAT solver.
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.
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 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.
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 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 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 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.
CAV award in 2021 for pionnering contributions to the foundations of SMT.
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.
Cosoco (my constraint solver) won the first prize on the track Fast COP, at XCSP22 competition.
glucose and syrup obtained several medals. First in the parallel track, 2nd in incremental track and also 2nd in agile track.
Glucose 4.0 was ranked first in parallel track and 3rd in incremental track.
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.
Glucose 2.3 obtained 5 prizes !
PeneLoPe was ranked 3rd in parallel track.
Glucose 2.1 was ranked 1st (single engine solver).
PeneLoPe was ranked 2nd in parallel track.
Glucose 2.0 obtained three medals:
Glucose 1.0 obtained two medals