Quantified Linear and Polynomial Arithmetic Satisfiability via Template-based Skolemization

📄 arXiv: 2412.16226v1 📥 PDF

作者: Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Harshit J Motwani, Maximilian Seeliger, Đorđe Žikelić

分类: cs.LO, cs.AI

发布日期: 2024-12-18

备注: Accepted at AAAI 2025

💡 一句话要点

提出基于模板的Skolem化方法，高效解决量化线性/多项式算术公式的可满足性问题

🎯 匹配领域: 支柱一：机器人控制 (Robot Control)

关键词: 量化公式 可满足性问题 Skolem化 量词消除 线性实数算术 非线性实数算术 Positivstellensätze 模板方法

📋 核心要点

  1. 量化LRA/NRA公式可满足性问题在AI和程序分析等领域有广泛应用，但现有方法在量词消除步骤计算开销巨大。
  2. 论文提出基于模板的Skolem化方法，利用代数几何中的Positivstellensätze定理，自动合成Skolem函数以消除量词。
  3. 实验结果表明，该方法在LRA和NRA基准测试中，相比现有SMT求解器，在求解实例数量和运行时间上均有显著提升。

📝 摘要（中文）

本文提出了一种新的方法，用于高效地消除量化线性实数算术(LRA)和非线性实数算术(NRA)公式中的量词。该方法采用基于模板的Skolem化方法，自动合成线性/多项式Skolem函数，从而消除公式中的量词。该方法的核心技术在于代数几何中的Positivstellensätze定理，它能够高效地处理多项式不等式。该方法在理论上具有良好的性质，并且在实践中表现出色。理论上，该方法是可靠的、半完备的，并且在亚指数时间和多项式空间内运行，而现有的可靠且完备的量词消除方法则在双指数时间和至少指数空间内运行。在实践方面，实验表明，在LRA和NRA基准测试中，该方法在已解决实例的数量和运行时间方面均优于最先进的SMT求解器。

🔬 方法详解

问题定义：论文旨在解决量化线性实数算术(LRA)和非线性实数算术(NRA)公式的可满足性问题。现有方法的主要痛点在于量词消除步骤的计算复杂度过高，通常需要双指数时间和至少指数空间，限制了其在实际问题中的应用。

核心思路：论文的核心思路是采用基于模板的Skolem化方法来高效地消除量词。Skolem化通过引入Skolem函数来替换量词，将量化公式转化为无量词公式。关键在于如何有效地找到合适的Skolem函数。论文利用预定义的模板（线性或多项式函数）来限制Skolem函数的搜索空间，从而降低了搜索的复杂度。

技术框架：整体流程如下：1) 输入量化的LRA/NRA公式；2) 根据公式的结构，选择合适的Skolem函数模板（线性或多项式）；3) 利用Positivstellensätze定理，将量词消除问题转化为求解多项式不等式组的问题；4) 使用优化技术（如半定规划）求解多项式不等式组，得到Skolem函数的具体参数；5) 将求解得到的Skolem函数代入原公式，消除量词，得到无量词公式；6) 使用现有的SMT求解器验证无量词公式的可满足性。

关键创新：最重要的技术创新点在于将模板化的Skolem函数与Positivstellensätze定理相结合。传统的Skolem化方法需要搜索整个函数空间，而模板化方法大大缩小了搜索空间，提高了效率。Positivstellensätze定理提供了一种有效的方法来处理多项式不等式，使得量词消除过程更加高效。与现有方法的本质区别在于，该方法避免了昂贵的完全量词消除过程，而是通过求解多项式不等式来寻找合适的Skolem函数。

关键设计：Skolem函数的模板选择是关键设计之一，需要根据公式的结构选择合适的模板，以保证Skolem化后的公式仍然能够表达原公式的语义。Positivstellensätze定理的具体应用也需要仔细设计，需要选择合适的证书（certificates）来保证求解的正确性和效率。此外，求解多项式不等式组的优化算法的选择也会影响整体性能。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

实验结果表明，该方法在LRA和NRA基准测试中，显著优于最先进的SMT求解器。在已解决的实例数量上，该方法比现有求解器提高了XX%（具体数据未在摘要中给出，此处用XX%代替）。在运行时间上，该方法也比现有求解器缩短了YY%（具体数据未在摘要中给出，此处用YY%代替）。这些结果表明，该方法在实际应用中具有很强的竞争力。

🎯 应用场景

该研究成果可广泛应用于人工智能、程序分析、形式验证等领域。例如，在AI中，可用于解决涉及量化约束的规划和推理问题；在程序分析中，可用于验证程序的正确性和安全性；在形式验证中，可用于验证硬件和软件系统的正确性。该方法能够提高这些应用中相关问题的求解效率，推动相关领域的发展。

📄 摘要（原文）

The problem of checking satisfiability of linear real arithmetic (LRA) and non-linear real arithmetic (NRA) formulas has broad applications, in particular, they are at the heart of logic-related applications such as logic for artificial intelligence, program analysis, etc. While there has been much work on checking satisfiability of unquantified LRA and NRA formulas, the problem of checking satisfiability of quantified LRA and NRA formulas remains a significant challenge. The main bottleneck in the existing methods is a computationally expensive quantifier elimination step. In this work, we propose a novel method for efficient quantifier elimination in quantified LRA and NRA formulas. We propose a template-based Skolemization approach, where we automatically synthesize linear/polynomial Skolem functions in order to eliminate quantifiers in the formula. The key technical ingredients in our approach are Positivstellensätze theorems from algebraic geometry, which allow for an efficient manipulation of polynomial inequalities. Our method offers a range of appealing theoretical properties combined with a strong practical performance. On the theory side, our method is sound, semi-complete, and runs in subexponential time and polynomial space, as opposed to existing sound and complete quantifier elimination methods that run in doubly-exponential time and at least exponential space. On the practical side, our experiments show superior performance compared to state-of-the-art SMT solvers in terms of the number of solved instances and runtime, both on LRA and on NRA benchmarks.