Adapting Real Quantifier Elimination Methods for Conflict Set Computation

Abstract : The satisfiability problem in real closed fields is decidable. In the context of satisfiability modulo theories, the problem restricted to conjunctive sets of literals, that is, sets of polynomial constraints, is of particular importance. One of the central problems is the computation of good explanations of the unsatisfiability of such sets, i.e. obtaining a small subset of the input constraints whose conjunction is already unsatisfiable. We adapt two commonly used real quantifier elimination methods, cylindrical algebraic decomposition and virtual substitution, to provide such conflict sets and demonstrate the performance of our method in practice.
Type de document :
Communication dans un congrès
Carsten Lutz; Silvio Ranise. Frontiers of Combining Systems (FroCoS), 2015, Wroclaw, Poland. Springer, 9322, pp.151-166, 2015, LNCS. 〈http://frocos2015.ii.uni.wroc.pl/〉. 〈10.1007/978-3-319-24246-0_10〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01240343
Contributeur : Pascal Fontaine <>
Soumis le : jeudi 17 décembre 2015 - 23:20:13
Dernière modification le : lundi 20 novembre 2017 - 15:14:02
Document(s) archivé(s) le : samedi 29 avril 2017 - 20:36:43

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Copyright (Tous droits réservés)

Identifiants

Collections

Citation

Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine. Adapting Real Quantifier Elimination Methods for Conflict Set Computation. Carsten Lutz; Silvio Ranise. Frontiers of Combining Systems (FroCoS), 2015, Wroclaw, Poland. Springer, 9322, pp.151-166, 2015, LNCS. 〈http://frocos2015.ii.uni.wroc.pl/〉. 〈10.1007/978-3-319-24246-0_10〉. 〈hal-01240343〉

Partager

Métriques

Consultations de la notice

154

Téléchargements de fichiers

62