Z3的搜索时间对公式顺序敏感吗？

Question

在许多编程语言中，分支效率取决于提供子句的顺序。例如，在 Python 中，

if p or q :

将在p 评估为真时立即分支到 if 语句，因此首先提供计算量少的子句通常是个好主意。我想知道 Z3 中的可满足性检查是否也是如此。换句话说，检查And(P, Q) 和And(Q, P) 有什么区别，前提是其中一个公式比另一个复杂得多？

Answer 1

是的，您指定子句的顺序会有所不同。然而，当涉及到 Z3 时，重新排列子句可能不会有什么好处。此外，事先确定一个通用的“最佳顺序”可能很困难（而且可能不值得花时间）。

对于其他 SMT 求解器，我以一种极端的方式观察到您所描述的内容。对于某些求解器，它可以决定计算的成败，因为我已经看到某些情况下，当子句以一个顺序呈现时求解器会超时，但当相同的子句以不同的顺序呈现时，它会迅速找到解决方案.但是，对我来说，这表明求解器设计不佳。 Z3 和其他现代 SMT 求解器（例如 CVC4）比旧的或不太健壮的 SMT 求解器更不容易受到此类问题的影响。

关于实际找到最佳排序，对于 SMT 求解器而言，构成“计算轻量级”或“更复杂”的要素与传统计算机语言不同。真正重要的是连词中的某个子句是否可能导致冲突，或者析取词中的某个特定子句是否可能导致解决方案。这类似于试图从迷宫中找到出路——如果你早早转错了方向，那么你可能会在死胡同之前花费很长时间，然后才最终决定回到起点并采取不同的方式分支。同样，现代 SMT 和 SAT 求解器具有缓解此问题的技术。

另外，当谈到 Z3 时，如果 Z3 可以通过按照一些人类可理解和通用的复杂性度量对子句进行排序来提高实际应用程序的效率，那么这可能已经添加为前-处理步骤到 Z3。通常，对于涉及多个因素（例如 Z3 实现的细节）的复杂优化问题，您必须尝试多种方法，并针对与您的应用程序相关的一组测试示例进行基准测试。

作为我上述一些主张的一点证据，我写了这个 SMT 问题的小例子：

(declare-fun p () Int)
(declare-fun q () Int)
(declare-fun n () Int)
(assert (> p 1))
(assert (> q 1))
(assert (and (= n 18679565357) (= n (* p q))))
(check-sat)
(get-value (p q n))
(exit)

在and 语句中交换子句的顺序对我的系统几乎没有影响（小于 1%）。如果我将其分解为两个单独的断言，那么差异会更大，但要知道这种差异是否普遍存在（针对此类的不同 SMT 问题），我必须运行一个具有许多此类问题的基准测试套件。