boolean-logic - 布尔函数，DNF和CNF的目的是什么？

Question

布尔函数可以用析取范式 (DNF) 或合取范式 (CNF) 表示。谁能解释为什么这些表格有用？

Answer 1

CNF 很有用，因为这种形式直接描述了布尔 SAT 问题，虽然 NP 完全，但有许多不完全和启发式指数时间求解器。CNF 已被进一步标准化为一种称为“ DIMACS CNF 文件格式”的文件格式，大多数求解器都可以对其进行操作。因此，例如，芯片行业可以通过转换为 DIMACS CNF 并输入任何可用的求解器来验证其电路设计。Tseitin变换可以将电路转换为等值的CNF。

DNF 实际上并没有那么有用，但是将公式转换为 DNF 意味着可以看到满足公式的可能分配列表。不幸的是，一般来说，将公式转换为 DNF 很困难，并且可能导致指数级爆炸（非常大的 DNF），这很明显，因为可以有指数级数量的满足分配给公式。

虽然 CNF 与 DNF 相比可以更简洁，但有时很难推理，因为它在从电路转换时可能会丢失结构，因此另一种简洁的形式会很有用。and-inverter 图数据结构就是为此目的而设计的；它可以更紧密地模拟电路的结构，因此在某些类型的公式中更容易推理。然而，在它上面运行的求解器并不多。

其他形式包括：

• 二元决策图
• 命题有向无环图
• 否定范式
• 其他（维基百科）

Answer 2

它有助于以某种标准方式表达功能。这样，自动通过许多算法就更容易了。

例如，这两种形式都可以用于自动定理求解，即解析方法中的 CNF。