Compressing boolean formulae

Question

Syntax

~ not
/\ and
\/ or
t true
f false
P, Q, FISH, etc: variables

(Operators are given in order of precedence)

Introduction

Some boolean formulae can be changed to different forms to make them shorter. For example, the formula

~(~P /\ ~Q)

can be changed to the shorter form

P\/Q

while the formula

P \/ ~P

can be changed to the shorter form

t

---

Challenge

In this challenge, you are required to write a program that, given any boolean formula using only /\, \/, ~, t, f, parentheses, boolean variables (in uppercase), and whitespace, outputs a shortest form (since there may be more than one shortest form) in characters of that expression which is equivalent for all assignments of the variables. Shortest code (in any language) wins. I/O can be done in any reasonable manner.

Also, since answers are difficult to verify, it would be helpful (but isn't required) to include a brief explanation of how the code works.

Answer 1

Python 616

Not particularly efficient, but works in reasonable time for inputs whose results are around 5 or 6 characters. To check a string to see if it matches, it loops through every possible combination of truth/false values for all the variables and makes sure each one agrees. Using this it checks every possible string comprised of the relevant characters (not even necessarily a syntactically correct one).

It actually will print every equivalent expression (of every size) and does not actually ever terminate.

Code:

c=['t','f'];o=['1 ','0 ']
def e(s,v):
 for k in v:s=s.replace(k,v[k])
 return eval(s)
def z(t,p='~/\\() '):
 w=[]
 if p=='':return[t]*(t not in['']+c)
 for s in t.split(p[0]):w.extend(z(s,p[1:]))
 w.sort(key=lambda v:-len(v));return w
def m(v):
 l=list('~\\/()')+v
 for s in l:yield s
 for r in m(v):
    for s in l:yield s+r
def n(x):
 if x<1:yield []
 else:
    for l in n(x-1):
     for b in o:yield[b]+l
t=raw_input();v=z(t)+c;l=len(v)
for s in m(v):
 g=1
 for y in n(l):
    y[-2:]=o;d=dict(zip(v+['/\\','\\/','~'],y+['and ','or ','not ']))
    try:
     if e(s,d)!=e(t,d):g=0
    except:g=0
 if g:print s

Input/Ouput:

> ~(~P /\ ~Q)
Q\/P
P\/Q
...

> P /\ ~P
f
~t
...

> (P \/ Q) /\ P
P
(P)
...

Answer 2

Oh right, I forgot to ever actually post my answer. It uses essentially the exact same approach which KSab's answer uses, but prints only the shortest valid expression.

Python3, 493 484

e=lambda x:eval(x.replace('\\/','+').replace('/\\','%'),None,w)
class V(int):
 def __add__(s,o):return V(s|o)
 def __mod__(s,o):return V(s*o)
 def __invert__(s):return V(1-s)
import re;from itertools import product as P;t=V(1);f=V(0);i=input();v=re.findall('[A-Z]+',i)
for k in range(1,len(i)):
 for m in P(i+'~/\\tf()',repeat=k):
  m=''.join(m)
  try:
   for d in P((V(0),V(1)),repeat=len(v)):
    w=dict(zip(v,d))
    if e(m)!=e(i):raise
  except:continue
  print(m);exit()
print(i)

Edit: fixed a bug where parentheses might not be generated, and golfed the computation of m a bit. Also replaced -s+1 with 1-s.