Russell Bradford
James H. Davenport
Matthew England
ABSTRACT
This 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 truth values of certain quantifier free formulae involving them. This motivates our definition of a Truth Table Invariant CAD (TTICAD). We generalise the theory of equational constraints to design an algorithm which will efficiently construct a TTICAD for a wide class of problems, producing stronger results than when using equational constraints alone. The algorithm is implemented fully in Maple and we present promising results from experimentation.
- R. Bradford, J.H. Davenport, M. England, and D. Wilson. Optimising Problem Formulation for Cylindrical Algebraic Decomposition. In Press: Proc. CICM '13. Preprint: http://opus.bath.ac.uk/34373.Google Scholar
- C.W. Brown. Simplification of truth-invariant cylindrical algebraic decompositions. Proc. ISSAC '98, pages 295--301, 1998. Google ScholarDigital Library
- C.W. Brown. QEPCAD B: A program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bulletin, 37:4, pages 97--108, 2003. Google ScholarDigital Library
- C.W. Brown. The McCallum projection, lifting, and order-invariance. Technical report, U.S. Naval Academy, Computer Science Department, 2005.Google Scholar
- C.W. Brown and J.H. Davenport. The Complexity of Quantifier Elimination and Cylindrical Algebraic Decomposition. Proc. ISSAC '07, pages 54--60, 2007. Google ScholarDigital Library
- C.W. Brown and S. McCallum. On using bi-equational constraints in CAD construction. Proc. ISSAC '05, pages 76--83, 2005. Google ScholarDigital Library
- B. Buchberger and H. Hong. Speeding-up Quantifier Elimination by Gröbner Bases. RISC Technical Report 91-06, 1991.Google Scholar
- C. Chen, M. Moreno Maza, B. Xia, and L. Yang. Computing Cylindrical Algebraic Decomposition via Triangular Decomposition. Proc. ISSAC '09, pages 95--102, 2009. Google ScholarDigital Library
- G.E. Collins. Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. Proc. 2nd. GI Conference Automata Theory & Formal Languages, pages 134--183, 1975. Google ScholarDigital Library
- G.E. Collins. Quantifier elimination by cylindrical algebraic decomposition -- twenty years of progess. Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 8--23, 1998.Google ScholarCross Ref
- G.E. Collins and H. Hong. Partial Cylindrical Algebraic Decomposition for Quantifier Elimination. J. Symbolic Comp., 12:3, pages 299--328, 1991. Google ScholarDigital Library
- J.H. Davenport, R. Bradford, M. England, and D. Wilson. Program verification in the presence of complex numbers, functions with branch cuts etc. Proc. SYNASC '12, pages 83--88, 2012. Google ScholarDigital Library
- J.H. Davenport and J. Heintz. Real Quantifier Elimination is Doubly Exponential. J. Symbolic Comp., 5:1--2, pages 29--35, 1988. Google ScholarDigital Library
- A. Dolzmann, A. Seidl, and Th. Sturm. Efficient Projection Orders for CAD. Proc. ISSAC '04, pages 111--118, 2004. Google ScholarDigital Library
- M. England. An implementation of CAD utilising McCallum projection in Maple. University of Bath, Dept. Computer Science Technical Report Series, 2013:2. http://opus.bath.ac.uk/33180, 2013.Google Scholar
- H. Hong and M. Safey El Din. Variant quantifier elimination. J. Symbolic. Comp., 47:883--901, 2012. Google ScholarDigital Library
- W. Kahan. Branch Cuts for Complex Elementary Functions. A. Iserles and M.J.D. Powell, editors, Proc. The State of the Art in Numerical Analysis, pages 165--211, 1987.Google Scholar
- S. McCallum. An Improved Projection Operation for Cylindrical Algebraic Decomposition of Three-dimensional Space. J. Symbolic Comp., 5:1--2, pages 141--161, 1988. Google ScholarDigital Library
- S. McCallum. An Improved Projection Operation for Cylindrical Algebraic Decomposition. Quantifier Elimination and Cylindrical Algebraic Decomposition, pages 242--268, 1998.Google ScholarCross Ref
- S. McCallum. On Projection in CAD-Based Quantifier Elimination with Equational Constraints. Proc. ISSAC '99, pages 145--149, 1999. Google ScholarDigital Library
- S. McCallum. On Propagation of Equational Constraints in CAD-Based Quantifier Elimination. Proc. ISSAC '01, pages 223--230, 2001. Google ScholarDigital Library
- N. Phisanbut, R.J. Bradford, and J.H. Davenport. Geometry of Branch Cuts. Communications in Computer Algebra, 44:132--135, 2010. Google ScholarDigital Library
- J.T. Schwartz and M. Sharir. On the "Piano-Movers" Problem: II. General Techniques for Computing Topological Properties of Real Algebraic Manifolds. Adv. Appl. Math., 4:298--351, 1983.Google Scholar
- A. Strzeboński. Cylindrical algebraic decomposition using validated numerics. Journal of Symbolic Computation, 41:9, pages 1021--1038, 2006.Google ScholarCross Ref
- A. Strzeboński. Computation with semialgebraic sets represented by cylindrical algebraic formulas. Proc. ISSAC '10, pages 61--68. ACM, 2010. Google ScholarDigital Library
- D.J. Wilson, R.J. Bradford, and J.H. Davenport. A Repository for CAD Examples. ACM Communications in Computer Algebra, 46:3 pages 67--69, 2012. Google ScholarDigital Library
Index Terms
- Cylindrical algebraic decompositions for boolean combinations
Recommendations
Improving the Use of Equational Constraints in Cylindrical Algebraic Decomposition
ISSAC '15: Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic ComputationWhen 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 ...
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 ...
Open Non-uniform Cylindrical Algebraic Decompositions
ISSAC '15: Proceedings of the 2015 ACM on International Symposium on Symbolic and Algebraic ComputationThis paper introduces the notion of an Open Non-uniform Cylindrical Algebraic Decomposition (NuCAD), and presents an efficient model-based algorithm for constructing an Open NuCAD from an input formula. Using a limited experimental implementation of the ...
Comments