Papers

Peer-reviewed
Apr, 2013

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

THEORETICAL COMPUTER SCIENCE
  • Hidenao Iwane
  • ,
  • Hitoshi Yanami
  • ,
  • Hirokazu Anai
  • ,
  • Kazuhiro Yokoyama

Volume
479
Number
1
First page
43
Last page
69
Language
English
Publishing type
Research paper (scientific journal)
DOI
10.1016/j.tcs.2012.10.020
Publisher
ELSEVIER SCIENCE BV

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.

Link information
DOI
https://doi.org/10.1016/j.tcs.2012.10.020
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000317320400004&DestApp=WOS_CPL
ID information
  • DOI : 10.1016/j.tcs.2012.10.020
  • ISSN : 0304-3975
  • eISSN : 1879-2294
  • Web of Science ID : WOS:000317320400004

Export
BibTeX RIS