有没有办法使用 z3 将公式转换为 CNF（使用 Tseitsin 样式编码）？我正在寻找类似simplify命令的东西，但保证返回的公式是 CNF。
问问题
3081 次
1 回答
4
您可以使用该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：
于 2012-06-12T08:19:30.610 回答