smallest independent set

Question

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

It seems to me the naive approach would take O(2^|s|) complexity. Is there a more efficient method ? Can this problem be encoded some how that can take advantage of current smt/sat solvers (e.g. unsat core)?

I think you can use Z3 for that. That looks like a use-case for Arrays and Bags. However, Z3 will not give you any information on runtime-complexity. Also, since the problem is sat, it can only ever solve the problem for a given instance (and not the general case). Personally, would find it easier to write down your problem in Alloy than Z3. — Jonny

sean sean · Accepted Answer · 2014-06-09T05:54:50

Maybe it's too late for you now. But you can compute such a set by 1 loop.

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 set IS contains the independent set.

smallest independent set

1 Answers