如何将公式转换为析取范式? [英] How to convert a formula to Disjunctive Normal Form?

问题描述

说给定一个公式

(t1>=2 或 t2>=3) 和 (t3>=1)

(t1>=2 or t2>=3) and (t3>=1)

我希望得到它的析取范式(t1>=2 and t3>=1) 或 (t2>=3 and t3>=1)

I wish to get its disjunctive normal form (t1>=2 and t3>=1) or (t2>=3 and t3>=1)

如何在 Z3 中实现这一点?

How to achieve this in Z3?

推荐答案

Z3 没有用于将公式转换为 DNF 的 API 或策略.但是，它支持使用策略 split-clause 将目标分解为多个子目标.给定 CNF 中的输入公式，如果我们详尽地应用这种策略，每个输出子目标都可以被视为一个大连接.这是有关如何执行此操作的示例.

Z3 does not have an API or tactic for converting formulas into DNF. However, it has support for breaking a goal into many subgoals using the tactic split-clause. Given an input formula in CNF, if we apply this tactic exhaustively, each output subgoal can be viewed as a big conjunction. Here is an example on how to do it.

http://rise4fun.com/Z3/zMjO

命令如下:

(apply (then simplify (repeat (or-else split-clause skip))))

repeat 组合子不断应用策略，直到它不执行任何修改.如果输入没有子句，策略 split-clause 将失败.这就是为什么我们使用 or-else 组合器和 skip(什么都不做)策略.我们可以通过在每个子句拆分为案例后使用应用简化的策略(例如，simplify、solve-eqs)来改进命令.

The repeat combinator keeps applying the tactic until it does not perform any modification. The tactic split-clause fails if the input does not have a clause. That is why we use an or-else combinator with the skip (do nothing) tactic. We can improve the command by using tactics that apply simplifications (e.g., simplify, solve-eqs) after each clause is split into cases.

请注意，上面的脚本假设输入公式为 CNF.

Note that, the script above assumes the input formula is in CNF.

这篇关于如何将公式转换为析取范式?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！