Python 3, 432431 bytes

Not very golfed right now, but I figure I'd get the ball rolling with an answer. Try it herehere, 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':' andor ','^':'*','<->':'==','->':'<=','-':'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)

Python 3, 487432 bytes

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

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

Python 3, 487 bytes

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

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

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