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 2013 – 2014

  • 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, to appear. 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
  • Just-In-Time Compilation of Knowledge Bases. Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, in 23rd International Joint Conference on Artificial Intelligence (IJCAI-13), 2013.
  • Resolution and Parallelizability: Barriers to the Efficient Parallelization of SAT Solvers. George Katsirelos, Ashish Sabharwal, Horst Samulowitz, Laurent Simon, in Proceedings of the Twenty-Seventh Conference on Artificial Intelligence (AAAI-13), 2013.
  • Improving Glucose for Incremental SAT Solving with Assumption: Application to MUS Extraction. Gilles Audemard, Jean-Marie Lagniez, Laurent Simon, in Proceedings of SAT 2013, 2013.
  • Du Glucose en goutte à goutte pour les coeurs inconsistants, G. Audemard, J.-M. Lagniez, L. Simon. In Neuvièmes Journées Francophones de Programmation par Contraintes (JFPC 2013)}, 2013. french