×

zbMATH — the first resource for mathematics

Truth table invariant cylindrical algebraic decomposition. (English) Zbl 1351.68314
Summary: 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 formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD).
In [“Cylindrical algebraic decompositions for Boolean combinations”, in: Proceedings of the 38th international symposium on symbolic and algebraic computation, ISSAC’13. New York, NY: Association for Computing Machinery (ACM). 125–132 (2013; doi:10.1145/2465506.2465516)] the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum’s theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint.
The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.

MSC:
68W30 Symbolic computation and algebraic computation
14P99 Real algebraic and real-analytic geometry
14Q99 Computational aspects in algebraic geometry
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Arnon, D., A cluster-based cylindrical algebraic decomposition algorithm, J. Symb. Comput., 5, 1-2, 189-212, (1988) · Zbl 0648.68056
[2] Arnon, D.; Collins, G.; McCallum, S., Cylindrical algebraic decomposition I: the basic algorithm, SIAM J. Comput., 13, 865-877, (1984) · Zbl 0562.14001
[3] Arnon, D.; Collins, G.; McCallum, S., Cylindrical algebraic decomposition II: an adjacency algorithm for the plane, SIAM J. Comput., 13, 878-889, (1984) · Zbl 0562.14001
[4] Arnon, D.; Collins, G.; McCallum, S., An adjacency algorithm for cylindrical algebraic decompositions of three-dimensional space, J. Symb. Comput., 5, 1/2, 163-187, (1988) · Zbl 0648.68055
[5] Basu, S.; Pollack, R.; Roy, M., On the combinatorial and algebraic complexity of quantifier elimination, J. ACM, 43, 6, 1002-1045, (1996) · Zbl 0885.68070
[6] Bradford, R.; Chen, C.; Davenport, J. H.; England, M.; Moreno Maza, M.; Wilson, D., Truth table invariant cylindrical algebraic decomposition by regular chains, (CASC ’14, (2014), Springer), 44-58 · Zbl 1350.68293
[7] Bradford, R.; Davenport, J. H., Towards better simplification of elementary functions, (ISSAC ’02, (2002), ACM), 16-22 · Zbl 1072.68651
[8] Bradford, R.; Davenport, J. H.; England, M.; McCallum, S.; Wilson, D., Cylindrical algebraic decompositions for Boolean combinations, (ISSAC ’13, (2013), ACM), 125-132 · Zbl 1359.68327
[9] Bradford, R.; Davenport, J. H.; England, M.; Wilson, D., Optimising problem formulations for cylindrical algebraic decomposition, (Intelligent Computer Mathematics, LNAI, vol. 7961, (2013), Springer Berlin, Heidelberg), 19-34 · Zbl 1390.68775
[10] Brown, C., Simplification of truth-invariant cylindrical algebraic decompositions, (ISSAC ’98, (1998), ACM), 295-301 · Zbl 0918.68058
[11] Brown, C., Improved projection for cylindrical algebraic decomposition, J. Symb. Comput., 32, 5, 447-465, (2001) · Zbl 0981.68186
[12] Brown, C., A program for computing with semi-algebraic sets using cads, ACM SIGSAM Bull., 37, 4, 97-108, (2003) · Zbl 1083.68148
[13] Brown, C., Companion to the tutorial, cylindrical algebraic decomposition, (ISSAC ’04, (2004))
[14] Brown, C., The mccallum projection, lifting, and order-invariance, (2005), U.S. Naval Academy, Computer Science Department, Tech. Rep
[15] Brown, C., Constructing a single open cell in a cylindrical algebraic decomposition, (ISSAC ’13, (2013), ACM), 133-140 · Zbl 1360.68924
[16] Brown, C.; Davenport, J. H., The complexity of quantifier elimination and cylindrical algebraic decomposition, (ISSAC ’07, (2007), ACM), 54-60 · Zbl 1190.68028
[17] Brown, C.; Kahoui, M. E.; Novotni, D.; Weber, A., Algorithmic methods for investigating equilibria in epidemic modelling, J. Symb. Comput., 41, 1157-1173, (2006) · Zbl 1120.92034
[18] Brown, C.; McCallum, S., On using bi-equational constraints in CAD construction, (ISSAC ’05, (2005), ACM), 76-83 · Zbl 1360.68925
[19] Buchberger, B.; Hong, H., Speeding up quantifier elimination by Gröbner bases, (1991), RISC, Johannes Kepler University, Tech. Rep. 91-06
[20] Chen, C.; Davenport, J. H.; May, J.; Moreno Maza, M.; Xia, B.; Xiao, R.; Xie, Y., User interface design for geometrical decomposition algorithms in Maple, (Proc. Mathematical User-Interface, (2009)), 12 pp
[21] Chen, C.; Moreno Maza, M.; Xia, B.; Yang, L., Computing cylindrical algebraic decomposition via triangular decomposition, (ISSAC ’09, (2009), ACM), 95-102 · Zbl 1237.14068
[22] Collins, G., Quantifier elimination by cylindrical algebraic decomposition - 20 years of progress, (Caviness, B.; Johnson, J., Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts & Monographs in Symbolic Computation, (1998), Springer-Verlag), 8-23 · Zbl 0900.03053
[23] Collins, G.; Hong, H., Partial cylindrical algebraic decomposition for quantifier elimination, J. Symb. Comput., 12, 299-328, (1991) · Zbl 0754.68063
[24] Davenport, J. H.; Bradford, R.; England, M.; Wilson, D., Program verification in the presence of complex numbers, functions with branch cuts etc, (SYNASC ’12, (2012), IEEE), 83-88
[25] Davenport, J. H.; Heintz, J., Real quantifier elimination is doubly exponential, J. Symb. Comput., 5, 1-2, 29-35, (1988) · Zbl 0663.03015
[26] Dolzmann, A.; Seidl, A.; Sturm, T., Efficient projection orders for CAD, (ISSAC ’04, (2004), ACM), 111-118 · Zbl 1134.68575
[27] England, M.; Bradford, R.; Chen, C.; Davenport, J. H.; Moreno Maza, M.; Wilson, D., Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition, (Intelligent Computer Mathematics, LNAI, vol. 8543, (2014), Springer International), 45-60 · Zbl 1304.68223
[28] England, M.; Bradford, R.; Davenport, J. H., Improving the use of equational constraints in cylindrical algebraic decomposition, (ISSAC ’15, (2015), ACM), 165-172 · Zbl 1346.68283
[29] England, M.; Bradford, R.; Davenport, J. H.; Wilson, D., Understanding branch cuts of expressions, (Intelligent Computer Mathematics, LNAI, vol. 7961, (2013), Springer Berlin, Heidelberg), 136-151 · Zbl 1390.68777
[30] England, M.; Bradford, R.; Davenport, J. H.; Wilson, D., Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition, (Mathematical Software - ICMS 2014, LNCS, vol. 8592, (2014), Springer Heidelberg), 450-457 · Zbl 1350.68294
[31] England, M.; Cheb-Terrab, E.; Bradford, R.; Davenport, J. H.; Wilson, D., Branch cuts in {\scmaple 17}, ACM CCA, 187, 1, 24-27, (2014) · Zbl 1369.68358
[32] England, M.; Wilson, D.; Bradford, R.; Davenport, J. H., Using the regular chains library to build cylindrical algebraic decompositions by projecting and lifting, (Mathematical Software - ICMS 2014, LNCS, vol. 8592, (2014), Springer Heidelberg), 458-465 · Zbl 1437.14008
[33] Erascu, M.; Hong, H., Synthesis of optimal numerical algorithms using real quantifier elimination (case study: square root computation), (ISSAC ’14, (2014), ACM), 162-169 · Zbl 1325.68276
[34] Fotiou, I.; Parrilo, P.; Morari, M., Nonlinear parametric optimization using cylindrical algebraic decomposition, (CDC-ECC ’05, (2005)), 3735-3740
[35] Han, J.; Dai, L.; Xia, B., Constructing fewer open cells by gcd computation in CAD projection, (ISSAC ’14, (2014), ACM), 240-247 · Zbl 1325.68286
[36] Hong, H., An improvement of the projection operator in cylindrical algebraic decomposition, (ISSAC ’90, (1990), ACM), 261-264
[37] Huang, Z.; England, M.; Wilson, D.; Davenport, J. H.; Paulson, L.; Bridge, J., Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition, (Intelligent Computer Mathematics, LNAI, vol. 8543, (2014), Springer International), 92-107 · Zbl 1304.68224
[38] Iwane, H.; Yanami, H.; Anai, H.; Yokoyama, K., An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination, (SNC ’09, (2009)), 55-64 · Zbl 1356.68282
[39] Jovanovic, D.; de Moura, L., Solving non-linear arithmetic, (IJCAR, LNCS, vol. 7364, (2012), Springer), 339-354 · Zbl 1358.68257
[40] Kahan, W., Branch cuts for complex elementary functions, (Iserles, A.; Powell, M., Proc. State of Art in Numerical Analysis, (1987), Clarendon Press), 165-211 · Zbl 0615.65014
[41] Lazard, D., An improved projection for cylindrical algebraic decomposition, (Algebraic Geometry and Its Applications: Collections of Papers from Abhyankar’s 60th Birthday Conference, (1994), Springer Berlin), 467-476 · Zbl 0822.68118
[42] McCallum, S., An improved projection operation for cylindrical algebraic decomposition, (1985), Univ. Wisconsin-Madison, PhD thesis (Computer Sciences Tech. Rep. 578)
[43] McCallum, S., An improved projection operation for cylindrical algebraic decomposition of three-dimensional space, J. Symb. Comput., 5, 1-2, 141-161, (1988) · Zbl 0648.68054
[44] McCallum, S., An improved projection operation for cylindrical algebraic decomposition, (Caviness, B.; Johnson, J., Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts & Monographs in Symbolic Computation, (1998), Springer-Verlag), 242-268 · Zbl 0900.68279
[45] McCallum, S., On projection in CAD-based quantifier elimination with equational constraint, (ISSAC ’99, (1999), ACM), 145-149
[46] McCallum, S., On propagation of equational constraints in CAD-based quantifier elimination, (ISSAC ’01, (2001), ACM), 223-231 · Zbl 1356.68287
[47] Paulson, L., Metitarski: past and future, (Interactive Theorem Proving, LNCS, vol. 7406, (2012), Springer), 1-10 · Zbl 1360.68765
[48] Phisanbut, N.; Bradford, R.; Davenport, J. H., Geometry of branch cuts, ACM CCA, 44, 3, 132-135, (2010) · Zbl 1305.68367
[49] Schwartz, J.; Sharir, M., On the “piano-movers” problem: II. general techniques for computing topological properties of real algebraic manifolds, Adv. Appl. Math., 4, 298-351, (1983) · Zbl 0554.51008
[50] Seidl, A.; Sturm, T., A generic projection operator for partial cylindrical algebraic decomposition, (ISSAC ’03, (2003), ACM), 240-247 · Zbl 1072.68696
[51] Strzeboński, A., Cylindrical algebraic decomposition using validated numerics, J. Symb. Comput., 41, 9, 1021-1038, (2006) · Zbl 1124.68123
[52] Strzeboński, A., Computation with semialgebraic sets represented by cylindrical algebraic formulas, (ISSAC ’10, (2010), ACM), 61-68 · Zbl 1321.68543
[53] Strzeboński, A., Cylindrical algebraic decomposition using local projections, (ISSAC ’14, (2014), ACM), 389-396 · Zbl 1325.68302
[54] Wilson, D.; Bradford, R.; Davenport, J. H., A repository for CAD examples, ACM CCA, 46, 3, 67-69, (2012) · Zbl 1322.68294
[55] Wilson, D.; Bradford, R.; Davenport, J. H., Speeding up cylindrical algebraic decomposition by Gröbner bases, (Intelligent Computer Mathematics, LNAI, vol. 7362, (2012), Springer), 280-294 · Zbl 1360.68959
[56] Wilson, D.; Bradford, R.; Davenport, J. H.; England, M., Cylindrical algebraic sub-decompositions, Math. Comput. Sci., 8, 263-288, (2014) · Zbl 1309.68232
[57] Wilson, D.; Davenport, J. H.; England, M.; Bradford, R., A “piano movers” problem reformulated, (SYNASC ’13, (2013), IEEE), 53-60
[58] Wilson, D.; England, M.; Bradford, R.; Davenport, J. H., Using the distribution of cells by dimension in a cylindrical algebraic decomposition, (SYNASC ’14, (2014), IEEE), 53-60
[59] Yanami, H.; Anai, H., Development of synrac, (Proc. 6th Intl. Conf. on Computational Science: Part II, ICCS ’06, LNCS, vol. 3992, (2006)), 462-469 · Zbl 1155.68599
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.