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

(Operators are given in order of precedence)


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


while the formula

P \/ ~P

can be changed to the shorter form



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.

  • \$\begingroup\$ In your "Challenge" section you do not mention any whitespace, but your examples have them. Should I handle them? \$\endgroup\$ – Victor Stafusa Mar 10 '14 at 1:53
  • 4
    \$\begingroup\$ I think Florent's point is that it is a difficult problem to solve in general, let alone to golf. Among other things, the parser will need to be able to determine if two arbitrary formulae have the same truth conditions. Reducing p ^ ~p is easy enough if p is atomic, but how about ((A^B)v(A^C)) ^ ~(A^(BvC)) ? I think it is a cool problem and I am curious to see some responses. But if you want short solutions, the problem could be made more conducive to golfing by A. using prefix notation and B. providing a list of required reductions. \$\endgroup\$ – dfernig Mar 12 '14 at 2:34
  • 1
    \$\begingroup\$ I have a valid (golfed) solution in more than 5000 characters. This is ridiculous... It is composed of a tokenizer, an AST-parser, an AST-rewriter and an expression generator. \$\endgroup\$ – Florent Mar 12 '14 at 13:27
  • 1
    \$\begingroup\$ Mathematica can do it in one function call (BooleanMinimize) \$\endgroup\$ – Florent Mar 12 '14 at 15:07
  • 1
    \$\begingroup\$ For the record, I have a 498-character solution now, whose sha256sum is b9c98d088b78c30bb2108008a064a7b95722a4694d90ddad94a025c2eb4ed30a. I'll post the actual code at a later date, as I don't want to stifle creativity. \$\endgroup\$ – Lily Chung Mar 13 '14 at 2:40

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

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(-s+1)
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(''.join(v)+'~/\\tf',repeat=k):
   for d in P((V(0),V(1)),repeat=len(v)):
    if e(m)!=e(i):raise

Note that the hash I computed earlier included the trailing newline and was before I golfed def e(x): return to e=lambda x:


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.


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='~/\\() '):
 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):
 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 []
    for l in n(x-1):
     for b in o:yield[b]+l
for s in m(v):
 for y in n(l):
    y[-2:]=o;d=dict(zip(v+['/\\','\\/','~'],y+['and ','or ','not ']))
     if e(s,d)!=e(t,d):g=0
 if g:print s


> ~(~P /\ ~Q)

> P /\ ~P

> (P \/ Q) /\ P

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.