Publications

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 our "scientific life" publicly available). I really hope you'll find something interesting in this web site, and forget about this "formal" basis for colleagues.

My Top Papers

If you want to know my work, I would like to point out this "Top 10" selection:

SAT

  • Resolution and Parallelizability: Barriers to the Efficient Parallelization of SAT Solvers. G. Katsirelos, A. Sabharwal, H. Samulowitz, L. Simon, in AAAI, 2013.
  • A Restriction of Extended Resolution for Clause Learning SAT Solvers. G. Audemard, G. Katsirelos and L. Simon, in AAAI, 2010.
  • Predicting Learnt Clauses Quality in Modern SAT Solver. G. Audemard, L. Simon, in IJCAI, 2009.

AI

  • Just-In-Time Compilation of Knowledge Bases. G. Audemard, J.-M. Lagniez, L. Simon, in IJCAI, 2013.
  • Efficient consequence finding. L. Simon and A. del Val. In IJCAI 2001.
  • Multi-Resolution on compressed sets of clauses. P. Chatalic and L. Simon. In ICTAI, 2000.

Competitions

  • The International SAT Solver Competition, M. Järvisalo, D. Le Berre, O. Roussel, L. Simon, A.I. Mag, 2012.
  • Fifty-five solvers in Vancouver: The sat 2004 competition. D. Le Berre and L. Simon. In SAT, 2004.

P2P Reasoning

  • Distributed tree decomposition with privacy. V. Armant, P. Dague and L. Simon, in CP, 2012.
  • 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. In JAIR, 2005.


Citations Banks

  • Google Scholar is up to date (I spend some time removing/adding papers by hand).
  • DBLP, with some mistakes (I'm not all the Laurent Simon in it).
Microsoft Academic Research is full of mistakes (too many Laurent Simon for it!). It's too time consuming to fix more than a couple algorithms outputs and this last one is probably the one with the more mistakes (one lucky homonym has many, many papers . Hopefully, at some point A.I. will make progress here.

Bibliography

  • 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
  • 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
  • Optimizing with Minimum Satisfiability, Chu Min Li, Zhu Zhu, Felip Manyà, Laurent Simon, Artificial Intelligence, 2012.
  • The International SAT Solver Competition, Matti Järvisalo, Daniel Le Berre, Olivier Roussel, Laurent Simon, Artificial Intelligence Magazine, 2012.
  • Distributed tree decomposition with privacy. Vincent Armant, Philippe Dague and Laurent Simon, in Proceedings of the 22nd International Conference on Principles and Practice of Constraint Programming (CP-12), 2012.
  • Eigenvector centrality in industrial SAT instances. George Katsirelos and Laurent Simon, in Proceedings of the 22nd International Conference on Principles and Practice of Constraint Programming (CP-12), 2012.
  • Refining restarts strategies for SAT and UNSAT formulae. Gilles Audemard and Laurent Simon, in Proceedings of the 22nd International Conference on Principles and Practice of Constraint Programming (CP-12), 2012.
  • Learning Polynomials over GF(2) in a SAT Solver. George Katsirelos and Laurent Simon. In Proceedings of SAT 2012, LNCS 7317, 496--497, 2012.
  • GLUCOSE 2.1: Aggressive – but Reactive – Clause Database Management, Dynamic Restarts. In Pragmatics of SAT (Workshop of SAT'12), Gilles Audemard and Laurent Simon, Juin 2012.
  • Distributed Tree Decomposition by Local Elections with One Token, V. Armant et L. Simon. Dans Sixièmes Journées d'Intelligence Artificielle Fondamentale (JIAF), 2012. french
  • Minimum Satisfiability and its Applications. Chu-Min Li, Zhu Zhu, Felip Manya, Laurent Simon, in IJCAI-2011, july 2011.
  • Satisfiabilité Minimale et Applications, Chu Min Li, Zhu Zhu, Felip Manyà, L. Simon. In Septièmes Journées Francophones de Programmation par Contraintes (JFPC 2011), 2011. french
  • Logique Propositionnelle~: un langage simple, des problèmes complexes, Habilitation à diriger des Recherches, Spécialité Informatique, Université Paris-Sud 11. Soutenue le 13 décembre 2010 devant le jury composé de Christian Bessière, Armin Biere, Lakhdar Saïs (Rapporteurs), Philippe Jégou, Bertrand Mazure (Examinateurs) et Philippe Dague (Directeur). french
  • A Restriction of Extended Resolution for Clause Learning SAT Solvers. G. Audemard, G. Katsirelos and L. Simon, in AAAI-2010, july 2010.
  • Une restriction de la résolution étendue pour les démonstrateurs SAT modernes. G. Audemard, G. Katsirelos and L. Simon, in JFPC'10, june 2010. french
  • 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.
  • Pourquoi les solveurs SAT modernes se piquent-ils contre des cactus ? G. Audemard, M. S. Modeliar and L. Simon, in JFPC'09, june 2009. french
  • Distributed Consistency-Based Diagnosis V. Armant, P. Dague, L. Simon. in LPAR'08, [ pdf ].
  • Distributed Consistency-Based Diagnosis without Conflicts V. Armant, P. Dague, L. Simon. in DX'08, [ pdf ].
  • Diagnostic distribué à base de modèles sans calcul préalable des conflits V. Armant, P. Dague, L. Simon. in JFPC'08 (French Conference) french [ pdf ].
  • 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 ]
  • 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 ). french
  • 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.
  • 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.
  • 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 ]
  • 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.
    [ .pdf ]
  • 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.
    [ .ps.gz ]
  • 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.
    [ .pdf ]
  • 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.
  • Somewhere in the semantic web. Philippe Adjiman, Philippe Chatalic, Francois Goasdoue, Marie-Christine Rousset, and Laurent Simon. Technical report, LRI, 2004.
    [ .pdf ]
  • 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.
    [ .ps.gz | .pdf ]
  • 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.
    [ .ps.gz ]
  • 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.
  • 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.
    [ .ps.gz ]
  • 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.
  • Multiresolution for sat checking. P. Chatalic and L. Simon. Journal of Artificial Intelligence Tools, 10(4), December 2001.
    [ .ps.gz ]
  • 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.
    [ http | .ps.gz | .pdf ]
  • 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.
    [ .ps.gz | .pdf ]
  • 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.
    [ .ps.gz | .pdf ]
  • 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.
    [ .ps.gz | .pdf ]
  • 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.
  • 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.
    [ .ps.gz ]
  • 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.
    [ .ps.gz ]
  • 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.
    [ .ps.gz ]
  • 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.
    [ .ps.gz ]
  • 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.
    [ .ps.gz ]
  • 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.
    [ .ps.gz ]
  • Algorithmes de calcul de résolvant. Laurent Simon. Technical report, Université Orsay Paris XI, France, Septembre 1997. Stage de DEA (only in french).
    [ .ps.gz ]