问题标签 [cnf]

我有一个清单：

我需要输出到 CNF 格式的文件（'output.txt'），如下所示：

那我现在该怎么办？

我想将公式转换为 CNF。有图书馆可以做到这一点吗？这是我的代码。我创建了许多函数来将任何（a 或 b）转换为 CNF 格式。

但是如果有很多命题，那就很难像 (a > b) & (c & d) or not(f) ..

这是我的代码：

而不是input =(a,b)打电话Equivalent function我想输入(a=b)。我怎样才能做到这一点？我试图控制元素之前和下一个，=并在您输入（a = b）时将其添加到Equivalent功能中，输出应该是(a|~b)&(b|~a)但它不起作用。

我正在尝试解决一个简单的练习，我必须在 CNF 中转换一个命题句：

这是句子： P => (Q <=> R)

根据解析规则，我做的第一件事是以这种方式消除 <=> 符号：

P => (Q <=> R) ---> P => (QVR) /\ (RVQ)

然后我删除了 => 符号：

P => (QVR) /\ (RVQ) ------> ¬PV (QVR) /\ (RVQ)

所以我的解决方案是：(¬PVQVR) /\ (¬PVRVQ)

而右边的是：(¬PV ¬QVR) /\ (¬PV ¬RVQ)

谁能帮我理解我哪里出错了？

我正在尝试在 mysql 中使用 cat /etc/my.cnf 但是当我这样做时，它只是显示->希望我继续输入。

但是，当我在末尾加上分号时。

猫 /etc/my.cnf;

它抛出一个错误。

如何编辑 /etc/my.cnf 文件？

我在 Mac 上的终端上运行它，并使用命令进入 mysql 服务器

sudo /usr/local/mysql/bin/mysql -u root

.

我有一个学校项目，我必须使用 SAT Solver 找到游戏“Lights Out”（https://en.wikipedia.org/wiki/Lights_Out_(game)）的解决方案，但我在尝试设置连接词时遇到了麻烦游戏的正常形式。

游戏由 5 x 5 的灯光网格组成。按下任何一个灯都会切换它和四个相邻的灯。谜题的目标是关掉所有的灯。

到目前为止我是如何尝试的：

对于 3x3 网格（开始），我设置了 9 个术语（每个按钮），因此：

C11 : 位置 1,1 的按钮变亮 C12 : 位置 1,2 的按钮变亮 C13 : 位置 1,3 的按钮变亮。[...]

由于 1,1 处的按钮熄灭 1,2 和 2,1 位置处的按钮

我做了 C11 => C12 和 C21 1,2 处的按钮熄灭了位置 1,1 和 1,3 和 2,2 我做了 C12 => C11 和 C13 和 C22

并继续另一个：

然后我只是将这些转换为 CNF 以获得 sat 求解器所需的子句，但似乎我做错了..

谁能帮我把这个游戏写成 CNF 形式？

非常感谢 ！

如果您需要更好地理解它，这里是游戏：

https://www.geogebra.org/m/JexnDJpt#material/KArehWn8

我编写了一个脚本，它读取 .cnf 文件，分析一些内容，然后输出一些结果（通过print()）。为了读取 .cnf 文件，我使用以下行：

现在，如果我在 Spyder 环境（Python 3.6）中运行它，一切正常。脚本读取 config.cnf，执行操作并输出结果。如果我在 Linux 上运行完全相同的脚本（config.cnf 位于同一目录中），则会显示以下错误消息：

我使用以下命令：

我是 Python 和 Linux 的新手，所以如果这是一些基本错误，请不要厌倦。谢谢你。

我试图编译一个名为 CADET 的 QBF 求解器工具。CADET 只能解决 QDIMACS 的格式类型。

克隆存储库并安装工具后，只需一个简单的命令即可。./cadet <filename>.qdimacs需要执行该文件。给出了错误的照片和 QDIMACS 文件。

这是 .qdimacs 文件代码

这是我在执行期间收到的警告：

我正在做一个项目，我必须读取一个表示图形的文件。我使输入文件看起来像这样：

所以每一行都代表一个节点。例如，第一行是连接到b 和c 的节点a，第二行是连接到a、c 和d 的节点b。所以我不确定从哪里开始。我知道我们需要一堆 if 和 else 语句，以便共享一条边的两个节点不能具有相同的颜色，并且每个节点应该至少具有一种颜色。但是，我怎样才能创建节点变量本身，因为文本文件可以包含任意数量的节点。我知道我必须为一堆 if 和 else 语句做些什么，但我不知道如何使用它来将其简化为 miniSAT 格式，例如：

其中第一个“3”代表变量的数量，第二个 3 代表子句的数量。其他行由不同的变量组成，每个不同的数字都是它自己的变量，如果它是正的，那么它是真的，否则是假的

我真正想做的是将布尔表达式转换为整数线性规划约束。我试图首先将表达式转换为 CNF（使用pyeda），然后从 CNF 形成约束（因为这非常简单）。但是，我无法理解.to_ast()函数输出的抽象语法树。例如，在.to_ast()表达式上运行时(~C1 | ~P1 | ~O1) & (~C1 | ~P1 | ~O2)，输出为

很明显，-是否定的，整数代表变量之一。有谁知道是否存在从整数到变量的映射？简短问题的详细描述...