Hidenao Iwane
ABSTRACT
Recently quantifier elimination (QE) has been of great interest in many fields of science and engineering. In this paper an effective symbolic-numeric cylindrical algebraic decomposition (SNCAD) algorithm and its variant specially designed for QE are proposed based on the authors' previous work and our implementation of those is reported. Based on analysing experimental performances, we are improving our design/synthesis of the SNCAD for its practical realization with existing efficient computational techniques and several newly introduced ones. The practicality of the SNCAD is now examined by a number of experimental results including practical engineering problems, which also reveals the quality of the implementation.
- H. Anai and S. Hara. Fixed-structure robust controller synthesis based on sign definite condition by a special quantifier elimination. In Proceedings of American Control Conference 2000, pp. 1312--1316, 2000.Google Scholar
Cross Ref
- H. Anai and P. A. Parrilo. Convex quantifier elimination for semidefinite programming. In Proceedings of the 6th International Workshop on Computer Algebra in Scientific Computing 2003. pp. 3--11, 2003.Google Scholar
- H. Anai, H. Yanami, K. Sakabe, and S. Hara. Fixed-structure robust controller synthesis based on symbolic-numeric computation: design algorithms with a CACSD toolbox (invited paper). In Proceedings of CCA/ISIC/CACSD 2004 (Taipei, Taiwan), pp. 1540--1545, 2004.Google ScholarCross Ref
- H. Anai and K. Yokoyama. Numerical cylindrical algebraic decomposition with certificated reconstruction. In Proceedings of 11th GAMM - IMACS International Symposium on Scientific Computing, Computer Arithmetic, and Validated Numerics (Fukuoka, Japan), pp. 31, 2004.Google Scholar
- H. Anai and K. Yokoyama. Cylindrical algebraic decomposition via numerical computation with validated symbolic reconstruction. In Proceedings of the A3L 2005, pp. 25--30, 2005.Google Scholar
- C. W. Brown. Solution formula construction for truth-invariant CADs. PhD thesis, 1999. Google ScholarDigital Library
- C. W. Brown. Improved projection for cylindrical algebraic decomposition. J. Symb. Comput., 32(5):447--465, 2001. 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, Dec. 2003. Google ScholarDigital Library
- B. Caviness and J. Johnson, editors. Quantifier elimination and cylindrical algebraic decomposition. Texts and monographs in symbolic computation. Springer-Verlag, 1998.Google Scholar
- G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition - preliminary report. SIGSAM Bull., 8(3):80--90, 1974. Google ScholarDigital Library
- G. E. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput., 12(3):299--328, Sep. 1991. Google ScholarDigital Library
- G. E. Collins, J. R. Johnson, and W. Krandick. Interval arithmetic in cylindrical algebraic decomposition. J. Symb. Comput., 34(2):145--157, 2002. Google ScholarDigital Library
- A. Dolzmann, T. Sturm, and V. Weispfenning. Real quantifier elimination in practice. In B. H. Matzat, G.-M. Greuel, and G. Hiss, editors, Algorithmic Algebra and Number Theory, pp. 221--247. Springer, Berlin, 1998.Google Scholar
- A. Dolzmann, A. Seidl, and T. Sturm. Efficient projection orders for CAD. In Proceedings of ISSAC 2004, pp. 111--118, 2004. Google ScholarDigital Library
- J. D. Dora, C. Dicrescenzo, and D. Duval. About a new method for computing in algebraic number fields. In B. F. Caviness, editor, European Conference on Computer Algebra (2), Lecture Notes in Computer Science, 204:289--290. Springer, 1985. Google ScholarDigital Library
- D. Duval. Algebraic numbers: an example of dynamic evaluation. J. Symb. Comput., 18:429--445, 1994. Google ScholarDigital Library
- J.-C. Faugère, G. Moroz, F. Rouillier and M. S. El Din. Classification of the perspective-three-point problem, discriminant variety and real solving polynomial systems of inequalities. In Proceedings of ISSAC 2008, pp. 79--86, 2008. Google ScholarDigital Library
- L. González-Vega. Applying quantifier elimination to the Birkhoff interpolation problem. J. Symb. Comput., 22(1):83--103 1966. Google ScholarDigital Library
- L. González-Vega. A combinatorial algorithm solving some quantifier elimination problems. In B. F. Caviness and J. R. Johnson, editors, Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation, pp. 365--375. Springer, Wien, New York, 1998.Google Scholar
- H. Hong. Efficient method for analyzing topology of plane real algebraic curves. In the International Symposium on Symbolic and Algebraic Computation (ISSAC 93), pp. 264--274, 1993.Google Scholar
- H. Hong. Quantifier elimination for formulas constrained by quadratic equations. In Manuel Bronstein, editor, Proceedings of the International Symposium on Symbolic and Algebraic Computation (ISSAC 93), pp. 264--274, Kiev, Ukraine, ACM, ACM Press, Jul. 1993. Google ScholarDigital Library
- R. Krawczyk. Newton-Algorithmen zur Bcstimmung yon Nullstellen mit Fehlerschranken. Computing, 4:187-201, 1969.Google ScholarCross Ref
- J. B. Lasserre. Global optimization with polynomials and the problems of moments. SIAM Journal on Optimization, 11:796--817, 2001. Google ScholarDigital Library
- R. Loos and V. Weispfenning. Applying linear quantifier elimination. The Computer Journal, Special issue on computational quantifier elimination, 36(5):450--462, 1993.Google Scholar
- R. E. Moore. A test for existence of solutions to nonlinear systems. SlAM J. Numer. Anal., 14(4):611--615, Sep. 1977.Google ScholarCross Ref
- R. E. Moore, and S. T. Jones. Safe starting regions for iterative methods. SIAM J. Numer. Anal., 14(6):1051--1065, Dec. 1977.Google ScholarCross Ref
- P. Parrilo, and S. Lall. Semidefinite Programming Relaxation and Algebraic Optimization in Control. Mini-course on Polynomial Equations and Inequalities I and II, MTNS, 2006.Google Scholar
- S. Ratschan. Approximate quantified constraint solving by cylindrical box decomposition. Reliable Computing, 8(1):21--42, 2002.Google ScholarCross Ref
- S. M. Rump. Algebraic computation, numerical computation and verified inclusions. In R. Janssen, editor, Trends in Computer Algebra, Lecture Notes in Computer Science, 296:177--197. Springer-Verlag, New York, 1988. Google ScholarDigital Library
- S. M. Rump. Computer-assisted proofs and self-validating methods. In B. Einarsson, editor, Accuracy and Reliability in Scientific Computing, Vol. 18 of Software, Environments, Tools, Chap. 10, pp. 195--240. Society for Industrial and Applied Mathematics, Philadelphia, PA, 2005.Google Scholar
- A. W. Strzeboński. A real polynomial decision algorithm using arbitrary-precision floating point arithmetic. Reliable Computing, 5(3):337--346, 1999.Google ScholarCross Ref
- A. W. Strzeboński. Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput., 41(9):1021--1038, 2006.Google ScholarCross Ref
- T. Sturm and V. Weispfenning. Rounding and blending of solids by a real elimination method. Proceedings of the 15th IMACS World Congress on Scientific Computation, Modelling, and Applied Mathematics (IMACS 97), 2:727--732, Aug. 1997.Google Scholar
- V. Weispfenning. The complexity of linear problems in fields. J. Symb. Comput., 5(1-2):3--27, Feb.-Apr. 1988. Google ScholarDigital Library
- V. Weispfenning. Simulation and optimization by quantifier elimination. J. Symb. Comput., 24:208, 1997. Google ScholarDigital Library
- V. Weispfenning. Quantifier elimination for real algebra - the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing, 8(2):85--101, Feb. 1997.Google ScholarCross Ref
- H. Yanami and H. Anai. Development of SyNRAC - formula description and new functions. In Proceedings of International Workshop on Computer Algebra Systems and their Applications (CASA) 2004: ICCS 2004, LNCS 3039, pp. 286--294. Springer, 2004.Google ScholarCross Ref
- H. Yanami and H. Anai. The Maple package SyNRAC and its application to robust control design. Future Generation Comp. Syst., 23(5):721--726, 2007. Google ScholarDigital Library
Index Terms
- An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
Recommendations
Quantifier elimination for a class of exponential polynomial formulas
Quantifier elimination is a foundational issue in the field of algebraic and logic computation. In first-order logic, every formula is well composed of atomic formulas by negation, conjunction, disjunction, and introducing quantifiers. It is often made ...
An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination
With many applications in engineering and scientific fields, quantifier elimination (QE) has received increasing attention. Cylindrical algebraic decomposition (CAD) is used as a basis for a general QE algorithm. In this paper we present an effective ...
An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for optimization problems
SNC '11: Proceedings of the 2011 International Workshop on Symbolic-Numeric ComputationWith many applications in engineering and in scientific fields, quantifier elimination (QE) has been attracting more attention these days. Cylindrical algebraic decomposition (CAD) is used as a basis for a general QE algorithm. We propose an effective ...
Comments