问将公式转换为CNF
EN

Stack Overflow用户

提问于 2012-06-12 15:52:21

回答 1查看 3K关注 0票数 4

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

回答已采纳

发布于 2012-06-12 16:19:31

您可以使用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

票数 4

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/10992531

复制

相似问题

问将公式转换为CNFEN