Laurent Simon's Home Page

Recent News (3th of July, 2009): glucose, our SAT solver (with G. Audemard), is the world's best SAT solver on Application/Industrial benchmarks, UNSAT category (according to the last SAT competition). Go to glucose home page.

Research interests

I am Assistant Professor (Maître de Conférences), in the Artificial Intelligence and Inference System group (IASI) of the LRI laboratory in Paris 11, France, since 2002. Our team is a joint-team with INRIA, around the GEMO project.
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).

Before winning a trophy in the SAT Competition 2009, I was involved as a co-organizer of all previous competition (SAT02, SAT03, SAT04, SAT05, SAT07 competitions). In 2009, to be allowed to win the first prize, I was just a 'Technical Advisor' instead of a co-organizer. For more information about those outstanding events of the SAT community, please visit the official competition web page, located at www.satcompetition.org

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 (project web page available soon).

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 !

Softwares

glucose

Our SAT solver, glucose (the SAT solver that looks for glue clauses), won the SAT Competition 2009 in the Application (Industrial) UNSAT Track, a track of particular interest for many industrial applications of SAT. It also has the silver medal in the SAT+UNSAT track (it solved the same number of benchmarks as precosat). This is the first time a french team wins the competition in the Application/Industrial track. Our solver is based on the last publicly available version of Minisat and illustrates the efficiency of our new static score of clauses, based on our IJCAI'09 paper (see below).

Source code and paper available at glucose home page

somewhere

SomeWhere is a Java-Based semantic peer-to-peer data management system that promotes a small is beautiful vision of the Semantic Web based on simple personalized ontologies (e.g., taxonomies of classes) but which are distributed at a large scale. In this vision of the Semantic Web, no user imposes to others his own ontology. Logical mappings between ontologies make possible the creation of a web of people in which personalized semantic marking up of data cohabits nicely with a collaborative exchange of data. In this view, the Web is a huge peer-to-peer data management system based on simple distributed ontologies and mappings. You can see how the Firefox somewhere extension works. Project done with P. Adjiman, M.-C. Rousset, F. Goasdoué, P. Chatalic.

zres

zres is an implementation of the very procedure of Davis and Putnam as stated in 1960. It uses ZBDDs as a data structure to represent set of clauses. It demonstrates the efficiency of multi-resolution for symbolic reasoning. The package used to manipulate ZBDD is the CUDD package (a great BDD package), available the home page of Fabio Somenzi, its main author.

zres is a very good solver for prime implicates generation, one of the hardest tasks of classical A.I. approaches to reasonning.

zres was successfully extended to QBF by M. Vardi to QMRes with Guoqiang Pan.

satex

The SatEx was a web-site publishing experiments of solvers on benchmarks. It has been replaced by all sat competitions and sat races web sites. If you need to acces to my old datas (old solvers, old benchmarks (before 2002)), please contact me. I'm trying to build a new satex web site, but this may take me some time.

Selected bibliography

2009

[AS09a]	Predicting Learnt Clauses Quality in Modern SAT Solver G. Audemard, L. Simon, in Twenty-first International Joint Conference on Artificial Intelligence (IJCAI'09), july 2009.
[AS09a]	Pourquoi les solveurs SAT modernes se piquent-ils contre des cactus ? G. Audemard, M. S. Modeliar and L. Simon, in JFPC'09, june 2009.

2008

[ADS08c]	Distributed Consistency-Based Diagnosis V. Armant, P. Dague, L. Simon. in LPAR'08, [pdf ].
[ADS08b]	Distributed Consistency-Based Diagnosis without Conflicts V. Armant, P. Dague, L. Simon. in DX'08, [pdf ].
[ADS08a]	Diagnostic distribué à base de modèles sans calcul préalable des conflits V. Armant, P. Dague, L. Simon. in JFPC'08 (French Conference) [pdf ].
[AS08a]	Experimenting with Small Changes in Conflict-Driven Clause Learning Aglorithms G. Audemard, L. Simon. in CP'08. You may find our A0 poster here. The paper is here: [ pdf ]
[DS08a]	Algorithmes de Recherche Systématique , Chapitre de Livre (in French) dans SAT : Progrès et défis, G. Dequen, L. Simon. Editeur Lakhdar Saïs, chez Hermès Lavoisier Editions (lien vers le livre ).

2007

[AS07a]

GUNSAT: A Greedy Local Seach Algorithm for Unsatisfiability G. Audemard, L. Simon. in IJCAI'07, as a short/poster paper. You may find our A0 poster here. [ pdf ]
You can also download the gunsat-V1 jar file used in the experiments.

2005

[ACG⁺05b]	Distributed Reasoning in a Peer-to-Peer Setting: Application to the Semantic Web P. Adjiman, P. Chatalic, F. Goasdoué, M.-C. Rousset, and L. Simon. JAIR.
[S05]	Some Results and Lessons from the SAT Competitions. L. Simon. Invited Talk in the Second International Workshop on Constraint Propagation and Implementation, held in conjunction with Eleventh International Conference on Principles and Practice of Constraint Programming (CP'2005), Sitges, Spain, 2005. Slides Only. [ zip ]
[ACG⁺05a]	Scalability study of peer-to-peer consequence finding. P. Adjiman, P. Chatalic, F. Goasdoué, M.-C. Rousset, and L. Simon. In International Joint Conference on Artificial Intelligence (IJCAI), 2005. [ bib \| .pdf ]

2004

[BS04]	Fifty-five solvers in vancouver: The sat 2004 competition. D. Le Berre and L. Simon. In Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT2004), volume Lecture Notes in Computer Science. 2004. Accepted for publication. [ bib \| .ps.gz ]
[DLBT04]	The second qbf solvers comparative evaluation. L. Simon D. Le Berre, M. Narizzano and A. Tacchella. In Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT2004), volume Lecture Notes in Computer Science. 2004. Accepted for publication. [ bib \| .pdf ]
[ACG⁺04a]	Distributed reasoning in a peer-to-peer setting. Philippe Adjiman, Philippe Chatalic, Francois Goasdoue, Marie-Christine Rousset, and Laurent Simon. In European Conference on Artificial Intelligence (ECAI'04),, 2004. [ bib ]
[ACG⁺04c]	Somewhere in the semantic web. Philippe Adjiman, Philippe Chatalic, Francois Goasdoue, Marie-Christine Rousset, and Laurent Simon. Technical report, LRI, 2004. [ bib \| .pdf ]
[ACG⁺04b]	Raisonnement distribué dans un environnement de type pair-à-pair. Philippe Adjiman, Philippe Chatalic, Francois Goasdoue, Marie-Christine Rousset, and Laurent Simon. In Actes des Dixièmes Journées Nationales sur la Résolution Pratique de Problèmes NP-Complets (JNPC'04), pages 259-270, Angers, 21-22-23 Juin 2004. [ bib \| .ps.gz \| .pdf ]

2003

[BS03]	The Essentials of the Sat'03 competition. D. Le Berre and L. Simon. In A. Tacchella E. Giunchiglia, editor, Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT2003), volume Lecture Notes in Computer Science 2919, pages 452-467. June 2003. [ bib \| .ps.gz ]
[BST03]	Challenges in the qbf arena: the sat'03 evaluation of qbf solvers. D. Le Berre, L. Simon, and A. Tachella. In A. Tacchella E. Giunchiglia, editor, Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT2003), volume Lecture Notes in Computer Science 2919, pages 468-485. June 2003. [ bib ]

2002

[SBH05]	The SAT 2002 competition. L. Simon, D. Le Berre, and E. Hirsch. Accepted for publication in Annals of Mathematics and Artificial Intelligence (AMAI), 43:343-378, 2005. [ bib \| .ps.gz ]
[PPS05]	A phylogenetic tree for the sat 2002 contest. D. Le Berre P. Purdom and L. Simon. Accepted for publication in Annals of Mathematics and Artificial Intelligence (AMAI), 43, 2005. [ bib ]

2001

[CS01a]	Multiresolution for sat checking. P. Chatalic and L. Simon. Journal of Artificial Intelligence Tools, 10(4), December 2001. [ bib \| .ps.gz ]
[SC01]	SATEx: a Web-based Framework for SAT Experimentation. Laurent Simon and Philippe Chatalic. In Henry Kautz and Bart Selman, editors, Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001), Boston University, Massachusetts, USA, June 14th-15th 2001. Online Publication. [ bib \| http \| .ps.gz \| .pdf ]
[SdV01]	Efficient consequence finding. Laurent Simon and Alvaro del Val. In 17th International Joint Conference on Artificial Intelligence (IJCAI'01), pages 359-365, Seattle, Washington, USA, 2001. [ bib \| .ps.gz \| .pdf ]
[CS01b]	SatEx : un cadre de travail dynamique pour l'expérimentation SAT. Philippe Chatalic and Laurent Simon. In Actes des Septièmes Journées Nationales sur la Résolution Pratique de Problèmes NP-Complets (JNPC'01), pages 259-270, Toulouse, 27-28-29 Juin 2001. [ bib \| .ps.gz \| .pdf ]
[Sim01b]	SatEx: towards and exhaustive and up-to-date SAT experimentation. Laurent Simon. IJCAI'01 Workshop on Empirical Methods in Artificial Intelligence (Organized by H. Hoos and T. Stützle), August 4th 2001. [ bib \| .ps.gz \| .pdf ]
[Sim01a]	Multirésolution pour le test de consistance et la déduction en logique propositionnelle. L. Simon. PhD thesis, Université Orsay Paris XI, Décembre 2001. [ bib ]

2000

[CS00e]	Zres: The old Davis-Putnam procedure meets ZBDDs. Philippe Chatalic and Laurent Simon. In David McAllester, editor, 17th International Conference on Automated Deduction (CADE'17), number 1831 in Lecture Notes in Artificial Intelligence (LNAI), pages 449-454, June 2000. [ bib \| .ps.gz ]
[CS00a]	Are pigeon hole and urquhart problems really exponential for DP? Philippe Chatalic and Laurent Simon. In Third Workshop on the Satisfiability Problem (SAT2000), May 2000. Slides of the presentation only. [ bib \| .ps.gz ]
[CS00b]	Davis and Putnam 40 years later: a first experimentation. Philippe Chatalic and Laurent Simon. Technical Report 1237, LRI, Université Paris-Sud, 91405 Orsay Cedex, France, 2000. [ bib \| .ps.gz ]
[CS00c]	Multi-Resolution on compressed sets of clauses. Philippe Chatalic and Laurent Simon. In Twelth International Conference on Tools with Artificial Intelligence (ICTAI'00), pages 2-10, 2000. [ bib \| .ps.gz ]
[CS00d]	Résolution sur des ensembles de clauses compressés : comment doper dp. Philippe Chatalic and Laurent Simon. In Actes des Cinquièmes Journées Nationales sur la Résolution Pratique de Problèmes NP-Complets (JNPC'00), pages 107-118, Marseilles, 2000. [ bib \| .ps.gz ]

Before 2000

[CS99]	Davis et putnam, 40 ans après : une première expérimentation. Philippe Chatalic and Laurent Simon. In Actes des Sixièmes Journées Nationales sur la Résolution Pratique de Problèmes NP-Complets (JNPC'99), pages 9-16, Lyon, 1999. [ bib \| .ps.gz ]
[Sim97]	Algorithmes de calcul de résolvant. Laurent Simon. Technical report, Université Orsay Paris XI, France, Septembre 1997. Stage de DEA (only in french). [ bib \| .ps.gz ]

Some Conferences/Journal/Administrative involvement

Editorial Board Member of JSAT. This electronic Jounal is The Journal on Satisfiability, Boolean Modeling and Computation. Please do follow the link!
Guest Editor of a Special Issue on SAT 2006 Competitions and Evaluations.
PC Member of ECAI 2006 (august 28th - September 1st, 2006 in Trentino, Italia).
PC Member of SAT-03, SAT-04, SAT-05, SAT-07 and SAT-10 conferences on Satisfiability.
PC Member of ESCAR-05, Workshop on Empirically Successful Classical Automated Reasoning, ESCoR-06, the FLoC'06 Workshop on Empirically Successful Computerized Reasonning, and on the Special Issue of the Journal of Applied Logic on Empirically Successful Computerized Reasoning (ESCoR) .
SAT-2002, 2003, 2004, 2005 and 2007 Competition Chair (with Daniel le Berre, and Edward Hirsch (for SAT-2002))
PC Member of JNPC-03, JNPC-04, JFPC-05, JFPC-06 and JFPC-07 (French Conferences). These conferences are supported by the AFPC, the Association Française pour la Programmation par Contraintes, in which I'm also involved.
Commission de Spécialiste (27) Member of university of Marseille (from 2007-Now), and Commision de Spécialiste Mixte (27) of University of Paris 11 (in the IFIPS Commission, from 2006-Now).

Teaching

Here is a picture of our 2005 engineering high school diploma ceremony.

2003- now: In charge of the last year of our university engineering school, computer science department IFIPS. You can find my current teaching home page here . I am teaching Languages and Data structures, Artificial Intelligence and Artificial Intelligence for Computer Games (especially Real-time video games (FPS/RTS)).
2002-2003: Operating Systems, Computer architecture, Networks, Unix Systems, Languages and Data structures and Artificial Intelligence
2001-2002: Operating Systems, C projects , Imperative Programming Approach
2000-2001: Computer architecture, Operating Systems
1999-2000: Languages and Data structures, Imperative Programming Approach
1998-1999: Languages and Data structures, Functional Programming Approach
before 1998: Office (Windows, Excel, Word...) Tools and Pascal Programming

How to contact me

By post mail:
Laurent Simon,
LRI / INRIA Futurs,
Parc Club Université,
Batiment G, 4, rue Jacques Monod
91893 Orsay cedex
FRANCE

By phone:
+33 1 72 92 59 85
Fax : +33 1 69 15 65 86

By e-mail:
my email for spammers

On the spot:
Office G005,
(Enter the building, you'll see me).

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

2000-2009
Comments, suggestions
my email for spammers