The researcher Alessio Mansutti is from Udine, a city in north-eastern Italy, he tells us it is a wonderful city to live in and from there you can reach either the Adriatic Sea or the Alps in 1 hour. He did the bachelor and master studies in Udine, his PhD in École Normale Supérieure Paris-Saclay, and before joining IMDEA Software, he was a postdoctoral researcher in University of Oxford.
We asked him at what point did he decide to study a scientific career and he told us he was not sure if he made this choice consciously: “I was drawn to science since I was a kid. For what I remember, throughout elementary school my main hobbies where basketball and doing science experiments. At the time, a well-known publisher in Italy started several series of biweekly science magazines for kids (one in astronomy, one on the human body, etc.). I had almost all volumes of all series. I would do all experiments in these volumes with my dad, and he had an agreement with my math teacher to redo the best ones in my class.” From that point onward, his fascination with scientific topics only grew.
As of how he ended up pursuing a PhD, “it was a very pleasant accident”, he says. In fact, he had decided the opposite, to not do a PhD, and already started interviewing for a few companies (this was a bit before the end of his Master). According to Alessio: “the day after my master’s Viva I received an email from Angelo Montanari (one of my University professors in Udine) about the possibility of doing a PhD in Paris. Stéphane Demri, who later became my PhD advisor invited me there for one week. I really liked the lab and Stéphane, so I threw away my “PhD Pros and Cons” list and decided to move to France.”
“I work in computational logic, and nowadays mainly in algorithms for arithmetic theories. Arithmetic theories are languages to specify statements about numbers. Algorithms for these types of statements can be mainly categorized into four groups: algorithms that find whether a statement is true or false, algorithms that return some (or all) solutions for which a statement is true, algorithms that count the number of solutions, and algorithms that find an optimal solution satisfying a certain statement”, remarks Mansutti.
For Alessio, arithmetic theories are essential in several areas of computer science and computational mathematics. He gives us three examples of why they are so important:
Algorithms for arithmetic theories are used inside Satisfiability Modulo Theories (SMT) tools. These are tools that are nowadays widely used in industries, in particular for the verification and debugging of Software and Hardware systems. Arithmetic theories are also used inside compilers, for both type checking and code optimization.
Society heavily relies on solving optimization and planning problems: airport need to schedule flights, routes to transport goods need to be optimized, and so on. All these optimization and planning problems can be encoded into arithmetic theories and then solved using tools for these theories.
Recently, several mathematical statements only conjectured to be true where proven using solvers for arithmetic theories. Doing this only requires finding a smart way to encode the statement of the problem in the language of arithmetic, and let the solver run until completion. Currently, these mathematical statements do not have a practical impact in industries (they might have in the future), but if anything, they showcase how solvers are nowadays able to find solutions to problems that not even experts are able to solve.
