The Potential and Challenges of CAD with Equational Constraints for SC-Square
arXiv:1711.00312 · doi:10.1007/978-3-319-72453-9_22
Abstract
Cylindrical algebraic decomposition (CAD) is a core algorithm within Symbolic Computation, particularly for quantifier elimination over the reals and polynomial systems solving more generally. It is now finding increased application as a decision procedure for Satisfiability Modulo Theories (SMT) solvers when working with non-linear real arithmetic. We discuss the potentials from increased focus on the logical structure of the input brought by the SMT applications and SC-Square project, particularly the presence of equational constraints. We also highlight the challenges for exploiting these: primitivity restrictions, well-orientedness questions, and the prospect of incrementality.
arXiv commentAccepted into proceedings of MACIS 2017
References in corpus (6)
- Truth Table Invariant Cylindrical Algebraic Decomposition
- Cylindrical Algebraic Decompositions for Boolean Combinations
- Satisfiability Checking meets Symbolic Computation (Project Paper)
- Improving the use of equational constraints in cylindrical algebraic decomposition
- The complexity of cylindrical algebraic decomposition with respect to polynomial degree
- Need Polynomial Systems be Doubly-exponential?