The cylindrical algebraic covering method was originally proposed to decide the satisfiability of a set of non-linear real arithmetic constraints. We reformulate and extend the cylindrical algebraic covering method to allow for checking the truth of arbitrary non-linear arithmetic formulas, adding support for both quantifiers and Boolean structure. Furthermore, we also propose a variant to perform quantifier elimination on such formulas. After introducing the algorithm, we elaborate on various extensions, optimizations and heuristics. Finally, we present an experimental evaluation of our implementation and provide a comparison with state-of-the-art SMT solvers and quantifier elimination tools.

翻译：圆柱代数覆盖方法最初被提出用于判定一组非线性实算术约束的可满足性。我们对圆柱代数覆盖方法进行了重构与扩展，使其能够检验任意非线性算术公式的真值，新增了对量词与布尔结构的支持。此外，我们还提出了一种变体方法，用于对此类公式执行量词消元。在介绍算法后，我们详细阐述了多种扩展、优化与启发式策略。最后，我们展示了所实现系统的实验评估结果，并与当前最先进的SMT求解器及量词消元工具进行了比较。