# Python 3, 432 bytes

<!-- language-all: lang-python -->

Not very golfed right now, but I figure I'd get the ball rolling with an answer. Try it [here][1], `g()` is the main function.

    import re,itertools as H
    def g(i):
     y=re.sub(r'\W','',''.join(set(i)).upper());l=i.split()
     def e(s):
      def f(a):
       for v,w in a:exec(v+'='+w)
       return eval(re.sub('[^A-Z()]+',lambda x:{'v':' and ','^':'*','<->':'==','->':'<=','-':'not '}[x.group()],s))
      return[c for c in H.product("01",repeat=len(y))if f(zip(y,c))]
     for n in range(len(l),-1,-1):
      for q in H.combinations(l,n):
       if e('('+')^('.join(q)+')'):return' '.join(q)


  [1]: https://repl.it/BCyz/10