8

我在以下看似微不足道的基准测试中尝试了几个 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 中量化算术的推理限制是什么？

4

2 回答 2

9

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

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

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

我刚刚提交了检测代码LIA（即使set-logic未使用）。该更改已在unstable（工作中）分支中可用。它将在明天的夜间版本和下一个正式版本中提供。

于 2013-02-20T22:01:52.670 回答
2

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

LIA 即Presburger 算术承认量词消除 (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 执行，我得到了unsat结果。

这里的qe策略是应用 end-game tactic 之前的预处理步骤smt。

于 2013-02-20T19:39:55.797 回答