系统科学与数学2024,Vol.44Issue(9) :2826-2849.DOI:10.12341/jssms22799

基于强化学习的柱形代数分解变元择序

Variable Ordering Selection for Cylindrical Algebraic Decomposition via Reinforcement Learning

荆瑞娟 钱铖镕 陈长波
系统科学与数学2024,Vol.44Issue(9) :2826-2849.DOI:10.12341/jssms22799

基于强化学习的柱形代数分解变元择序

Variable Ordering Selection for Cylindrical Algebraic Decomposition via Reinforcement Learning

荆瑞娟 1钱铖镕 1陈长波2
扫码查看

作者信息

  • 1. 江苏大学数学科学学院,镇江 212023
  • 2. 中国科学院重庆绿色智能技术研究院,自动推理与认知重庆市重点实验室,重庆 400714
  • 折叠

摘要

柱形代数分解是半代数系统求解和实量词消去的基本工具.实际求解过程中,不同变元序的选择对柱形代数分解的效率影响重大.目前已有的启发式或机器学习择序的方法基本都建立在多项式系统的支撑集是影响变元序的决定因素这一隐含假设上.文章首先通过设计同支撑集变系数的实验对这一假设进行了检验,实验表明支撑集确实是影响最佳变元序的重要因素但并非唯一因素.针对同支撑集变系数的柱形代数分解最佳择序问题,文章设计了基于强化学习的择序方案,四变元的实验表明该方案可以突破已有方法只依赖支撑集选择最佳变元序准确率的上限.另外,针对多达二十万亿可选序系统的实验表明,该方案远优于传统的启发式方法.同已有的针对较少变元的监督学习择序方案相比,该强化学习方案克服了变元增多导致序数量组合爆炸时获得高质量标记数据的困难.

Abstract

Cylindrical algebraic decomposition is a basic tool in semi-algebraic sys-tem solving and real quantifier elimination.In the actual solving process,the choice of a variable ordering may have a significant impact on the efficiency of cylindri-cal algebraic decomposition.At present,the existing heuristic or machine learning ordering selection methods are basically based on the implicit assumption that the support set of a polynomial system is the determinant for affecting the variable order-ings.In this paper,we first test this hypothesis by designing an experiment with the support set fixed but the coefficients varying.The experimentation shows that the support set is indeed an important factor,though not the only factor,determining the optimal variable ordering.Aiming at selecting the optimal ordering for computing cylindrical algebraic decompositions for systems with the same support set but dif-ferent coefficients,this paper designs an ordering selection scheme via reinforcement learning.The experimentation on four variables shows that this scheme can surpass the accuracy limit of existing methods on selecting the optimal variable ordering that rely solely on the support set.In addition,experiments on systems owning up to 20 trillion of possible orderings show that the scheme is much more efficient than tradi-tional heuristic methods.In contrast to the existing supervised learning methods for selecting the variable ordering of a few variables,this reinforcement learning scheme overcomes the difficulty of obtaining high-quality labeled data when the number of variables increases,which may lead to the combinatorial explosion of the number of variable orderings.

关键词

半代数系统/柱形代数分解/变元序/强化学习/支撑集

Key words

Semi-algebraic system/cylindrical algebraic decomposition/variable or-dering/reinforcement learning/support set

引用本文复制引用

基金项目

国家自然科学基金(12101267)

江苏省自然科学基金(BK 20200903)

江苏大学高层次人才引进计划(19JDG035)

江苏省双创博士项目()

重庆英才计划青年拔尖项目(2021000263)

国家重点研发计划(2020YFA0712300)

重庆市院士牵头科技创新引导专项(cstc2021yszxjcyjX0005)

重庆市院士牵头科技创新引导专项(cstc2022YSZX-JCX0011CSTB)

重庆市自然科学基金(cstc2021jcyjmsxmX0821)

出版年

2024
系统科学与数学
中国科学院数学与系统科学研究院

系统科学与数学

CSTPCD北大核心
影响因子:0.425
ISSN:1000-0577
参考文献量1
段落导航相关论文