SMT 究竟是针对哪些量词完成的？
Exactly what quantifiers is SMT complete for?
我一直在研究各种 SMT 求解器，主要是 Z3、CVC4 和 VeriT。他们都对自己用量词解决 SMT 问题的能力有模糊的描述。他们的文档主要基于示例 (Z3)，或由学术论文组成，描述可能会或可能不会实际实施的可能更改。
我知道一阶逻辑有可判定的片段，比如：
- 有限界量词
- 单子一阶逻辑
我想知道的是，FOL 的哪些（如果有）类 是各种 SMT 求解器保证完整的？我怎么知道我正在查看的问题是否在它们完整的片段中？
CVC4 完成的量化公式有两类。
(1) 有限域的量化公式。
CVC4 finite-model-complete 关于未解释排序的量词，这意味着如果存在一个模型，其中所有未解释排序都被解释为有限的，那么 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 支持的任何理论。如果理论是可判定的并且量化不涉及（无限）解释排序，那么 finite-model-completeness 保证仍然存在。
对于某些片段，例如Bernays-Schoenfinkel-Ramsey片段（EPR），该方法也是refutation-complete，这意味着对于该片段中任何无法满足的问题，CVC4最终都会回答"unsat" .
如果您对此功能感兴趣，默认情况下 CVC4 不会对输入问题使用有限模型查找。 command-line 选项“--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
冒着无助于不回答问题的风险，这个 material 很难找到是有原因的。
可决定性和 "actually can solve my specific problem in an amount of time I am willing to wait" 之间的 link 并没有那么强。因此，示例、基准集和实验结果通常是更好的指标（因此呈现）。
此外，大多数求解器在尝试求解之前都会进行大量启发式重写和问题处理。因此，表达可判定片段的经典句法方式并不总是适用，因为其他问题可以重写为可判定片段（希望不是相反，但我不能保证它永远不会发生！）。
最后，许多求解器使用启发式半决策程序，这些程序运行良好但很难用比代码更正式的东西来描述。因此，有些东西可能不会出现在任何已知的可判定片段中，但可以找到答案。
我一直在研究各种 SMT 求解器，主要是 Z3、CVC4 和 VeriT。他们都对自己用量词解决 SMT 问题的能力有模糊的描述。他们的文档主要基于示例 (Z3)，或由学术论文组成，描述可能会或可能不会实际实施的可能更改。
我知道一阶逻辑有可判定的片段，比如：
- 有限界量词
- 单子一阶逻辑
我想知道的是，FOL 的哪些（如果有）类 是各种 SMT 求解器保证完整的？我怎么知道我正在查看的问题是否在它们完整的片段中？
CVC4 完成的量化公式有两类。
(1) 有限域的量化公式。
CVC4 finite-model-complete 关于未解释排序的量词，这意味着如果存在一个模型，其中所有未解释排序都被解释为有限的，那么 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 支持的任何理论。如果理论是可判定的并且量化不涉及（无限）解释排序，那么 finite-model-completeness 保证仍然存在。
对于某些片段，例如Bernays-Schoenfinkel-Ramsey片段（EPR），该方法也是refutation-complete，这意味着对于该片段中任何无法满足的问题，CVC4最终都会回答"unsat" .
如果您对此功能感兴趣，默认情况下 CVC4 不会对输入问题使用有限模型查找。 command-line 选项“--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
冒着无助于不回答问题的风险，这个 material 很难找到是有原因的。
可决定性和 "actually can solve my specific problem in an amount of time I am willing to wait" 之间的 link 并没有那么强。因此，示例、基准集和实验结果通常是更好的指标（因此呈现）。
此外，大多数求解器在尝试求解之前都会进行大量启发式重写和问题处理。因此，表达可判定片段的经典句法方式并不总是适用，因为其他问题可以重写为可判定片段（希望不是相反，但我不能保证它永远不会发生！）。
最后，许多求解器使用启发式半决策程序，这些程序运行良好但很难用比代码更正式的东西来描述。因此，有些东西可能不会出现在任何已知的可判定片段中，但可以找到答案。