Merge branch 'master' of mygit.th-deg.de:ap04811/zerosumset

zerosumset/__init__.py

@@ -43,3 +43,49 @@ def zerosumset(elems):
         return []
 
 
+def maxzerosumset(elems):
+    """
+    >>> from z3 import *
+
+    >>> zerosumset([1, 500, -1])
+    [1, -1]
+    >>> zerosumset([8, -7, -1, 20])
+    [8, -7, -1]
+    >>> zerosumset([50, -3, 4, 2, 1])
+    [-3, 2, 1]
+
+    >>> zerosumset([1, 2, 3])
+    []
+
+    >>> zerosumset([])
+    []
+    """
+    
+    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 optimizer
+    s = Optimize()
+
+    # 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)
+    # is replaced by computing the number of elements in the sublist
+    sublist_len = Int('sublist_len')
+    s.add(sublist_len == Sum(is_in))
+
+    # 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)
+
+    s.maximize(sublist_len)
+    
+    # Check satisfiability and print solution if found
+    if s.check() == sat:
+        result = [elems[i] for i in range(n) if s.model().eval(is_in[i], model_completion=True) == 1]
+    else:
+        result = []
+    return result