是否有一种用于还原CNF的算法

Question

我在联合正常形式（CNF）中有一个布尔配方： $（a \ vee b \ vee c）\ wedge（a \ vee b \ vee \ neg c）\ wedge（x \ vee y）$

我知道这可以简化为： $（a \ vee b）\ wedge（x \ vee y）$ 。

a）有没有算法来确定CNF是否已经处于缩小的形式或不_

b）是否有一种算法可以以比较每对子句更有效的方式来实现这种算法，以便可以减少任何配对的条款？我希望自动化任何CNF的减少，我正在寻找我可以借用/实施的任何算法。

Answer 1

CNF最小化很难;查看 https://cstheory.stackexchange.com/q/9839/5038 。它肯定是NP - 硬，并且有一种意义的是“甚至更难”。

一种方法来获得一些直觉，为什么它很难就是如果cnf是不可取的，那么它的缩小形式是“假”，而如果它是满足的，则其缩小的形式是其他的。因此，如果您有一个有效的方法来查找缩小的形式，那将立即为您提供一种方法来判断CNF是否满足 - 我们知道的任务是NP-HARD。

看 https://cstheory.stackexchange.com/q/9839/5038 https://en.wikipedia.org/wiki/logic_optimization#circuit_minimization_in_boolean_algebra 对于某些点进入文献中此任务的算法。