New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis

Tereso del Río; Matthew England

doi:10.1007/978-3-031-14788-3_17

New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis

Tereso del Río, Matthew England

Research Centre for Computational Science and Mathematical Modelling

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

7 Citations (Scopus)

58 Downloads (Pure)

Abstract

It is well known that the variable ordering can be critical to the efficiency or even tractability of the cylindrical algebraic decomposition (CAD) algorithm. We propose new heuristics inspired by complexity analysis of CAD to choose the variable ordering. These heuristics are evaluated against existing heuristics with experiments on the SMT-LIB benchmarks using both existing performance metrics and a new metric we propose for the problem at hand. The best of these new heuristics chooses orderings that lead to timings on average 17% slower than the virtual-best: an improvement compared to the prior state-of-the-art which achieved timings 25% slower.

Original language	English
Title of host publication	Computer Algebra in Scientific Computing CASC 2022
Editors	François Boulier, Matthew England, Timur M. Sadykov, Evgenii V. Vorozhtsov
Publisher	Springer International Publishing
Pages	300–317
Number of pages	18
Volume	13366
ISBN (Electronic)	978-3-031-14788-3
ISBN (Print)	978-3-031-14787-6
DOIs	https://doi.org/10.1007/978-3-031-14788-3_17
Publication status	Published - 11 Aug 2022
Event	International Workshop on Computer Algebra in Scientific Computing - Gebze, Turkey Duration: 22 Aug 2022 → 26 Aug 2022 https://www.casc-conference.org/

Publication series

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

Workshop

Workshop	International Workshop on Computer Algebra in Scientific Computing
Abbreviated title	CASC 2022
Country/Territory	Turkey
City	Gebze
Period	22/08/22 → 26/08/22
Internet address	https://www.casc-conference.org/

Bibliographical note

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

Copyright © and Moral Rights are retained by the author(s) and/ or other copyright owners. 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.

The research of the first author is supported financially from a scholarship of Coventry University. The research of the second author is supported by EPSRC Grant EP/T015748/1, Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition (the DEWCAD Project).

Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Keywords

Symbolic Computation
Cylindrical Algebraic Decomposition
Heuristic
Quantifier elimination

Access to Document

10.1007/978-3-031-14788-3_17

Post-PrintAccepted author manuscript, 818 KB

Cite this

del Río, T., & England, M. (2022). New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis. In F. Boulier, M. England, T. M. Sadykov, & E. V. Vorozhtsov (Eds.), Computer Algebra in Scientific Computing CASC 2022 (Vol. 13366, pp. 300–317). (Lecture Notes in Computer Science; Vol. 13366). Springer International Publishing. https://doi.org/10.1007/978-3-031-14788-3_17

New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis. / del Río, Tereso ; England, Matthew.
Computer Algebra in Scientific Computing CASC 2022. ed. / François Boulier; Matthew England; Timur M. Sadykov; Evgenii V. Vorozhtsov. Vol. 13366 Springer International Publishing, 2022. p. 300–317 (Lecture Notes in Computer Science; Vol. 13366).

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

del Río, T & England, M 2022, New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis. in F Boulier, M England, TM Sadykov & EV Vorozhtsov (eds), Computer Algebra in Scientific Computing CASC 2022. vol. 13366, Lecture Notes in Computer Science, vol. 13366, Springer International Publishing, pp. 300–317, International Workshop on Computer Algebra in Scientific Computing, Gebze, Turkey, 22/08/22. https://doi.org/10.1007/978-3-031-14788-3_17

del Río T , England M. New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis. In Boulier F, England M, Sadykov TM, Vorozhtsov EV, editors, Computer Algebra in Scientific Computing CASC 2022. Vol. 13366. Springer International Publishing. 2022. p. 300–317. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-14788-3_17

del Río, Tereso ; England, Matthew. / New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis. Computer Algebra in Scientific Computing CASC 2022. editor / François Boulier ; Matthew England ; Timur M. Sadykov ; Evgenii V. Vorozhtsov. Vol. 13366 Springer International Publishing, 2022. pp. 300–317 (Lecture Notes in Computer Science).

@inproceedings{f236eee03f11452fa2d3074b9c45fd0e,

title = "New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis",

abstract = " It is well known that the variable ordering can be critical to the efficiency or even tractability of the cylindrical algebraic decomposition (CAD) algorithm. We propose new heuristics inspired by complexity analysis of CAD to choose the variable ordering. These heuristics are evaluated against existing heuristics with experiments on the SMT-LIB benchmarks using both existing performance metrics and a new metric we propose for the problem at hand. The best of these new heuristics chooses orderings that lead to timings on average 17% slower than the virtual-best: an improvement compared to the prior state-of-the-art which achieved timings 25% slower. ",

keywords = "Symbolic Computation, Cylindrical Algebraic Decomposition, Heuristic, Quantifier elimination",

author = "{del R{\'i}o}, Tereso and Matthew England",

note = "The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-031-14788-3_17 Copyright {\textcopyright} and Moral Rights are retained by the author(s) and/ or other copyright owners. 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. The research of the first author is supported financially from a scholarship of Coventry University. The research of the second author is supported by EPSRC Grant EP/T015748/1, Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition (the DEWCAD Project). Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; International Workshop on Computer Algebra in Scientific Computing, CASC 2022 ; Conference date: 22-08-2022 Through 26-08-2022",

year = "2022",

month = aug,

day = "11",

doi = "10.1007/978-3-031-14788-3_17",

language = "English",

isbn = "978-3-031-14787-6",

volume = "13366",

series = "Lecture Notes in Computer Science",

publisher = "Springer International Publishing",

pages = "300–317",

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

booktitle = "Computer Algebra in Scientific Computing CASC 2022",

address = "United Kingdom",

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

}

TY - GEN

T1 - New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis

AU - del Río, Tereso

AU - England, Matthew

N1 - The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-031-14788-3_17 Copyright © and Moral Rights are retained by the author(s) and/ or other copyright owners. 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. The research of the first author is supported financially from a scholarship of Coventry University. The research of the second author is supported by EPSRC Grant EP/T015748/1, Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition (the DEWCAD Project). Publisher Copyright: © 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.

PY - 2022/8/11

Y1 - 2022/8/11

N2 - It is well known that the variable ordering can be critical to the efficiency or even tractability of the cylindrical algebraic decomposition (CAD) algorithm. We propose new heuristics inspired by complexity analysis of CAD to choose the variable ordering. These heuristics are evaluated against existing heuristics with experiments on the SMT-LIB benchmarks using both existing performance metrics and a new metric we propose for the problem at hand. The best of these new heuristics chooses orderings that lead to timings on average 17% slower than the virtual-best: an improvement compared to the prior state-of-the-art which achieved timings 25% slower.

AB - It is well known that the variable ordering can be critical to the efficiency or even tractability of the cylindrical algebraic decomposition (CAD) algorithm. We propose new heuristics inspired by complexity analysis of CAD to choose the variable ordering. These heuristics are evaluated against existing heuristics with experiments on the SMT-LIB benchmarks using both existing performance metrics and a new metric we propose for the problem at hand. The best of these new heuristics chooses orderings that lead to timings on average 17% slower than the virtual-best: an improvement compared to the prior state-of-the-art which achieved timings 25% slower.

KW - Symbolic Computation

KW - Cylindrical Algebraic Decomposition

KW - Heuristic

KW - Quantifier elimination

UR - http://www.scopus.com/inward/record.url?scp=85136984155&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-14788-3_17

DO - 10.1007/978-3-031-14788-3_17

M3 - Conference proceeding

SN - 978-3-031-14787-6

VL - 13366

T3 - Lecture Notes in Computer Science

SP - 300

EP - 317

BT - Computer Algebra in Scientific Computing CASC 2022

A2 - Boulier, François

A2 - England, Matthew

A2 - Sadykov, Timur M.

A2 - Vorozhtsov, Evgenii V.

PB - Springer International Publishing

T2 - International Workshop on Computer Algebra in Scientific Computing

Y2 - 22 August 2022 through 26 August 2022

ER -

New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis

Abstract

Publication series

Workshop

Bibliographical note

Keywords

Access to Document

Other files and links

Fingerprint

Cite this