面向 SMT 的圆柱代数覆盖优化：求解带因素的集合覆盖问题
数据结构与算法
2026-01-22 v1 组合数学
摘要
冲突驱动的圆柱代数覆盖 (CDCAC) 算法已被证明适用于在非线性实算术的满足模理论范式中执行理论验证检查。CDCAC 将经典圆柱代数分解的理论基础用于 SMT 求解，并实现于 SMT 求解器 cvc5 和 SMT-RAT 以及计算机代数系统 Maple 中。此前观察到，当使用圆柱代数分解进行 SMT 理论调用时，可通过求解单个最小化冲突子句的集合覆盖问题实例来优化输出。在本文中，我们考虑对 CDCAC 的相应优化，观察到 CDCAC 在单次调用中自然产生多个此类优化。每次在一个维度上对覆盖进行广化后，下一个维度中的细胞都标记为无法同时满足的理论约束。我们寻求一组约束的最小子集，其联合覆盖当前覆盖中所有标签。我们将此优化问题称为带因素的集合覆盖问题。为简化此问题，我们引入一种数据降级步骤，对经典集合覆盖问题的 Beasley 缩减进行推广，证明此步骤alone即可解决许多来自 SMT-LIB 基准测试的实例。随后我们提出一种基于线性规划的精确求解器，以高效求解剩余案例。将这些技术集成到 CDCAC 中，可能显著提高非线性实算术问题的 SMT 求解器性能。
引用
@article{arxiv.2601.14424,
title = {Optimising Cylindrical Algebraic Coverings for use in SMT by Solving a Set Covering Problem with Reasons},
author = {Abiola Babatunde and Matthew England and AmirHosein Sadeghimanesh},
journal= {arXiv preprint arXiv:2601.14424},
year = {2026}
}
备注
22 pages, 4 figures, 3 tables. Submitted to the European Journal of Operational Research