最小独立集答案

【问题标题】：smallest independent set最小独立集
【发布时间】：2012-09-27 17:45:27
【问题描述】：

给定一组公式s，我想找到s 的最小子集s'，它暗示s 中的每个公式。我称s 为最小的独立集，因为对于s' 中的每一对a,b，a 并不意味着b，反之亦然。

在我看来，幼稚的方法需要O(2^|s|) 复杂性。有没有更有效的方法？这个问题可以编码一些如何利用当前的 smt/sat 求解器（例如 unsat 核心）吗？

【问题讨论】：

我认为你可以使用 Z3。这看起来像是Arrays and Bags 的用例。但是，Z3 不会为您提供有关运行时复杂性的任何信息。此外，由于问题已经解决，它只能解决给定实例的问题（而不是一般情况）。就个人而言，会发现在Alloy 中写下您的问题比在 Z3 中更容易。

【解决方案1】：

也许现在对你来说太晚了。但是您可以通过 1 个循环来计算这样的集合。

IS = F1 // first formula in s
for each formula Fi in {F2,..Fn} in s
  if ((not IS) AND Fi) is UNSAT
     IS = IS AND Fi

集合IS 包含独立集合。

【讨论】：