论文标题
新的启发式方法可以选择一个由复杂性分析激励的圆柱代数分解变量
New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
论文作者
论文摘要
众所周知，变量排序对于圆柱代数分解（CAD）算法的效率甚至障碍至关重要。我们提出了受CAD复杂性分析的启发的新启发式方法，以选择变量顺序。使用现有的性能指标和我们针对当前问题提出的新指标，通过对SMT-LIB基准测试进行实验对现有启发式方法进行了评估。这些新的启发式方法中最好的选择是，与实际的最新时间相比，该订单平均速度比虚拟最佳速度慢17％：这是一种改善，该时间速度速度慢了25％。
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.
