给定一组公式 s
,我想找到 s
的最小子集 s'
,它暗示 中的每个公式s
。我将 s
称为最小独立集,因为对于 s'
中的每一对 a,b
, a
并不意味着b
反之亦然。
在我看来,简单的方法需要O(2^|s|)
复杂度。有没有更有效的方法?这个问题能否以某种方式编码,以利用当前的 smt/sat 求解器(例如 unsat 核心)?
最佳答案
也许现在对你来说已经太晚了。但你可以通过 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
包含独立集合。
关于constraints - 最小独立集,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/12765396/