Alessio Mansutti's ICALP paper “Integer Linear-Exponential Programming in NP by Quantifier Elimination” wins the Track B Best Paper Award

September 26, 2024

Alessio Mansutti's ICALP paper “Integer Linear-Exponential Programming in NP by Quantifier Elimination” wins the Track B Best Paper Award

IMDEA Software researcher Alessio Mansutti’s paper “Integer Linear-Exponential Programming in NP by Quantifier Elimination”, coauthored by Dmitry Chistikov and Mikhail Starchak, won the Track B Best Paper Award at the International Colloquium on Automata, Languages, and Programming (ICALP) 2024, which is a flagship research meeting.

Integer Linear Programming

Can you give $15$ Euro to someone by using fewer $5$ Euro bills than $2$ Euro coins? Computer scientists and mathematicians may see this problem as the task of finding a solution to the system of equations

$5 x + 2 y = 15$
$x < y$
$x \geq 0$
$y \geq 0$

where $x$ and $y$ are variables representing the amount of $5$ Euro bills and $2$ Euro coins to be used. The constraints $x \geq 0$ and $y \geq 0$ specify that this amount cannot be negative, whereas the constraints $5 x + 2 y = 15$ and $x < y$ encode our problem of reaching exactly $15$ Euro using fewer bills than coins. Tearing $5$ Euro bills in half is not allowed: $x$ and $y$ must be whole numbers!

The problem above (which, by the way, has a solution: $x = 1$ and $y = 5$ ) is an instance of a more general problem called Integer Linear Programming (ILP). This problem asks if it is possible to assign integer values to a bunch of variables $x_{1}, \dots, x_{d}$ in a way that satisfies a system of several equations of the form

$a_{1} \cdot x_{1} + \dots + a_{d} \cdot x_{d} \leq c$ ,

where $a_{1}, \dots, a_{d}$ and $c$ are integer constants (for instance, above, $2$ and $15$ are some of these constants).

ILP is a fundamental problem in computer science, and after many decades of research and engineering we now have efficient software to solve this problem. Finding the best route for a driver to bring a parcel at your address? That’s solved with ILP. Scheduling aircrafts, their routes, and their crew members? Airlines use ILP not only for these tasks, but also for optimising ticket pricing! How do banks quantify the risk involved when lending money to a borrower? They use ILP solvers. How are the available frequencies in GSM mobile networks distributed across antennas so that interference is minimised? ILP! Whenever companies need to solve a difficult planning problem, their rely on ILP.

Integer Linear-Exponential Programming

There are problems that cannot be solved with ILP. Let us take for instance the following program

Input: an integer $y \geq 1$
Output: an integer $x$
$x \leftarrow 1$
while $y > 0$ do
$y \leftarrow y - 1$
$x \leftarrow 2 \cdot x$
end while
return $x$

This program takes as input a positive integer $y$ , and repeatedly subtracts $1$ from it until it becomes zero. Each time a subtraction is performed, a variable $x$ , that is initially set to $1$ , is multiplied by $2$ . Once $y$ becomes zero, the program returns the current value of $x$ . We can ask for a system of constraints characterising the possible values that $x$ takes at the end of the program, for the different choices of the input $y$ . For $y = 1$ , $x$ is $2$ . For $y = 2$ , $x$ is $4$ . $y = 3$ , $x$ is $8$ , and so on. In general, we get the system of constraints

$y \geq 1$
$x = 2^{y}$

where $2^{y}$ is the exponential function: $2$ multiplied to itself $y$ times.

Many techniques to prove that programs do not contain bugs require putting together several systems of constraints as the one above and check whether the resulting system has a solution. We face however a major problem: the exponential function cannot be expressed in ILP. How can we then check if the system has a solution? Is this even possible to check?

The above is an instance of the Integer Linear-Exponential Programming problem: is it possible to assign integer values to variables $x_{1}, \dots, x_{d}$ in a way that satisfies a system of equations of the form

$a_{1} \cdot x_{1} + \dots + a_{d} \cdot x_{d} + b_{1} \cdot 2^{x_{1}} + \dots + b_{d} \cdot 2^{x_{d}} \leq c$ ,

where $a_{1}, \dots, a_{d}$ , $b_{1}, \dots, b_{d}$ and $c$ are integer constants? Alessio, Dmitry and Mikhail’s work shows not only that there is an algorithm to solve this problem, but also that it can be done (for the moment, in theory) as fast as solving ILP! More precisely, their paper shows that Integer Linear-Exponential Programming belongs to NP, the complexity class at the centre of the renowned P vs. NP dilemma. This is an exciting news, as it may pave the way for extending ILP solvers to handle problems requiring the exponential function, as the ones stemming from program verification.

Want to know more? Check out the paper!

About ICALP

The International Colloquium on Automata, Languages and Programming (ICALP) is the flagship conference and annual meeting of the European Association for Theoretical Computer Science (EATCS). The conference was launched in 1972, and this year was its 51st edition. It took place in Tallinn, Estonia, on the 8th to 12th of July 2024.