z3 - SMT 到底是针对什么量词完成的？

Question

我一直在研究各种 SMT 求解器，主要是 Z3、CVC4 和 VeriT。他们对使用量词解决 SMT 问题的能力都有模糊的描述。他们的文档主要基于示例 (Z3)，或由学术论文组成，描述了可能实际实施或未实施的可能变化。

我知道一阶逻辑有可判定的片段，例如：

• 有界量词
• 一阶一阶逻辑

我想知道的是，哪些（如果有的话）FOL 类是保证完成的各种 SMT 求解器？我如何知道我正在查看的问题是否存在于它们完成的片段中？

Answer 1

CVC4 完成了两类量化公式。

(1) 有限域的量化公式。

CVC4 在未解释排序上的量词上是有限模型完备的，这意味着如果存在一个模型，其中所有未解释排序都被解释为有限，那么 CVC4 最终会找到它。详情可以看这篇论文：
http
://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf ，这里总结了会议论文：http:
//homepage.divms.uiowa.edu/~ajreynol/cav13 .pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
请注意，这些技术与 CVC4 支持的任何理论相结合。如果理论是可判定的并且量化不涉及（无限）解释排序，那么有限模型完整性保证仍然存在。

该方法对于某些片段也是完全反驳的，例如 Bernays-Schoenfinkel-Ramsey 片段 (EPR)，这意味着对于该片段中的任何无法满足的问题，CVC4 最终都会回答“unsat”。

如果您对此功能感兴趣，CVC4 默认不会对输入问题使用有限模型查找。命令行选项“--finite-model-find”将启用这些技术。

(2) 一些理论中的量化公式，它们发出量词消除。

例如，对于（纯）量化线性算术，CVC4 是完整的。有关详细信息，您可以查看这篇论文：
http
://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf ，它基于早期的会议论文：
http ://homepage.divms.uiowa.edu/~ajreynol /cav15a.pdf

这在精神上与其他方法相似，例如在 Z3 中：
https ://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-qplay-lpar20.pdf

Answer 2

冒着不回答问题的风险，很难找到这种材料是有原因的。

可决定性和“实际上可以在我愿意等待的时间内解决我的具体问题”之间的联系并不那么强烈。因此，示例、基准集和实验结果通常是更好的指标（因此被呈现）。

此外，大多数求解器在尝试求解之前都会进行大量启发式重写和问题处理。因此，表达可判定片段的经典句法方式并不总是适用，因为其他问题可以重写为可判定的问题（希望不是相反，但我不能保证它永远不会发生！）。

最后，许多求解器使用启发式半决策程序，这些程序运行良好，但很难用比代码更正式的方式来描述。因此，有些事情可能不会出现在任何已知的可判定片段中，但可以找到答案。