Thèmes Publications Prix et distinctions Encadrement de la recherche

Thèmes de recherche

Je m'intéresse à la résolution pratique de problèmes de décision et d'optimisation difficiles, plus particulièrement des problèmes de satisfiabilité (SAT), de satisfiabilité maximum (Max-SAT) et plus récemment de satisfiabilité minimum (Min-SAT). SAT est NP-complet tandis que Max-SAT et Min-SAT sont NP-difficiles. Les approches de résolution que je développe sont principalement basées sur des méthodes arborescentes et de recherche locale, avec la prise en considération des informations structurelles et une meilleure exploitation des règles d'inférence liées à ces problèmes.

Mots-clés. Intelligence artificielle, SAT, Max-SAT, Min-SAT, NP-complétude, Recherche arborescente, Recherche locale, Résolution pratique de problèmes NP-difficiles.

Publications

Revues internationales avec comité de rédaction

  • A. Abramé, D. Habet, D. Toumi, "Improving Configuration Checking for Satisfiable Random k-SAT Instances". In Annals of Mathematics and Artificial Intelligence, pp. 79(1-3): 5–24, 2017.
  • A. Abramé, D. Habet, "Ahmaxsat : Description and Evaluation of a Branch and Bound Max-SAT solver". In Journal on Satisfiability, Boolean Modeling and Computation. Vol. 9, pp. 89–128, 2015.
  • D. Habet, M. Vasquez, Y. Vimont, "Bounding the Optimum for the Problem of Scheduling the Photographs of an Agile Earth Observing Satellite". In Journal of Computational Optimization and Applications, Vol. 47 (2), pp. 307–333, 2010. Ed. Springer Netherlands, ISSN : 0926-6003 (Print), 1573-2894 (Online). DOI 10.1007/s10589-008-9220-7.
  • M. Vasquez, A. Dupont, D. Habet, "Consistency Checking within Local Search Applied to the Frequency Assignment Problem with Polarization". In RAIRO Operations Research, Vol. 37, pp. 311–323, 2004.

Chapitres d'ouvarges internationaux

  • D. Habet, "Tabu Search to Solve Real-Life Combinatorial Optimization Problems : A Case of Study", In A. Abrham et al. (Ed.), "Book on Foundations of Computational Intelligence Volume 3 - Global Optimization”, Springer Verlag, ch. 6, pp. 129-151, 2009. DOI 10.1007/978-3-642-01085-9.
  • M. Vasquez, A. Dupont, D. Habet, "Consistent Neighborhood in a Tabu Search", Kluwer Academic Publishers, Metaheuristics : Progress as real Problem Solvers, MIC 2003 Post-conference volume, pp. 369 – 388, 2005.

Conférences internationales avec actes et comité de lecture

  • M. S. Cherif, D. Habet, "Towards the Characterization of Max-Resolution Transformations of UCSs by UP-Resilience", In Proceedings of The 25th International Conference on Principles and Practice of Constraint Programming (CP 2019), pp. 91-107, 2019.
  • D. Habet, C. Terrioux, "Conflict History Based Search for Constraint Satisfaction Problem", In Proceedings of The 34th ACM/SIGAPP Symposium On Applied Computing, pp. 1117-1122, 2019.
  • A. Abramé, D. Habet, "Learning Nobetter Clauses in Max-SAT Branch and Bound Solvers", In Proceedings of IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2016), pp. 452-459, 2016.
  • A. Abramé, D. Habet, "On the Resiliency of Unit Propagation to Max-Resolution", In Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), pp. 268–274, 2015.
  • A. Abramé, D. Habet, "Local Search Algorithm for the Partial Minimum Satisfiability Problem. In Proceedings of IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015), pp. 821-827, 2015.
  • A. Abramé, D. Habet, D. Toumi, "Tie-Breaking Heuristic in Configuration Checking for Random 3-SAT instances", In Proceedings of the 11th Metaheuristics International Confe- rence (MIC 2015), pp. 61 :1-9, 2015.
  • A. Abramé, D. Habet, "Efficient Application of Max-SAT Resolution on Inconsistent Subsets", In Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming (CP 2014), pp. 92–107, 2014.
  • A. Abramé, D. Habet, D. Toumi, "Improving Configuration Checking for Satisfiable Random k-SAT Instances", International Symposium on Artificial Intelligence and Mathematics (ISAIM 2014), 2014.
  • A. Abramé, D. Habet, "Maintaining and Handling All Unit Propagation Reasons in Exact Max-SAT Solvers", In Proceedings of the Seventh Annual Symposium on Combinatorial Search (SOCS 2014), 2014.
  • A. Abramé, D. Habet, "Local Max-Resolution in Branch and Bound Solvers for Max-SAT", In Proceedings of IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2014), pp. 336–343, 2014.
  • A. Abramé, D. Habet, "On the Extension of Learning for Max-SAT", In Proceedings of the 7th European Starting AI Researcher Symposium (STAIRS 2014), pp. 1–10, 2014.
  • A. Abramé, D. Habet, D. Toumi, " A Two-Levels Local Search Algorithm for Random SAT Instances with Long Clauses", In Proceedings of the 7th European Starting AI Researcher Symposium (STAIRS 2014), pp. 11–20, 2014.
  • D. Habet, D. Toumi, "Empirical Study of the Behavior of Conflict Analysis in CDCL Solvers", In Proceedings of the 19th International Conference on Principles and Practice of Constraint Programming (CP 2013), pp. 578-693, 2013.
  • D. Habet, D. Toumi, "Local Search Based on Conflict Analysis for the Satisfiability Problem", In Proceedings of the 24th IEEE International Conference on Tools with Artificial In- telligence (ICTAI 2012), pp. 892-896, 2012.
  • A. Abramé, D. Habet, "Inference Rules in Local Search for Max-SAT", In Proceedings of the 24th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2012), pp. 207-214, 2012.
  • D. Habet, L. Paris, C. Terrioux, "A Tree Decomposition Based Approach to Solve Structured SAT Instances", In Proceedings of the 21th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2009), pp. 115-122, 2009.
  • D. Habet, "Enhancing the Robustness/Efficiency of Local Search Algorithms for SAT". In proceedings of the 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2008), volume 1, pp. 255-262, 2008.
  • D. Habet, Lionel Paris, Cyril Terrioux, "Consistent Neighborhood for the Satisfiability Problem". In proceedings of the 19th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2007), pp. 497-501, 2007.
  • D. Habet, M. Vasquez, "Improving Local Search for Satisfiability Problem by Integrating Structural Properties", In proceedings of the 5th International Conference on Research, Innovation and Vision for the Future (RIVF’07), pp. 50-57, 2007.
  • D. Habet, M. Vasquez, "Solving the Selecting and Scheduling Satellite Photographs Problem with a Consistent Neighborhood Heuristic", In Proceedings of the 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2004), pp. 302-309, 2004.
  • M. Vasquez, D. Habet, "Using Symmetries for Coloring Queen Graphs", In Proceedings of the 16th European Conference on Artificial Intelligence (ECAI 2004), IOS Press, pp. 226-230, 2004.
  • D. Habet, M. Vasquez, "Consistent and Saturated Neighborhood for Selecting and Scheduling Photographs of an Agile Earth Observing Satellite", In proceedings of the Fifth Metaheuristics International Conference (MIC2003), pp. 28 : 1–6, 2003.
  • M. Vasquez, A. Dupont, D. Habet, "Consistent Neighborhood in a Tabu Search", In proceedings of the Fifth Metaheuristics International Conference (MIC2003), pp. 77 : 1–6, 2003.
  • D. Habet, CM. Li, L. Devendeville, M. Vasquez, "A Hybrid Approach for SAT", In Proceedings of the Eighth International Conference on Principles and Practice of Constraint Programming (CP 2002), Springer, Vol. 2470, pp. 172-184, Lecture Notes in Computer Science (LNCS), 2002.

Workshops internationaux avec comité de lecture et actes

  • D. Habet, C. Terrioux, "Conflict History Based Branching Heuristic for CSP Solving". CIMA@ICTAI 2018: 70-80
  • D. Habet, P. Jégou, "Toward a Generalization and a Reformulation of Goods in SAT - Preliminary Report". AAAI 2010 Workshop on Abstraction, Reformulation, and Approximation (WARA 2010), pp. 26-31, Atlanta, USA, 2010.

Conférences nationales avec actes et comité de lecture

  • D. Habet, C. Terrioux, "Une heuristique basée sur l'historique des conflits pour les problèmes de satisfaction de contraintes", Dans les Actes des 15èmes Journées Francophones de Programmation par Contraintes (JFPC), pp.153-154, 2019.
  • M. S. Cherif, D. Habet, "Sur l'UP-résilience des k-UCSs binaires", Dans les Actes des 15èmes Journées Francophones de Programmation par Contraintes (JFPC), pp. 177-180, 2019.
  • A. Abramé, D. Habet, "Apprentissage de clauses nobetters dans les solveurs séparation et évaluation pour Max-SAT", Dans les actes des Treizièmes Journées Francophones de Programmation par Contraintes (JFPC 2017), pp. 111-112, 2016.
  • A. Abramé, D. Habet, "De la résilience de la propagation unitaire aux transformations par max-résolution", Dans les actes des Douzièmes Journées Francophones de Programmation par Contraintes (JFPC 2016), pp. 217-218, 2016.
  • A. Abramé, D. Habet, "Application efficace de la résolution pour Max-SAT sur les ensembles inconsistants", Dans les actes des Onzièmes Journées Francophones de Programmation par Contraintes (JFPC 2015), pp. 2-3, 2015.
  • A. Abramé, D. Habet, "Maintenir et traiter toutes les sources de propagation unitaire dans les solveurs exacts pour Max-SAT", Dans les actes des Onzièmes Journées Francophones de Programmation par Contraintes (JFPC 2015), pp. 4-5, 2015.
  • A. Abramé, D. Habet, "Vers l’extension de l’apprentissage pour Max-SAT", Dans les actes des Onzièmes Journées Francophones de Programmation par Contraintes (JFPC 2015), pp. 6-15, 2015.
  • A. Abramé, D. Habet, "Application Locale de la Max-Resolution dans les Solvers Branch and Bound pour Max-SAT", Dans les actes des Dixièmes Journées Francophones de Programmation par Contraintes (JFPC 2014), pp. 203-211, 2014.
  • D. Habet, D. Toumi, "Une étude empirique du module d’analyse de conflits dans les solveurs CDCL", Dans les actes des Neuvièmes Journées Francophones de Programmation par Contraintes (JFPC 2013), pp. 303-312, 2013.
  • A. Abramé, D. Habet, "Règles d’inférence et recherche locale pour Max-SAT et MaxSAT valué", Dans les actes des Neuvièmes Journées Francophones de Programmation par Contraintes (JFPC 2013), pp. 1-10, 2013.
  • D. Habet, D. Toumi, "Une recherche locale dirigée par l’analyse de conflits pour la satisfiabilité", Dans les actes des huitièmes Journées Francophones de Programmation par Contraintes (JFPC 2012), pp. 131-135, 2012.
  • D. Habet, L. Paris, C. Terrioux, "Une approche basée sur la décomposition arborescente pour la résolution d’instances SAT structurées", Dans les actes des 5èmes Journées Francophones de Programmation par Contraintes (JFPC 2009), pp. 85-94, 2009.
  • L. Paris, D. Habet, B. Benhamou, "Voisinage consistant pour le problème de satisfiabilité", Dans les actes des troisièmes Journées Francophones de Programmation par Contraintes (JFPC 2007), pp. 58-66, 2007.
  • D. Habet, M. Vasquez, A. Dupont, "Voisinage consistant sur des configurations partielles pour la résolution de problèmes réels de grande taille", Dans les actes des Premières Journées Francophones de Programmation par Contraintes (JFPC 2005), pp. 439, 442, 2005.
  • M. Vasquez, D. Habet, "Algorithmes complet et incomplet pour la coloration des graphes de reines", Dans les actes des Treizièmes Journées Francophones de Programmation en Logique et de programmation par Contraintes (JFPLC 2004), pp. 239-252, 2004.
  • D. Habet, CM. Li, L. Devendeville, JL. Guérin, M. Vasquez, "Une approche hybride pour SAT", Dans les actes des huitièmes Journées Nationales sur la résolution Pratique de Problèmes NP-Complets (JNPC 2002), pp. 115-125, 2002.

Publications et workshop sans actes

  • A. Dupont, M. Vasquez, D.Habet, "Consistent Neighbourhood in a Tabu Search", Workshop on Combination of metaheuristic and local search with Constraint Programming techniques (MLS+CP), University of Nantes, 2005.
  • M. Vasquez, A. Dupont, D. Habet, "Neighborhood Design by Consistency Checking", International Federation of Operational Research Societies (IFORS), 2005. Papier Invité.
  • D. Habet, M. Vasquez, "Tabu Search on a Consistent and Saturated Neighborhood for Selecting and Scheduling Photographs of an Agile Earth Observing Satellite", Bulletin de la société française de recherche Opérationnelle et d’Aide à la Décision (ROADEF) (10), pp. 11-14, 2003. Papier Invité.

Rapports de recherche

  • D. Habet, D. Toumi, "Relevant Clause Analysis in Modern SAT Solvers", LSIS, 2012.
  • D. Habet, L. Paris, C. Terrioux, "A Tree Decomposition Based Approach to Solve Structured Satisfiability Instances", LSIS, 2009.

Prix et distinctions

Max-SAT International Evaluations

Avec André Abramé, nous avons développé un démonstrateur de type séparation et évaluation ahmaxsat pour la résolution du problème Max-SAT. Ce démonstrateur a participé aux éditions 2014, 2015 et 2016 de MaxSAT International Evaluation. Cet événement est une compétition internationale servant à évaluer des démonstrateurs Max-SAT issus des travaux de la communauté scientifique. La participation de ahmaxat à ces événements a été couronnée de succès par l’obtention des distinctions principales suivantes :

  • Édition 2014 : 33 démonstrateurs complets participants
    • First place in the Unweighted Random Track.
    • First place in the Unweighted Crafted Track.
    • First place in the Partial Random Track.
    • Second place in the Weighted Partial Random Track.

  • Édition 2015 : 27 démonstrateurs complets participants
    • First place in the Unweighted Random Track.
    • First place in the Unweighted Crafted Track.
    • First place in the Partial Random Track.
    • Third place in the Weighted Partial Random Track.

  • Édition 2016 : 17 démonstrateurs complets participants
    • First place in the Unweighted Random Track.
    • First place in the Unweighted Crafted Track.
    • First place in the Partial Random Track.
    • Third place in the Weighted Partial Random Track.
    • Third place in the Weighted Partial Crafted Track.

SAT International Competition 2013

Dans le cadre de SAT, nous avons développé (avec André Abramé et Donia Toumi) le démonstrateur basé sur la recherche locale Ncca+. Il a participé à l’évènement SAT International Competition 2013. Nous avons obtenu le prix Bronze medal in the Random Satisfiable Track. 25 démonstrateurs ont concouru à ce track.

Challenge ROADEF’2003

En 2003 et sur un ensemble de 12 équipes participantes, j’ai obtenu le premier prix en catégorie junior du challenge ROADEF’2003, de la société française de recherche opérationnelle et d’aide à la décision, du meilleur logiciel pour la résolution d’un problème industriel : Gestion de la mission de satellites d’observation de la Terre.

Encadrement de la recherche

Thèse de doctorat

  • Mohamed Sami Cherif
    • Directeurs : Djamal Habet et Richard Ostrowski
    • Titre : Structures des formules du problème de satisfiabilité
    • En cours

  • Matthieu Py
    • Directeurs : Djamal Habet
    • Titre : Vers une unification des algorithmes de résolution du problème de satisfiabilité maximum
    • En cours

  • André Abramé
    • Directeurs : Djamal Habet et Philippe Jégou
    • Titre : Max-résolution et apprentissage pour la résolution du problème de satisfiablité maximum
    • Soutenue le 25 septembre 2015

  • Donia Toumi
    • Directeurs : Djamal Habet et Philippe Jégou
    • Titre : Analyse de conflits et méthodes incomlètes pour la satisfiabilité propositionnelle
    • Soutenue le 04 décembre 2014

Master recherche en Informatique

Depuis 2006, j'ai encadré 6 stages de Master recherche en informatique.