Recherche/Research Activities

Je m'intéresse a la résolution automatique de problèmes en logique propositionnelle.

Mes travaux se situent plus particulièrement autour des thèmes suivants:

• SAT
• QBF
• Raisonnement non monotone

Logiciels/Software

SAT4J

Alloy4Eclipse: write Alloy 4 specifications within Eclipse. Powered in part by SAT4J.

If you like Sudoku, you should take a look at the Sudoku as Satisfiability web page.

Former projects

Animation de la recherche

Projets/Grants

• 2006/2007 PAI PESSOA MUSICA (with INESC)
• 2005 Action integree Luso Francaise de la CPU (PB05, with INESC)
• 2003 Action integree Luso Francaise de la CPU (OpenSAT, with INESC)
• 2003 Action Specifique STIC-CNRS (ASQBF, with LRI)

Membre de comité éditorial/editorial board member

Présentations invitées / Invited talks

• Software dependency management: from p2 to p2cudf (LoCoCo 2011)
• SAT4J: pseudo-boolean optimization and dependency management problems (SAT/SMT summer school @ MIT 2011)
• A brief introduction to practical SAT solving: what can I expect from SAT today? (Workshop on SAT solving, Tuebingen)
• Lecture on SAT (part1, part2) (Summer School 2009: Verification Technology, Systems & Applications)
• Some Applications of SAT, SAT assessing the progress, Baltimore, 2008 (report)

Membre de comité de programme/Program committee membership

Autre/Other

Technical consultant for the SAT Race 2006 and the upcoming SAT Race 2008.

New web site for the SAT competitions: satcompetition.org

SAT2005 competition

SAT2004 competition

QBF2004 Evaluation

SAT2003 competition

QBF2003 Evaluation

Co-organisateur, avec Laurent Simon et Edward Hirsh, de la compétition de prouveur SAT associée a la conférence SAT2002.

Je maintiens un site web dédié au problème SAT appelé/I maintain a web site dedicated to SAT called SAT Live!.

Publications majeures/Selected publications

Editorial activities

SAT

Paul W. Purdom, Daniel Le Berre, Laurent Simon, A Parsimony Tree for the SAT2002 Competition, Annals of Mathematics and Artificial Intelligence, Volume 43, Issue 1 - 4, Jan 2005, Pages 343 - 365(online)

LE BERRE D. et Simon L., "The essentials of the SAT 2003 competition". Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT2003). Lecture Notes in Computer Science 2919, pp 452-467, 2003.(Postscript)

AUDEMARD G., LE BERRE D., ROUSSEL O., "OpenSAT: une plateforme SAT Open Source", Actes des Neuvièmes Journées Nationales sur la Résolution Pratique de Problèmes NP-Complets (JNPC'03), Juin 2003.

Gilles Audemard, Daniel LE BERRE, Olivier Roussel, Ines Lynce and Joao Marques Silva. "OpenSAT: an open source SAT solftware project". Poster to be presented at SAT2003.

LE BERRE D., "Exploiting the real power of unit propagation lookahead", dans : Henry Kautz and Bart Selman, Proceedings of the Workshop on Theory and Applications of Satisfiability Testing (SAT2001), Elsevier Science Publishers, vol. 9, Electronic Notes in Discrete Mathematics, Boston University, Massachusetts, USA, Juin 2001 (Postscript, Slides).

QBF

COSTE-MARQUIS S., Fargier H., Lang J., LE BERRE D., MARQUIS P., "Résolution de formules booléennes quantifiées : problèmes et algorithmes", Actes du 13e Congrès AFRIF-AFIA Reconnaissance des Formes et Intelligence Artificielle (RFIA-02), pp 289-298, Angers, France, 2002 (Postscript)

Raisonnement non monotone/Nonmonotonic reasoning

Benferhat S., Kaci S., LE BERRE D., Williams M.-A., "Weakening conflicting information for iterated revision and knowledge integration", Artificial Intelligence, vol. 153, pp 339-371, 2004. Version étendue du papier IJCAI'01.

Brewka G., Benferhat S., LE BERRE D., "Qualitative Choice Logic", Proceedings of the 8th International Conference on Principles of Knowledge Representation and Reasoning (KR'02), Morgan Kaufmann Publishers, Inc., pp 158-169, Toulouse, France, Avril 2002 (Postscript)

Benferhat S., Kaci S., LE BERRE D., Williams M.-A., "Weakening conflicting information for iterated revision and knowledge integration", Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI'01), Morgan Kaufmann Publishers, Inc., vol. 1, pp 109-115, Seattle, Washington, USA, Août 2001 (Postscript)

Dubois D., LE BERRE D., Prade H., Sabbadin R., "Using possibilistic logic for modeling qualitative decision: Atms-based algorithms", Fundamenta Informaticae, vol. 37, pp 1-30, 1999

Dubois D., LE BERRE D., Prade H., Sabbadin R., "Logical representation and computation of optimal decisions in a qualitative setting", Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI'98), pp 588-593, Madison, 1998 (Postscript)

Castell T., Cayrol C., Cayrol M., LE BERRE D., "Modèles P-restreints : application à l'inférence propositionnelle", Actes du Onzième Congrès Reconnaissance des Formes et Intelligence Artificielle (RFIA'98), pp 205-214, Clermont-Ferrand (France), 1998

Castell T., Cayrol C., Cayrol M., LE BERRE D., "Using the Davis and Putnam procedure for an efficient computation of preferred models", Proceedings of the Twelfth European Conference on Artificial Intelligence (ECAI'96), pp 350-354, Budapest (Hongrie), 1996 (Postscript)