constraints - 最小独立集合

Question

式のセットが与えられた場合、 内のすべての式を意味する最小のサブセットをs見つけたいと思います。のすべてのペアについて、 は意味を持たず、その逆も成り立つため、私は最小の独立集合と呼びます 。s'sssa,bs'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には独立セットが含まれます。