Fully incremental cylindrical algebraic decomposition
| Autor: | Erika Ábrahám, Gereon Kremer |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Algebra and Number Theory
Backtracking Computation 010102 general mathematics 010103 numerical & computational mathematics Solver Data structure 01 natural sciences Satisfiability Cylindrical algebraic decomposition Algebra Computational Mathematics Satisfiability modulo theories ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION Quantifier elimination 0101 mathematics Mathematics |
| Zdroj: | Journal of Symbolic Computation. 100:11-37 |
| ISSN: | 0747-7171 |
| DOI: | 10.1016/j.jsc.2019.07.018 |
| Popis: | Collins introduced the cylindrical algebraic decomposition method for eliminating quantifiers in real arithmetic formulas. In our work we use this method for satisfiability checking in satisfiability modulo theories solver technologies, and tune it by trying to avoid some computation steps that are needed for quantifier elimination but not for satisfiability checking. We further propose novel data structures and adapt the method to work incrementally and to support backtracking. We verify the effectiveness experimentally by comparing different versions of the cylindrical algebraic decomposition used within a state-of-the-art satisfiability modulo theories solver. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect