Abstract

Cylindrical Algebraic Decomposition (CAD) was the first practical means for doing Real Quantifier Elimination (QE), and is still a major method. Nevertheless, its complexity is inherently doubly exponential in the number of variables. Where applicable, virtual term substitution (VTS) is more effective, turning a QE problem in n variables to one in n-1 variables in one application, and so on. Hence there is scope for hybrid methods: doing VTS where possible then using CAD. This paper describes such a poly-algorithmic implementation, based on the second author's Ph.D. thesis. The version of CAD used is based on a new implementation of Lazard's method, with improvements to handle equational constraints, similar to the equational constraint handling in previous CAD algorithms.

Original languageEnglish
Title of host publicationProceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023
EditorsSorin Stratulat, Mircea Marin, Viorel Negru, Daniela Zaharie
Place of PublicationU. S. A.
PublisherIEEE
Pages44-51
Number of pages8
ISBN (Electronic)9798350394122
ISBN (Print)9798350394139
DOIs
Publication statusE-pub ahead of print - 11 Sept 2023
Event25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023 - Nancy, France
Duration: 11 Sept 202314 Sept 2023

Publication series

NameProceedings - 2023 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023

Conference

Conference25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2023
Country/TerritoryFrance
CityNancy
Period11/09/2314/09/23

Keywords

  • Cylindrical Algebraic Decomposition
  • Quantifier Elimination
  • Virtual Term Substitution

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Computer Science Applications
  • Software
  • Numerical Analysis
  • Computational Mathematics
  • Health Informatics

Cite this