2

我想以析取范式（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 实现。

再见

4

1 回答 1

1

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

用于执行此操作的常用算法是卡诺图和Quine-McCluskey算法。

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

于 2012-09-05T15:42:46.470 回答