4

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)?

Vu Nguyen
  • 987
  • 1
  • 9
  • 20
  • I think you can use Z3 for that. That looks like a use-case for [Arrays and Bags](http://rise4fun.com/z3/tutorialcontent/guide#h26). 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](http://alloy.mit.edu/alloy/) than Z3. – Jonny Nov 22 '12 at 11:47

1 Answers1

0

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.

sean
  • 1,632
  • 2
  • 15
  • 34