Fully incremental cylindrical algebraic decomposition

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.