Using Machine Learning to Improve Cylindrical Algebraic Decomposition

Using Machine Learning to Improve Cylindrical Algebraic Decomposition
复制标题

DOI:
10.1007/s11786-019-00394-8
复制
发表时间:
2019-12-01
影响因子:
0.8
通讯作者:
Paulson, Lawrence C.
Paulson, Lawrence C.
中科院分区:
其他
文献类型:
--
作者:
Huang, Zongyan;England, Matthew;Paulson, Lawrence C.

文献摘要

被引文献

相似文献

柱面代数分解(CAD)是计算代数几何中的一个重要工具,最著名的是实现实闭数域上的量词消去。然而,它的最坏情况的复杂性是输入大小的两倍指数,这在实践中经常遇到。已经观察到,对于许多问题,算法设置或问题公式的改变会导致运行时成本的巨大差异,将问题实例从难处理变为容易。已经开发了许多启发式算法来帮助进行这样的选择,但所涉及的几何关系的复杂性质意味着这些都是不完美的,有时会做出糟糕的选择。我们研究了机器学习(特别是支持向量机)的使用来做出这样的选择。机器学习是基于从测量数据中学习的属性将计算机模型适应复杂函数的过程。在本文中,我们将它应用于两个案例研究:第一个是在选择CAD变量排序的启发式方法之间进行选择;第二个是确定一个CAD问题实例何时将受益于Grobner基预条件。这似乎是机器学习在符号计算中的首次应用。我们在这两种情况下都证明了机器学习的选择比人类开发的启发式方法性能更好。
Cylindrical Algebraic Decomposition (CAD) is a key tool in computational algebraic geometry, best known as a procedure to enable Quantifier Elimination over real-closed fields. However, it has a worst case complexity doubly exponential in the size of the input, which is often encountered in practice. It has been observed that for many problems a change in algorithm settings or problem formulation can cause huge differences in runtime costs, changing problem instances from intractable to easy. A number of heuristics have been developed to help with such choices, but the complicated nature of the geometric relationships involved means these are imperfect and can sometimes make poor choices. We investigate the use of machine learning (specifically support vector machines) to make such choices instead. Machine learning is the process of fitting a computer model to a complex function based on properties learned from measured data. In this paper we apply it in two case studies: the first to select between heuristics for choosing a CAD variable ordering; the second to identify when a CAD problem instance would benefit from Grobner Basis preconditioning. These appear to be the first such applications of machine learning to Symbolic Computation. We demonstrate in both cases that the machine learned choice outperforms human developed heuristics.