constraints - 最小独立集

Question

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

在我看来，天真的方法需要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包含独立集合。