Romain Wallon, Associate Professor at Artois University Romain Wallon

Short Biography

Romain Wallon

In 2012, I got a Scientifical Baccalauréat with speciality in Mathematics. I then got a Bachelor’s Degree in Computer Science and in Mathematics in 2015, and a Master’s Degree in Computer Science (speciality in Artificial Intelligence) in 2017 from Artois University. In 2020, I got a PhD on Pseudo-Boolean Reasoning and Compilation from Artois University, advised by Daniel Le Berre and Pierre Marquis and supervised by Stefan Mengel.

Between October 2020 and September 2021, I was a Postdoc in the OptimiX team of the Laboratoire d’Informatique de l’École Polytechnique (LIX), where I worked on integrating speculative programming techniques in different kinds of solvers, supervised by Claudia D’Ambrosio, Rémi Delmas and Youssef Hamadi.

Since October 2021, I am an Associate Professor in Computer Science at Artois University, where I teach at the IUT (Technical Institute) of Lens and I do my research at the Lens Computer Science Research Lab (CRIL).

Romain Wallon

In 2012, I got a Scientifical Baccalauréat with speciality in Mathematics. I then got a Bachelor’s Degree in Computer Science and in Mathematics in 2015, and a Master’s Degree in Computer Science (speciality in Artificial Intelligence) in 2017 from Artois University. In 2020, I got a PhD on Pseudo-Boolean Reasoning and Compilation from Artois University, advised by Daniel Le Berre and Pierre Marquis and supervised by Stefan Mengel.

Between October 2020 and September 2021, I was a Postdoc in the OptimiX team of the Laboratoire d’Informatique de l’École Polytechnique (LIX), where I worked on integrating speculative programming techniques in different kinds of solvers, supervised by Claudia D’Ambrosio, Rémi Delmas and Youssef Hamadi.

Since October 2021, I am an Associate Professor in Computer Science at Artois University, where I teach at the IUT (Technical Institute) of Lens and I do my research at the Lens Computer Science Research Lab (CRIL).

CV

Below are briefly presented my experiences, diplomas and skills.

Teaching

Below are presented the various lessons I gave. Click on the year in which you are interested for more details.

Research

I am interested in satisfiability solving, and in particular in approaches based on pseudo-Boolean reasoning. I also work on different applications of SAT solvers, such as constrained optimization and knowledge compilation. Below are presented my different research works, which may also be retrieved on DBLP, HAL, ORCID, ResearchGate, or Semantic Scholar.

Keywords: automated reasoning, explainable and robust AI, knowledge compilation, knowledge representation, pseudo-Boolean constraints, satisfiability, solvers, speculative programming

International Journals

Graph Width Measures for CNF-Encodings with Auxiliary Variables
March 2020
Stefan Mengel and Romain Wallon, in Journal of Artificial Intelligence Research (JAIR), volume 67.

International Conferences

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

National Conferences

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

International Workshops

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

Presentations

Hypergraph Partitioning for Compiling Pseudo-Boolean Formulae
May 26th, 2021
Presentation at an OptimiX team seminar (remote).
Deep Dive into CDCL Pseudo-Boolean Solvers
May 20th, 2021
Invited talk at LaBRI (Laboratoire Bordelais de Recherche en Informatique) (remote).
Deep Dive into CDCL Pseudo-Boolean Solvers
February 23rd, 2021
Invited talk at the Beyond Satisfiability workshop of the Simons Institute for the Theory of Computing (remote), with Daniel Le Berre.
Pseudo-Boolean Reasoning and Compilation
December 14th, 2020
PhD Defense.
Metrics: A Unified Library for Experimenting Solvers
September 17-24th, 2020
Presentation at the weekly CRIL seminars, with Thibault Falque and Hugues Wattez.
Tuning Sat4j PB Solvers for Decision Problems
August 28th, 2020
Invited seminar at the Mathematical Insights into Algorithms for Optimization (MIAO) research group (remote).
Pseudo-Boolean Constraints: Reasoning and Compilation
September 11th, 2017
Invited seminar at the Royal Institute of Technology (KTH), Stockholm, Sweden.

Manuscripts

Pseudo-Boolean Reasoning and Compilation
December 2020
PhD Dissertation.
Raisonnement à partir de contraintes pseudo-booléeennes et compilation
September 2017
Master Thesis.
Heuristiques pour la décomposition de formules CNF
June 2016
Survey and Research Work (TER).

Software

Below are presented the software programs and libraries (from academia or not) that I developed or to which I contributed.

Sat4j

I am a committer of the solver Sat4j, a “full featured Boolean reasoning library designed to bring state-of-the-art SAT technologies to the Java Virtual Machine”.

Metrics

As a member of the WWF team (Hugues Wattez, Romain Wallon and Thibault Falque), I am involved in the development of the Metrics open-source library, designed to facilitate the conduction of experiments and their analysis. The main objective of Metrics is to provide a complete toolchain from the execution of “experimentwares” to the analysis of their performance. In particular, the development of Metrics started with the observation that, in the SAT community, the process of experimenting solvers remains mostly the same: everybody collects almost the same statistics about the solver execution. However, there are probably as many scripts as researchers in the domain for retrieving experimental data and drawing figures. There is thus clearly a need for a tool that unifies and makes easier the analysis of solver experiments. The ambition of Metrics is thus to simplify the retrieval of experimental data from many different inputs (including the solver’s raw output), and to provide a nice interface for drawing commonly used plots, computing statistics about the execution of the solver, and effortlessly organizing them. In the end, the main purpose of Metrics is to favor the sharing and reproducibility of experimental results and their analysis.

Autograph

During the development of Metrics, I also worked on the Autograph library, which provides a unified interface for various popular plotting libraries in Python (for instance, Maplotlib or Plotly).

PBD4

I created PBD4, a Java implementation of the D4 compiler that extends it to allow the native compilation of pseudo-Boolean formulae (ongoing development).

JKaHyPar

I developed JKaHyPar, a Java binding of the KaHyPar (Karlsruhe Hypergraph Partitioning) library for hypergraph partitioning.

Gitmoji4Eclipse

I participated, together with Thibault Falque, to the design of the gitmoji4eclipse plugin (available under EPL), which provides a view integrating in the Eclipse IDE the choice of the most suitable Gitmoji when writing a commit message, so that the purpose of this commit is visually clearer.

AcronymMaker

I developed a tool for generating acronyms, called AcronymMaker, which allows to easily find a name for projects (such as software programs, for instance) from a phrase describing the purpose of this project. This tool implements different strategies allowing to customize the way acronyms are generated.