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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [27 references]  Display  Hide  Download

https://hal.inria.fr/hal-01240343
Contributor : Pascal Fontaine <>
Submitted on : Thursday, December 17, 2015 - 11:20:13 PM
Last modification on : Tuesday, February 19, 2019 - 3:40:03 PM
Long-term archiving on : Saturday, April 29, 2017 - 8:36:43 PM

File

article.pdf
Files produced by the author(s)

Licence


Copyright

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

251

Files downloads

184