algorithm - SAT/CNF优化

问题

我正在寻找SAT优化问题的一个特殊子集。对于不熟悉SAT和相关主题的人，这里是related Wikipedia article。

TRUE=(a OR b OR c OR d) AND (a OR f) AND ...

没有NOT，它是合取范式。这很容易解决。但是，我正在尝试以最小化真正的赋值的数量，以使整个语句为真。我找不到解决该问题的方法。

可能的解决方案

我想出了以下解决方法:

转换为有向图，并搜索最小生成树，仅跨越顶点的子集。有埃德蒙(Edmond)的算法，但是它给出了完整图形的MST，而不是顶点的子集。

也许有一个Edmond算法的版本可以解决部分顶点的问题？

也许有一种方法可以用其他算法可以解决的原始问题构造图形？

使用SAT解算器，LIP解算器或详尽搜索。我对这些解决方案不感兴趣，因为我试图将这个问题用作讲义 Material 。

问题

您有什么想法/意见吗？您能否提出其他可行的方法？

最佳答案

这个问题也是NP-Hard。

可以显示Hitting Set的东移:

命中集问题:给定S1,S2,...,Sn集和数字k:选择S大小的set k，这样，对于每个Si，在s中都有一个元素S，使得s在Si中。 [替代定义:每个Si和S之间的交集都不为空]。

减少:
对于命中集的实例(S1,...,Sn,k)，请构造您的问题的实例:(S'1 AND S'2 And ... S'n,k)，其中S'i是Si中的所有元素，并带有OR。 S'i中的这些元素是公式中的变量。

证明:
命中集->此问题:如果存在hittins集实例S，则通过将S的所有元素分配为true，该公式满足k元素的要求，因为每个S'i都有一些变量v，在S和Si中，因此也在S'i中。
，此问题->命中集:使用所有赋值为真的元素构建S [与Hitting Set->此问题相同的想法]。

由于您正在为此寻找优化问题，因此它也是NP-Hard，如果您正在寻找精确的解决方案，则应尝试指数算法

关于algorithm - SAT/CNF优化，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/8895982/