我有两个文件，除了放置断言的顺序之外，其内容相同：在一个文件中，断言的放置顺序与另一个文件的顺序相反。第一个文件（po-9.z3）在不到一秒的时间内被 Z3 声明为不可满足，而另一个文件（po.z3）在一分钟内无法验证。
造成这种差异的原因是什么？我认为将验证中涉及的断言放在文件的前面会提高性能。但是，通过验证的文件 (po-9.z3) 在文件底部具有大部分相关/问题特定的断言。另外，在 po.z3 中，虽然要证明的定理和假设位于文件的顶部，但一个重要的断言（lambda 表达式的一阶公式）却放在文件的底部。当我将其置于顶部时，po.z3 会在不到一秒的时间内进行验证。
在 z3 smt2 文件中生成断言的最佳顺序是什么？
造成这种差异的原因是什么？
SMT 求解器实现 DPLL(T) 算法，该算法是 DPLL 过程和决策过程（的变体）的组合。
DPLL 的性能很大程度上受分支变量选择的影响。在某些情况下，根据变量的选择，运行时间是恒定的或指数的。
如果两个公式在逻辑上是等价的（需要仔细检查），那么我认为唯一的可能是，两个公式中的顺序不同导致变量选择的顺序不同，最终导致性能的差异。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
