From f575eb0ab81ea2c644fd998c36632dc6648de0e8 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Sat, 31 Dec 2022 09:51:36 -0500
Subject: [PATCH] New Post

---
 .../blog/obtaining-multiple-solutions-z3.md   | 90 +++++++++++++++++++
 1 file changed, 90 insertions(+)
 create mode 100644 content/blog/obtaining-multiple-solutions-z3.md

diff --git a/content/blog/obtaining-multiple-solutions-z3.md b/content/blog/obtaining-multiple-solutions-z3.md
new file mode 100644
index 0000000..4ef1b5f
--- /dev/null
+++ b/content/blog/obtaining-multiple-solutions-z3.md
@@ -0,0 +1,90 @@
+---
+title: "Obtaining Multiple Solutions Z3"
+date: 2022-12-31T09:52:00-05:00
+draft: false
+tags: []
+math: true
+---
+
+Playing around with Diophantine solvers, I wanted to obtain the solutions of the following equation:
+$$
+5a + 4b - 3c = 0
+$$
+Let's encode that using Z3
+
+```python
+from z3 import *
+
+# Encode Equation
+a, b, c = Ints("a, b, c")
+s = Solver()
+s.add(5 * a + 4 * b - 3 * c == 0)
+
+# Find solution
+result = s.model()
+if result == sat:
+    print(result)
+```
+
+This code snippet returns
+
+```
+[a = 0, b = 0, c = 0]
+```
+
+Now there are multiple solutions to this Diophantine equation, so how do we get the others? It turns out after searching around StackOverflow (see references) the only way is to add the previous solutions as constraints.
+
+```python
+# This encodes the last solution as a constraint
+block = []
+for var in m:
+    block.append(var() != m[var])
+s.add(Or(block))
+```
+
+Formulaically, this corresponds to: 
+$$
+a \ne 0 \vee b \ne 0 \vee c \ne 0
+$$
+If you look at the references, it's hard to encode these constraints generally. This is because Z3 is a powerful SMT solver working with many different theories.  Though if we restrict ourselves to the Diophantine equations, we can write a function that acts as a generator for all of the solutions:
+
+```python
+import z3
+
+def get_solutions(s: z3.z3.Solver):
+    result = s.check()
+    # While we still get solutions
+    while (result == z3.sat):
+      m = s.model()
+      yield m
+      # Add new solution as a constraint
+      block = []
+      for var in m:
+          block.append(var() != m[var])
+      s.add(z3.Or(block))
+      # Look for new solution
+      result = s.check()
+```
+
+Now for our example, this allows us to do the following:
+
+```python
+from z3 import *
+
+a, b, c = Ints("a, b, c")
+s = Solver()
+s.add(5 * a + 4 * b - 3 * c == 0)
+
+solutions = get_solutions(s)
+upper_bound = 10
+for solution, _ in zip(solutions, range(upper_bound)):
+    print(solution)
+```
+
+The solutions of a linear Diophantine equation can be easily parameterized so I don't recommend using Z3 in this way. Though I think this exercise is informative for other theories you might be trying to satisfy. 
+
+## References
+
+- https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation/70656700#70656700
+- https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation/70656700#70656700
+- https://stackoverflow.com/questions/63231398/trying-to-find-all-solutions-to-a-boolean-formula-using-z3-in-python/63232953#63232953