SMT and Functional Equation Solving over the Reals: Challenges from the IMO
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911046304792576 |
|---|---|
| author | Brown, Chad E. Chvalovský, Karel Janota, Mikoláš Olšák, Mirek Ratschan, Stefan |
| author_facet | Brown, Chad E. Chvalovský, Karel Janota, Mikoláš Olšák, Mirek Ratschan, Stefan |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_15645 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | SMT and Functional Equation Solving over the Reals: Challenges from the IMO Brown, Chad E. Chvalovský, Karel Janota, Mikoláš Olšák, Mirek Ratschan, Stefan Logic in Computer Science 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. |
| title | SMT and Functional Equation Solving over the Reals: Challenges from the IMO |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.15645 |