SAT/CNF 优化

Question

问题

我正在研究 SAT 优化问题的一个特殊子集。对于那些不熟悉 SAT 和相关主题的人，这里是 相关维基百科文章.

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

没有 NOT，它是合取范式。这很容易解决。不过我正在努力 最大限度地减少真实分配的数量 使整个陈述成立。我找不到解决该问题的方法。

可能的解决方案

我想出了以下方法来解决它：

1. 转换为有向图并搜索最小生成树，仅生成顶点的子集。有 Edmond 算法，但它给出的是完整图的 MST，而不是顶点的子集。
   • 也许埃德蒙算法的一个版本可以解决顶点子集的问题？
   • 也许有一种方法可以从原始问题构建一个可以用其他算法解决的图？
2. 使用 SAT 求解器、LIP 求解器或穷举搜索。我对这些解决方案不感兴趣，因为我试图使用这个问题作为讲座材料。

问题

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

Answer 1

这个问题是 NP-硬 以及。

可以显示从东减少 击球组:

命中设定问题:给定集合 S1,S2,...,Sn 和一个数字 k:选择集 S 尺寸的 k, ，这样对于每个 Si 有一个元素 s 在 S 这样 s 是在 Si. 。[替代定义：每个之间的交集 Si 和 S 不为空]。

减少:
举个例子 (S1,...,Sn,k) 点击设置，构建问题的实例： (S'1 AND S'2 And ... S'n,k) 在哪里 S'i 是所有元素在 Si, ，与或。S'i 中的这些元素是公式中的变量。

证明：
点击设置->这个问题:如果存在设置的 hittins 实例， S 然后通过分配所有 S的元素为 true，则公式满足 k 元素，因为对于每个 S'i 有一些变数 v 这是在 S 和 Si 因而也在 S'i.
这个问题 -> 命中设置:建造 S 与分配为真的所有元素[与命中集->此问题相同的想法]。

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