z3 - Z3 中断言顺序的重要性是什么？

Question

我有两个文件，除了放置断言的顺序外，它们的内容完全相同:在一个文件中，断言的放置顺序与另一个文件相反。第一个文件 (po-9.z3) 在不到一秒的时间内被 Z3 声明为无法满足，而另一个 (po.z3) 在一分钟内无法验证。

造成这种差异的原因可能是什么？我假设将验证中涉及的断言放在文件的较早位置会提高性能。然而，通过验证的那个 (po-9.z3) 在文件底部有大部分相关/问题特定的断言。此外，在 po.z3 中，虽然要证明的定理和假设位于文件顶部，但一个重要的断言(lambda 表达式的一阶公式)位于文件底部。当我将它带到顶部时，po.z3 会在不到一秒的时间内进行验证。

在 z3 smt2 文件中生成断言的最佳顺序是什么？

Answer 1

What could be the reason for this difference?

SMT 求解器实现 DPLL(T) 算法，该算法是 DPLL 过程和决策过程(的变体)的组合。

DPLL 的性能在很大程度上受分支变量选择的影响。根据变量的选择，存在运行时间为常数或指数的情况。

如果两个公式在逻辑上是等价的(需要仔细检查)，那么我认为唯一的可能是，两个公式中的顺序不同导致变量选择的顺序不同，最终导致性能差异.