SAT/CNF 优化

Question

问题

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

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

没有非，它是合取范式。这很容易解决。不过，我正在尝试尽量减少真正分配的数量，以使整个陈述成立。我找不到解决这个问题的方法。

可能的解决方案

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

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

问题

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

Answer 1

这个问题也是NP-Hard。

可以显示从Hitting Set 向东减少：

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

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

证明：
Hitting Set -> 这个问题：如果有一个 hittins 集合的实例，S 然后通过将所有S 的元素赋值为true，公式满足@987654340 @ 元素，因为对于每个S'i，都有一些变量v 在S 和Si 中，因此也在S'i 中。
This question -> Hitting set：使用所有赋值为真的元素构建S [与 Hitting Set->This question 的想法相同]。

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