SAT'11 Proc.


Aug, 2011: (New) Web Site opens

Last News

glucose v2.1 code released
Jul, 2012

glucose v2.1 won the "best single engine solver in the application track" category un the SAT challenge 2012.
Jun, 2012

glucose v.2 released
Jul. 12, 2011

glucose v2 won 3 medals at the SAT 2011 competition
Jun. 23, 2011

SAT Conference
June 19th to 22th, 2011 (inclusive)

Don't Miss this

SAT'2013 in Helsinki!


This Site will close! Since September 2013, I have a professor position at the Labri (Bordeaux). This web site is obsolete now and I strongly encourage you to jump to my new web site! In a few months, I'll close this web site and put redirections.

Me - At a glance

The PCRI Building, 2011
The PCRI Building
We moved here in july, 2011

I am Associate Professor (Maître de Conférences - HDR), in the Artificial Intelligence and Inference System group (IASI) of the LRI laboratory in the University of Orsay Paris 11, France, since 2002. My main research interests are on propositional-based reasoning, on efficient Prime Implicates generation, and SAT solvers. I'm also working on decentralized approaches to those 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 reasonning systems to diagnosis of (intrinsic) distributed systems.

Research around SAT

Glucose Glues Clauses
glues clauses

I started studying the SAT problem during my Master Thesis (already years ago!), mainly for fault-tree diagnosis, from an A.I. point of view. Then, I focused my research during my PhD on Knowledge Compilation techniques (based on BDD). I built the SATEX web site during the last year of my PhD and I was offered to organize the second cycle of SAT competitions (SAT02, SAT03, SAT04, SAT05, SAT07). In 2009, because we had made substantial progresses with our solver glucose, I asked to be just a "technical consultant" in the competition, in order to be able to participate to the contest. And, glucose won an trophy in 2009 (Applications, UNSAT), a Gold Medal in 2011 (glucose v2, Applications, SAT+UNSAT) and a best prize at last SAT Challenge (2012), as "the best single-engine solver in the application track". I'm really happy for this, especially for 2011/2012: there was a lot of competitors, and most solvers embedded our ideas of 2009, so we had to keep our advance by new ideas!
I really think that we'll see a new era of solvers in the very next few years. The last "SAT revolution" was in 2001, and nowadays solvers are more and more uncomplete, fast, robust... I'm thus working on a new generation of SAT solvers. That's an incredibly exciting challenge!

I'm also reponsible for a national (french) project ("ANR Blanc", a 3-years grants from the French National Agency for Research, started in january 2009) on Uncomplete search algorithms for Unsatisfiability, called UNLOC.

Responsabilities and teaching

Since 2011, September, I'm very happy to be in charge of the Computer Science teachings of our first year students, first semester (L1) at our university. Before that, I was in charge of the last year of the computer science engineering school (Polytech Paris Sud). This was very exciting, and really interesting, but I wanted to move to a broader "audience".

I'm teaching Artificial Intelligence and Computer Science, mainly. But you can find more details in the "teaching" part of this site.

At last (but not at least!) I'm also in the Editorial Board of in The Journal on Satisfiability, Boolean Modeling and Computation. It's a peer reviewed Journal guaranteeing fast publication on SAT. I was also in a number of Program Commitees, that can be found in a small part of this site.

About this site

Home pages of researchers are strange: it's like a "live" CV opened worldwide. Don't misunterpret this point: It's just the usual way of introducing ourselves to colleagues and to make the research living (when we look for a paper, for a reviewer, for a program committee, for a project, we like to find everything we need on the web: so, we also make oure "scientific life" publicly available). I really hope you'll find something interesting in this web site, and forget about this "formal" basis for colleagues.

How to contact me

By post mail:
Laurent Simon,
LRI (Laboratoire de Recherche en Informatique),
Bâtiment 650 (PCRI),
91405 Orsay
By phone:
+33 1 69 15 71 72
Fax : +33 1 69 15 65 86

By e-mail:
my email for spammers

On the spot:
Office 271,
(Second Floor, East).

You can also use my public PGP key to send me encrypted PGP messages, or check my e-mail signature.