MCSAT Modulo Transcendental Arithmetics
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916070592348160 |
|---|---|
| author | Gallego-Hernández, Jorge Lipparini, Enrico Mansutti, Alessio |
| author_facet | Gallego-Hernández, Jorge Lipparini, Enrico Mansutti, Alessio |
| contents | We propose a framework for solving quantifier-free formulas from (undecidable) extensions of non-linear real arithmetic (NRA) with transcendental functions, such as exponential and trigonometric ones. The framework extends the Model Constructive Satisfiability calculus (MCSAT), and leverages procedures for NRA and methods from real analysis. At its core, our procedure abstracts the input formula to NRA, and lets MCSAT and an NRA plugin incrementally build a partial model of the abstracted formula. A Transcendental Real Arithmetic plugin, acting as an intermediary between MCSAT and the NRA plugin, ensures the consistency of the partial model and is responsible for refining the abstracted formula. We implemented our procedure in the Yices2 SMT solver for the sine and exponential functions, and conducted an extensive empirical evaluation that shows that our prototype outperforms state-of-the-art solvers on both SAT and UNSAT instances. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2606_00697 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | MCSAT Modulo Transcendental Arithmetics Gallego-Hernández, Jorge Lipparini, Enrico Mansutti, Alessio Logic in Computer Science We propose a framework for solving quantifier-free formulas from (undecidable) extensions of non-linear real arithmetic (NRA) with transcendental functions, such as exponential and trigonometric ones. The framework extends the Model Constructive Satisfiability calculus (MCSAT), and leverages procedures for NRA and methods from real analysis. At its core, our procedure abstracts the input formula to NRA, and lets MCSAT and an NRA plugin incrementally build a partial model of the abstracted formula. A Transcendental Real Arithmetic plugin, acting as an intermediary between MCSAT and the NRA plugin, ensures the consistency of the partial model and is responsible for refining the abstracted formula. We implemented our procedure in the Yices2 SMT solver for the sine and exponential functions, and conducted an extensive empirical evaluation that shows that our prototype outperforms state-of-the-art solvers on both SAT and UNSAT instances. |
| title | MCSAT Modulo Transcendental Arithmetics |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2606.00697 |