Z3 布尔表达式简化

Question

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

(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

Answer 1

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

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