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
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.3601How 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.367Can 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 ofz[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 thez
s gives a total 9y
s? 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]
representy[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