Romain Wallon, Postdoc at LIX 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.

Then, 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.

Since October 2020, I am a postdoc in the OptimiX team of the Laboratoire d’Informatique de l’École Polytechnique (LIX), where I study how to integrate speculative programming techniques in different kinds of solvers, supervised by Claudia D’Ambrosio, Youssef Hamadi and Rémi Delmas.

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.

Then, 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.

Since October 2020, I am a postdoc in the OptimiX team of the Laboratoire d’Informatique de l’École Polytechnique (LIX), where I study how to integrate speculative programming techniques in different kinds of solvers, supervised by Claudia D’Ambrosio, Youssef Hamadi and Rémi Delmas.

CV

Below are presented my experiences, diplomas and skills. You can also download the more detailled PDF version of my CV.

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 HAL, DBLP, ORCID or ResearchGate.

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 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).
On Weakening Strategies for PB Solvers
July 2020
Daniel Le Berre, Pierre Marquis and Romain Wallon, in Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT’20).
Revisiting Graph Width Measures for CNF-Encodings
July 2019
Stefan Mengel and Romain Wallon, in Proceedings of the 21st 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

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çais 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 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 et Romain Wallon, presented at the 10th International Workshop on Pragmatics of SAT (POS’19).

Presentations

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 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 described 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”.

PBD4

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

Metrics

As a member of the WWF team (Hugues Wattez, Romain Wallon and Thibault Falque), I participate 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 software programs 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 solver 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 output), and 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.

JKaHyPar

I developed JKaHyPar, a Java binding of the KaHyPar (Karlsruhe Hypergraph Partitioning) library allowing to partition hypergraphs.

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, allowing 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.