Subtropical Satisfiability

Abstract : Quantifier-free nonlinear arithmetic (QF NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of single very large multivariate polynomials. Our method takes as input conjunctions of strict polynomial inequalities, which represent more than 40% of the QF NRA section of the SMT-LIB library of benchmarks. The method takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. It then uses, in turn, SMT to solve linear problems over the reals to heuristi-cally find suitable points that translate back to satisfying points for the original problem. Systematic experiments on the SMT-LIB demonstrate that our method is not a sufficiently strong decision procedure by itself but a valuable heuristic to use within a portfolio of techniques.
Type de document :
Communication dans un congrès
Clare Dixon; Marcelo Finger. FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. Springer, 10483, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-319-66167-4〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01590899
Contributeur : Thomas Sturm <>
Soumis le : jeudi 30 novembre 2017 - 13:23:51
Dernière modification le : mercredi 12 septembre 2018 - 01:27:04

Fichier

10.1007-978-3-319-66167-4_11.p...
Accord explicite pour ce dépôt

Identifiants

Citation

Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Vu. Subtropical Satisfiability. Clare Dixon; Marcelo Finger. FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. Springer, 10483, Lecture Notes in Artificial Intelligence. 〈10.1007/978-3-319-66167-4〉. 〈hal-01590899v2〉

Partager

Métriques

Consultations de la notice

353

Téléchargements de fichiers

45