Implement superoptimizer for addition
Python, 644

A simple recursive equation generator.  S generates an equation that is satisfied iff the list of vars adds up to total.

There are some obvious improvements to be done.  For instance, there are a lot of common subexpressions that appear in the 15/5 output.

def S(vars, total):
    # base case
    if total == 0:
        return "(" + " and ".join("not " + x for x in vars) + ")"
    if total == len(vars):
        return "(" + " and ".join(vars) + ")"

    # recursive case
    n = len(vars)/2
    clauses = []
    for s in xrange(total+1):
        if s &gt; n or total-s &gt; len(vars)-n: continue
        a = S(vars[:n], s)
        b = S(vars[n:], total-s)
        clauses += ["(" + a + " and " + b + ")"]
    return "(" + " or ".join(clauses) + ")"

def T(n, total):
    e = S(["x[%d]"%i for i in xrange(n)], total)
    print "equation", e
    print "score", e.count("[")

    # test it
    for i in xrange(2**n):
        x = [i/2**k%2 for k in xrange(n)]
        if eval(e) != (sum(x) == total):
            print "wrong", x

T(2, 1)
T(5, 2)
T(15, 5)


Generates:

equation (((not x[0]) and (x[1])) or ((x[0]) and (not x[1])))
score 4
equation (((not x[0] and not x[1]) and (((not x[2]) and (x[3] and x[4])) or ((x[2]) and (((not x[3]) and (x[4])) or ((x[3]) and (not x[4])))))) or ((((not x[0]) and (x[1])) or ((x[0]) and (not x[1]))) and (((not x[2]) and (((not x[3]) and (x[4])) or ((x[3]) and (not x[4])))) or ((x[2]) and (not x[3] and not x[4])))) or ((x[0] and x[1]) and (not x[2] and not x[3] and not x[4])))
score 27
equation (((not x[0] and not x[1] and not x[2] and not x[3] and not x[4] and not x[5] and not x[6]) and (((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (x[11] and x[12] and x[13] and x[14])) or ((((not x[7] and not x[8]) and (x[9] and x[10])) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((x[7] and x[8]) and (not x[9] and not x[10]))) and (((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (x[13] and x[14])) or ((x[11] and x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))))) or ((((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (x[9] and x[10])) or ((x[7] and x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10]))))) and (((not x[11] and not x[12]) and (x[13] and x[14])) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((x[11] and x[12]) and (not x[13] and not x[14])))) or ((x[7] and x[8] and x[9] and x[10]) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))))) or ((((not x[0] and not x[1] and not x[2]) and (((not x[3] and not x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (not x[5] and not x[6])))) or ((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (not x[3] and not x[4] and not x[5] and not x[6]))) and (((not x[7] and not x[8] and not x[9] and not x[10]) and (x[11] and x[12] and x[13] and x[14])) or ((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (x[13] and x[14])) or ((x[11] and x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))))) or ((((not x[7] and not x[8]) and (x[9] and x[10])) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((x[7] and x[8]) and (not x[9] and not x[10]))) and (((not x[11] and not x[12]) and (x[13] and x[14])) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((x[11] and x[12]) and (not x[13] and not x[14])))) or ((((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (x[9] and x[10])) or ((x[7] and x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10]))))) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))) or ((x[7] and x[8] and x[9] and x[10]) and (not x[11] and not x[12] and not x[13] and not x[14])))) or ((((not x[0] and not x[1] and not x[2]) and (((not x[3] and not x[4]) and (x[5] and x[6])) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((x[3] and x[4]) and (not x[5] and not x[6])))) or ((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (((not x[3] and not x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (not x[5] and not x[6])))) or ((((not x[0]) and (x[1] and x[2])) or ((x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2]))))) and (not x[3] and not x[4] and not x[5] and not x[6]))) and (((not x[7] and not x[8] and not x[9] and not x[10]) and (((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (x[13] and x[14])) or ((x[11] and x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))))) or ((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (((not x[11] and not x[12]) and (x[13] and x[14])) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((x[11] and x[12]) and (not x[13] and not x[14])))) or ((((not x[7] and not x[8]) and (x[9] and x[10])) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((x[7] and x[8]) and (not x[9] and not x[10]))) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))) or ((((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (x[9] and x[10])) or ((x[7] and x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10]))))) and (not x[11] and not x[12] and not x[13] and not x[14])))) or ((((not x[0] and not x[1] and not x[2]) and (((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (x[5] and x[6])) or ((x[3] and x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))))) or ((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (((not x[3] and not x[4]) and (x[5] and x[6])) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((x[3] and x[4]) and (not x[5] and not x[6])))) or ((((not x[0]) and (x[1] and x[2])) or ((x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2]))))) and (((not x[3] and not x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (not x[5] and not x[6])))) or ((x[0] and x[1] and x[2]) and (not x[3] and not x[4] and not x[5] and not x[6]))) and (((not x[7] and not x[8] and not x[9] and not x[10]) and (((not x[11] and not x[12]) and (x[13] and x[14])) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((x[11] and x[12]) and (not x[13] and not x[14])))) or ((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))) or ((((not x[7] and not x[8]) and (x[9] and x[10])) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((x[7] and x[8]) and (not x[9] and not x[10]))) and (not x[11] and not x[12] and not x[13] and not x[14])))) or ((((not x[0] and not x[1] and not x[2]) and (x[3] and x[4] and x[5] and x[6])) or ((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (x[5] and x[6])) or ((x[3] and x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))))) or ((((not x[0]) and (x[1] and x[2])) or ((x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2]))))) and (((not x[3] and not x[4]) and (x[5] and x[6])) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((x[3] and x[4]) and (not x[5] and not x[6])))) or ((x[0] and x[1] and x[2]) and (((not x[3] and not x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (not x[5] and not x[6]))))) and (((not x[7] and not x[8] and not x[9] and not x[10]) and (((not x[11] and not x[12]) and (((not x[13]) and (x[14])) or ((x[13]) and (not x[14])))) or ((((not x[11]) and (x[12])) or ((x[11]) and (not x[12]))) and (not x[13] and not x[14])))) or ((((not x[7] and not x[8]) and (((not x[9]) and (x[10])) or ((x[9]) and (not x[10])))) or ((((not x[7]) and (x[8])) or ((x[7]) and (not x[8]))) and (not x[9] and not x[10]))) and (not x[11] and not x[12] and not x[13] and not x[14])))) or ((((((not x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2])))) or ((x[0]) and (not x[1] and not x[2]))) and (x[3] and x[4] and x[5] and x[6])) or ((((not x[0]) and (x[1] and x[2])) or ((x[0]) and (((not x[1]) and (x[2])) or ((x[1]) and (not x[2]))))) and (((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (x[5] and x[6])) or ((x[3] and x[4]) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))))) or ((x[0] and x[1] and x[2]) and (((not x[3] and not x[4]) and (x[5] and x[6])) or ((((not x[3]) and (x[4])) or ((x[3]) and (not x[4]))) and (((not x[5]) and (x[6])) or ((x[5]) and (not x[6])))) or ((x[3] and x[4]) and (not x[5] and not x[6]))))) and (not x[7] and not x[8] and not x[9] and not x[10] and not x[11] and not x[12] and not x[13] and not x[14])))
score 644