我想在中压缩正命题公式析取范式（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实现。
再见
我认为你需要的是一个系统的算法来计算两层布尔表达式的最小值（输入变量的连接的析取或输入变量的析取的连接）。
通常使用的算法是卡诺图和奎因-麦克罗斯基算法。
这些算法确实适用于否定的变量。在任何情况下，至少如果你的输入是析取范式（DNF），并且没有否定变量出现，那么表示为输入变量的析取和的输出也不会有否定变量）。