Adapting Real Quantifier Elimination Methods for Conflict Set Computation - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

Adapting Real Quantifier Elimination Methods for Conflict Set Computation

Résumé

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.
Fichier principal
Vignette du fichier
article.pdf (401.15 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01240343 , version 1 (17-12-2015)

Licence

Copyright (Tous droits réservés)

Identifiants

Citer

Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine. Adapting Real Quantifier Elimination Methods for Conflict Set Computation. Frontiers of Combining Systems (FroCoS), 2015, Wroclaw, Poland. pp.151-166, ⟨10.1007/978-3-319-24246-0_10⟩. ⟨hal-01240343⟩
109 Consultations
85 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More