将公式转换为 CNF答案

【问题标题】：Convert formula to CNF将公式转换为 CNF
【发布时间】：2012-06-12 07:52:20
【问题描述】：

有没有办法使用 z3 将公式转换为 CNF（使用 Tseitsin 样式编码）？我正在寻找类似simplify 命令的东西，但要保证返回的公式是CNF。

【问题讨论】：

标签： z3

【解决方案1】：

您可以使用apply 命令来执行此操作。我们可以为这个命令提供任意的战术/策略。有关 Z3 4.0 中的战术和策略的更多信息，请查看教程http://rise4fun.com/Z3/tutorial/strategies

命令(help-tactic)可用于显示Z3 4.0中所有可用的战术及其参数。程序化使用更方便，更灵活。这是一个基于新 Python API 的教程：http://rise4fun.com/Z3Py/tutorial/strategies。 .Net 和 C/C++ API 中提供了相同的功能。

以下脚本演示了如何使用此框架将公式转换为 CNF：

http://rise4fun.com/Z3/TEu6

【讨论】：

太好了，谢谢！这正是我一直在寻找的。再说一句：还有没有办法让 z3 告诉我每个新变量 (k!0, k!1, ...) 代表的函数？还是我必须从 Tseitin 公理“逆向工程”？
不，我们不提供此信息。但是，Z3 会为每个预处理步骤生成一个“模型转换器”。模型转换器是将结果公式的模型转换为原始公式的模型的函数。对于 CNF 转换，模型转换器很简单。它只是删除了对新变量k!0、k!1、...的解释。因此，它没有提供您想要的信息。
好的，非常感谢。无论如何，从 Tseitin 公理重构新变量的函数似乎相当简单。
@LeonardodeMoura 最后一个链接坏了;(

【解决方案2】：

@Leonardo 提供的示例链接现在已损坏。使用回路机找到代码。将其发布在这里，以便未来的求职者可以使用它：

(declare-const x Int)
(declare-const y Int)
(declare-const z Int)

(assert (iff (> x 0) (> y 0)))
(assert (or (and (= x 0) (= y 0)) (and (= x 1) (= y 1)) (and (= x 2) (= y 2))))
(assert (if (> x 0) (= y x) (= y (- x 1))))
(assert (> z (if (> x 0) (- x) x)))
(apply (then (! simplify :elim-and true) elim-term-ite tseitin-cnf))

(echo "Trying again without using distributivity...")
(apply (then (! simplify :elim-and true) elim-term-ite (! tseitin-cnf :distributivity false)))

【讨论】：