Home » Évènement

Soutenance de thèse de Mathieu Vavrillé

Mathieu Vavrillé, doctorant au sein de l’équipe TASC, présentera sa thèse intitulée :

« Trouver des Solutions Diverses en Programmation par Contraintes avec des Approches Probabilistes »

Elle aura lieu le 14.09.2023 à 14h, Salle 3, bâtiment 11, UFR Sciences & Techniques

 

Résumé : Dans cette thèse, je présente de nouvelles approches pour générer des solutions aléatoires ou diverses dans le cadre de la Programmation Par Contraintes (PPC). Utilisées comme outil d’aide à la décision, les solutions impactent les personnes : la planification d’employé·es, l’itinéraire des livreur·euses, les congés des soignant·es de garde. L’algorithme utilisé dans les solveurs de PPC est efficace, mais c’est un cadre rigide, qui renvoie des solutions basées sur des heuristiques de branchement qui peuvent être biaisées en faveur d’un espace de solution particulier. Les décideur·euses veulent aussi choisir entre plusieurs solutions, ces solutions doivent donc être diversifiées.
Mon travail s’appuie sur des outils probabilistes. Le hasard est utilisé pour briser la rigidité du backtrack-search des solveurs de PPC et pour trouver des solutions dans un ordre différent à présenter à l’utilisateur·ice. Pour ce faire, j’ai conçu TableSampling, un échantillonneur travaillant dans le cadre de la PPC, qui bénéficie ainsi de toutes les améliorations des solveurs de PPC (temps d’exécution, ou nouvelles contraintes).
Cependant, le caractère aléatoire n’est pas suffisant pour assurer la diversité. J’ai étudié et modifié des stratégies de recherche aléatoire pour générer des solutions diverses. La recherche peut ainsi être guidée vers des solutions dans des espaces intéressants.

Mots-clés : Programmation par Contraintes, Échantillonnage, Approche Probabiliste, Diversité, Solution

Abstract : In this thesis, I present new approaches to generate random or diverse solutions in the Constraint Programming (CP) framework. When used as a decision support tool, the solutions have an impact on people: the scheduling of employees, the route of delivery drivers, the day off for healthcare workers on rosters. The backtrack-search algorithm used in CP solvers is efficient, but it is also a rigid framework, returning solutions based on branching heuristics that may be biased towards a particular solution space. Furthermore, decision makers may also want to choose between multiple solutions, so these solutions should be diverse.
My work relies on probabilistic tools. Randomness is used to break the rigid backtrack-search of CP solvers and find solutions in a different order to present to a user. To do so, I designed TableSampling, a sampler working in the CP framework, that thus benefits from all the improvements in CP solvers (running time, or new constraints).
However, randomness alone is not sufficient to provide diversity. I studied and modified random search strategies to generate diverse solutions. The search can thus be guided to solutions in interesting spaces.

 

Keywords: Constraint Programming, Sampling, Probabilistic Approach, Diversity, Solution

 

Soutenance de thèse d’Arthur GODET (équipe TASC)

Arthur Godet, doctorant au sein de l’équipe TASC, soutiendra sa thèse intitulée « Sur le tri de tâches pour résoudre des problèmes d’ordonnancement avec la program­mation par contraintes » / « On the use of tasks ordering to solve scheduling problems with constraint programming« 
jeudi 23 septembre 2021 à 14h, à IMT Atlantique – campus de Nantes en salle C114. La soutenance sera retransmise en direct sur Webex (1759749054@imtatlantique.webex.com).
Jury :
– Directeur de thèse : Nicolas BELDICEANU Professeur à IMT Atlantique
– Co-directeur de thèse : Xavier LORCA Directeur centre Génie Industriel à IMT Mines Albi-Carmaux
– Encadrant de thèse : Gilles SIMONIN Maître de conférences à IMT Atlantique
– Rapporteurs : Christian ARTIGUES Directeur de recherche au LAAS-CNRS ; Claude-Guy QUIMPER Professeur à l’Université Laval
– Examinateurs : Hadrien CAMBAZARD Maître de conférences à l’Université Grenoble Alpes ; Samir LOUDNI Professeur à IMT Atlantique ; Christine SOLNON Professeure à l’INSA de Lyon
 
Résumé : Au cours des deux dernières décennies, la programmation par contraintes s’est illustrée de par son efficacité à résoudre des problèmes d’ordonnancement. Grâce à la grande expressivité permise par le paradigme, différents algorithmes et techniques de résolution provenant d’autres domaines de l’Optimisation Combinatoire ont pu être intégrés au sein des solveurs de contraintes. Toutefois, cette grande expressivité fait que les solveurs ne sont pas des boîtes noires et demandent une expertise pour être paramétrés correctement pour résoudre effica­cement les problèmes souhaités. Dans cette  thèse, nous explorons l’introduction et l’utilisation d’algorithmes de liste ordonnée en programmation par contraintes pour résoudre  des problèmes d’ordonnancement. Nous revi­sitons également la contrainte AllDiffPrec, dé­finie comme une contrainte Alldifferent et des précédences entre variables, pour laquelle nous proposons également un nouvel algorithme de filtrage.
Mots-clés : programmation par contraintes, ordonnancement, AllDiffPrec, liste ordonnée
——————————————————————————————————————————————————————————————————————-
Abstract: During the last two decades, Constraint Programming gets very good results ­to solve scheduling problems. Thanks to the great expressivity of the paradigm, different al gorithms and solving techniques from other fields within Combinatorial Optimisation have been integrated into constraint solvers. However this great expressivity cornes with a price:  constraint solvers are not the black box one might think of and require expertise to be correctly configured to efficiently solve problems. ln this thesis, we explore the introduction and the use of list ordering algorithms into Constraint Programming to solve scheduling problems. We also revisit the AIIDiffPrec constraint, defined as an Allditferent constraint with precedence between some variables, for which we propose a new filtering algorithm.
Keywords: constraint programming, scheduling, ordering, AllDiffPrec, list ordering

Entrepreneuriat, numérique et mixité

L’Université de Nantes et le Laboratoire des Sciences du Numérique de Nantes (LS2N) vous proposent une demi-journée autour de l’entrepreneuriat, du numérique et de la mixité. Ouvert à tous.tes (tous cursus et niveaux confondus).

Objectifs de cette demi-journée :

  • Découvrir le numérique à travers des ateliers ludiques
  • S’inspirer de chercheuses et entrepreneures spécialisées dans le numérique (réalité virtuelle, IA, …)
  • Enrichir son réseau (étudiant.e.s, entrepreneur.e.s, coachs, etc.)
  • En savoir plus sur l’entrepreneuriat-étudiant et les possibilités de développer un projet à l’Université

Programme : s’inspirer, faire et échanger

Séquence « témoignages » pour faire le plein d’inspiration

  • Témoignage de Charlotte Truchet (équipe TASC du LS2N)
  • Témoignage de Chloë Bidet, fondatrice d’Oséos, solutions de réalité virtuelle au service des personnes en situation de handicap

Des ateliers pratiques et ludiques pour apprendre

Proposition de 2 ateliers par le jeu : 

  • Initiation au langage PYTHON
  • Algorithmes : comment ça marche ?

Partager son travail, échanger et réseauter

A l’issue des ateliers, les participant.e.s seront  invité.e.s à échanger autour d’un moment convivial !

Participation de Charlotte Truchet à l’écriture du Calendrier 2020 des mathématiques « une histoire d’algorithmes »

Après le monde de l’aléatoire traité en 2019, c’est celui des algorithmes qui sera le thème du Calendrier Mathématique 2020.
Chaque jour, excepté les week-ends, une question de mathématique à résoudre. Au fil des mois, un algorithme est présenté à travers une magnifique illustration enrichie d’un texte explicatif.

Les réponses sont fournies en dernière page du calendrier et présentées de façon détaillée dans le livret des réponses, offert avec le calendrier.

Ana Rechtman Bulajich est maître de conférences en mathématiques à l’université de Strasbourg. Chercheuse engagée dans la promotion des mathématiques, elle souhaite, en parallèle à sa carrière universitaire, faire partager son plaisir de faire des maths. Elle a ainsi participé à la création du concept du Calendrier mathématique édité au Mexique depuis 2002 et en a proposé son adaptation en France.
Exercices (traduction) : Maxime Bourrigan, Pierre Dehornoy, Nicolas Hussenot Desenonges, Sylvain Porret-Blanc, Marion Senjan, Denis Staub.
Textes de Serge Abiteboul, et de Charlotte Truchet.

Lire un extrait.

Journées annuelles du groupe de travail Vérification du GDR Informatique et Mathématiques

Les prochaines journées annuelles du GT Vérif auront lieu du 17 au 19 juin 2019 au bâtiment S sur le site de Centrale Nantes.

Elles visent à rassembler la communauté française en vérification formelle, et en particulier les chercheurs juniors, doctorants et post-doctorants, avec pour objectif de favoriser les collaborations et l’ouverture sur des thématiques liées à la vérification. Les domaines inclus sont :

  • la vérification informatique de systèmes, modélisant des systèmes de freinage aux protocoles de communications en passant par les programmes,
  • l’emploi de techniques de preuve automatiques ou interactives (model-checking, déduction automatique, assistants de preuve, solveurs SMT, etc. ainsi que leurs combinaisons),
  • l’utilisation de logiques pour raisonner sur les propriétés des systèmes (par exemple les logiques temporelles, spatiales, probabilistes ou avec données),
  • les techniques d’abstraction pour la vérification.

Programme :

  • Mardi 18/06 16:10-17:00 : Olivier H. Roux (LS2N) : Model-checking real-time systems with Roméo
  • Mercredi 19/06 9:00-9:50 : Charlotte Truchet (LS2N) et Ghiles Ziat (LIP6) : Programmation par contraintes et interprétation abstraite

Pour plus d’infos, voir le site http://gt-verif.loria.fr/Wiki.jsp?page=JA-2019

Séminaire invité : Peter Van Roy (Université Catholique de Louvain)

L’équipe TASC du LS2N est heureuse d’accueillir le professeur Peter Van Roy, de l’Université Catholique de Louvain (Belgique).

Ce dernier animera un séminaire en anglais relatif au système de programmation Lasp : « Lasp: Elements of a programming language for edge computing »

vendredi 8 mars 2019 à 9h, dans la salle 3, au RDC du bâtiment 11 du LS2N, sur le site de la Faculté des Sciences et Techniques de Nantes (arrêt de tram : Michelet Science).

Voir sa bio.

Abstract: The Internet is turning inside out: the edge (e.g., mobile networks and Internet of Things) is growing exponentially and the center (data centers) is stable. In a few years, most of the Internet will be at the edge. This poses the question: how do we develop applications to run on edge networks? These networks are highly dynamic with unreliable nodes and intermittent connectivity. In our approach, we consider that these properties are inherent and that edge networks will always be unreliable. Our approach combines convergent computation with hybrid gossip. Convergent computation implements consistent replicated data on unreliable distributed systems. It starts with convergent data structures (CRDTs: Conflict-Free Replicated Data Types) and builds applications by composing them. Hybrid gossip algorithms, such as Plumtree and HyParView, provide a communication layer that maintains connectivity even when 70% or more of nodes fail. The result is the Lasp language and system. Lasp looks to the programmer like a combination of streaming dataflow and functional programming. In this talk, we explain the problems of edge computing and we present Lasp as a first step towards solving them. We give the semantics of Lasp in Sebastien Burckhardt’s abstraction execution formalism. Lasp is so far implemented as a library in Erlang, but eventually it will become a standalone language. We show that the functional approach is well-adapted to edge networks. We have only scratched the surface of this programming style, and we give an overview of the challenges that remain.

***********

The TASC team of the LS2N lab is honored to welcome Professor Peter Van Roy (Université Catholique de Louvain, Belgium) who will present his research in English on « Lasp: Elements of a programming language for edge computing« 

Friday, 8 of March at 9 am.
Room 3, building 11, FST site (Michelet Science tram stop)

Séminaire invité : Kazunori UEDA (Université de Waseda, Japon)

L’équipe TASC a le plaisir de recevoir le professeur Kazunori Ueda (Université de Waseda, Japon) au LS2N qui fera une présentation en anglais sur

« Analyzing and Understanding Nondeterministic Systems with LMNtal and LaViT »

jeudi 7 mars 2019 à 10h, en salle 3 au RDC du bâtiment 11, sur le site FST .

Abstract:
This talk is a gentle introduction to state-space search and model checking with LMNtal and LaViT, an IDE for LMNtal powered by visualizers.
LMNtal is a language model based on hierarchical graph rewriting that uses point-to-point links to represent connectivity and membranes to represent hierarchy. LMNtal was designed to be a substrate language of various computational models, especially those addressing concurrency, mobility and multiset rewriting. It has close connections with Colored Petri Nets, Interaction Nets, Chemical Abstract Machines, Constraint Handling Rules and Bigraphs. The expressive power of the language was demonstrated through the encoding of diverse computational models including the strong lambda calculus.
Our publicly available LMNtal implementation has evolved into a parallel LTL model checker. The strengths of our LMNtal model checker are its powerful data structures with an inherent symmetry reduction mechanism, highly nondeterministic computation it can express, and little discrepancy between programming and modeling languages. The
implementation achieved high scalability on shared-memory machines and enabled us to handle models with more than a billion states.
The visualizer of the LaViT IDE turned out to be extremely useful in understanding models by state space browsing, which is in sharp contrast with other black-box model checkers. The talk will be given with live demos of examples taken from the fields of model checking, concurrency and AI search.

Soutenance de thèse de Ekaterina ARAFAILOVA

Ekaterina Arafailova, doctorante au sein de l’équipe TASC, soutiendra sa thèse intitulée « Functional Description of Sequence Constraints and Synthesis of Combinatorial Objects »

mardi 25 septembre 2018 à 14h30 à l’IMT Atlantique dans l’amphi Besse.

La soutenance aura lieu en Anglais. / The defence will be in English and will take place on Tuesday, on the 25th of September, at 14h30, at IMT Atlantique (Nantes) in the Besse amphitheatre

Jury : Nicolas Beldiceanu (directeur), Rémi Douence (co encadrant), Michela Milano (Rapporteur, Università di Bologna, Bologne, Italie), Stanislav Zivny (Rapporteur, University of Oxford, Oxford, Royaume-Uni), John Hooker (Carnegie Mellon University, Pittsburgh, États-Unis), Claude Jard

Résumé :
À l’opposé de l’approche consistant à concevoir au cas par cas des contraintes et des algorithmes leur étant dédiés, l’objet de cette thèse concerne d’une part la description de familles de contraintes en termes de composition de fonctions, et d’autre part la synthèse d’objets combinatoires pour de telles contraintes. Les objets concernés sont des bornes précises, des coupes linéaires, des invariants non-linéaires et des automates finis ; leur but principal est de prendre en compte l’aspect combinatoire d’une seule contrainte ou d’une conjonction de contraintes. Ces objets sont obtenus d’une façon systématique et sont paramétrés par une ou plusieurs contraintes, par le nombre de variables dans une séquence, et par les domaines initiaux de ces variables. Cela nous permet d’obtenir des objets indépendants d’une instance considérée. Afin de synthétiser des objets combinatoires nous tirons partie de la vue déclarative de telles contraintes, basée sur les expressions régulières, ansi que la vue opérationnelle, basée sur les automates à registres et les transducteurs finis. Il y a plusieurs avantages à synthétiser des objets combinatoires par rapport à la conception d’algorithmes dédiés : 1) on peut utiliser ces formules paramétrées dans plusieurs contextes, y compris la programmation par contraintes et la programmation linéaire, ce qui est beaucoup plus difficile avec des algorithmes ; 2) la synergie entre des objets combinatoires nous donne une meilleure performance en pratique ; 3) les quantités calculées par certaines des formules peuvent être utilisées non seulement dans le contexte de l’optimisation mais aussi pour la fouille de données.

Mots- clés : programmation par contraintes, automates, transducteurs, expressions régulières, séries temporelles, objets combinatoires paramétrés, invariants linéaires et non-linéaires

*********

Abstract:
Contrary to the standard approach consisting of introducing ad hoc constraints and designing dedicated algorithms for handling their combinatorial aspect, this thesis takes another point of view. On the one hand, it focusses on describing a family of sequence constraints in a compositional way by multiple layers of functions. On the other hand, it addresses the combinatorial aspect of both a single constraint and a conjunction of such constraints by synthesising compositional combinatorial objects, namely bounds, linear inequalities, non-linear constraints and finite automata. These objects are obtained in a systematic way and are not instance-specific: they are parameterised by one or several constraints, by the number of variables in a considered sequence of variables, and by the initial domains of the variables. When synthesising such objects we draw full benefit both from the declarative view of such constraints, based on regular expressions, and from the operational view, based on finite transducers and register automata.
There are many advantages of synthesising combinatorial objects rather than designing dedicated algorithms: 1) parameterised formulae can be applied in the context of several resolution techniques such as constraint programming or linear programming, whereas algorithms are typically tailored to a specific technique; 2) combinatorial objects can be combined together to provide better performance in practice; 3) finally, the quantities computed by some formulae can not just be used in an optimisation setting, but also in the context of data mining.

Keywords: constraint programming, automata, transducers, regular expressions, time series, parameterised combinatorial objects, linear and non-linear invariants

Retour sur la conférence de clôture du cycle IA à Stéréolux : « Quel futur pour l’intelligence artificielle ? »

Le 14 décembre 2017, Florian Richoux (équipe TASC) a animé la conférence de clôture du cycle sur l’IA proposé par Stéréolux.

Un soixante de personnes s’étaient déplacés pour assister à cette présentation d’un peu plus d’une heure. Les avenirs possibles et impossibles de l’IA dans 10 ans d’un point de vue scientifique et technique ont été abordés. Florian a également parlé d’IA, d’art et de créativité : ce que l’on arrive à faire aujourd’hui et vers quoi on tend certainement. Une conclusion assez large a permis de lancer des questions autour de l’IA dans la société (éthique, droit, travail, etc).

Retouvez :

  • la captation vidéo de l’événement sur la chaîne Youtube du Labo Arts et Tech de Stéréolux
  • le podcast de la conférence sur le site de la radio SUN (Le Son Unique à Nantes).

Soutenance d’HDR de Charlotte TRUCHET (équipe TASC)

Charlotte Truchet soutiendra son Habilitation à Diriger des Recherches, intitulée « Vers une programmation par contraintes moins contrainte, outils venant de l’Interprétation Abstraite et de l’Analyse en Moyenne pour définir des solveurs plus expressifs et faciles à utiliser »

jeudi 30 novembre 2017 à 10h, sur le site de la FST.

Jury : Nadia Creignou (Aix-Marseille Université – rapporteure), Christian Schulte (KTH, Suède – rapporteur), Pascal Van Hentenryck (University of Michigan, USA – rapporteur), Gérard Assayag (IRCAM), Frédéric Benhamou (Université de Nantes), Eric Goubault (Ecole Polytechnique), Thomas Jensen (INRIA), Brigitte Vallée (CNRS).

Le manuscrit est disponible en ligne (lien pdf).

Copyright : LS2N 2017 - Mentions Légales - 
 -