Abstract
Many nonlinear optimisation problems involving systems of multivariate polynomial constraints can be expressed as Quantifier Elimination problems. In this regard, the need to eliminate quantifiers presents itself in many real problems such as in economics, mechanics, and motion planning. We focus on using Cylindrical Algebraic Decomposition and Virtual Term Substitution simultaneously. In this paper, we introduce the state-of-the-art theory behind an implementation of these methods produced in collaboration with Maplesoft.
| Original language | English |
|---|---|
| Pages (from-to) | 41-49 |
| Number of pages | 9 |
| Journal | CEUR Workshop Proceedings |
| Volume | 3273 |
| Publication status | Published - 23 Oct 2022 |
| Event | 6th Satisfiability Checking and Symbolic Computation-Square Workshop, SC-Square 2021 - Virtual, Online, USA United States Duration: 19 Aug 2021 → 20 Aug 2021 |
Bibliographical note
Funding Information:The authors are grateful to Marek Košta and Jürgen Gerhard for correspondence about Appendix A. The first author would like to thank the EPSRC grant number EP/T015713/1 for supporting his research. The second author would like to thank EPSRC and Maplesoft for funding his research studentship. The third author would like to thank the EPSRC grant number EP/T015713/1 and the FWF grant P-34501N for partially supporting his research.
Funding
The authors are grateful to Marek Košta and Jürgen Gerhard for correspondence about Appendix A. The first author would like to thank the EPSRC grant number EP/T015713/1 for supporting his research. The second author would like to thank EPSRC and Maplesoft for funding his research studentship. The third author would like to thank the EPSRC grant number EP/T015713/1 and the FWF grant P-34501N for partially supporting his research.
Keywords
- Cylindrical Algebraic Decomposition
- Equational Constraints
- Quantifier Elimination
- Virtual Term Substitution
ASJC Scopus subject areas
- General Computer Science