Smallest independent set

Question

Given the set s formula, I want to find the smallest subset of s' of s , which implies every formula in s . I call s smallest independent set, because for each pair a,b in s' , a does not imply b and vice versa.

It seems to me that a naive approach will require complexity O(2^|s|) . Is there a more efficient method? Could this problem be encoded in some way, how can it use the current smt / sat solvers (e.g. unsat core)?

Answer 1

You may be too late. But you can calculate such a set for 1 cycle.

 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 

The IS set contains an independent set.