Minimal-model-guided approaches to solving polynomial constraints and extensions
Visualitza/Obre
10.1007/978-3-319-09284-3-25
Inclou dades d'ús des de 2022
Cita com:
hdl:2117/24333
Tipus de documentText en actes de congrés
Data publicació2014
EditorSpringer
Condicions d'accésAccés obert
Tots els drets reservats. Aquesta obra està protegida pels drets de propietat intel·lectual i
industrial corresponents. Sense perjudici de les exempcions legals existents, queda prohibida la seva
reproducció, distribució, comunicació pública o transformació sense l'autorització del titular dels drets
Abstract
In this paper we present new methods for deciding the satisfiability of formulas involving integer polynomial constraints. In previous work we proposed to solve SMT(NIA) problems by reducing them to SMT(LIA): non-linear monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. When variables do not have finite domains, artificial ones can be introduced by imposing a lower and an upper bound, and made iteratively larger until a solution is found (or the procedure times out). For the approach to be practical, unsatisfiable cores are used to guide which domains have to be relaxed (i.e., enlarged) from one iteration to the following one. However, it is not clear then how large they have to be made, which is critical. Here we propose to guide the domain relaxation step by analyzing minimal models produced by the SMT(LIA) solver. Namely, we consider two different cost functions: the number of violated artificial domain bounds, and the distance with respect to the artificial domains. We compare these approaches with other techniques on benchmarks coming from constraint-based program analysis and show the potential of the method. Finally, we describe how one of these minimal-model-guided techniques can be smoothly adapted to deal with the extension Max-SMT of SMT(NIA) and then applied to program termination proving.
CitacióLarraz, D. [et al.]. Minimal-model-guided approaches to solving polynomial constraints and extensions. A: International Conference on Theory and Applications of Satisfiability Testing. "Theory and Applications of Satisfiability Testing, SAT 2014 : 17th International Conference, held as part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014 : Proceedings". Vienna: Springer, 2014, p. 333-350.
Versió de l'editorhttp://link.springer.com/chapter/10.1007%2F978-3-319-09284-3_25
Fitxers | Descripció | Mida | Format | Visualitza |
---|---|---|---|---|
sat14.pdf | 136,1Kb | Visualitza/Obre |