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 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.
ANR SATAS starts this year.
Take a look to Ampharos a distributed SAT solver.
Glucose and Glucose-syrup obtained good results during SAT-RACE 2015
Glucose 4.0 is out! This version participated to SAT competition 2014. We merge the parallel and the sequential version inside one source code. The sequential version always contains incremental task (see SAT 2013 paper) and can extract a certified UNSAT (using DRUP format). The parallel version uses an original mechanism for clause sharing (see SAT14 paper)
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.
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