Séminaires

Séminaires

Mercredi 14 février 2024 à 15h

  • 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.

Mercredi 24 janvier 2024 à 15h

  • 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

Mercredi 20 décembre 2023 à 15h

  • 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

Mercredi 6 décembre 2023 à 15h

  • 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

Mercredi 18 octobre 2023 à 15h

  • 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

Mercredi 4 octobre 2023 à 15h30

  • 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

Mercredi 14 juin 2023 à 15h

  • 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

Mercredi 5 avril 2023 à 10h

  • 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