Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
arXiv:1904.11061 · doi:10.1007/978-3-030-23250-4_7
Abstract
There has been recent interest in the use of machine learning (ML) approaches within mathematical software to make choices that impact on the computing performance without affecting the mathematical correctness of the result. We address the problem of selecting the variable ordering for cylindrical algebraic decomposition (CAD), an important algorithm in Symbolic Computation. Prior work to apply ML on this problem implemented a Support Vector Machine (SVM) to select between three existing human-made heuristics, which did better than anyone heuristic alone. The present work extends to have ML select the variable ordering directly, and to try a wider variety of ML techniques. We experimented with the NLSAT dataset and the Regular Chains Library CAD function for Maple 2018. For each problem, the variable ordering leading to the shortest computing time was selected as the target class for ML. Features were generated from the polynomial input and used to train the following ML models: k-nearest neighbours (KNN) classifier, multi-layer perceptron (MLP), decision tree (DT) and SVM, as implemented in the Python scikit-learn package. We also compared these with the two leading human constructed heuristics for the problem: Brown's heuristic and sotd. On this dataset all of the ML approaches outperformed the human made heuristics, some by a large margin.
Accepted into CICM 2019
References in corpus (23)
- Scikit-learn: Machine Learning in Python
- SATzilla: Portfolio-based Algorithm Selection for SAT
- DeepMath - Deep Sequence Models for Premise Selection
- Truth Table Invariant Cylindrical Algebraic Decomposition
- Cylindrical Algebraic Decompositions for Boolean Combinations
- Satisfiability Checking meets Symbolic Computation (Project Paper)
- Program Verification in the presence of complex numbers, functions with branch cuts etc
- Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
- A Case Study on the Parametric Occurrence of Multiple Steady States
- Improving the use of equational constraints in cylindrical algebraic decomposition
- Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains
- Optimising Problem Formulation for Cylindrical Algebraic Decomposition
- Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting
- Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- Using Machine Learning to Improve Cylindrical Algebraic Decomposition
- Symbolic Versus Numerical Computation and Visualization of Parameter Regions for Multistationarity of Biological Networks
- Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
- Cylindrical Algebraic Sub-Decompositions
- Machine Learning for Mathematical Software
- Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases
- TheoryGuru: A Mathematica Package to apply Quantifier Elimination
- Using the distribution of cells by dimension in a cylindrical algebraic decomposition
- A "Piano Movers" Problem Reformulated
Cited by in corpus (8)
- Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
- Algorithmically generating new algebraic features of polynomial systems for machine learning
- New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
- Improved cross-validation for classifiers that make algorithmic choices to minimise runtime without compromising output correctness
- Lessons on Datasets and Paradigms in Machine Learning for Symbolic Computation: A Case Study on CAD
- A machine learning based software pipeline to pick the variable ordering for algorithms with polynomial inputs
- Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition
- Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure