Revues Internationales : Journal on Satisfiability, Boolean Modeling and Computation (JSAT), Constraints, International Journal of Advanced Information Technology (IJAIT), ICGA Journal
Conférences internationales : SAT 2009, SAT 2010, SAT 2011, SAT 2013, CP 2011, CP 2012, CP 2013, AAAI 2011, CPAIOR 2012, AAAI-17
Projets
ANR SATAS SATAS -- SAT As a Service (2015-2019). Le projet SATaS est un projet qui propose de réaliser des avancées significatives dans l’état de l’art de la résolution du problème SAT, dans les environnements massivement parallèles (“Many Integrated Component” (MIC) et “Cloud computing”). Le projet se focalise notamment sur les problèmes applicatifs que ce type de solution impose. L'objectif final est de fournir une interface SAT en tant que service dans le “cloud”.
ANR BR4CP -- Modèles et algorithmes pour le conseil et la gestion des préférences en configuration de produit (2011–2014). Son objectif est de proposer aux applications de configuration en ligne des modèles formels et des outils algorithmiques pour la prise en compte des préférences client et la mise en oeuvre de recommandations sur des domaines structurés et fortement combinatoires. Il s’agit d’intégrer dans les configurateurs, qui permettent à l’utilisateur de construire interactivement le produit qu’il achètera et de naviguer ainsi dans une offre combinatoire, des fonctions de recommandation, capables de raisonner sur les préférences de l’utilisateur.
Le projet PAJERO, sous l’égide de OSEO (2011-2015). Ce projet comprend 3 laboratoires (PRISM (Versailles), I3S (NICE) et CRIL (Lens)) ainsi que 3 entreprises (HSW, ICAPS et EquiTime). L’objectif consiste à développer une plateforme logicielle permettant, la gestion complexe de ressources multiples (ressources humaines, planification, gestion des temps et activités associées...).
2006-2007 : PESSOA MUSICA Une collaboration franco-portuguaise sur le thème de la localisation de l'incohérence en logique propositionnelle.
Logiciels
PeneLoPe est un solveur SAT paralèlle basé sur le schéma portfolio. Maintenu par Benoit Hoessen, il est le fruit d'une collaboration avec Gilles Audemard et Said Jabbour. Notre solveur, basé sur Minisat, possède un schéma complet de stratégies pour l'échange de clauses. La technique de gestion de clauses apprises PSM, permettant de sortir les nogoods des structures de données sans les supprimer de la mémoire est également implémentée, et permet une gestion très fine des échanges d'information au sein des différents workers. PeneLoPe (qui était la seule fille de la compétition) a fini 2e (sur 19) dans la "Parallel Track" du SAT Challenge 2012. Elle s'est également bien défendue cette année, en terminant 3e de la track "Core Solvers, Parallel" de la SAT Competition 2013.
(A)OMUS est un extracteur de Formules Minimales Insatisfiables (MUS) basé sur la recherche locale, présenté ici : [pdf]. Une comparaison entre les techniques permettant l'approximation d'un MUS, et une autre où le but est d'extraire un MUS sont également disponibles. Le code source est disponible ici.
AOMUS peut être greffé au nouvel algorithme d'extraction de MUS, MiniUnsat, développé par Siert Wieringa. Cette combinaison d'algorithmes permet d'obtenir de très bons résultats en pratique, tels que ceux présentés dans l'article "Finding guaranteed MUSes fast" (par Hans van Maaren et Siert Wieringa, SAT'08).
HYCAM est une version améliorée d'un algorithme de Mark Liffiton et Karem Sakallah (basé sur Minisat) dont le but est de calculer tous les MUS d'une formule CNF. C'est en fait une hybridation d'une méthode complète avec une recherche locale permettant un gain d'un ordre de grandeur pour de nombreuses CNF, sans être plus lents en cas d'échec. L'idée générale est présentée ici : [pdf], et la procédure est disponible ici.
The MUC Extraction Page Cette page propose une approche heuristique récente pour calculer un ensemble insatisfiable minimal de contraintes de CSP discrets, également appelés MUC. Cette technique, baptisée CB(full-wcore), est basée sur des informations heuristique fournies par des preuves d'incohérence d'un problème donné. Il améliore une technique précédemment proposée, qui était la plus efficace à ce jour. Exécutables, résultats expérimentaux et jeux de tests sont disponibles [ici] (en anglais uniquement).
MUSTER est un extracteur de MUST (Minimally Unsatisfiable Set of Tuples) au sein d'un CSP insatisfiable, présenté ici : [pdf]
ReVivAl
Fruit d'une collaboration avec Youssef Hamadi, Lakhdar Saïs, ReVivAl (pour pReprocessing based on Vivification Algorithm)
est une nouveau prétraitement pour formules CNF qui vise à produire des sous-clauses et générer de nouvelles clauses pertinentes. Son efficacité est liée à sa complète intégration au sein d'un solver SAT. Ainsi, il bénéficie des structures de données/mécanismes classiques des implémentations CDCL modernes (watched literals, apprentissage, heuristiques de type VSIDS, etc.), accélérant la production de (sous-)clauses. Une page dédiée à ReVivAl est disponible ici (en anglais). Differentes combinaisons de ReVivAl et SatElite ont été soumises au preprocessor track de la compétition SAT 2009. Les résultats finaux placent les procédures soumises 2ème pour les catégories APPLICATION et CRAFTED (et 1ère dans la catégorie UNSAT CRAFTED).
