Professor at the Bordeaux Computer Science Laboratory (Labri) / Bordeaux Institute of Technology (INP) since 2013.
Previously Associate Professor at the Computer Science Laboratory of Orsay (LRI).
Clearly, the contest 2013 was for the Lingeling family and the "in-processing" techniques. However, Glucose performed very well in
New SAT 2016 Will be in Bordeaux!
I'm very pleased to be the local organizer for the SAT 2016 Conference. The Program Chairs are Daniel Le Berre and Nadia Creignou. Do take a look at this very nice web site about SAT 2016 to check the upcoming deadlines and all the associated events. You can also check the social links for this event:
Glucose is a SAT solver based on a particular scoring scheme for the clause learning mechanism, based on the paper Gilles Audemard 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.
SAT is a fundamental problem of computer science that, intuitively, captures all the easiest of the hard problems. Hard problems mean problem that cannot be solved efficiently (you'll need more time than the universe had on large problems!). If you want to read more about it, why not taking your with the Wikipedia page about SAT ?
Those events are very important for the whole SAT community. I was involved in the first cycle of competitions (2002-2009). In 2009, I chosen to act only as an "advisor" to focus on Glucose, on which I had many expectations. I'm now "off" the competition. But I had fun with it! Take a look at the competition web site . In the next few weeks, I'll try to put all the datas I have about past competitions. Stay tuned.