SMT量化算法的推理极限是什么？

Question

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

Answer 1

Pad是正确的,qe预处理器可能非常昂贵.此外,它在来自VCC,Poirot,Dafny,VeriFast,Why3和ESCJava2等软件验证工具的公式中无效.它无效,因为这些应用程序生成的公式还包含未解释的函数,数组等.

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

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

我刚刚提交了检测代码LIA(即使set-logic没有使用).该变更已在unstable(正在进行中)分支中提供.它将在明天的夜间版本和下一个正式版本中提供.

Answer 2

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

LIA，即普雷斯堡算术承认量词消除（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策略是应用最终游戏策略之前的预处理步骤smt。