SMT and Functional Equation Solving over the Reals: Challenges from the IMO
By: Chad E. Brown , Karel Chvalovský , Mikoláš Janota and more
Potential Business Impact:
Lets computers solve hard math competition problems.
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.
Similar Papers
Towards Learning Infinite SMT Models (Work in Progress)
Logic in Computer Science
Finds patterns in math problems for computers.
Synthesiz3 This: an SMT-Based Approach for Synthesis with Uncomputable Symbols
Logic in Computer Science
Makes computers write code from math problems.
Efficient Volume Computation for SMT Formulas
Logic in Computer Science
Measures how much space a math problem's answers fill.