我当前正在使用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赛道上竞争并表现出色，但是我找不到用于该竞赛的细节论点。
您可以尝试" - finite-model-find"，可以在此处找到更多信息：SMT究竟是什么量化器完成的？
如果那不起作用，您可能想尝试查看SMT-COMP中使用的配置：https://www.starexec.org/starexec/secure/details/configuration.jsp?id=220723我首先在那里找到了该选项，然后向我指出了堆栈越过的问题。