转换公式CNF(Convert formula to CNF)

有没有办法使用Z3（使用Tseitsin式编码）转换成一个公式来CNF的方法吗？ 我在寻找类似的simplify命令，但保证返回的公式为CNF。

Answer 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

文章来源: Convert formula to CNF