Matthew England
Russell Bradford
James H. Davenport
ABSTRACT
When building a cylindrical algebraic decomposition (CAD) savings can be made in the presence of an equational constraint (EC): an equation logically implied by a formula.
The present paper is concerned with how to use multiple ECs, propagating those in the input throughout the projection set. We improve on the approach of McCallum in ISSAC 2001 by using the reduced projection theory to make savings in the lifting phase (both to the polynomials we lift with and the cells lifted over). We demonstrate the benefits with worked examples and a complexity analysis.
- D. Arnon, G.E. Collins, and S. McCallum. Cylindrical algebraic decomposition I: The basic algorithm. SIAM J. of Computing, 13:865--877, 1984. Google Scholar
Digital Library
- S. Basu, R. Pollack, and M.F. Roy. Algorithms in Real Algebraic Geometry. (Volume 10 of Algorithms and Computations in Mathematics). Springer-Verlag, 2006. Google ScholarDigital Library
- R. Bradford, C. Chen, J.H. Davenport, M. England, M. Moreno Maza, and D. Wilson. Truth table invariant cylindrical algebraic decomposition by regular chains. In Computer Algebra in Scientific Computing (LNCS 8660), pages 44--58. Springer, 2014.Google ScholarCross Ref
- R. Bradford, J.H. Davenport, M. England, S. McCallum, and D. Wilson. Cylindrical algebraic decompositions for boolean combinations. In Proc. ISSAC '13, pages 125--132. ACM, 2013. Google ScholarDigital Library
- R. Bradford, J.H. Davenport, M. England, S. McCallum, and D. Wilson. Truth table invariant cylindrical algebraic decomposition. Submitted for Publication. Preprint:textttarXiv:1401.0645, 2015.Google Scholar
- R. Bradford, J.H. Davenport, M. England, and D. Wilson. Optimising problem formulations for cylindrical algebraic decomposition. In Intelligent Computer Mathematics (LNCS 7961), pages 19--34. Springer Berlin Heidelberg, 2013. Google ScholarDigital Library
- C.W. Brown. QEPCAD B: A program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin, 37(4):97--108, 2003. Google ScholarDigital Library
- C.W. Brown. Constructing a single open cell in a cylindrical algebraic decomposition. In Proc. ISSAC '13, pages 133--140. ACM, 2013. Google ScholarDigital Library
- C.W. Brown, M. El Kahoui, D. Novotni, and A. Weber. Algorithmic methods for investigating equilibria in epidemic modelling. J. Symbolic Computation, 41:1157--1173, 2006.Google ScholarCross Ref
- C.W. Brown and S. McCallum. On using bi-equational constraints in CAD construction. In Proc. ISSAC '05, pages 76--83. ACM, 2005. Google ScholarDigital Library
- C. Chen, M. Moreno Maza, B. Xia, and L. Yang. Computing cylindrical algebraic decomposition via triangular decomposition. In Proc. ISSAC '09, pages 95--102. ACM, 2009. Google ScholarDigital Library
- G.E. Collins. Quantifier elimination by cylindrical algebraic decomposition -- 20 years of progress. In Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 8--23. Springer-Verlag, 1998.Google ScholarCross Ref
- J.H. Davenport, R. Bradford, M. England, and D. Wilson. Program verification in the presence of complex numbers, functions with branch cuts etc. In Proc. SYNASC '12, pages 83--88. IEEE, 2012. Google ScholarDigital Library
- J.H. Davenport and J. Heintz. Real quantifier elimination is doubly exponential. J. Symbolic Computation, 5(1--2):29--35, 1988. Google ScholarDigital Library
- A. Dolzmann, A. Seidl, and T. Sturm. Efficient projection orders for CAD. In Proc. ISSAC '04, pages 111--118. ACM, 2004. Google ScholarDigital Library
- M. England, R. Bradford, C. Chen, J.H. Davenport, M. Moreno Maza, and D. Wilson. Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In Intelligent Computer Mathematics (LNAI 8543), pages 45--60. Springer, 2014.Google ScholarCross Ref
- M. England, D. Wilson, R. Bradford, and J.H. Davenport. Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting. Mathematical Software -- ICMS 2014 (LNCS 8592), pages 458--465. Springer Heidelberg, 2014.Google Scholar
- M. Erascu and H. Hong. Synthesis of optimal numerical algorithms using real quantifier elimination (Case Study: Square root computation). In Proc. ISSAC '14, pages 162--169. ACM, 2014. Google ScholarDigital Library
- I.A. Fotiou, P.A. Parrilo, and M. Morari. Nonlinear parametric optimization using cylindrical algebraic decomposition. In Proc. CDC-ECC '05, pages 3735--3740, 2005.Google ScholarCross Ref
- H. Hong. An improvement of the projection operator in cylindrical algebraic decomposition. In Proc. ISSAC '90, pages 261--264. ACM, 1990. Google ScholarDigital Library
- Z. Huang, M. England, D. Wilson, J.H. Davenport, L. Paulson, and J. Bridge. Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. In Intelligent Computer Mathematics (LNAI 8543), pages 92--107. Springer, 2014.Google ScholarCross Ref
- H. Iwane, H. Yanami, H. Anai, and K. Yokoyama. An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. In Proc. SNC '09, pages 55--64, 2009. Google ScholarDigital Library
- S. McCallum. An improved projection operation for cylindrical algebraic decomposition. In Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 242--268. Springer-Verlag, 1998.Google ScholarCross Ref
- S. McCallum. On projection in CAD-based quantifier elimination with equational constraint. In Proc. ISSAC '99, pages 145--149. ACM, 1999. Google ScholarDigital Library
- S. McCallum. On propagation of equational constraints in CAD-based quantifier elimination. In Proc. ISSAC '01, pages 223--231. ACM, 2001. Google ScholarDigital Library
- S. McCallum and C.W. Brown. On delineability of varieties in CAD-based quantifier elimination with two equational constraints. In Proc. ISSAC '09, pages 71--78. ACM, 2009. Google ScholarDigital Library
- L.C. Paulson. Metitarski: Past and future. In Interactive Theorem Proving (LNCS 7406), 1--10. Springer, 2012.Google ScholarCross Ref
- A. Seidl. Cylindrical decomposition under application-oriented paradigms. PhD Thesis (University of Passau, Germany), 2006.Google Scholar
- A. Strzeboński. Cylindrical algebraic decomposition using validated numerics. J. Symbolic Computation, 41(9):1021--1038, 2006.Google ScholarCross Ref
- A. Strzeboński. Cylindrical algebraic decomposition using local projections. In Proc. ISSAC '14, pages 389--396. ACM, 2014. Google ScholarDigital Library
- D. Wilson, M. England, J.H. Davenport, and R. Bradford. Using the distribution of cells by dimension in a cylindrical algebraic decomposition. Proc. SYNASC '14, pages 53--60. IEEE, 2014.Google ScholarCross Ref
Index Terms
- Improving the Use of Equational Constraints in Cylindrical Algebraic Decomposition
Recommendations
Truth table invariant cylindrical algebraic decomposition
When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free ...
Cylindrical algebraic decompositions for boolean combinations
ISSAC '13: Proceedings of the 38th International Symposium on Symbolic and Algebraic ComputationThis article makes the key observation that when using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is not always the signs of those polynomials that are of paramount importance but rather the ...
Cylindrical algebraic decomposition with equational constraints
AbstractCylindrical Algebraic Decomposition (CAD) has long been one of the most important algorithms within Symbolic Computation, as a tool to perform quantifier elimination in first order logic over the reals. More recently it is finding ...
Comments