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

Question

我有两个文件,其内容相同,除了我放置断言的顺序:在一个文件中,断言按照另一个的相反顺序放置.第一个文件(po-9.z3)在不到一秒的时间内被Z3声明为不可用,而另一个(po.z3)在一分钟内无法验证.

造成这种差异的原因是什么？我假设将先前在验证中涉及的断言放在文件中会改善性能.但是,通过验证的那个(po-9.z3)在文件的底部有大多数相关/特定于问题的断言.另外,在po.z3中,虽然要证明的定理和假设位于文件的顶部,但是一个重要的断言(lambda表达式的一阶公式)放在文件的底部.当我把它带到顶部时,po.z3会在不到一秒的时间内完成验证.

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

Answer 1

造成这种差异的原因是什么？

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

DPLL的性能受到分支变量选择的严重影响.根据变量选择,存在运行时间恒定或指数的情况.

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