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

【问题标题】：What is the importance of the order of the assertions in Z3?Z3 中断言顺序的重要性是什么？
【发布时间】：2014-06-21 21:58:37
【问题描述】：

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

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

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

【问题讨论】：

标签： z3

【解决方案1】：

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

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

DPLL 的性能在很大程度上受分支变量选择的影响。有些情况下，运行时间是常数或指数取决于变量的选择。

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

【讨论】：

谢谢，很高兴知道。有什么方法可以预测订单的影响吗？换句话说，既然我生成了 z3 文件，我该如何选择断言的顺序，以最大限度地提高 z3 在简单输入时不会经常超时的机会？
变量选择是一种启发式方法，通常包括随机性。所以我不知道如何让你的公式更容易用于 z3。您可能想查看 z3.codeplex.com/SourceControl/latest#src/sat/sat_solver.cpp 中的函数 solver::next_var() ，了解启发式是如何工作的。
你能帮我找出数字（0到num_vars()）和变量“名称”之间的映射吗？实际上，我正在尝试更改 smt_case_split_queue.cpp 中的类似代码。