The Conflict-Driven Cylindrical Algebraic Covering algorithm has proven well suited for performing theory validation checks in the satisfiability modulo theories paradigm for non-linear real arithmetic. CDCAC repurposes the theory underpinning classical cylindrical algebraic decomposition for SMT solving and is implemented in the SMT solvers cvc5 and SMT-RAT, as well as the computer algebra system Maple. It was previously observed that when using cylindrical algebraic decomposition for an SMT theory call, the output can be optimised by solving a single set covering problem instance that minimises the conflict clause. In this paper we consider the corresponding optimisation for CDCAC and observe that CDCAC naturally gives rise to multiple such optimisations within a single call. Each time a covering is generalised in one dimension, the resulting cell in the next dimension is labelled with theory constraints that cannot be satisfied together. We seek the smallest subset of constraints whose union covers all labels from the cells in the current covering. We call this optimisation problem a set covering problem with reasons. To simplify this problem, we introduce a data reduction step that generalises Beasley reduction for the classical set covering problem and show that this step alone solves many of the instances arising from SMT-LIB benchmarks. We then propose an exact solver based on linear programming to efficiently solve the remaining cases. Integrating these techniques into CDCAC has the potential to significantly improve SMT solver performance for non-linear real arithmetic problems.

翻译：冲突驱动的柱形代数覆盖算法已被证明非常适用于在非线性实数算术的可满足性模理论范式下执行理论有效性检验。CDCAC将经典柱形代数分解的理论基础重新应用于SMT求解，并已在SMT求解器cvc5和SMT-RAT以及计算机代数系统Maple中实现。先前研究发现，当使用柱形代数分解处理SMT理论调用时，可通过求解单个最小化冲突子句的集合覆盖问题实例来优化输出结果。本文针对CDCAC提出相应的优化方法，并观察到CDCAC在单次调用中自然产生多个此类优化机会。每次在一维空间中对覆盖进行泛化时，下一维空间中生成的单元会被标记为无法同时满足的理论约束集合。我们寻求约束的最小子集，其并集能够覆盖当前覆盖中所有单元的标记。我们将此优化问题称为带理由的集合覆盖问题。为简化该问题，我们引入数据约简步骤，该步骤推广了经典集合覆盖问题的Beasley约简法，并证明仅此步骤即可解决大量源自SMT-LIB基准测试的实例。随后我们提出基于线性规划的精确求解器以高效处理剩余案例。将这些技术集成到CDCAC中，有望显著提升SMT求解器在非线性实数算术问题上的性能表现。