Fully incremental cylindrical algebraic decomposition. (September 2020)

• Record Type: Journal Article
• Authors: Kremer, Gereon; Ábrahám, Erika
• Is Part Of: Journal of symbolic computation. Volume 100(2020)
• Page Start: 11
• Page End: 37
• Publication Date: 2020-09
• Subjects: Cylindrical algebraic decomposition -- Incrementality -- Backtracking -- Satisfiability modulo theories; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2019.07.018
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: 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.