Implement superoptimizer for addition

The task is to write code that can find small logical formulae for sums of bits.

The overall challenge is for your code to find the smallest possible propositional logical formula to check if the sum of y binary 0/1 variables equals some value x. Let us call the variables x1, x2, x3, x4 etc. Your expression should be equivalent to the sum. That is, the logical formula should be true if and only if the sum equals x.

Here is a naive way to do it to start with. Say y=15 and x = 5. Pick all 3003 different ways of choosing 5 variables and for each make a new clause with the AND of those variables AND the AND of the negation of the remaining variables. You end up with 3003 clauses each of length exactly 15 for a total cost of 45054.

Your answer should take be a logical expression of that sort that can just be pasted into python, say, so I can test it. If two people get the same size expression, the code that runs the fastest wins.

You ARE allowed to introduce new variables into your solution. So in this case your logical formula consists of the y binary variables, x and some new variables. The whole formula would be satisfiable if and only if the sum of the y variables equals x.

As a starting exercise some people may want to start with y=5 variables adding to x=2. The naive method will then give a cost of 50.

The code should take two values y and x as inputs and output the formula and its size as the output. The cost of a solution is just the raw count of variables in its output. So (a or b) and (!a or c) counts as 4. The only allowed operators are and, or and not.

Update It turns out there is a clever method for solving this problem when x =1, at least in theory .

user9206

Posted 2013-09-27T18:14:10.063

Reputation:

1This is off-topic. As you said: this question is about optimizing a logical expression. It's not a programming challenge/puzzle in any way. – shiona – 2013-09-27T18:50:46.643

@shiona The challenge is to think of a clever way to do it that runs quickly enough. Maybe I should rephrase to make this clearer. I think of it like a challenge to write a superoptimizer. – None – 2013-09-27T18:58:29.410

1Please define more precisely the "size". Your description implies NOT isn't counted. Or just raw variable negation doesn't count? Each binary AND/OR counts as one? – Keith Randall – 2013-09-27T22:25:38.603

Is this a golf or a challenge or what ? (It's an interesting problem area so I'd like to see the question's short-comings fixed - it would be a shame if it got closed.) – Paul R – 2013-09-29T11:49:56.473

@PaulR It's meant to be a programming challenge (not a challenge to write the shortest code). I have hopefully added a better tag. – None – 2013-09-29T14:34:25.260

Can you confirm exactly which operators are allowed in the final expression ? Would is just be AND/OR/NOT ? How about XOR ? NAND/NOR ? Arithmetic operators such as +/- ? – Paul R – 2013-09-29T16:18:30.377

@PaulR Thanks for asking and sorry it wasn't clear before. Just AND/OR/NOT . – None – 2013-09-29T16:24:56.290

Yeah. 4 close votes and everything that prevents me from closing this question is an open bounty. – Johannes Kuhn – 2013-09-29T18:28:04.677

@JohannesKuhn Is there anything I can do to improve the question? – None – 2013-09-29T18:33:20.963

So for the example with y=5 and x=2, the output would be a logical expression that holds when exactly 2 of the y_i's are true, and the goal is to express this with as few {and,or,not}s as possible. Is this correct? – FireFly – 2013-09-29T19:09:08.787

@Firefly Yes. Well you can have as many nots as you like. I am just counting the number of occurrences of variables in the score. The logical expression (not y[0] and y[1] ) or (y[0] and not y[1]) would give a score of 4, for example, if it were actually correct for something. – None – 2013-09-29T19:16:00.360

1How will introducing new variables work with the score? Say I want to let z[0] = y[0] and y[1], how do you want this indicated? – Kaya – 2013-10-04T04:47:58.360

@Kaya The new variables would have to be in the logical formula and so are counted the same way as all the other variables. See my latest edit to the question or http://www.cs.cmu.edu/~wklieber/papers/2007_efficient-cnf-encoding-for-selecting-1.pdf for some concrete examples of how to introduce new variables.

– None – 2013-10-04T08:21:08.367

Can you include an example including the result and how it's scored in your question? You haven't specified anything about how new variables are counted. If someone says z[0] = (y[0] or y[0]) and not y[1] with a result of z[0] or not z[0] or z[0], how is the scoring calculation done? Is it 3 because only the variables in the result expression count? Is it 9 because recursively expanding the zs gives a total 9 ys? Is it 7, since that's the count of variables that appear anywhere? Is it 6 because anything on the left side of an assignment equal sign doesn't count? Is it something else? – Olathe – 2013-10-04T12:39:02.720

@Olathe The logical formula output can't have an equals sign in it, it is just a logical formula that is satisfiable if and only if the sum of the binary y variables equals x. Did I misunderstand you? – None – 2013-10-04T13:19:09.267

1@Lembik thanks for the pdf link, I believe I understand now. If I desire to have the variable z[0] represent y[0] or y[1] then I would just need to introduce a clause that looks like (y[0] or y[1]) or not z[0] (or any equivalent statement using the 3 operators allowed). – Kaya – 2013-10-04T14:32:54.400

@Kaya That is my understanding too. Now the problem is how to search for the minimal representation :) – None – 2013-10-04T14:37:09.707

@Lembik, I haven't done these kinds of problems before and Kaya's statement clears up what's going on. – Olathe – 2013-10-04T15:39:45.283

@Olathe Great and thanks to Kaya. – None – 2013-10-04T15:40:18.423

Answers

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 > n or total-s > 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

Keith Randall

Posted 2013-09-27T18:14:10.063

Reputation: 19 865

This is very nice. How much smaller do you think the solutions could be? – None – 2013-09-29T18:40:34.283

@Lembik: haven't really thought about it. You'd have to define new variables for common subexpressions. For instance, not x[0] and not x[1] and not x[2] appears 5 times in the 15/5 expression. – Keith Randall – 2013-09-30T03:22:11.690

I would have made this a comment, but I don't have a reputation. I wanted to comment that the results of Kwon & Klieber (known as the "Commander" encoding) for k=1 have been generalised for k>=2 by Frisch et al. "SAT Encodings of the At-Most-k Constraint." What you're asking about is a special case of the AM-k constraint, with an additional clause to guarantee At-Least-k, which is trivial, just a disjunction of the all variables to the AM-k constraint. Frisch is a leading researcher in constraint modelling, so I would feel comfortable suggesting that [(2k+2 C k+1) + (2k+2 C k-1)] * n/2 is the best bound known on the number of clauses required, and k*n/2 for the number of new variables to be introduced. The details are in the quoted paper, along with the instructions of how this encoding to built. It's fairly simple to write a program to generate this formula, and I think such a solution would be competitive with any other solutions you'll likely find for now. HTH.

zendessert

Posted 2013-09-27T18:14:10.063

Reputation: 71

Thank you. It would be interesting to see if this is still the best for my cost measurement for small problem sizes where some exhaustive super optimization might be possible. Hopefully someone here will try this out. – None – 2013-10-04T08:27:00.277