SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Logic in Computer Science
2025-07-10 v2
Abstract
We use SMT technology to address a class of problems involving uninterpreted functions and nonlinear real arithmetic. In particular, we focus on problems commonly found in mathematical competitions, such as the International Mathematical Olympiad (IMO), where the task is to determine all solutions to constraints on an uninterpreted function. Although these problems require only high-school-level mathematics, state-of-the-art SMT solvers often struggle with them. We propose several techniques to improve SMT performance in this setting.
Keywords
Cite
@article{arxiv.2504.15645,
title = {SMT and Functional Equation Solving over the Reals: Challenges from the IMO},
author = {Chad E. Brown and Karel Chvalovský and Mikoláš Janota and Mirek Olšák and Stefan Ratschan},
journal= {arXiv preprint arXiv:2504.15645},
year = {2025}
}