SMT中量化算术的推理限制是什么？答案

【问题标题】：What are the limits of reasoning in quantified arithmetic in SMT?SMT中量化算术的推理限制是什么？
【发布时间】：2013-02-05 22:52:08
【问题描述】：

我在以下看似微不足道的基准测试中尝试了几种 SMT 求解器（CVC3、CVC4 和 Z3）：

(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat)
(exit)

求解器都返回未知数。我知道这是一个不可判定的片段（非线性），但我期待会有一些简单的实例化启发式方法可以解决它。我还尝试使用常量添加一些额外的断言，但它没有帮助。

有没有办法解决这些问题？SMT 中量化算术的推理限制是什么？

【问题讨论】：

标签： z3 smt cvc4

【解决方案1】：

您的示例属于线性整数算术 (LIA) 类别。

LIA 即Presburger Arithmetic 承认量词消除 (qe)，尽管 qe 过程的时间复杂度高得令人望而却步。

我不确定 CVC3 和 CVC4 是否支持 LIA 的量词消除，但在 Z3 中你可以做到

(set-logic LIA)
(set-info :smt-lib-version 2.0)
(assert (forall (( x Int)) (forall ((y Int)) (= y x))))
(check-sat-using (then qe smt))

从Rise4Fun execution，我得到unsat 结果。

这里的qe 策略是应用终局策略smt 之前的预处理步骤。

【讨论】：

【解决方案2】：

Pad 是正确的，qe 预处理器可能相当昂贵。此外，它对来自软件验证工具的公式无效，例如VCC、Poirot、Dafny、VeriFast、Why3 和ESCJava2。它没有效果，因为这些应用程序生成的公式还包含未解释的函数、数组等。

正如 Pad 的回答所暗示的，Z3 是引擎的集合。它提供 API 和命令，允许用户选择将使用哪个引擎（或引擎组合）来解决问题。当用户只是说(check-sat) 时试图猜测解决输入公式的最佳引擎是什么。猜测基于输入公式的结构和用户提供的注释（例如：set-logic 命令）。我们正在不断扩展自动检测的片段集，以及我们提供的引擎集。

话虽如此，令人尴尬的是Z3错过了LIA这样的片段并且没有自动对其应用qe过程。对于LIA 公式，qe 通常是最佳选择。基于 E-matching 或 MBQI 的替代方案无效，因为它们适用于完全不同的片段。

我只是检测到LIA 的committed code（即使没有使用set-logic）。 unstable (working-in-progress) 分支中已经提供了更改。它将在明天的夜间版本和下一个正式版本中提供。

【讨论】：