CVC4:用量词在bools上合成函数的设置？

Question

我目前正在使用CVC4来解决以下形式的公式：

exists f1, ..., fn . P(f1, ..., fn) /\ forall (b1...bk) . Q(f1,...fn,b1,...bk)

在这里，f1...fn是从一定数量的Bool到Bool的函数，而b1...bk是布尔值。

我的问题完全归结于SMT的UF片段:它有量词，但除了函数和布尔值之外，没有其他类型。

当我尝试使用CVC4上的默认设置时，它会立即返回未知，尽管我的所有量化都是在有限域上进行的。

问题是，CVC4有很多处理量词的选项:有一堆cegqi，一堆fmf，还有mbqi等等。我的印象是，这些都是从特定的研究项目中添加出来的，我不想读20篇不同的论文，只是为了解决这个问题。

我的问题：是否有一套解决这类问题的推荐方案？

我知道CVC4是有可能的，因为他们在SMT比赛的UF轨道上表现得很好，但是我找不到用于那场比赛的具体论据。

Answer 1

您可以尝试“--有限模型-查找”，在这里可以找到更多的信息：SMT到底用于什么量词？。

如果这不起作用，您可能想试着查看stack：https://www.starexec.org/starexec/secure/details/configuration.jsp?id=220723中使用的配置，我首先在那里找到了选项，然后向我指出了堆栈溢出问题。