Pour tout renseignement ou proposition de séminaire, merci de contacter Cyril Pain-Barre.

Quelques informations utiles :

• Lien vers le plan d'accès aux locaux de l'équipe COALA

• Plan d'accès et informations diverses sur au campus de Marseille St Jérôme

• Date & Heure : Mercredi 19 juin 2024 à 15h

• Lieu : Salle de réunion COALA, dans les locaux de l'équipe.

• Orateur : Benjamin BERGOUGNOUX, Postdoc à l'université de Varsovie, Pologne

• Information(s) diverse(s) : exposé en anglais

• Titre : Neighborhood operator logics: efficient model checking in terms of width parameters

• Résumé : In this talk, I will introduce the family of neighborhood operator (NEO) logics which are extensions of existential MSO with predicates for querying neighborhoods of vertex sets. NEO logics have interesting modeling powers and nice algorithmic applications for several width parameters such as tree-width. NEO logics capture many important graphs problems such as Independent Set, Dominating Set and many of their variants. Moreover, some NEO logics capture CNF-SAT via the signed incidence graphs! We can capture more problems by considering various extensions of NEO logics. For example, we can capture problems with global constraints such as Hamiltonian Cycle via the extension of NEO logics with predicates for checking the connectivity/acyclicity of vertex sets.

  In terms of algorithmic applications, NEO logics seem to be the perfect candidates for capturing many problems that can be solved efficiently in terms of width parameters.

  This is suggested by the following three results:

  • For tree-width, the most powerful NEO logics can be model checked in single exponential time in terms of tree-width as implied by a result of Michal Pilipczuk [MFCS 2011].

  • Jan Dreier, Lars Jaffke and I proved that, for an extension of one NEO logic, we can obtain an efficient model-checking algorithm in terms of several width parameters more general than tree-width such as clique-width, rank-width and mim-width [SODA 2023].

  • Vera Checkan, Giannos Stamoulis and I are currently proving that some NEO logic can be solved in single exponential time and polynomial space for tree-depth: the shallow restriction of tree-width. This last result could be interesting in practice where space usage is crucial. I will present these three results after a friendly introduction on width parameters.

• Lieu : Salle de réunion COALA, dans les locaux de l'équipe.

• Orateur : Alexandre COPPÉ, Doctorant, Équipe COALA, LIS

• Information(s) diverse(s) : exposé en français

• Titre : Un algorithme de routage de navires générant des trajets précis et diversifiés

• Résumé : Nous présentons un algorithme déterminant avec précision des trajectoires optimales d'un navire dans un contexte multi-objectif et dynamique, où il faut notamment prendre en compte le temps de trajet et la consommation de carburant, dans des conditions météorologiques qui varient pendant le trajet. Notre approche combine deux algorithmes récents, NAMOA*-TD et WRM, nous permettant d'obtenir un panel de trajectoires (sous-ensemble du front de Pareto) précises et diversifiés parmi lesquels un utilisateur peut choisir. Les premières expérimentations effectuées à partir de données météorologiques réelles nous permettent de montrer l'efficacité de cette approche.

• Lieu : en visio (Zoom) et en projection commune en salle de réunion COALA, dans les locaux de l'équipe.

• Lien Zoom (avec salle d'attente) : https://univ-amu-fr.zoom.us/j/86782217844?pwd=b01wQTJ3N1ZOYVRqUW1waFlMU0Z4UT09 (ID 867 8221 7844 , Code secret 583541)

• Oratrice : Mme Zouhaira AYADI (PhD, ATER à l'Université de Montpellier, Équipe COCONUT du LIRMM)

• Information(s) diverse(s) : exposé en français

• Titre : Graphe et réseau de contrainte pour l'interprétation spatiale et spatio-temporelle des connaissances dans un environnement incertain

• Résumé : Les flux de données spatiales et spatio-temporelles, extraites à partir d’images satellitaires, sont riches en détails et en informations. De plus, ces informations réelles disponibles sont généralement sujettes à de l’incertitude. Cette dernière se présente sous plusieurs formes (incertitude, imprécision, incomplétude, etc.) et influence la qualité des données du système en lui-même et des résultats finaux obtenus. L’extraction des informations pertinentes à partir du grand volume de données incertaines et le suivi de la dynamique des objets (les changements aux niveaux des propriétés, de l’agencement spatial, etc.) demeurent un défi majeur pour la communauté de la télédétection. Par conséquent, le processus d’analyse et d’interprétation des images satellitaires devient plus compliqué. Plus précisément, ce processus doit passer par trois étapes essentielles : (i) la reconnaissance des divers objets pertinents (le quoi), (ii), la définition de leur agencement spatial (le où), ainsi que (iii) l’identification du moment du changement (le quand). La prise en compte du caractère complexe (temporel, spatial et incertain) des objets géographiques pose des problèmes de modélisation et d’analyse des informations.

Mes travaux de recherche s’inscrivent dans ce contexte, se situant à l’intersection de trois axes de recherche à savoir, (1) la modélisation des connaissances, (2) l’analyse et la fouille de données complexes, et (3) le raisonnement dans un environnement incertain. Un premier objectif était de concevoir et développer un système d’interprétation spatio-temporelle des images satellitaires capable d’extraire des objets géographiques complexes et de suivre leurs changements au cours du temps, en utilisant les réseaux de contrainte et une modélisation sous forme de graphes. Ce système combine deux modules s’inscrivant sur deux volets différents : sur le volet statique ou mono-date, il s’agissait de proposer un système de reconnaissance des objets complexes à partir d’une image satellitaire en se basant sur un raisonnement spatial et contraint, sur le volet dynamique ou multi-date, il s’agissait de proposer un système de suivi et d’analyse des évolutions des objets initialement identifiés. Le deuxième objectif portait sur l’utilisation de l’analyse de sensibilité et la propagation des incertitudes pour quantifier les incertitudes affectant les modèles de prédiction de changements de l’occupation du sol. Ces travaux de recherche ont démontré l’efficacité des CSP (Constraint Satisfaction Problem) dans la résolution des problèmes complexes, notamment, la reconnaissance des objets complexes en se basant sur des modèles représentatifs et le suivi de leurs changements.

Cette présentation vise à exposer mes activités de recherche antérieures. Je commencerais par vous présenter mes thématiques de recherche et mon domaine d’application. Ensuite, je détaillerais chaque thématique.

• Lieu : Salle de réunion COALA, dans les locaux de l'équipe.

• Oratrice : Hélène VERHAEGHE (PostDoctorante à KULeuven, Belgique)

• Information(s) diverse(s) : exposé en anglais

• Titre : Best of both worlds: synergies between Constraint Programming and Machine Learning

• Résumé : This talk will be about the synergies that exist between constraint programming and machine learning. Constraint programming is a technique to solve combinatorial optimization problems. It is very efficient in providing solutions that respects given constraints but take some times when solving huge problems. On the other hand machine learning is very able to deal with huge amounts of datas while having difficulties when dealing with hard constraints. Developing synergies between these two families of methods can help bring the best of both worlds together.

• À propos de l'oratrice : Hélène Verhaeghe got her Ph.D. in 2021 from UCLouvain (Belgium), with her thesis about the extensional constraint. She then went to Polytechnique Montréal (Canada) for a first post-doc. She is now back in Belgium since last May for a second post-doc at KULeuven, under the supervision of Prof. Tias Guns.

• Copie des Slides

• Lieu : Salle de réunion COALA, dans les locaux de l'équipe.

• Orateur : Hugues WATTEZ (PostDoctorant, Computer science Research Institute of Lens - CRIL)

• Information(s) diverse(s) : exposé en français

• Titre : Identification de la meilleure heuristique pour les solveurs de problèmes combinatoires

• Résumé : Pour les solveurs de problèmes combinatoires (CP, PB, SAT, etc.), l'heuristique de choix de variable occupe une place centrale en sélectionnant les variables sur lesquelles brancher lors de la recherche avec retour-arrière. Comme de nombreuses heuristiques de branchement ont été proposées dans la littérature, une question clé est d'identifier, à partir d'un ensemble d'heuristiques candidates, laquelle est la meilleure pour résoudre une tâche de satisfaction (ou d'optimisation) donnée. En se basant sur l'observation que les solveurs modernes utilisent des séquences de redémarrage, le problème d'identification de la meilleure heuristique peut être considéré dans le contexte des bandits multi-bras comme un problème d'identification du meilleur bras. En d'autres termes, à chaque run d'une séquence de redémarrage donnée, le bandit sélectionne une heuristique et reçoit une récompense pour cette heuristique avant de passer au run suivant. L'objectif est d'identifier la meilleure heuristique en le moins de runs possible. Lors de ce séminaire, nous présentons l'application des algorithmes de bandit multi-bras de l'état de l'art jusqu'à la proposition d'un nouveau bandit exploitant l'aspect non-stochastique des heuristiques tout en se basant sur une suite de redémarrage souvent adoptée dans ces solveurs : la suite de Luby. Au-delà de ces travaux, nous proposons une vue sur de possibles adaptations aux solveurs d'optimisation, ainsi que dans la domaine de l'hybridation de solveurs PB/MILP.

• Copie des Slides

• Lieu : Salle de réunion COALA, dans les locaux de l'équipe.

• Orateur : Alexis DE COLNET (PostDoctorant, Institute of Logic and Computation, Vienne)

• Information(s) diverse(s) : exposé en français

• Titre : Compilation de connaissances et Bornes Inférieures pour les Systèmes de Preuve

• Résumé : La compilation de connaissances est un domaine de l'informatique qui étudie différentes classes -- ou langages -- de représentations pour les fonctions, et les algorithmes permettant de passer d'une classe à l'autre. On présente les bases de la compilation de connaissances ainsi que certaines classes de représentations -- certains langages -- qui sont la cible des compilateurs en pratique. Puis on montre comment des bornes inférieures sur la taille des représentations pour des fonctions dans certains langages peuvent être converties en bornes inférieures pour des systèmes de preuve. On explique notamment comment on a utilisé cette approche pour prouver des bornes inférieures exponentielles sur les réfutations de CNF spécifiques appelées formules de Tseitin dans deux systèmes de preuve : les réfutations OBDD(∧,r) et les réfutations par résolution régulière.

• Copie des Slides

• Lieu : Salle de réunion COALA, dans les locaux de l'équipe.

• Oratrice : Roza AMOKRANE (Doctorante, Équipe COALA, LIS)

• Information(s) diverse(s) : exposé en anglais

• Titre : Comprehensive Survey on the container stowage planning problem

• Résumé : The container stowage planning problem consists of determining a suitable arrangement of the containers in a ship during its multiport journey. It's one of the main challenges in the realm of maritime logistics that shipping companies have to face on a daily basis. In our presentation, we will explore the problem in depth, examining its constraints and objectives. We will then briefly review the different approaches documented in the literature, giving a brief but instructive overview of the strategies employed to solve this complex logistics problem.

• Copie des Slides

• Lieu : Salle de réunion COALA, dans les locaux de l'équipe.

• Oratrice : Shuolin LI (Doctorante, Equipe COALA, LIS)

• Titre : A New Variable Ordering for In-processing Bounded Variable Elimination in SAT Solvers

• Résumé : Bounded Variable Elimination (BVE) is an important Boolean formula simplification technique in which the variable ordering is crucial. We define a new variable ordering based on variable activity, called ESA (variable Elimination Scheduled by Activity), for in-processing BVE in Conflict-Driven Clause Learning (CDCL) SAT solvers, and incorporate it into several state-of-the-art CDCL SAT solvers. Experimental results show that the new ESA ordering consistently makes these solvers solve more instances on the benchmark set including all the 5675 instances used in the Crafted, Application and Main tracks of all SAT Competitions up to 2022. In particular, one of these solvers with ESA, Kissat_MAB_ESA, won the Anniversary track of the SAT Competition 2022. The behaviour of ESA and the reason of its effectiveness are also analyzed.

• Information(s) diverse(s) : exposé en anglais

• Copie des Slides

• Lieu : Salle de réunion COALA, dans les locaux de l'équipe.

• Orateur : Amir Hosein VALIZADEH (Doctorant, Equipe COALA, LIS)

• Titre : À venir

• Résumé : À venir

• Information(s) diverse(s) : exposé en anglais

• Lieu : Salle de réunion COALA, dans les locaux de l'équipe.

• Oratrice : Yousra EL-GHAZI (Doctorante, Equipe COALA, LIS)

• Titre : Conception des lignes d'un réseau de transport maritime à l'aide de la PPC

• Résumé : Le problème de conception des lignes d'un réseau de transport maritime consiste, pour un armateur, à déterminer, d'une part, quelles sont les lignes maritimes (sous forme de rotations permettant de desservir un ensemble de ports) à ouvrir, et, d'autre part, l'affectation des navires (porte-conteneurs) avec les tailles adaptées pour les différentes lignes permettant d'acheminer tous les flux de conteneurs. Dans cet exposé, nous proposons une modélisation de ce problème à l'aide de la programmation par contraintes. Puis, nous présentons une étude préliminaire de sa résolution à l'aide de solveurs de l'état de l'art

• Lieu : salle de réunion COALA, dans les locaux de l'équipe.

• Orateur : Richard OSTROWSKI (Equipe COALA, LIS)

• Titre : Nouvel encodage SAT des problèmes de Packing Orthogonal

• Résumé : D'années en années, les solveurs se montrent de plus en plus efficaces pour la résolution pratique du problème SAT. Cependant, la capacité des solveurs à résoudre divers types de problèmes, à fermer certains problèmes mathématiques jusque-là restés ouverts (boolean pythagorian triples) est fortement lié à la manière dont sont modélisés ces problèmes. Dans les années 1997, 10 challenges ont été proposés. Les fameux problèmes 32 bits parity (parity-32) résistaient toujours et des solveurs dédiés ont vu le jour dans les années 2000 (lsat, eqsatz,march). Par la suite, des travaux sur une représentation efficace des contraintes de cardinalités, a permis une meilleure réécriture de ces problèmes et de les résoudre avec les solveurs de l'époque. De manière générale, différents codages existent pour modéliser en SAT (codage direct, codage des supports, codage logarithmique). Depuis 2011, l'order encoding, semble être le plus efficace. Un encodage doit offrir un bon compromis entre la propagation des contraintes et la compacité de la formule. Dans cet exposé, je m'intéresse aux problèmes de packing (OPP). Une idée intéressante, pour la résolution, est de considérer le problème sous la forme de graphes d'intervalles. Cette modélisation offre l'avantage de supprimer de nombreuses symétries de placement. À l'époque, S. Grandcolas et C. Pinto ont proposé une formulation pour SAT. Cependant, cette modélisation comportait 2 inconvénients : (1) il fallait modéliser, sous la forme de contraintes, la notion de stables i-faisables (exponentiel dans certains cas) et (2) de nombreuses configurations sont explorées alors qu'elles ne correspondent pas à la réalité. Une nouvelle reformulation sera proposée et des premiers résultats expérimentaux encourageants seront présentés.

• Copie des Slides