Daniel Le BerreProfesseur à l'Université d'Artois, membre du CRIL

Père fondateur du logiciel libre Sat4j, utilisé par des millions de personnes à travers le monde, Daniel Le Berre est enseignant-chercheur à l’université
d’Artois-Centre de recherche en informatique de Lens1 .

Daniel Le Berre réalise des travaux de recherche dans le domaine de l’intelligence artificielle et s’intéresse en particulier à la conception et à l’évaluation d’algorithmes pour l’inférence et la prise de décision. C’est également un passionné de génie logiciel, qu’il enseigne aux étudiants de l’université d’Artois. Mobilisant les deux facettes de son métier d’enseignant-chercheur, Daniel Le Berre étudie la résolution pratique de problèmes spécifiques au génie logiciel. Il utilise des approches à base de contraintes booléennes pour aborder la gestion des dépendances, les lignes de produits logiciels et la synthèse automatique de correctifs logiciels. Il crée en 2004 le logiciel Sat4j, qui propose un ensemble d’outils de raisonnement en variables booléennes pour le langage Java. Conçu dès le départ comme un logiciel libre pouvant être facilement réutilisable dans d’autres logiciels, Sat4j intègre en 2005 le consortium ObjectWeb (maintenant OW2), qui promeut le développement d’intergiciels libres, et s’est imposé comme l’un des logiciels phares du consortium. Sat4j totalise plus de 200 000 téléchargements depuis janvier 2006 et se classe à la 15e place des projets les plus téléchargés d’OW2. En 2008, Sat4j intègre la plateforme ouverte Eclipse, atelier logiciel destiné à la production de logiciels libres. Toutes les applications basées sur Eclipse bénéficient de l’intégration du logiciel de Daniel Le Berre.

"J’ai écrit mon premier logiciel de résolution du problème de la cohérence en logique propositionnelle (solveur SAT) en 1994, lors de mon stage de DEA à l’Institut de recherche en informatique de Toulouse. À l’époque, ces logiciels permettaient de résoudre des instances comportant quelques centaines de variables et milliers de clauses. Durant ma thèse, j’ai utilisé des solveurs SAT dans des algorithmes de raisonnement non monotone, mais les performances limitées des solveurs ne permettaient pas d’évaluer ces algorithmes sur des cas concrets de taille significative. Ce n’est qu’à partir de 2001 qu’une nouvelle génération de solveurs SAT a vu le jour et a permis de résoudre des instances comportant quelques centaines de milliers de variables et de clauses, devenues aujourd’hui des millions. Les grandes entreprises comme IBM, Intel, Microsoft ont rapidement intégré les solveurs SAT à leurs outils et la communauté scientifique a adopté leur usage. Une véritable révolution qui est pourtant passée inaperçue aux yeux du grand public ! Le logiciel Sat4j est né de la volonté d’étendre les bénéfices de cette avancée majeure dans la résolution de problèmes combinatoires aux développeurs Java."

• Centre de recherche en informatique de Lens
• Institut des sciences de l’information et de leurs interactions
• Délégation Nord – Pas de Calais et Picardie

• 1Université Artois/CNRS