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

Research output: Chapter in Book/Report/Conference proceedingConference proceedingpeer-review

4 Citations (Scopus)
48 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 languageEnglish
Title of host publicationComputer Algebra in Scientific Computing CASC 2022
EditorsFrançois Boulier, Matthew England, Timur M. Sadykov, Evgenii V. Vorozhtsov
PublisherSpringer International Publishing
Pages300–317
Number of pages18
Volume13366
ISBN (Electronic)978-3-031-14788-3
ISBN (Print)978-3-031-14787-6
DOIs
Publication statusPublished - 11 Aug 2022
EventInternational Workshop on Computer Algebra in Scientific Computing - Gebze, Turkey
Duration: 22 Aug 202226 Aug 2022
https://www.casc-conference.org/

Publication series

NameLecture Notes in Computer Science
Volume13366
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Workshop on Computer Algebra in Scientific Computing
Abbreviated titleCASC 2022
Country/TerritoryTurkey
CityGebze
Period22/08/2226/08/22
Internet address

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

Fingerprint

Dive into the research topics of 'New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis'. Together they form a unique fingerprint.

Cite this