最小的独立集

Question

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

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

Answer 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包含独立集合。