constraints - 最小独立集

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