Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition (Extended Abstract of Invited Talk)

Matthew England

doi:10.1007/978-3-031-69070-9_1

Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition (Extended Abstract of Invited Talk)

Matthew England

Research Centre for Computational Science and Mathematical Modelling

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

1 Citation (Scopus)

19 Downloads (Pure)

Abstract

This extended abstract accompanies an invited talk at CASC 2024, which surveys recent developments in Real Quantifier Elimination (QE) and Cylindrical Algebraic Decomposition (CAD). After introducing these concepts we will first consider adaptations of CAD inspired by computational logic, in particular the algorithms which underpin modern SAT solvers. CAD theory has found use in collaboration with these via the Satisfiability Modulo Theory (SMT) paradigm; while the ideas behind SAT/SMT have led to new algorithms for Real QE. Second we will consider the optimisation of CAD through the use of Machine Learning (ML). The choice of CAD variable ordering has become a key case study for the use of ML to tune algorithms in computer algebra. We will also consider how explainable AI techniques might give insight for improved computer algebra software without any reliance on ML in the final code.

Original language	English
Title of host publication	Computer Algebra in Scientific Computation
Editors	François Boulier, Chenqi Mou, Timur M. Sadykov, Evgenii V. Vorozhtsov
Publisher	Springer
Chapter	1
Pages	1-10
Number of pages	10
Volume	14938
ISBN (Electronic)	978-3-031-69070-9
ISBN (Print)	978-3-031-69069-3
DOIs	https://doi.org/10.1007/978-3-031-69070-9_1
Publication status	Published - 21 Aug 2024
Event	26th International Computer Algebra in Scientific Computing - Rennes, France Duration: 2 Sept 2024 → 6 Sept 2024 https://casc-conference.org/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	26th International Computer Algebra in Scientific Computing
Abbreviated title	CASC 2024
Country/Territory	France
City	Rennes
Period	2/09/24 → 6/09/24
Internet address	https://casc-conference.org/

Bibliographical note

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-031-69070-9_1

© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders.

This document is the author’s post-print version, incorporating any revisions agreed during the peer-review process. Some differences between the published version and this version may remain and you are advised to consult the published version if you wish to cite from it.

Funding

The author is currently supported by UKRI EPSRC grant EP/T015748/1: Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition (the DEWCAD Project). Some of the work surveyed was supported by UKRI EPSRC grant EP/R019622/1, Embedding Machine Learning within Quantifier Elimination Procedures; and EU H2020 FET CSA 712689, Satisfiability Checking and Symbolic Computation (the SC Project).

Funders	Funder number
Engineering and Physical Sciences Research Council	EP/T015748/1, EP/R019622/1
Horizon Europe	FET CSA 712689

Keywords

Quantifier elimination
Cylindrical algebraic decomposition
SAT
SMT
Machine learning
Explainable AI

Access to Document

10.1007/978-3-031-69070-9_1

England2024AAMAccepted author manuscript, 1.2 MB

Cite this

England, M. (2024). Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition (Extended Abstract of Invited Talk). In F. Boulier, C. Mou, T. M. Sadykov, & E. V. Vorozhtsov (Eds.), Computer Algebra in Scientific Computation (Vol. 14938, pp. 1-10). (Lecture Notes in Computer Science). Springer . https://doi.org/10.1007/978-3-031-69070-9_1

Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition (Extended Abstract of Invited Talk). / England, Matthew.
Computer Algebra in Scientific Computation . ed. / François Boulier; Chenqi Mou; Timur M. Sadykov; Evgenii V. Vorozhtsov. Vol. 14938 Springer , 2024. p. 1-10 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding › peer-review

England, M 2024, Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition (Extended Abstract of Invited Talk). in F Boulier, C Mou, TM Sadykov & EV Vorozhtsov (eds), Computer Algebra in Scientific Computation . vol. 14938, Lecture Notes in Computer Science, Springer , pp. 1-10, 26th International Computer Algebra in Scientific Computing, Rennes, France, 2/09/24. https://doi.org/10.1007/978-3-031-69070-9_1

@inproceedings{6e6600802ebc4c56aafcafdc3a90eeab,

title = "Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition (Extended Abstract of Invited Talk)",

abstract = "This extended abstract accompanies an invited talk at CASC 2024, which surveys recent developments in Real Quantifier Elimination (QE) and Cylindrical Algebraic Decomposition (CAD). After introducing these concepts we will first consider adaptations of CAD inspired by computational logic, in particular the algorithms which underpin modern SAT solvers. CAD theory has found use in collaboration with these via the Satisfiability Modulo Theory (SMT) paradigm; while the ideas behind SAT/SMT have led to new algorithms for Real QE. Second we will consider the optimisation of CAD through the use of Machine Learning (ML). The choice of CAD variable ordering has become a key case study for the use of ML to tune algorithms in computer algebra. We will also consider how explainable AI techniques might give insight for improved computer algebra software without any reliance on ML in the final code.",

keywords = "Quantifier elimination, Cylindrical algebraic decomposition, SAT, SMT, Machine learning, Explainable AI",

author = "Matthew England",

note = "The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-031-69070-9\_1 {\textcopyright} 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders. This document is the author{\textquoteright}s post-print version, incorporating any revisions agreed during the peer-review process. Some differences between the published version and this version may remain and you are advised to consult the published version if you wish to cite from it. ; 26th International Computer Algebra in Scientific Computing, CASC 2024 ; Conference date: 02-09-2024 Through 06-09-2024",

year = "2024",

month = aug,

day = "21",

doi = "10.1007/978-3-031-69070-9\_1",

language = "English",

isbn = "978-3-031-69069-3",

volume = "14938",

series = "Lecture Notes in Computer Science",

publisher = "Springer ",

pages = "1--10",

editor = "Fran{\c c}ois Boulier and Chenqi Mou and Sadykov, \{Timur M.\} and Vorozhtsov, \{Evgenii V.\}",

booktitle = "Computer Algebra in Scientific Computation",

address = "Switzerland",

url = "https://casc-conference.org/",

}

TY - GEN

T1 - Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition (Extended Abstract of Invited Talk)

AU - England, Matthew

N1 - The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-031-69070-9_1 © 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG. A copy can be downloaded for personal non-commercial research or study, without prior permission or charge. This item cannot be reproduced or quoted extensively from without first obtaining permission in writing from the copyright holder(s). The content must not be changed in any way or sold commercially in any format or medium without the formal permission of the copyright holders. This document is the author’s post-print version, incorporating any revisions agreed during the peer-review process. Some differences between the published version and this version may remain and you are advised to consult the published version if you wish to cite from it.

PY - 2024/8/21

Y1 - 2024/8/21

N2 - This extended abstract accompanies an invited talk at CASC 2024, which surveys recent developments in Real Quantifier Elimination (QE) and Cylindrical Algebraic Decomposition (CAD). After introducing these concepts we will first consider adaptations of CAD inspired by computational logic, in particular the algorithms which underpin modern SAT solvers. CAD theory has found use in collaboration with these via the Satisfiability Modulo Theory (SMT) paradigm; while the ideas behind SAT/SMT have led to new algorithms for Real QE. Second we will consider the optimisation of CAD through the use of Machine Learning (ML). The choice of CAD variable ordering has become a key case study for the use of ML to tune algorithms in computer algebra. We will also consider how explainable AI techniques might give insight for improved computer algebra software without any reliance on ML in the final code.

AB - This extended abstract accompanies an invited talk at CASC 2024, which surveys recent developments in Real Quantifier Elimination (QE) and Cylindrical Algebraic Decomposition (CAD). After introducing these concepts we will first consider adaptations of CAD inspired by computational logic, in particular the algorithms which underpin modern SAT solvers. CAD theory has found use in collaboration with these via the Satisfiability Modulo Theory (SMT) paradigm; while the ideas behind SAT/SMT have led to new algorithms for Real QE. Second we will consider the optimisation of CAD through the use of Machine Learning (ML). The choice of CAD variable ordering has become a key case study for the use of ML to tune algorithms in computer algebra. We will also consider how explainable AI techniques might give insight for improved computer algebra software without any reliance on ML in the final code.

KW - Quantifier elimination

KW - Cylindrical algebraic decomposition

KW - SAT

KW - SMT

KW - Machine learning

KW - Explainable AI

UR - https://www.scopus.com/pages/publications/85202601332

U2 - 10.1007/978-3-031-69070-9_1

DO - 10.1007/978-3-031-69070-9_1

M3 - Conference proceeding

SN - 978-3-031-69069-3

VL - 14938

T3 - Lecture Notes in Computer Science

SP - 1

EP - 10

BT - Computer Algebra in Scientific Computation

A2 - Boulier, François

A2 - Mou, Chenqi

A2 - Sadykov, Timur M.

A2 - Vorozhtsov, Evgenii V.

PB - Springer

T2 - 26th International Computer Algebra in Scientific Computing

Y2 - 2 September 2024 through 6 September 2024

ER -

Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition (Extended Abstract of Invited Talk)

Abstract

Publication series

Conference

Bibliographical note

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this