使用 Python z3 API 简化方程答案

【问题标题】：Simplifying Equations with Python z3 API使用 Python z3 API 简化方程
【发布时间】：2019-10-23 16:34:23
【问题描述】：

我正在尝试学习如何在 Python z3 API 中使用表达式来完成一些事情。

我希望能够简化/减少包含中间变量的方程组。假设我有方程(A = B && C) 和(C = D || E)。在 z3 中，这些将表示为 (Bool('A') == And(Bool('B'), Bool('C')) 和 (Bool('C') == Or(Bool('D'), Bool('E'))。是否有一些函数或一系列函数可用于生成简化和简化方程(A = B && (D || E))？
我希望能够将 z3 表达式转换为乘积之和形式（即 Or(minterm1, minterm2,...)。
一种确定两个布尔方程逻辑等价的有效方法。
一种将布尔方程作为格式化字符串返回的方法（即不在用于声明函数的嵌套函数形式中。）

如果有人对这些项目有任何见解，我们将非常感谢您的意见。另外，如果需要进一步说明需要什么，请告诉我。

谢谢，

【问题讨论】：

标签： python logic z3 solver z3py

【解决方案1】：

好问题。

不，一般来说不是。您可以使用 z3 来简化方程式，但您对“简单”的概念不太可能与其内部目的所认为的简单相匹配。人们经常要求这个功能，但它通常是一个非常困难的问题，并不清楚简单是什么意思。话虽如此，z3 确实有Goal 和Tactic 的概念，您甚至可以使用simplify 策略。它会简化公式，但让它完全按照您希望它的方式运行是愚蠢的差事。

查看这个关于战术的重要资源，也许您可以四处寻找适合您的东西：http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm
我相信，简化策略确实有一个som 选项。这可能会奏效。同样，请参阅上面的链接，其中有示例：
```
s = Then(With('simplify', arith_lhs=True, som=True),
     'normalize-bounds', 'lia2pb', 'pb2bv', 
     'bit-blast', 'sat').solver()
```
nugget som=True 告诉求解器使用 sum-of-minterms。同样，您的里程可能会因公式的确切结构而异，并且 z3 可能会引入可能会破坏目的的新名称。
绝对！这就是z3擅长的。只需断言f != g 其中f 和g 是您的方程式。如果 z3 显示 unsat，那么您知道它们对于所有变量赋值都是等价的。如果它给了你一个模型，那就是它们等价的反例。（否定相等技巧在 SMT 求解中非常常见：当它的否定不能满足时，公式就是重言式。所以，你可以断言你想要的否定，看看它是否返回 unsat。）

请注意，这是 SMT（和 SAT）求解器擅长的。
对于您构建的任何公式f，您可以发出print f，它会打印出来。但正如您可能已经观察到的那样，它不会看起来像您的教科书逻辑公式。漂亮的打印机有一些选项来控制它的行为，但它可能不是你想要的。

但是，API 提供了沿 AST 遍历并根据需要提取节点的功能。因此，如果您愿意，您可以编写自己的漂亮打印机。这样做并不是非常困难，但这并不意味着它很简单：有很多情况需要考虑，根据我的经验，这样的打印机通常并不难欺骗；即，对于输入的微小变化会产生更糟糕的结果。

从实用的角度来看，虽然 z3 及其在 Python、C、Java 等中的高级 API 能够做任何你想做的事情，但除了 #3 之外，它不会是开箱即用的.我的建议是自己编写其他所有代码，并依靠 z3 来检查它擅长的相等性。当然，这完全取决于您要做什么。祝你好运！

【讨论】：