我正在尝试优化使用 Z3 来证明有关一阶理论的事实。目前，我在 Python 中指定了一个一阶理论，将量词固定在那里，并将所有子句连同证明目标的否定一起发送到 Z3。我有以下想法，希望可以优化结果：我只想将与证明目标相关的理论公式发送到 Z3。我不会详细讨论这个概念，但我认为直觉很简单：我的理论是公式的合取，我只想发送可能影响证明目标真值的合取。
我的问题是：这是否会导致效率的提高，或者 Z3 是否已经使用了类似的方法？我猜不会，因为我不认为 Z3 总是假设最后一个断言是证明目标，所以它没有办法对此进行优化。
是的，删除不相关的事实可以产生很大的不同。假设我们有一个形式为 的不可满足的公式F_1 and F_2 and (not G)。此外，让我们假设它F_1 and (not G)是不可满足的，并且F_2是可满足的。F_2就是你所说的无关紧要。如果在将配方发送到 Z3 之前有一种便宜的方法可以去除F_2，它可能会产生很大的不同。
Z3 具有“忽略”不相关事实的启发式方法，但它们只是启发式方法。对于我们的示例，最坏的情况是F_2Z3 很难满足的情况。Z3 本质上是在尝试构建满足输入公式（F_1 an F_2 and (not G)我们工作示例中的公式）的解释/解决方案。当 Z3 可以表明不可能建立解释时，公式是不可满足的。在实践中，该公式F_2对于 Z3 无关紧要，前提是它可以快速表明它是可满足的，并且对于 的解释/解决方案F_2不冲突F_1 and (not G)。如果不是这样，Z3 会浪费大量资源F_2。