压缩正 DNF

Question

我想将 正 命题公式压缩为 析取范式（DNF）。

我暂时只假设简单的 DNF 没有否定 文字。逆过程，解压很容易 定义。对于仅由合取和析取构成的公式， 以下重写规则将生成一个 DNF：

A & (B v C) --> (A & B) v (A & C)
(A v B) & C --> (A & C) v (B & C)

这里是一个解压的例子：

Example: Decompression
Input:
  (p & (q v r) & s & (t v u)) v
  w.

Output:
  (p & q & s & t) v
  (p & r & s & t) v
  (p & q & s & u) v
  (p & r & s & u) v
  w.

现在我想知道周围是否有一些算法 它可以从 DNF 生成单个公式。 我已经研究过二元决策图。这 我遇到的问题是它们不能结合 途中所有的分离。

例如二元决策图的算法 使用共享，期间仍然会显示类似的分支 打印和/或引入新的介词变量， 这两件事都不是我们想要的：

Example: Compression (Bad)
Input:
  (p & q & s & t) v
  (p & r & s & t) v
  (p & q & s & u) v
  (p & r & s & u) v 
  w.

Output:
  (p & ((q & s & (t v u)) v (r & s & (t v u)))) v
  w.

- or -

Output:
  (p & ((q & h) v (r & h))) & (h <-> s & (t v u))) v
  w.

结果应该是一个公式，不再是 DNF， 比二元决策图更紧凑 仅使用析取和合取的算法， 和已经在 原版DNF。以下是所需压缩的示例：

Example: Compression (Good)
Input:
  (p & q & s & t) v
  (p & r & s & t) v
  (p & q & s & u) v
  (p & r & s & u) v
  w.

Output:
  (p & (q v r) & s & (t v u)) v
  w.

你会怎么想？首选 Prolog 实现。

再见

Answer 1

我认为您需要一种系统算法来计算两层中布尔表达式的最小值（输入变量的合取或输入变量的合取）。

用于执行此操作的常用算法是 Karnaugh maps 和 Quine-McCluskey 算法。

这些算法确实适用于否定变量。在任何情况下，至少如果您的输入是析取范式（DNF）并且没有出现否定变量，则表示为输入变量的结合析取的输出也不会有否定变量）。