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在默认情况下不会使用有限模型查找输入问题。命令行选项“有限模型查找”将启用这些技术。

(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

冒着无济于事不回答问题的风险，我们有理由很难找到这种材料。

决定能力和“实际上可以在我愿意等待的时间内解决我的具体问题”之间的联系并不是很强。因此，例子、基准集和实验结果往往是一个更好的指标(并由此提出)。

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

最后，许多求解者使用启发式半决策过程，它们工作得很好，但很难用比代码更正式的方式来描述。因此，有些东西可能不会出现在任何已知的可判定片段中，但可以找到答案。