Journal
JOURNAL OF SYMBOLIC COMPUTATION
Volume 100, Issue -, Pages 11-37Publisher
ACADEMIC PRESS LTD- ELSEVIER SCIENCE LTD
DOI: 10.1016/j.jsc.2019.07.018
Keywords
Cylindrical algebraic decomposition; Incrementality; Backtracking; Satisfiability modulo theories
Ask authors/readers for more resources
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. (c) 2019 Elsevier Ltd. All rights reserved.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available