cnf - 如何读取 CNF 文件？

Question

我正在研究 Dung 制作的论证系统如何阅读此文件内容？它是一个 cnf 文件，描述了一个抽象的论证框架

在此处输入图像描述

Answer 1

该文件定义了用 Conjuctive Normal Form 编写的布尔表达式。基本上它是由 AND 连接的子句，子句中的每个变量 ORed 在一起。

文件格式 (.cnf) 的第一行以

p cnf num_variables num_clauses

因此，在您的示例中，7 是变量的数量，12 是子句的数量。

然后每一行定义一个子句。例如：

(A v B v C) ^ (A v D v E) ^ (B v C v D) 

变量数为 5 (ABCDE)，子句数为 3（由 AND 分隔） 变量索引从 1 开始，每个子句单独一行。每行以 0 结尾，表示子句的结束。要显示否定，请在变量前添加“-”（负号）。

p cnf 5 3
1 2 3 0
1 4 5 0
2 3 4 0

我不知道第一行的 e 是什么。