11
\$\begingroup\$

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 .

\$\endgroup\$
  • 1
    \$\begingroup\$ This is off-topic. As you said: this question is about optimizing a logical expression. It's not a programming challenge/puzzle in any way. \$\endgroup\$ – shiona Sep 27 '13 at 18:50
  • \$\begingroup\$ @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. \$\endgroup\$ – user9206 Sep 27 '13 at 18:58
  • 1
    \$\begingroup\$ Please 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? \$\endgroup\$ – Keith Randall Sep 27 '13 at 22:25
  • 1
    \$\begingroup\$ How 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? \$\endgroup\$ – Kaya Oct 4 '13 at 4:47
  • 1
    \$\begingroup\$ @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). \$\endgroup\$ – Kaya Oct 4 '13 at 14:32
8
\$\begingroup\$

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
\$\endgroup\$
  • \$\begingroup\$ This is very nice. How much smaller do you think the solutions could be? \$\endgroup\$ – user9206 Sep 29 '13 at 18:40
  • \$\begingroup\$ @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. \$\endgroup\$ – Keith Randall Sep 30 '13 at 3:22
2
+50
\$\begingroup\$

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.

\$\endgroup\$
  • \$\begingroup\$ 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. \$\endgroup\$ – user9206 Oct 4 '13 at 8:27

Your Answer

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