Skip to content

Instantly share code, notes, and snippets.

@tomsaleeba
Last active Apr 15, 2020
Embed
What would you like to do?
Kimmy's "dress the man" puzzle
from z3 import *
shoes = Int('shoes')
man = Int('man')
glasses = Int('glasses')
glove = Int('glove')
s = Solver()
s.add(3 * shoes == 60)
s.add(shoes + (2 * man) == 30)
s.add((2 * glasses) + man == 9)
s.add(shoes + glove + glasses == 42)
s.check()
m = s.model()
print(m)
shoes_result = m[shoes].as_long()
one_shoe = shoes_result / 2
glasses_result = m[glasses].as_long()
man_result = m[man].as_long()
glove_result = m[glove].as_long()
dressed_man = ( \
(2 * one_shoe) +
(2 * glove_result) +
man_result + glasses_result \
)
print('Dressed man is worth %d' % dressed_man)
result = one_shoe + dressed_man * glasses_result
print('? is %d' % result)
# output:
# [glove = 20, glasses = 2, man = 5, shoes = 20]
# Dressed man is worth 67
# ? is 144
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment