Laurent Simon Research & Teaching web pages

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

A.I. Theorem Prover Propositional Logic Constraints SAT P2P Reasoning Diagnosis Metabolic Pathways Analysis
P/NP A.I. C Programming Web Programming Video Games POSIX
Research Keywords
Current Teaching Keywords

Glucose in the Contest 13

Clearly, the contest 2013 was for the Lingeling family and the "in-processing" techniques. However, Glucose performed very well in

  • Certified UNSAT, when you want a proof for the UNSAT answer;
  • Hard Combinatorial problems.
A two-words analysis : In processing techniques are indeed harder to implement if you want to be able to produce a trace of your solver, and thus Lingling was not participating this track. However, we think that Glucose is very good at producing some kind of short – and easy to find – proofs. This could explain both good positions of Glucose in the contest 2013 rankings.


What's next?

Our Glucose secret agenda is
  • Parallelizing Glucose (2015)
  • Adding inProcessing
  • Understand Glucose (yes!)
  • and really secret things


Upcoming Deadlines

New SAT 2016 Will be in Bordeaux!

About me in two words

My main research interests are on propositional-based reasoning, SAT solving and efficient Prime Implicates generation / Knowledge Base Compilation. I'm also working on decentralized approaches of some of these topics (reasoning on top of P2P and social networks) and how to push computer science to a real experimental science (especially search algorithms). I'm also trying to apply those decentralized reasoning systems to diagnosis of (intrinsic) distributed systems.


SAT 2016 In Bordeaux ! Don't miss it!

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:


About Glucose Our SAT Solver

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.

More About Glucose »

What is SAT?

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 ?

About SAT Competitions

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.


Last Papers (since 2014)

  • Diagnosability Planning for Controllable Discrete Event Systems. Hassan Ibrahim, Philippe Dague, Alban Grastien, Lina Ye, Laurent Simon, in AAAI Conference on Artificial Intelligence (AAAI 2017), 2017.
  • Seeking Practical CDCL Insights from Theoretical SAT Benchmarks. Jan Elffers, Jakob Nordstrom, Laurent Simon, Karem A. Sakallah, in Pragmatics of SAT Workshop, 2016.
  • SAT-Based Testing of Diagnosability and Predictability of Centralized and Distributed Discrete Event Systems. Hassan Ibrahim, Philippe Dague, Laurent Simon, in Eighth International Conference on Advances in System Testing and Validation Lifecycle (VALID), 2016.
  • Minimality of Metabolic Flux Modes under Boolean Regulation Constraints. Martin Morterol, Philippe Dague, Sabine Peres, Laurent Simon, in Workshop on Constraint-Based Methods for Bioinformatics (WCB), 2016.
  • Aberrations dans les Problèmes SAT. Gilles Audemard, Laurent Simon, in Journées Francophones de Programmation par Contraintes (JFPC 2014), 2016. french
  • Extreme Cases in SAT Problems. Gilles Audemard, Laurent Simon, in International Conference on Theory and Applications of Satisfiability Testing (SAT)em>, 2016.
  • Using community structure to detect relevant learnt clauses. Carlos Ansótegui, Jesús Giráldez-Cru, Jordi Levy, Laurent Simon, in International Conference on Theory and Applications of Satisfiability Testing (SAT), 2015.
  • Glucose and Syrup in the SAT Race 2015. Gilles Audemard, Laurent Simon in Reports on the SAT 2015 Competition, 2015.
  • Using Incremental SAT for Testing Diagnosability of Distributed DES. Hassan Ibrahim, Philippe Dague, Laurent Simon, in DX@Safeprocess, 2015.
  • Lazy Clause Exchange Policy for parallel SAT solvers. Gilles Audemard, Laurent Simon, in 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), 2014.
  • Impact of Community Structure on SAT Solver Performance. Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, in 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), 2014.
  • Post Mortem Analysis of SAT Solver Proofs. Laurent Simon, in Fifth Pragmatics of SAT workshop (POS'14), 2014.
  • SAT-Based Metabolics Pathways Analysis Without Compilation. Sabine Peres, Martin Morterol and Laurent Simon, in 12th Conference on Computational Methods in Systems Biology (CMSB'14), 2014.
  • Améliorer SAT dans le cadre incrémental. Gilles Audemard, Armin Biere, Jean-Marie Lagniez, Laurent Simon, in Revue d'Intelligence Artificielle (RIA), 2014. french
  • Oublier pour mieux régner : une courte étude expérimentale. Laurent Simon, in Dixièmes Journées Francophones de Programmation par Contraintes (JFPC 2014), 2014. french