使用 Z3 进行的简化并没有像预期的那样简化

Question

在我的应用程序中，我想使用 Z3 求解器简化公式。我知道普通的

simplify

策略不够强大，所以我使用

ctx-solver-simplify

。然而，即使这种策略也没有像我希望的那样简化。特别是在涉及不平等的情况下。

假设我有一个公式

b > 1 || b > 2

，即

(declare-const b Real)

(assert (or (> b 1.0) (> b 2.0)))

(apply ctx-solver-simplify)

这显然相当于

b > 1

，但 Z3 返回

(or (not (<= b 1.0)) (> b 2.0))

。 但是，如果子句交换，即

(assert (or (> b 2.0) (> b 1.0)))

，Z3 将按预期返回

(> b 1.0)

。我不明白为什么这个顺序在这里相关。

此外，如果添加另一个子句，比如

(declare-const a Bool)
(declare-const b Real)

(assert (or a (> b 2.0) (> b 1.0)))

(apply ctx-solver-simplify)

即使交换顺序也不会导致简化的结果。事实上，Z3根本没有修改公式。但如果

a

位于末尾，

(assert (or (> b 2.0) (> b 1.0)) a)

，这实际上再次起作用，我们得到

(> b 1.0)

。

我在这里遗漏了什么还是我使用了错误的策略？为什么子句的顺序会有所不同？我使用的是4.12.2版本。预先感谢。

Answer 1

不幸的是，简短的答案是，z3 不是一个用来简化此类术语的好工具。它并不是为执行此类任务而设计的，一般的 SMT 求解策略也不允许使用求解器来执行任意简化。

搜索 https://stackoverflow.com/search?q=%5Bz3%5D+simplify 将向您展示无数问题/答案，讨论如何将 z3 用作简化器。为了更广泛地了解问题，值得仔细阅读它们。

长话短说，z3 认为的“简单”和我们（作为人类）认为的“简单”不一定匹配。虽然 z3 确实提供了战术、策略、探测等来允许一定程度的控制，但这些机制很脆弱。 （即，从版本到版本，不能保证它们的行为。）您可能需要查看 https://microsoft.github.io/z3guide/programming/Example%20Programs/Formula%20Simplification/.

如果您想要代数简化，SymPy 也可能是一个不错的选择。 （https://docs.sympy.org/latest/tutorials/intro-tutorial/simplification.html）。如果您还需要通用的SMT解决能力，可以将两个系统串联使用；但这既不自动化也不易于使用。 （如果您的公式仅具有特定的形状，则可能可以将其中的一些自动化；但一般来说，支持任意构造是一个难题。）