SAT/CNF优化

Question

问题

我在看SAT优化问题的一个特殊子集。对于那些不熟悉SAT和相关话题的人，请看下面的维基百科相关文章。

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

这里没有小点，它是以结合点的形式出现的。这很容易解决。然而，我正在尝试尽量减少真正赋值的数量，使整个语句变为真。我找不到解决那个问题的办法。

可能的解决办法

我想出了以下方法来解决这个问题：

1. 转换成有向图，搜索最小生成树，只生成一个顶点子集。这是Edmond的算法，但它给出了一个完整图的MST，而不是顶点的子集。
   • 也许有一个版本的Edmond算法可以解决顶点子集的问题？
   • 也许有一种方法可以从原来的问题中构造出一个可以用其他算法解决的图？

​

1. 使用SAT解算器、唇解器或穷尽搜索。我对这些解决方案不感兴趣，因为我试图用这个问题作为讲课材料。

问题

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

Answer 1

这个问题也是NP-硬问题。

我们可以从击打组中显示东降。

重击集问题：给定集合S1,S2,...,Sn和数字k：选择Set S of size k，这样，对于每个Si，S中都有一个元素s，使得s在Si中。替代定义:每个Si和S之间的交集不是空的。

还原：

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

证明：

点击集->问题：如果有hittins集合的实例，那么通过将S的所有元素赋值为true，则公式满足k元素，因为每个S'i都有一些变量v，它们在S和Si中，因此也在S'i中。

这个问题，->点击集：使用所有被分配的元素构建S，这与点击Set->这个问题是一样的。

由于您正在寻找这方面的优化问题，所以它也是NP困难的，如果您正在寻找一个精确的解，则应该尝试一种指数算法。