On Friday 30 November 2012, 14:00-14:30 INRIA Lille room B31 (new building), Daniel Le Berre (Université d’Artois ) will give a talk on “Des problèmes en variables booléennes à la gestion des dépendances entre logiciels”
Abstract:
Depuis une dizaine d’année, le nombre d’applications des outils basés sur la satisfiabilité de formules booléennes (SAT) ne cesse de croître : vérification de circuits, vérification de logiciels, bio-informatique, etc. Depuis juin 2008, la gestion des dépendances de la plate-forme ouverte Eclipse est effectuée par un outil d’optimisation en variable booléenne. Nos distributions Linux pourraient suivre une approche similaire pour la gestion de leurs paquets. Le but de ce séminaire est de présenter différents type de problèmes en variables booléennes (SAT, MAXSAT, Pseudo-Booléen, MUS) et leur application pratique dans le cadre de la gestion des dépendances entre logiciels. La modélisation utilisée dans le cadre du gestionnaire de dépendances p2 d’Eclipse sera détaillée. Le fonctionnement du gestionnaire de paquet Linux p2cudf, basé sur p2, sera ensuite introduit. La présentation se terminera par une présentation des travaux récents sur l’intégration d’approches en variables booléennes pour la configuration de produits manufacturés. Tous les problèmes présentés durant cette présentation peuvent être traités à l’aide de Sat4j (www.sat4j.org), notre outil de satisfaction et d’optimisation en variables booléennes.
Depuis une dizaine d’année, le nombre d’applications des outils basés sur la satisfiabilité de formules booléennes (SAT) ne cesse de croître : vérification de circuits, vérification de logiciels, bio-informatique, etc. Depuis juin 2008, la gestion des dépendances de la plate-forme ouverte Eclipse est effectuée par un outil d’optimisation en variable booléenne. Nos distributions Linux pourraient suivre une approche similaire pour la gestion de leurs paquets. Le but de ce séminaire est de présenter différents type de problèmes en variables booléennes (SAT, MAXSAT, Pseudo-Booléen, MUS) et leur application pratique dans le cadre de la gestion des dépendances entre logiciels. La modélisation utilisée dans le cadre du gestionnaire de dépendances p2 d’Eclipse sera détaillée. Le fonctionnement du gestionnaire de paquet Linux p2cudf, basé sur p2, sera ensuite introduit. La présentation se terminera par une présentation des travaux récents sur l’intégration d’approches en variables booléennes pour la configuration de produits manufacturés. Tous les problèmes présentés durant cette présentation peuvent être traités à l’aide de Sat4j (www.sat4j.org), notre outil de satisfaction et d’optimisation en variables booléennes.
