标题： SMT与实数上的函数方程求解：来自IMO的挑战 显示英文标题

标题： SMT and Functional Equation Solving over the Reals: Challenges from the IMO

摘要： 我们使用SMT技术来解决涉及未解释函数和非线性实数算术的一类问题。 特别是，我们关注在数学竞赛中常见的问题，例如国际数学奥林匹克竞赛（IMO），其中任务是确定对未解释函数的约束的所有解。 尽管这些问题只需要高中水平的数学知识，但最先进的SMT求解器通常会遇到困难。 我们提出几种技术来提高在此情境下的SMT性能。 显示英文摘要

摘要： 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.