问题描述
我一直在研究各种SMT求解器，主要是Z3，CVC4和VeriT.他们对用量词解决SMT问题的能力都有模糊的描述.他们的文档主要基于示例(Z3)，或由学术论文组成，描述了可能会或可能不会实际实施的更改.
I've been looking at various SMT solvers, mainly Z3, CVC4, and VeriT. They all have vague descriptions of their ability to solve SMT problems with quantifiers. Their documentation is primarily example based (Z3), or consists of academic papers, describing possible changes that may or may not actually be implemented.
我知道一阶逻辑存在可确定的片段，例如:
I know that there are decidable fragments of First-order logic, such as:
- 有限界量词
- 一元一阶逻辑
我想知道的是，各种SMT求解器可以保证完成哪些FOL类(如果有)?我怎么知道我要解决的问题是在完整的片段中?
What I'd like to know is, which (if any) classes of FOL are the various SMT solvers guaranteed to be complete for? How can I know whether a problem I'm looking at is in the fragments they are complete for?
推荐答案
CVC4完成了两类量化公式.
There are two categories of quantified formulas that CVC4 is complete for.
(1)具有有限域的量化公式.
(1) Quantified formulas with finite domains.
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支持的任何理论相结合.如果该理论是可判定的，并且量化不涉及(无限)解释的排序，那么保留有限模型完整性保证.
CVC4 is finite-model-complete on quantifiers over uninterpreted sorts, meaning that if there is a model where all uninterpreted sorts are interpreted as finite, then CVC4 will eventually find it. For details, you can see this paper:
http://homepage.divms.uiowa.edu/~ajreynol/tplp17.pdf
which summarizes the conference papers here:
http://homepage.divms.uiowa.edu/~ajreynol/cav13.pdf
http://homepage.divms.uiowa.edu/~ajreynol/cade24.pdf
Notice that these techniques combine with any theory supported by CVC4. Provided that the theory is decidable and the quantification does not involve (infinite) interpreted sorts, then the finite-model-completeness guarantee remains.
对于某些片段(例如Bernays-Schoenfinkel-Ramsey片段(EPR))，该方法也是完全驳斥的，这意味着对于该片段中任何无法满足的问题，CVC4最终都会回答不满意".
The approach is also refutation-complete for certain fragments, such as the Bernays-Schoenfinkel-Ramsey fragment (EPR), meaning that for any unsatisfiable problem in this fragment, CVC4 will eventually answer "unsat".
如果您对此功能感兴趣，则默认情况下，CVC4不会在输入问题上使用有限模型查找.命令行选项"--finite-model-find"将启用这些技术.
If you are interested in this feature, CVC4 will not by default use finite model finding on an input problem. The command-line option "--finite-model-find" will enable these techniques.
(2)一些理论中的量化公式发出了消除量词的功能.
(2) Quantified formulas in some theories that emit quantifier elimination.
例如，对于(纯)量化线性算术，CVC4是完整的.有关详细信息，请参见本文:
http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla .pdf
它建立在较早的会议论文的基础上:
http://homepage.divms.uiowa.edu/~ajreynol/cav15a.pdf
For example, CVC4 is complete for (pure) quantified linear arithmetic. For details you can see this paper:
http://homepage.divms.uiowa.edu/~ajreynol/fmsd17-instla.pdf
which builds upon an earlier conference paper:
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
This is similar in spirit to other approaches, for instance in Z3:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-qplay-lpar20.pdf
这篇关于SMT究竟要完成哪些量词?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！