More is Less: Adding Polynomials for Faster Explanations in NLSAT
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866914203867021312 |
|---|---|
| author | Promies, Valentin Nalbach, Jasper Ábrahám, Erika Wagner, Paul |
| author_facet | Promies, Valentin Nalbach, Jasper Ábrahám, Erika Wagner, Paul |
| contents | To check the satisfiability of (non-linear) real arithmetic formulas, modern satisfiability modulo theories (SMT) solving algorithms like NLSAT depend heavily on single cell construction, the task of generalizing a sample point to a connected subset (cell) of $\mathbb{R}^n$, that contains the sample and over which a given set of polynomials is sign-invariant.
In this paper, we propose to speed up the computation and simplify the representation of the resulting cell by dynamically extending the considered set of polynomials with further linear polynomials. While this increases the total number of (smaller) cells generated throughout the algorithm, our experiments show that it can pay off when using suitable heuristics due to the interaction with Boolean reasoning. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_14269 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | More is Less: Adding Polynomials for Faster Explanations in NLSAT Promies, Valentin Nalbach, Jasper Ábrahám, Erika Wagner, Paul Symbolic Computation To check the satisfiability of (non-linear) real arithmetic formulas, modern satisfiability modulo theories (SMT) solving algorithms like NLSAT depend heavily on single cell construction, the task of generalizing a sample point to a connected subset (cell) of $\mathbb{R}^n$, that contains the sample and over which a given set of polynomials is sign-invariant. In this paper, we propose to speed up the computation and simplify the representation of the resulting cell by dynamically extending the considered set of polynomials with further linear polynomials. While this increases the total number of (smaller) cells generated throughout the algorithm, our experiments show that it can pay off when using suitable heuristics due to the interaction with Boolean reasoning. |
| title | More is Less: Adding Polynomials for Faster Explanations in NLSAT |
| topic | Symbolic Computation |
| url | https://arxiv.org/abs/2512.14269 |