zerosumset

View Source
from z3 import *

def zerosumset(elems):

    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}") for i in range(n)]

    # Create Z3 solver
    s = Solver()

    # First constraint: is_in[i] is either 0 or 1
    for i in range(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] for i in range(n)]) == 0)

    # Check satisfiability and print solution if found
    if s.check() == sat:
        print([elems[i] for i in range(n) if s.model().eval(is_in[i], model_completion=True) == 1])
    else:
        print("Unsatisfiable!")
#   def zerosumset(elems):
View Source
def zerosumset(elems):

    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}") for i in range(n)]

    # Create Z3 solver
    s = Solver()

    # First constraint: is_in[i] is either 0 or 1
    for i in range(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] for i in range(n)]) == 0)

    # Check satisfiability and print solution if found
    if s.check() == sat:
        print([elems[i] for i in range(n) if s.model().eval(is_in[i], model_completion=True) == 1])
    else:
        print("Unsatisfiable!")