Médaille de l’innovation 2018 pour Daniel Le Berre

L’activité de recherche de Daniel Le Berre se situe dans le cadre général de l’intelligence artificielle, plus particulièrement autour de l’algorithmique pour l’inférence et la prise de décision. Il s’intéresse à la résolution pratique de problèmes logiques, des problèmes de satisfaction de formules logiques et d’optimisation en variables booléennes. Un problème SAT ou de « satisfaisabilité booléenne » est un problème de décision qui s’exprime sous la forme d’une formule de logique propositionnelle. Résoudre un tel problème consiste à déterminer s’il existe une assignation des variables propositionnelles qui rend la formule vraie. On peut modéliser de très nombreux problèmes de décision sous cette forme mais leur résolution algorithmique pose des problèmes majeurs de complexité dès lors qu’on s’attaque à des problèmes de grande taille (formules comportant beaucoup de variables). Ce domaine de recherche a connu un intérêt croissant ces quinze dernières années, par exemple pour des entreprises comme Intel, IBM ou Microsoft, parce que la communauté informatique a développé des outils efficaces qui permettent de résoudre des problèmes importants. Les applications phares de SAT au début des années 2000 étaient la vérification de programmes ou de circuits mais il en existe maintenant de nombreuses applications, dans des domaines variés de l’informatique (ex. bio-informatique, base de données, sécurité, génie logiciel) et dans tous ceux qui nécessitent de raisonner sur de grandes masses de données.

Daniel Le Berre a pris une part active au renouvellement de ces travaux au tournant des années 2000, avec notamment en 2002 la première compétition SAT « moderne », qui a eu un impact décisif sur la fiabilité, l’efficacité et le nombre des solveurs SAT qui sont disponibles aujourd’hui. Il est surtout l’auteur du plus connu de ces solveurs : Sat4j. Si d’un point de vue théorique le problème SAT est NPcomplet, c’est-à-dire insoluble en un temps raisonnable dans le pire des cas, il est aujourd’hui possible de résoudre en pratique et de manière efficace de nombreuses instances de ce problème. C’est ce que permet de faire Sat4j.

Daniel Le Berre développe Sat4j depuis 2004, avec l’aide d’Anne Parrain mais aussi avec Stéphanie Roussel, quand elle était ingénieure de recherche au CRIL, et Emmanuel Lonca en tant que doctorant et désormais comme ingénieur de recherche. Sat4j a été conçu dès le départ comme un logiciel libre pour être facilement intégrable dans d’autres logiciels écrits en Java (licence GNU LGPL). Sat4j est déposé à l’Agence de Protection des Programmes (APP, référence DL 04902-01-UMR8188) depuis novembre 2011. Il contient 43 000 lignes de code Java.

Projet de la fondation du même nom, Eclipse est un environnement de développement destiné à la production de logiciels libres. La plateforme de développement Eclipse est bien connue des développeurs : c’est la plus utilisée pour le langage Java. Conçue pour être extensible, universelle et polyvalente, elle se compose d’un ensemble de greffons (plug-in ou composants logiciels) mais la gestion des dépendances et possibles conflits entre greffons mis en œuvre pour une application donnée posait un problème critique. C’est là que Sat4j joue un rôle central et essentiel dans la plateforme Eclipse. Contrairement aux catalogues d’applications des téléphones, les greffons disponibles dans le catalogue d’Eclipse décrivent leurs dépendances et conflits avec d’autres greffons : le solveur Sat4j s’assure que les installations sont possibles en indiquant éventuellement quelles dépendances additionnelles doivent être installées. La fondation Eclipse a reconnu l’apport de Daniel Le Berre dès 2009 en l’élisant dans son équipe de développement pour assurer l’intégration fine de Sat4j dans Eclipse.

Eclipse est une base ouverte sur laquelle sont déployées de nombreuses applications, comme celles d’IBM, Oracle, SAP, Airbus, etc., qui bénéficient donc toutes de l’intégration de Sat4j, souvent sans même que leurs utilisateurs le sachent. Sat4j est aussi un logiciel très utilisé dans le monde de la recherche : dès 2005, il était utilisé dans le domaine des lignes de produits logiciels (AHEAD, University of Texas), pour les spécifications formelles (ALLOY 4, MIT) ou dans le domaine de la bio-informatique (logiciel GNA, équipe INRIA IBIS, société Genostar). Au-delà d’Eclipse, Sat4j est un logiciel phare du consortium OW2 : il totalise quasiment 201 000 téléchargements depuis janvier 2006, et est le 15ème projet le plus téléchargé sur OW2. Mais ces chiffres ne donnent qu’une vision incomplète du nombre d’utilisateurs de Sat4j. En effet, cette bibliothèque logicielle est disponible sur toutes les distributions Linux dans les dépôts standards et est disponible sur les dépôts Maven du consortium OW2.

Daniel Le Berre s’intéresse actuellement à l’intégration efficace et à la combinaison de plusieurs systèmes de preuves pour obtenir un système plus performant que les systèmes existants pris indépendamment. C’est un enjeu important parce qu’un solveur SAT ne sait pas compter ou résoudre certains problèmes qui peuvent apparaître simples alors que d’autres méthodes comme, par exemple, le système de preuve des « plans coupe » le permettent sans pour autant être très efficaces en pratique. Un autre aspect de son travail concerne le développement de solutions algorithmiques permettant de résoudre des problèmes plus difficiles que SAT.