Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
柱形代数分解（CAD）是求解实代数几何及其他问题的重要工具。近年来，一种新的方法已经被开发出来，其中规则链技术被用来首先在复杂空间中构建分解。我们认为，这是建立复杂的分解递增多项式和生产CAD的细胞上的一系列公式是真不变的最新的变种。像所有的CAD算法一样，用户必须提供一个变量排序，这对问题的可处理性有着深远的影响。我们评估现有的启发式算法，以帮助选择这种算法，提出改进建议，然后推导出一个新的启发式更紧密地配合新算法的机制。
2014-05-23 cs.SC
A Variant of Non-uniform Cylindrical Algebraic Decomposition for Real Quantifier Elimination
针对实代数求解中CAD方法双重指数复杂度高的问题，提出一种可同时用于实量词消去和SMT求解的新型NuCAD变体，完成实现并通过与CAlC的实验对比验证效果。
2025-08-01 cs.SC
Improving the use of equational constraints in cylindrical algebraic decomposition
当构建柱形代数分解（CAD）时，可以在等式约束（EC）存在的情况下进行节省：等式在逻辑上由公式隐含。本论文关注的是如何使用多个EC，传播那些在整个投影集的输入。我们改进了McCallum在ISSAC 2001中的方法，通过使用简化投影理论来节省提升阶段的费用（无论是提升多项式还是提升单元格）。我们展示了工作的例子和复杂性分析的好处。
2015-05-07 cs.SC
Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition
柱形代数分解（CAD）是求解实代数几何及其他问题的重要工具。我们最近提出了一个新的CAD算法结合两个进步：真值表不变性，使CAD不变的真理的逻辑公式，而不是多项式的符号;和CAD建设的规则链技术，其中第一个复杂的分解是通过细化树递增约束。我们在这里考虑如何最好地制定输入到这个算法的问题。我们专注于一个选择（不相关的其他CAD算法）的顺序，其中提出的约束。我们开发了新的算法来帮助做出这种选择，从而在实践中最好地使用该算法。我们还考虑了CAD问题公式化的其他选择，如CICM 2013中所讨论的，在新算法的背景下重新审视这些选择。
2014-04-25 cs.SC
Using the distribution of cells by dimension in a cylindrical algebraic decomposition
研究了柱形代数分解中胞元的维数分布。我们发现，他们遵循一个标准的分布，似乎在很大程度上独立的基本问题或CAD算法使用。相反，分布是圆柱形结构固有的，主要由变量的数量决定。然后将这种见解与仅产生全维单元的算法相结合，以给出预测完整CAD中单元数量的准确方法。由于只构建全维单元相对便宜（不涉及昂贵的代数数计算），这导致了用于帮助CAD问题公式化的各种问题的算法，例如选择最佳变量排序。我们的实验表明，这种方法是非常有效的。
2014-09-05 cs.SC
The DEWCAD Project: Pushing Back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition
本摘要旨在向国际空间应用咨询委员会介绍设在联合王国考文垂大学和巴斯大学的预警和计算机辅助发展项目。该项目旨在通过SAT/SMT技术的集成、Lazard投影理论的扩展以及基于CAD技术但不生产CAD本身的新算法的开发，来推回柱形代数分解的双指数壁。该项目还寻求开发CAD的应用，并将重点放在经济学和生物网络分析领域的应用上。
2021-06-16 cs.SC
Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting
柱形代数分解（CAD）是实数上量词消去的一个重要工具，也是一系列其他应用的一个重要工具。传统上，CAD是通过投影和提升的过程来构建的，以在改变维度的欧几里得空间内移动问题。最近，Maple的RegularChains Library中引入并实现了一种替代方法，该方法首先使用三角分解来分解复杂空间，然后再细化到真实空间。我们在这里描述了一个免费的软件包ProjectionCAD，它利用RegularChains Library中的例程通过投影和提升来构建CAD。我们详细介绍了如何修改投影和提升算法，以允许这一点，讨论的动机和调查的功能包。
2014-05-23 cs.SC
Divide-And-Conquer Computation of Cylindrical Algebraic Decomposition
我们提出了一个分而治之的版本的柱形代数分解（CAD）算法。该算法将输入表示为子公式的布尔组合，计算子公式的解集的柱形代数分解，并组合结果。我们提出了一个基于图形的启发式找到一个合适的分区的输入和目前的经验比较与直接CAD计算。
2014-02-04 cs.MS cs.SC
A Successive Resultant Projection for Cylindrical Algebraic Decomposition
本文证明了两个投影算子的等价性，这两个投影算子都可用于柱形代数分解（CAD）。布朗投影（Brown's Projection，C。W. Brown（2001））;另一种是杨路（L.Yang and S. H. Xia（2000）），其概述如下：给定$x_1,\,x_2,\,\cdots$中的多项式$f$，用$f_1$表示$f$及其关于$x_1$的偏导数的结果（去除多个因子），由$f_2$表示$f_1$及其相对于$x_2$的偏导数的结果，（去除多个因子），$\cdots$，连续重复此过程，直到最后一个结果成为一元多项式。利用恒等式证明了这两个投影算子的等价性。
2014-12-16 cs.SC
New heuristic to choose a cylindrical algebraic decomposition variable ordering motivated by complexity analysis
众所周知，变量排序对于柱形代数分解（CAD）算法的效率甚至是易处理性是至关重要的。我们提出了新的启发式的复杂性分析的CAD选择变量排序。这些算法对现有的算法进行了评估，并在SMT-LIB基准测试上进行了实验，使用现有的性能指标和我们为手头的问题提出的新指标。最好的这些新算法选择的排序导致时间平均比虚拟最好的慢17%：与现有技术相比，这是一个改进，它实现了时间慢25%。
2022-06-27 cs.SC
Cylindrical Algebraic Decompositions for Boolean Combinations
本文提出了一个关键的观察，当使用柱形代数分解（CAD）来解决一个问题的一组多项式，它并不总是那些多项式的符号是最重要的，而是某些量词自由公式涉及他们的真值。这激发了我们对真值表不变CAD（TTICAD）的定义。我们概括了方程约束的理论，设计一种算法，将有效地构建一个TTICAD的广泛的一类问题，产生更强的结果比单独使用方程约束。该算法是完全在Maple中实现的，我们从实验中提出了有前途的结果。
2013-04-29 cs.SC
Optimising Problem Formulation for Cylindrical Algebraic Decomposition
柱形代数分解（CAD）是研究实代数几何的重要工具，在数学和其他领域有着广泛的应用。已知在最坏情况下，它在变量数量上具有双指数复杂度，但实际计算时间可能会有很大变化。对于一个给定的问题，有可能提供不同的公式，从而导致在可处理性上的巨大差异。在本文中，我们提出了一个新的措施，考虑到真正的几何问题的CAD复杂性。这导致了新的数学选择：CAD问题的变量排序，指定的等式约束，和真值表不变CAD（TTICAD）的配方。然后，我们考虑使用Groebner基地的先决条件TTICAD的可能性，当这样的配方构成一个新的问题的创建。
2013-05-24 cs.SC
On some Exotic Cylindrical Algebraic Decompositions and Cells
本文通过构造特定的CADs和CAD细胞实例，推翻了关于拓扑假设的几个猜想和开放问题。
2026-01-14 cs.SC math.AG
Regular cylindrical algebraic decomposition
我们证明了有界半代数集的强良基圆柱代数分解P是正则胞腔剖分，在任何维度上，并且与P的构造方法无关。良基是P上的一个全局条件，适用于许多广泛使用的算法的输出。我们还表明，同样的S维至多3和P的一个强圆柱代数分解，是局部边界单连通的：这是一个纯粹的局部额外条件。
2018-03-11 cs.SC math.AG math.AT
Speeding up Cylindrical Algebraic Decomposition by Gröbner Bases
格罗布纳基和柱形代数分解通常被认为是两种相当不同的方法，用于研究方程组，在柱形代数分解的情况下，用于研究不等式。然而，即使对于等式和不等式的混合系统，也可以在调用CAD之前将格罗布纳基应用于（联合）等式。我们看到，这是，经常但不总是，一个有益的预处理的CAD问题。也可以相对于等式来预处理（联合的）不等式，这在许多情况下也是有用的。
2012-05-29 cs.SC math.AG
Cylindrical Algebraic Decomposition with Equational Constraints
柱形代数分解（CAD）是符号计算中最重要的算法之一，它是实域上一阶逻辑中的量词消去的工具。最近，它在可满足性检查社区中作为一种工具来识别非线性实数运算中问题的满意解决方案。原始算法根据多项式的符号产生分解，而通常需要的是根据包含这些多项式的公式的真值进行分解。一种实现更粗糙（但希望更便宜）分解的方法是减少CAD中识别的多项式，以反映减少解空间维度的逻辑结构：等式约束（EC）的存在。本文可以作为一个教程，使用CAD与EC：我们描述了所有必要的背景和当前的最先进的，特别是，我们目前最近的工作如何麦卡勒姆的理论减少投影可能会被利用，以进一步节省在提升阶段：无论是多项式，我们解除和解除的细胞。我们给出了一个新的复杂性分析，以证明在最坏情况下的CAD的复杂性界的双指数减少符合EC的数量。我们表明，减少可以适用于多项式的数量和他们的程度。
2019-03-20 cs.SC
Truth Table Invariant Cylindrical Algebraic Decomposition
当使用柱形代数分解（CAD）来解决关于一组多项式的问题时，可能不是那些多项式的符号是最重要的，而是涉及它们的某些量词自由公式的真值。这一观察激发了我们的文章和真值表不变CAD（TTICAD）的定义。在ISSAC 2013中，当前作者提出了一种算法，该算法可以有效地直接为公式列表构建TTICAD，其中每个公式都有一个等式约束。这是通过推广麦卡勒姆的理论减少投影算子。在本文中，我们提出了一个扩展版本，我们的理论，可以应用到一个任意列表的公式，实现储蓄，如果至少有一个等式约束。我们还解释了如何减少投影算子的理论可以允许进一步改进的CAD算法的提升阶段，即使在一个单一的等式约束的情况下。该算法是完全在Maple中实现的，我们从实验和复杂性分析中展示了我们的贡献的好处。
2015-11-13 cs.SC
A Geometric Approach to Cylindrical Algebraic Decomposition
本文从几何视角重新研究柱形代数分解，通过建立几何纤维基数与半代数连续截面存在性之间的联系，提出了一种能系统利用所有方程的新算法，实验验证了其高效性。
2025-03-28 cs.SC math.AC math.AG
Cylindrical Algebraic Decomposition in Macaulay2
该论文介绍了Macaulay2中首个圆柱代数分解实现，通过开放CAD和Lazard投影解决严格不等式问题，并引入新的变量排序启发式，可扩展至实量词消去。
2025-03-31 cs.SC math.AG
Truth Table Invariant Cylindrical Algebraic Decomposition by Regular Chains
基于最近的两个进展，提出了一种计算柱形代数分解的新算法。首先，输出是真值表不变的（TTICAD），这意味着给定的公式在分解的每个单元上具有恒定的真值。其次，计算使用规则链理论，首先建立一个圆柱形分解的复杂空间（CCD）递增多项式。对规则链技术进行了重大修改，以实现更复杂的不变性准则。在RegularChains Library for Maple中实现的实验结果验证了将这些进步相结合可以提供优于其各个组件的算法，并与最先进的算法竞争。
2014-06-10 cs.SC math.AG
Recent Developments in Real Quantifier Elimination and Cylindrical Algebraic Decomposition
本文综述了实量词消去与柱面代数分解的最新进展，重点探讨了受计算逻辑启发的算法改进、SAT/SMT协同应用、机器学习优化变量排序及可解释AI的潜在贡献。
2024-07-29 cs.SC
From Approximate Factorization to Root Isolation with Application to Cylindrical Algebraic Decomposition
我们提出了一种算法，用于隔离的根的任意复杂的多项式$p$，也适用于多项式的多个根的不同的根的数量$k$作为输入的一部分。它输出$k$成对不相交的磁盘，每个磁盘包含$p$的不同根之一及其多重性。该算法使用近似因式分解作为子程序。此外，我们应用新的根隔离算法最近的算法计算的拓扑结构的一个真正的平面代数曲线指定为零集的二元整数多项式和隔离的二元多项式系统的真正的解决方案。对于输入多项式的次数$n$和位大小$τ$，我们提高了目前最好的运行时间从$\tO(n^{9}τ+n^{8}τ^{2})$（确定性）的$\tO(n^{6}+n^{5}τ)$（随机）的拓扑计算和从$\tO(n^{8}+n^{7}τ)$（确定性）的$\tO(n^{6}+n^{5}τ)$（随机）解决二元系统。
2014-01-23 cs.SC
Cylindrical Algebraic Sub-Decompositions
柱形代数分解（CAD）是实代数几何中的一个重要工具，主要用于消除实数上的量词和研究半代数集。在本文中，我们介绍了圆柱代数子分解（子CAD），这是CAD的子集，包含指定一个给定的问题的解决方案所需的所有信息。我们定义了两种新类型的子CAD：品种子CAD是那些在CAD中的细胞躺在一个指定的品种;和分层子CAD只有那些细胞的尺寸高于指定值。我们提出的算法来产生这些，并描述了如何将这两种方法可以相互结合，最近的理论真值表不变CAD。我们给出了一个复杂性分析表明，这些技术可以提供大量的理论上的节省，这是支持使用在Maple实现的实验。
2014-04-24 cs.SC math.AG
Summer Research Report: Towards Incremental Lazard Cylindrical Algebraic Decomposition
柱形代数分解（Cylindrical Algebraic Decomposition，CAD）是计算实代数几何中的一个重要工具，它能够解决实数上的多项式系统的许多问题，但已知其最坏情况下的计算复杂性是变量数的双指数。它已经被符号计算社区研究了很长时间，并在各种计算机代数系统中实现，然而，它最近也被满足性检查社区用于SMT求解器。SCSC项目寻求在这些社区之间建立桥梁。本报告介绍了由欧盟H2020 SCSC CSA资助的2017年夏季研究实习期间取得的进展。我们描述了一个概念证明的增量CAD算法在Maple中的实现，其中CAD的建立和完善的多项式约束增量，在一个单一的计算从一个单一的输入的通常方法。这一进步将使CAD用于SMT求解器，SMT求解器通过不断重新制定逻辑公式和查询像CAD这样的求解器来搜索解决方案，以确定逻辑解决方案是否可接受。我们描述的概念证明，这清楚地显示了计算的优势相比，迭代重新计算的实验。此外，该项目在最近验证的Lazard投影方案（以及相应的Lazard评估）下实施了这项工作。这是理论上最小的完整CAD方法，这是第一个有文档记录的实现。
2018-04-23 cs.SC
Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition
University of Cambridge（剑桥大学）；University of Bath（巴斯大学）
柱形代数分解（cylindrical algebraic decomposition，CAD）是计算代数几何中的一个重要工具，特别是实闭域上的量词消去。在使用CAD时，通常可以选择变量的排序。这可能很重要，有些问题用一个变量排序是不可行的，但用另一个变量排序是容易的。机器学习是基于从测量数据中学习到的属性将计算机模型拟合到复杂函数的过程。在本文中，我们使用机器学习（特别是一个支持向量机）来选择一个变量排序，优于每一个单独的算法之间的选择。
2014-04-25 cs.LG cs.SC
Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure
柱形代数分解（CAD）在实代数几何等领域有着重要的作用。众所周知，计算CAD时变量排序的选择对计算的时间和内存使用以及计算的样本点数量有很大影响。在本文中，我们指出，典型的CAD算法，如果执行一种特殊的变量排序（称为“完美消除排序”），自然保持弦，这是一个重要的属性稀疏的变量。实验表明，如果所讨论的多项式系统的关联图是弦的（\emph{resp.}，几乎是弦的），则关联图的完美消除排序（\emph{resp.}，关联图的最小弦完成）可以是用于CAD计算的良好变量排序。也就是说，通过使用完美消除排序，CAD计算可以产生比通过使用其他朴素变量排序小得多的投影多项式的全集。更重要的是，对于CAD计算的复杂性分析通过一个完美的消除顺序，所谓的$(m,d)$ -性质的投影多项式的完整的集合通过这样的顺序获得，通过该集合的“大小”的特点。该性质表明，当对应的完全消除树具有较低的高度时，投影多项式的全集也倾向于具有较小的“大小”。这与实验结果是一致的，因此，具有较低的消除树高度的完美消除顺序进一步推荐用于CAD投影。
2021-02-04 cs.SC
Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition
Queen Mary University of London（伦敦大学玛丽女王学院）
提出一种通过柱形代数分解结合符号/数值积分，精确计算含随机输入的小型程序输出分布的方法，并验证了其在浮点算术和传感器库程序上的有效性。
2026-06-24 cs.SC math.PR
Further results on Minimal and Minimum Cylindrical Algebraic Decompositions
University of Liege（列日大学）
本文研究了半代数集的最小和最小圆柱代数分解的存在性，提出了一种计算方法并给出了判定标准。
2026-01-14 cs.SC
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
提出了一种确定实数上非线性多项式约束合取可满足性的新算法，该算法可作为非线性实数算术可满足性模理论（SMT）求解的理论求解器.该算法是适应于可满足性的柱形代数分解（CAD）的变体，其中解候选者（样本点）被增量地构造，直到找到满意的样本或者已经采样了足够的样本以得出不可满足性的结论。样本的选择由输入约束和先前的冲突指导。我们的新方法背后的关键思想是从部分样本开始;证明它不能扩展到完整样本;并从排除部分样本周围的更大空间的原因中，逐步建立成空间的圆柱代数覆盖。有相似之处的增量变化的CAD，NLSAT方法的Jovanovic和de Escha，和NuCAD算法的布朗，但我们目前的工作示例和实验结果的初步实施，以证明这些差异，和新方法的好处。
2020-11-23 cs.LO cs.SC
On Minimal and Minimum Cylindrical Algebraic Decompositions
本文研究适配于半代数集的柱形代数分解在加细偏序下的极小与最小元存在性，证明任意情形存在极小元、低维情形存在最小元，并给出高维反例及基于归约系统的计算与合流性刻画。
2024-11-20 cs.SC
Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases
University of Cambridge（剑桥大学）；Coventry University（考文垂大学）；University of Bath（巴斯大学）
柱形代数分解（CAD）是计算代数几何中的一个重要工具，特别是实闭域上的量词消去。然而，它可能是昂贵的，最坏情况下的复杂度是输入大小的两倍指数。因此，重要的是以CAD算法的最佳方式制定问题。一种可能性是使用Groebner基（GB）理论对输入多项式进行预处理。以前的实验表明，虽然这通常对CAD算法非常有益，但对于某些问题，它可能会显着恶化CAD性能。在本文中，我们调查是否机器学习，特别是一个支持向量机（SVM），可用于识别这些CAD问题，受益于GB预处理。我们对超过1000个问题（比以前的研究大很多倍）进行了实验，发现机器学习的选择比人类的启发式更好。
2016-08-15 cs.LG cs.SC
Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition
University of Cincinnati（辛辛那提大学）；Coventry University（考文垂大学）
本研究针对符号计算中柱形代数分解的变量序选择问题，探索可解释AI工具SHAP对ML模型的解释作用，提出可据此设计与人工启发式规模复杂度相近的新型启发式算法，为符号计算提供新洞见。
2023-08-29 cs.LG cs.SC
Levelwise construction of a single cylindrical algebraic cell
针对非线性实数算术SMT问题，本文提出柱形代数胞腔的分层构造方法，通过变量顺序逐层构建、启发式选择投影多项式优化胞腔形状，并以证明系统实现启发式与算法的解耦。
2023-07-20 cs.SC
Experience with Heuristics, Benchmarks & Standards for Cylindrical Algebraic Decomposition
在激发SC广场项目的论文中，[E。Abraham，在符号计算和可满足性检查之间建立桥梁，Proc. ISSAC '15，pp. 1-6，ACM，2015]作者将复杂的逻辑学的使用确定为可满足性检查社区擅长的技术，并且符号计算社区可能从中学习和繁荣。为了开始这个学习过程，我们总结了计算机代数算法柱形代数分解的启发式开发经验。我们还提出并讨论了标准和基准，作为符号计算可以从可满足性检查专业知识中蓬勃发展的另一个领域，注意到这些已被确定为CSA项目中新SC Square社区的初始行动，如[E.~ Abraham等人，SC $^2$：可满足性检查符合符号计算（项目论文）}，智能计算机数学（LNCS 9761），pp. 28- 43，Springer，2015]。
2016-09-29 cs.LO cs.SC
Towards Incremental Cylindrical Algebraic Decomposition in Maple
柱形代数分解（CAD）是计算实代数几何中的一个重要工具，能够解决实数上多项式系统的许多问题。它已经被符号计算社区研究了很长时间，并且最近在可满足性检查社区中发现了兴趣。本报告描述了一个概念验证的增量CAD算法在Maple中的实现，其中CAD的建立，然后细化为额外的多项式约束。其目的是使CAD适合用作SMT工具的理论求解器，SMT工具通过不断重新制定逻辑公式并查询逻辑解决方案是否可接受来搜索解决方案。我们描述的概念证明，这清楚地显示了计算的优势相比，迭代重新计算的实验。此外，该项目根据最近验证的Lazard投影方案（以及相应的Lazard估值）执行了这项工作。
2018-05-24 cs.CG cs.SC math.AG
Computing Equilibria of Semi-algebraic Economies Using Triangular Decomposition and Real Solution Classification
本文研究了经济模型中多重均衡存在性的判定问题。我们提出了一个一般的和完整的方法来确定多重的平衡在半代数经济，这可能是表示为半代数系统。该方法是基于三角分解和实解分类，两个强大的代数计算工具。两个应用实例说明了该方法的有效性。
2013-08-23 cs.SC
An implementation of Sub-CAD in Maple
柱形代数分解（CAD）是研究半代数集的重要工具，在代数几何等领域有着广泛的应用。我们以前曾报道过在Maple中实现CAD，它提供了Collins的原始投影和提升算法以及随后的改进。在这里，我们报告新的功能：特别是能够建立圆柱代数子分解（子CAD），其中只有某些细胞被返回。我们已经实现了返回指定维度或更高维度的单元格的算法（分层的{ \scad }），以及仅返回给定多项式为零的那些单元格的算法（变种{ \scad }）。这些可以大幅节省输出大小和计算时间。所描述的代码和演示该软件包全部功能的介绍性Maple工作表/ pdf可在http://opus.bath.ac.uk/43911/上免费获得。
2015-03-23 cs.SC
Using Machine Learning to Improve Cylindrical Algebraic Decomposition
University of Cambridge（剑桥大学）；Coventry University（考文垂大学）；University of Bath（巴斯大学）
柱形代数分解是计算代数几何中的一个重要工具，它是实闭域上的量词消去过程。然而，它在最坏情况下的复杂度是输入大小的两倍指数，这在实践中经常遇到。已经观察到，对于许多问题，算法设置或问题公式化的改变可以导致运行时成本的巨大差异，将问题实例从棘手变为容易。人们已经开发了一些几何学来帮助做出这样的选择，但是所涉及的几何关系的复杂性意味着这些几何学是不完美的，有时会做出糟糕的选择。我们研究使用机器学习（特别是支持向量机）来做出这样的选择。机器学习是基于从测量数据中学习到的属性将计算机模型拟合到复杂函数的过程。在本文中，我们将其应用在两个案例研究：第一个选择之间的选择CAD变量的排序;第二个确定当一个CAD问题的实例将受益于Groebner基础预处理。这些似乎是机器学习在符号计算中的首次应用。在这两种情况下，我们证明了机器学习的选择优于人类开发的算法。
2018-04-26 cs.LG cs.SC
Breaking the Data Barrier in Learning Symbolic Computation: A Case Study on Variable Ordering Suggestion for Cylindrical Algebraic Decomposition
School of Mathematical Sciences, Jiangsu University（江苏大学数学科学学院）；Chongqing Institute of Green and Intelligent Technology, Chinese Academy of Sciences（中国科学院重庆绿色智能技术研究所）；Chongqing School, University of Chinese Academy of Sciences（中国科学院大学重庆学院）
本研究通过预训练和微调Transformer模型，改进了圆柱代数分解中变量顺序建议的效率，提升了符号计算的性能。
2026-07-27 cs.LG cs.SC
Comparing machine learning models to choose the variable ordering for cylindrical algebraic decomposition
Coventry University（考文垂大学）
最近，人们对在数学软件中使用机器学习（ML）方法来做出影响计算性能而不影响结果的数学正确性的选择产生了兴趣。讨论了符号计算中的一个重要算法--柱形代数分解（CAD）的变量排序问题。之前将ML应用于这个问题的工作实现了一个支持向量机（SVM），以在三个现有的人工智能中进行选择，这比任何单独的启发式方法都要好。目前的工作扩展到让ML直接选择变量排序，并尝试更广泛的ML技术。我们尝试了NLSAT数据集和Maple 2018的正则链库CAD功能。对于每个问题，变量排序导致最短的计算时间被选为ML的目标类。特征从多项式输入中生成，并用于训练以下ML模型：k-最近邻（KNN）分类器，多层感知器（MLP），决策树（DT）和SVM，如在Python scikit-learn包中实现的。我们还比较了这些与两个领先的人类构建的启发式的问题：布朗的启发式和sotd。在这个数据集上，所有ML方法的表现都优于人工智能，其中一些方法的表现更好。
2019-06-05 cs.LG cs.SC
New Opportunities for the Formal Proof of Computational Real Geometry?
本文的目的是探讨这样一个问题：在什么程度上我们可以产生形式化的，机器可验证的，证明在真正的代数几何？“这个问题以前就被问过，但到目前为止，回答这些问题的主要算法还没有正式化。我们提出了一个论文，一个新的算法，用于确定可满足性的公式在实数通过圆柱代数覆盖[Ábrahám，达文波特，英格兰，克雷默，\emph{Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driver Search Using Cylindrical Algebraic Coverings}，2020]可能会提供跟踪和输出，使结果更容易受到机器验证比那些竞争的算法。
2020-04-08 cs.LO cs.SC
Triangular Decomposition of Semi-algebraic Systems
正则链和三角分解是描述多项式方程组复解的基本工具。本文提出了适应这些工具，重点解决方案的真正的模拟：半代数系统。我们证明了任何这样的系统都可以分解成n个{ \em正则半代数系统}。我们提出了两个规格，这样的分解，并提出相应的算法。在某些假设下，一种类型的分解可以在单指数时间w.r.t.内计算。变量的数量。我们实现了我们的算法，实验结果表明其有效性。
2010-05-13 cs.CG cs.MS cs.SC
Algebraic Machine Learning: Learning as computing an algebraic decomposition of a task
Champalimaud Research（尚帕利莫德研究院）；Champalimaud Centre for the Unknown（尚帕利莫德未知中心）；Algebraic AI（代数人工智能公司）
提出基于抽象代数的机器学习新范式，将任务编码为代数公理，通过子直积分解获得泛化模型，在标准数据集上性能媲美MLP，并能直接求解哈密顿环等形式化问题。
2025-02-27 cs.AI cs.DM cs.LG
