subsum.jl

from z3 import *

set =[-7, -3, -2, 5, 8]
set_len =len(set)

vars =[ Int('vars_%d' % i) for i in range ( set_len )]

s= Solver ()
rt =[]

for i in range ( set_len ):
    rt. append (vars[i]* set[i])
    s.add(Or(vars[i]==0 , vars[i]==1) ) # like bools

s.add(sum(vars)>=1)
s.add(sum(rt)==0)

if s. check ()== False :
    print "unsat "
    exit (0)
else:
    print "ok"

m=s. model ()

for i in range ( set_len ):
    if m[vars[i]]. as_long () ==1:
        print set[i],
print ""