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!")
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!")