### Abstract

There are a variety of choices to be made in both computer algebra systems (CASs) and satisfiability modulo theory (SMT) solvers which can impact performance without affecting mathematical correctness. Such choices are candidates for machine learning (ML) approaches, however, there are difficulties in applying standard ML techniques, such as the efficient identification of ML features from input data which is typically a polynomial system. Our focus is selecting the variable ordering for cylindrical algebraic decomposition (CAD), an important algorithm implemented in several CASs, and now also SMT-solvers. We created a framework to describe all the previously identified ML features for the problem and then enumerated all options in this framework to automatically generate many more features. We validate the usefulness of these with an experiment which shows that an ML choice for CAD variable ordering is superior to those made by human created heuristics, and further improved with these additional features. This technique of feature generation could be useful for other choices related to CAD, or even choices for other algorithms in CASs / SMT-solvers with polynomial systems as input.

Original language | English |
---|---|

Title of host publication | Proceedings of the 4th International Workshop on Satisfiability Checking and Symbolic Computation |

Publisher | CEUR Workshop Proceedings |

Number of pages | 12 |

Publication status | Published - 4 Oct 2019 |

Event | 4th International Workshop on Satisfiability Checking and Symbolic Computation - Bern , Switzerland Duration: 10 Jul 2019 → 10 Jul 2019 |

### Publication series

Name | CEUR Workshop Proceedings |
---|---|

Publisher | CEUR Workshop Proceedings |

Volume | 2460 |

ISSN (Print) | 1613-0073 |

### Conference

Conference | 4th International Workshop on Satisfiability Checking and Symbolic Computation |
---|---|

Abbreviated title | SIAM AG 2019 |

Country | Switzerland |

City | Bern |

Period | 10/07/19 → 10/07/19 |

### Fingerprint

### Bibliographical note

Copyright © 2019 for the individual papers by the papers' authors. This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0).### Keywords

- machine learning
- feature generation
- non-linear
- real arithmetic
- symbolic computation
- cylindrical algebraic decomposition

### ASJC Scopus subject areas

- Computer Science(all)

### Cite this

*Proceedings of the 4th International Workshop on Satisfiability Checking and Symbolic Computation*(CEUR Workshop Proceedings; Vol. 2460). CEUR Workshop Proceedings.

**Algorithmically generating new algebraic features of polynomial systems for machine learning.** / Florescu, Dorian; England, Matthew.

Research output: Chapter in Book/Report/Conference proceeding › Conference proceeding

*Proceedings of the 4th International Workshop on Satisfiability Checking and Symbolic Computation.*CEUR Workshop Proceedings, vol. 2460, CEUR Workshop Proceedings, 4th International Workshop on Satisfiability Checking and Symbolic Computation, Bern , Switzerland, 10/07/19.

}

TY - GEN

T1 - Algorithmically generating new algebraic features of polynomial systems for machine learning

AU - Florescu, Dorian

AU - England, Matthew

N1 - Copyright © 2019 for the individual papers by the papers' authors. This volume and its papers are published under the Creative Commons License Attribution 4.0 International (CC BY 4.0).

PY - 2019/10/4

Y1 - 2019/10/4

N2 - There are a variety of choices to be made in both computer algebra systems (CASs) and satisfiability modulo theory (SMT) solvers which can impact performance without affecting mathematical correctness. Such choices are candidates for machine learning (ML) approaches, however, there are difficulties in applying standard ML techniques, such as the efficient identification of ML features from input data which is typically a polynomial system. Our focus is selecting the variable ordering for cylindrical algebraic decomposition (CAD), an important algorithm implemented in several CASs, and now also SMT-solvers. We created a framework to describe all the previously identified ML features for the problem and then enumerated all options in this framework to automatically generate many more features. We validate the usefulness of these with an experiment which shows that an ML choice for CAD variable ordering is superior to those made by human created heuristics, and further improved with these additional features. This technique of feature generation could be useful for other choices related to CAD, or even choices for other algorithms in CASs / SMT-solvers with polynomial systems as input.

AB - There are a variety of choices to be made in both computer algebra systems (CASs) and satisfiability modulo theory (SMT) solvers which can impact performance without affecting mathematical correctness. Such choices are candidates for machine learning (ML) approaches, however, there are difficulties in applying standard ML techniques, such as the efficient identification of ML features from input data which is typically a polynomial system. Our focus is selecting the variable ordering for cylindrical algebraic decomposition (CAD), an important algorithm implemented in several CASs, and now also SMT-solvers. We created a framework to describe all the previously identified ML features for the problem and then enumerated all options in this framework to automatically generate many more features. We validate the usefulness of these with an experiment which shows that an ML choice for CAD variable ordering is superior to those made by human created heuristics, and further improved with these additional features. This technique of feature generation could be useful for other choices related to CAD, or even choices for other algorithms in CASs / SMT-solvers with polynomial systems as input.

KW - machine learning

KW - feature generation

KW - non-linear

KW - real arithmetic

KW - symbolic computation

KW - cylindrical algebraic decomposition

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

M3 - Conference proceeding

T3 - CEUR Workshop Proceedings

BT - Proceedings of the 4th International Workshop on Satisfiability Checking and Symbolic Computation

PB - CEUR Workshop Proceedings

ER -