Z3 布尔表达式简化答案

【问题标题】：Z3 Boolean Expression SimplificationZ3 布尔表达式简化
【发布时间】：2020-11-26 12:48:45
【问题描述】：

试图简化这个布尔表达式。

(not (and (or (not e) (not f) (not h))
          (or (not f) (not h) d)
          (or (not e) (not h) c)
          (or (not h) d c)
          (or (not e) (not f) (not g) a)
          (or (not f) d (not g) a)
          (or (not e) (not f) a i)
          (or (not f) d a i)
          (or (not e) c (not g) a)
          (or d c (not g) a)
          (or (not e) c a i)
          (or d c a i)
          (or (not e) (not f) a b)
          (or (not f) d a b)
          (or (not e) c a b)
          (or d c a b)))

这应该简化为这样的 cnf 形式的布尔表达式。

(and 
(or (not a) h)
(or (not b) (not i) g h)
(or (not c) f)
(or (not d) e))

我一直在尝试通过使用 "ctx-solver-simplify" 和 "tseitin-cnf" 策略来实现这一目标。如果仅应用 "ctx-solver-simplify"，则不会对这种情况执行简化。当then("tseitin-cnf", "ctx-solver-simplify") 应用这两种策略时，会返回一个包含大量辅助变量的结果。这也不是预期的简化形式。

有没有办法将此表达式简化为预期的输出？

编辑：在 Z3 github repo 中提出了同样的问题，并得到了非常好的工作响应。这就是问题所在。

https://github.com/Z3Prover/z3/issues/4822

【问题讨论】：

标签： z3 boolean-logic boolean-expression cnf

【解决方案1】：

Z3 的简化引擎不是解决这类问题的好选择。它确实会“简化”表达式，但它几乎永远不会匹配人类认为简单的表达式。许多“明显”的简化将不会被应用，因为从 SAT 求解器的角度来看，它们根本无关紧要。您可以在 stack-overflow 中搜索许多类似的问题，虽然 z3 策略可以起到很好的效果，但它们并不是为您想要做的事情而设计的。

如果您正在寻找“最小”（在启发式意义上）简化，您应该查看其他工具。例如，sympy 带有一组例程，可以很好地转换为规范形式和简化：https://stackoverflow.com/a/64626278/936310

【讨论】：