将公式转换为 CNF [英] Convert formula to CNF

问题描述

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

Is there a way to use z3 to convert a formula to CNF (using Tseitsin-style encoding)? I am looking for something like the simplify command, but guaranteeing that the returned formula is CNF.

推荐答案

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

You can use the apply command for doing it. We can provide arbitrary tactics/strategies to this command. For more information about tactics and strategies in Z3 4.0, check the tutorial http://rise4fun.com/Z3/tutorial/strategies

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

The command (help-tactic) can be used to display all available tactics in Z3 4.0 and their parameters. The programmatic is more convenient to use and flexible. Here is a tutorial based on the new Python API: http://rise4fun.com/Z3Py/tutorial/strategies. The same capabilities are available in the .Net and C/C++ APIs.

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

The following script demonstrates how to convert a formula into CNF using this framework:

http://rise4fun.com/Z3/TEu6

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