An effective implementation of symbolic-numeric cylindrical algebraic decomposition for quantifier elimination

被引：14
|
作者：
Iwane, Hidenao [1 ]
Yanami, Hitoshi [1 ]
Anai, Hirokazu [1 ,3 ]
Yokoyama, Kazuhiro [2 ]
机构：
[1] Fujitsu Labs Ltd, Nakahara Ku, Kawasaki, Kanagawa 2118588, Japan
[2] Rikkyo Univ, Toshima Ku, Tokyo 1718501, Japan
[3] Kyushu Univ, Nishi Ku, Fukuoka 8190395, Japan
来源：
THEORETICAL COMPUTER SCIENCE | 2013年 / 479卷
关键词：
Quantifier elimination; Cylindrical algebraic decomposition; Symbolic-numeric computation; GLOBAL OPTIMIZATION; POLYNOMIALS;
D O I：
10.1016/j.tcs.2012.10.020
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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 symbolic-numeric cylindrical algebraic decomposition (SNCAD) algorithm for QE incorporating several new devices, which we call "quick tests". The simple quick tests are run beforehand to detect an unnecessary procedure that might be skipped without violating the correctness of results and they thus considerably reduce the computing time. The effectiveness of the SNCAD algorithm is examined in a number of experiments including practical engineering problems, which also reveal the quality of the implementation. Experimental results show that our implementation has significantly improved efficiency compared with our previous work. (c) 2012 Elsevier B.V. All rights reserved.
引用
收藏
页码：43 / 69
页数：27
相关论文
共 20 条
  • [1] An Effective Implementation of a Symbolic-Numeric Cylindrical Algebraic Decomposition for Quantifier Elimination
    Iwane, Hidenao
    Yanami, Hitoshi
    Anai, Hirokazu
    Yokoyama, Kazuhiro
    [J]. SNC'09: PROCEEDINGS OF THE 2009 INTERNATIONAL WORKSHOP ON SYMBOLIC-NUMERIC COMPUTATION, 2009, : 55 - 64
  • [2] Construction of Explicit Optimal Value Functions by a Symbolic-Numeric Cylindrical Algebraic Decomposition
    Iwane, Hidenao
    Kira, Akifumi
    Anai, Hirokazu
    [J]. COMPUTER ALGEBRA IN SCIENTIFIC COMPUTING, 2011, 6885 : 239 - +
  • [3] Symbolic-numeric optimization by quantifier elimination : an application to biological kinetic model
    Oii, Shigeo
    Anai, Hirokazu
    Horimoto, Katsuhisa
    [J]. WMSCI 2005: 9TH WORLD MULTI-CONFERENCE ON SYSTEMICS, CYBERNETICS AND INFORMATICS, VOL 8, 2005, : 15 - 20
  • [4] CYLINDRICAL ALGEBRAIC DECOMPOSITION BY QUANTIFIER ELIMINATION
    ARNON, DS
    MCCALLUM, S
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1982, 144 : 215 - 222
  • [5] The Complexity of Quantifier Elimination and Cylindrical Algebraic Decomposition
    Brown, Christopher W.
    Davenport, James H.
    [J]. ISSAC 2007: PROCEEDINGS OF THE 2007 INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND ALGEBRAIC COMPUTATION, 2007, : 54 - 60
  • [6] PARTIAL CYLINDRICAL ALGEBRAIC DECOMPOSITION FOR QUANTIFIER ELIMINATION
    COLLINS, GE
    HONG, H
    [J]. JOURNAL OF SYMBOLIC COMPUTATION, 1991, 12 (03) : 299 - 328
  • [7] Quantifier elimination in applied mechanics problems with cylindrical algebraic decomposition
    Ioakimidis, NI
    [J]. INTERNATIONAL JOURNAL OF SOLIDS AND STRUCTURES, 1997, 34 (30) : 4037 - 4070
  • [8] Quantifier elimination by cylindrical algebraic decomposition based on regular chains
    Chen, Changbo
    Maza, Marc Moreno
    [J]. JOURNAL OF SYMBOLIC COMPUTATION, 2016, 75 : 74 - 93
  • [9] Exact symbolic-numeric computation of planar algebraic curves
    Berberich, Eric
    Emeliyanenko, Pavel
    Kobel, Alexander
    Sagraloff, Michael
    [J]. THEORETICAL COMPUTER SCIENCE, 2013, 491 : 1 - 32
  • [10] On the modular symbolic-numeric implementation of extended Kalman filters
    Sorlie, JA
    [J]. PROCEEDINGS OF THE 1996 IEEE INTERNATIONAL SYMPOSIUM ON COMPUTER-AIDED CONTROL SYSTEM DESIGN, 1996, : 510 - 515
12