In computer science, the subset sum problem is an important decision problem in complexity theory and cryptography. There are several equivalent formulations of the problem. One of them is: given a set (or multiset) of integers, is there a non-empty subset whose sum is zero? For example, given the set ~{−7, −3, −2, 9000, 5, 8}~, the answer is yes because the subset ~{−3, −2, 5}~ sums to zero.
[Wikipedia: Subset sum problem](https://en.wikipedia.org/wiki/Subset_sum_problem)
"""
fromz3import*
elems=[-7,-3,-2,9000,5,8]
n=len(elems)
# Symbolic variables: is_in[i] is 1, if element i is in the zero sum subset, 0 otherwise
is_in=[Int(f"{i}")foriinrange(n)]
# Create Z3 solver
s=Solver()
# First constraint: is_in[i] is either 0 or 1
foriinrange(n):
s.add(Or(is_in[i]==0,is_in[i]==1))
# Second constraint: at least one element should be in the zero sum subset:
s.add(Sum(is_in)>0)
# Third constraint: the sum of the elements in the zero sum subset should be zero:
s.add(Sum([elems[i]*is_in[i]foriinrange(n)])==0)
# Check satisfiability and print solution if found