Skip to content
Snippets Groups Projects
Commit 9821302e authored by apostnikova's avatar apostnikova
Browse files

Updated README.md. Added dev-requirements.txt, __init__.py.

parent 66ff72a9
No related branches found
No related tags found
No related merge requests found
Zerosumset
==========
Example
-------
```python
>>> import zerosumset
>>> elems = [-7, -3, -2, 9000, 5, 8]
>>> zerosumset.zerosumset(elems)
[-3, -2, 5]
>>> zerosumset.zerosumset(3, 1, 10, -4)
[3, 1, -4]
```
For developers
--------------
List of required packages in [dev-requirements.txt](dev-requirements.txt)
Project
-------
[THD](https://th-deg.de)
Licence
-------
[MIT](LICENSE)
pdoc
pytest
hypothesis
\ No newline at end of file
from z3 import *
elems = [-7, -3, -2, 9000, 5, 8]
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!")
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment