Romain Wallon, Postdoc au LIX Romain Wallon

Courte Biographie

Romain Wallon

Après avoir obtenu mon Baccalauréat Scientifique (spécialité Mathématiques) en 2012, j’ai effectué mon cursus universitaire à l’Université d’Artois. J’y ai obtenu une Licence d’Informatique et une Licence de Mathématiques en 2015, ainsi qu’un Master d’Informatique (parcours Intelligence Artificielle) en 2017.

Par la suite, j’ai obtenu mon Doctorat sur le Raisonnement à partir de contraintes pseudo-booléennes et la compilation à l’Université d’Artois, sous la direction de Daniel Le Berre et Pierre Marquis et co-encadré par Stefan Mengel.

Depuis octobre 2020, je suis en contrat postdoctoral au sein de l’équipe OptimiX du Laboratoire d’Informatique de l’École Polytechnique (LIX), où j’étudie l’intégration de techniques de programmation spéculative dans différents types de solveurs, encadré par Claudia D’Ambrosio, Youssef Hamadi et Rémi Delmas.

Romain Wallon

Après avoir obtenu mon Baccalauréat Scientifique (spécialité Mathématiques) en 2012, j’ai effectué mon cursus universitaire à l’Université d’Artois. J’y ai obtenu une Licence d’Informatique et une Licence de Mathématiques en 2015, ainsi qu’un Master d’Informatique (parcours Intelligence Artificielle) en 2017.

Par la suite, j’ai obtenu mon Doctorat sur le Raisonnement à partir de contraintes pseudo-booléennes et la compilation à l’Université d’Artois, sous la direction de Daniel Le Berre et Pierre Marquis et co-encadré par Stefan Mengel.

Depuis octobre 2020, je suis en contrat postdoctoral au sein de l’équipe OptimiX du Laboratoire d’Informatique de l’École Polytechnique (LIX), où j’étudie l’intégration de techniques de programmation spéculative dans différents types de solveurs, encadré par Claudia D’Ambrosio, Youssef Hamadi et Rémi Delmas.

CV

Ci-dessous sont présentés mes expériences, diplômes et compétences.

Enseignements

Ci-dessous sont présentés les différents enseignements que j’ai dispensés. Cliquez sur l’année qui vous intéresse pour plus de détails.

Recherche

Je m’intéresse à la résolution du problème de cohérence propositionnelle, notamment par le biais du raisonnement pseudo-booléen. J’étudie également diverses applications des solveurs SAT, comme l’optimisation sous contraintes et la compilation de connaissances. Ci-dessous sont présentés mes différents travaux de recherche. Vous pouvez également les retrouver sur DBLP, HAL, ORCID, ResearchGate, ou encore Semantic Scholar.

Journaux Internationaux

Graph Width Measures for CNF-Encodings with Auxiliary Variables
mars 2020
Stefan Mengel et Romain Wallon, dans le Journal of Artificial Intelligence Research (JAIR), volume 67.

Conférences Internationales

On Dedicated CDCL Strategies for PB Solvers
juillet 2021
Daniel Le Berre et Romain Wallon, dans les actes de la 24e International Conference on Theory and Applications of Satisfiability Testing (SAT’21).
On Weakening Strategies for PB Solvers
juillet 2020
Daniel Le Berre, Pierre Marquis et Romain Wallon, dans les actes de la 23e International Conference on Theory and Applications of Satisfiability Testing (SAT’20).
On Irrelevant Literals in Pseudo-Boolean Constraint Learning
juillet 2020
Daniel Le Berre, Pierre Marquis, Stefan Mengel et Romain Wallon, dans les actes de la 29e International Joint Conference on Artificial Intelligence (IJCAI’20).
Revisiting Graph Width Measures for CNF-Encodings
juillet 2019
Stefan Mengel et Romain Wallon, dans les actes de la 22e International Conference on Theory and Applications of Satisfiability Testing (SAT’19).
Pseudo-Boolean Constraints from a Knowledge Representation Perspective
juillet 2018
Daniel Le Berre, Pierre Marquis, Stefan Mengel et Romain Wallon, dans les actes de la 27e International Joint Conference on Artificial Intelligence (IJCAI’18).

Conférences Nationales

Adaptation des stratégies des solveurs SAT CDCL aux solveurs PB natifs
juin 2021
Daniel Le Berre et Romain Wallon, dans les Actes des 16es Journées Francophones de Programmation par Contraintes (JFPC’21).
Metrics : Mission Expérimentations
juin 2021
Thibault Falque, Romain Wallon et Hugues Wattez, dans les Actes des 16es Journées Francophones de Programmation par Contraintes (JFPC’21).
Partitionnement d’hypergraphes pour la compilation de formules pseudo-booléennes
avril 2021
Romain Wallon, à la 22e Conférence ROADEF de la Société Française de Recherche Opérationnelle et Aide à la Décision (présentation seulement).
De la pertinence des littéraux dans les contraintes pseudo-booléennes apprises
juin 2019
Daniel Le Berre, Pierre Marquis, Stefan Mengel et Romain Wallon, dans les Actes des 15es Journées Francophones de Programmation par Contraintes (JFPC’19).

Ateliers Internationaux

On Improving the Backjump Level in PB Solvers
juillet 2021
Romain Wallon, présenté au 12e International Workshop on Pragmatics of SAT (POS’21).
On Adapting CDCL Strategies for PB Solvers
juillet 2020
Romain Wallon, présenté au 11e International Workshop on Pragmatics of SAT (POS’20).
Metrics: Towards a Unified Library for Experimenting Solvers
juillet 2020
Thibault Falque, Romain Wallon et Hugues Wattez, présenté au 11e International Workshop on Pragmatics of SAT (POS’20).
On Irrelevant Literals in Pseudo-Boolean Constraint Learning
juillet 2019
Daniel Le Berre, Pierre Marquis, Stefan Mengel et Romain Wallon, présenté au 10e International Workshop on Pragmatics of SAT (POS’19).

Présentations

Hypergraph Partitioning for Compiling Pseudo-Boolean Formulae
26 mai 2021
Présentation réalisée dans le cadre des séminaires de l’équipe OptimiX (visioconférence).
Deep Dive into CDCL Pseudo-Boolean Solvers
20 mai 2021
Séminaire invité au LaBRI (Laboratoire Bordelais de Recherche en Informatique) (visioconférence).
Deep Dive into CDCL Pseudo-Boolean Solvers
23 février 2021
Séminaire invité dans le cadre de l’atelier Beyond Satisfiability du Simons Institute for the Theory of Computing (visioconférence), en collaboration avec Daniel Le Berre.
Pseudo-Boolean Reasoning and Compilation
14 décembre 2020
Soutenance de Thèse.
Metrics: A Unified Library for Experimenting Solvers
17-24 septembre 2020
Présentation réalisée dans le cadre des séminaires hebdomadaires du CRIL, en collaboration avec Thibault Falque et Hugues Wattez.
Tuning Sat4j PB Solvers for Decision Problems
28 août 2020
Séminaire invité au groupe de recherche Mathematical Insights into Algorithms for Optimization (MIAO) (visioconférence).
Pseudo-Boolean Constraints: Reasoning and Compilation
11 septembre 2017
Séminaire invité à l’Institut Royal de Technologie (KTH), Stockholm, Suède.

Manuscrits

Pseudo-Boolean Reasoning and Compilation
décembre 2020
Thèse de Doctorat.
Raisonnement à partir de contraintes pseudo-booléeennes et compilation
septembre 2017
Mémoire de stage de Master 2.
Heuristiques pour la décomposition de formules CNF
juin 2016
Mémoire de Travail d’Étude et de Recherche (TER) de Master 1.

Logiciels

Ci-dessous sont présentés les logiciels et bibliothèques (académiques ou non) que j’ai développés ou auxquels j’ai contribué.

Sat4j

Je suis un contributeur du solveur Sat4j, la « bibliothèque libre de satisfaction et d’optimisation en variables booléennes pour la machine virtuelle Java ».

Metrics

En tant que membre de l’équipe WWF (composée de Hugues Wattez, Romain Wallon et Thibault Falque), je participe au développement de la bibliothèque libre Metrics, conçue pour faciliter la réalisation d’expérimentations et leur analyse. L’objectif principal de Metrics est de fournir une chaîne complète d’outils allant de l’exécution du logiciel à l’analyse de ses performances. Le développement de Metrics a commencé en partant du constat que, dans la communauté SAT, le processus d’expérimentation des solveurs reste en grande partie le même : la plupart du temps, ce sont les mêmes statistiques sur l’exécution du solveur qui sont collectées. Cependant, il existe probablement autant de scripts que de chercheurs du domaine pour récupérer ces données expérimentales et produire les figures associées. L’ambition de Metrics est de simplifier la récupération des données expérimentales à partir de nombreuses entrées différentes (y compris les fichiers produits par le solveur), et fournir une interface simple pour produire des graphiques communément utilisés, calculer des statistiques sur l’exécution du solveur, et organiser le tout en un minimum d’efforts. Au final, le but principal de Metrics est de favoriser le partage et la reproductibilité des résultats expérimentaux et de leur analyse.

Autograph

Dans le cadre du développement de Metrics, j’ai participé à la création de la bibliothèqe Autograph, qui propose une interface unifiée pour différentes bibliothèques populaires permettant le tracé de diagrammes en Python (par exemple, Maplotlib ou Plotly).

PBD4

J’ai créé PBD4, un implantation en Java du compilateur D4 qui l’étend pour permettre la compilation native de formules pseudo-booléennes (développement en cours).

JKaHyPar

J’ai développé JKaHyPar, un binding Java de la bibliothèque KaHyPar (Karlsruhe Hypergraph Partitioning) permettant le partitionnement d’hypergraphes.

Gitmoji4Eclipse

J’ai participé, en collaboration avec Thibault Falque, à la conception du plugin gitmoji4eclipse (disponible sous licence EPL), qui propose une vue permettant d’intégrer dans l’IDE Eclipse le choix du Gitmoji le plus adapté au moment de rédiger un message de commit, afin de marquer visuellement le but dudit commit.

AcronymMaker

J’ai développé un outil de génération d’acronymes, appelé AcronymMaker, qui permet de facilement nommer des projets (tels que des logiciels, par exemple) à partir d’une phrase décrivant le rôle de ce projet. Cet outil implante différentes stratégies permettant de personnaliser la manière dont les acronymes sont générés.