problem 1.12 The Colossal Book of Short Puzzles and Problems-W. W. Norton & Company (2005)

solve.py

from z3 import *

size = 10

for i in xrange(size):
    globals()['x%i' % i]=BitVec('x%i' %i,32)

one = BitVec("one", 32)
zero = BitVec("zero", 32)

s = Solver()
s.add(one==1)
s.add(zero==0)
for i in xrange(size):
    s.add(globals()['x%i' % i] == Sum([If(globals()['x%i' % j] == i, one, zero) for j in xrange(size)]))

s.check()
m=s.model()

solution = int("".join(map(str, [m[globals()['x%i' % i]].as_long() for i in xrange(size)])))
print solution
assert(solution == 6210001000)