0

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

(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

4

1 回答 1

2

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

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

于 2020-11-28T01:32:53.990 回答