Skip to content
Snippets Groups Projects
Select Git revision
  • f5357ece6851bb5d6752223c82f61951bed13d10
  • main default protected
2 results

seminar.md

Blame
  • Séminaires

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