正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

我认为您需要的是一个系统的算法来计算两个层中布尔表达式的最小值(或者是输入变量的连词的分离，或者是输入变量的分离)。

常用的算法是卡诺图算法和奎因-麦克卢斯基算法。

这些算法确实适用于负变量。在任何情况下，至少如果您的输入是析取范式(DNF)，并且没有出现负变量，则表示为输入变量的连接分离的输出也不会有负值变量)。