MIAO wins two awards for best paper in 2022
Trustworthy combinatorial optimization
Combinatorial optimization deals with problems where solutions are constructed by combining objects in the best possible way, like when packages should be distributed between delivery trucks, or crews and planes should be assigned in an airline flight schedule. Such problems are computationally extremely challenging, but during the last decades so-called combinatorial solvers have been developed that often work amazingly well in practice. That is, except for the "dirty little secret" that even the best commercial tools sometimes produce incorrect solutions, and this can be very hard to detect.
The MIAO group aims to address this problem by designing a new generation of so-called certifying combinatorial solvers. Such solvers output not only solutions but also simple, machine-verifiable proofs that the claimed solutions are correct. These proofs can then be verified by a separate computer program, a proof checker, and if the proof checker accepts the proof, then the user can trust the result.
For this work, the MIAO group first won a Distinguished Paper Award this February at the AAAI Conference on Artificial Intelligence, one of the premier venues in AI research. In August, they followed up on this with a Best Paper Award at the International Conference on Theory and Applications of Satisfiability Testing, the flagship conference of the Boolean satisfiability (SAT) community.
Congratulations on the big win to the whole team!