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

Variable Ordering Selection for Cylindrical Algebraic Decomposition via Reinforcement Learning

作　　者：荆瑞娟 钱铖镕 陈长波[2] JING Ruijuan;QIAN Chengrong;CHEN Changbo(School of Mathematical Sciences,Jiangsu University,Zhenjiang 212023;Chongqing Key Laboratory of Automated Reasoning and Cognition,Chongqing Institute of Green and Intelligent Technology,Chinese Academy of Sciences,Chongqing 400714)

机构地区：[1]江苏大学数学科学学院,镇江212023 [2]中国科学院重庆绿色智能技术研究院,自动推理与认知重庆市重点实验室,重庆400714

出　　处：《系统科学与数学》2024年第9期2826-2849,共24页Journal of Systems Science and Mathematical Sciences

基　　金：国家自然科学基金(12101267);江苏省自然科学基金(BK 20200903);江苏大学高层次人才引进计划(19JDG035);江苏省双创博士项目;重庆英才计划青年拔尖项目(2021000263);国家重点研发计划(2020YFA0712300);重庆市院士牵头科技创新引导专项(cstc2021yszx-jcyjX0005,cstc2022YSZX-JCX0011CSTB);重庆市自然科学基金(cstc2021jcyj-msxmX0821)资助课题。

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

关 键 词：半代数系统 柱形代数分解 变元序 强化学习 支撑集 

分 类 号：O15[理学—数学]