Z3 中断言顺序的重要性是什么? [英] What is the importance of the order of the assertions in Z3?

问题描述

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

I have two files whose content is identical except for the order in which I placed the assertions: in one file, the assertions are placed in the reverse order of the other. The first file (po-9.z3) is declared unsatifiable by Z3 in less than a second while the other (po.z3) cannot be verified within a minute.

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

What could be the reason for this difference? I assumed that placing the assertions that will be involved in the verification earlier in the file would improve performances. However, the one that passes verification (po-9.z3) has most of the relevent / problem specific assertions at the bottom of the file. Also, in po.z3, while the theorem to be proved and the assumptions are at the top of the file, one important assertion (a first order formulation for a lambda expression) is put at the bottom of the file. When I bring it to the top, po.z3 verifies within less than a second.

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

What would be the best order for me to produce the assertions in a z3 smt2 file?

推荐答案

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

What could be the reason for this difference?

SMT 求解器实现 DPLL(T) 算法，它是 DPLL 程序和决策程序(的变体)的组合.

SMT solvers implement DPLL(T) algorithm, which is a combination of (a variant of) the DPLL procedure and decision procedures.

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

Performance of DPLL is heavily affected by the choice of variables for branching. There are the cases of which the running time is constant or exponential depending on variable selection.

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

If the two formulas are logically equivalent (you need to double-check), then I think the only possibility is that, the different order in the two formulas leads to different order in variable selection, which eventually leads to difference in performance.

这篇关于Z3 中断言顺序的重要性是什么?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！