Add second set of z3py notes

notes/z3py-intro-cont/sudoku.py

+from z3 import *
+
+sudoku = (
+    (0,0,0,0,0,0,7,0,1),
+    (8,0,4,0,0,3,5,0,6),
+    (0,0,0,0,0,0,0,0,0),
+    (1,0,0,0,2,4,0,0,0),
+    (3,9,0,0,6,0,0,0,0),
+    (0,0,0,0,0,5,0,0,0),
+    (0,0,0,0,0,0,0,2,0),
+    (7,1,0,5,0,0,8,0,9),
+    (0,9,0,0,8,0,1,3,0),
+)
+
+grid = [[Int(f'sudoku_{r}_{c}') for c in range(9)] for r in range(9)]
+solver = Solver()
+
+solver.add([
+    And(1 <= grid[r][c], grid[r][c] <= 9)
+    for r in range(9)
+    for c in range(9)
+])
+
+# # Equivalent to
+# for r in range(9):
+#     for c in range(9):
+#         # Note that I can expand into multiple conditions since the
+#         # And is top-level
+#         solver.add(1 <= grid[r][c])
+#         solver.add(grid[r][c] <= 9)
+
+solver.add([
+    grid[r][c] == sudoku[r][c]
+    for r in range(9)
+    for c in range(9)
+    # 0 is falsy!
+    if sudoku[r][c]
+])
+
+# # Equivalent to
+# for r in range(9):
+#     for c in range(9):
+#         # 0 is falsy!
+#         if sudoku[r][c]:
+#             solver.add(grid[r][c] == sudoku[r][c])
+
+# Rows
+solver.add([Distinct(grid[r]) for r in range(9)])
+
+# # Equivalent conditions for rows
+# for r in range(9):
+#     solver.add(Distinct(grid[r]))
+
+# Columns
+solver.add([Distinct([grid[r][c] for r in range(9)]) for c in range(9)])
+
+# # Equivalent conditions for columns
+# for c in range(9):
+#     col = []
+#     for r in range(9):
+#         col.append(grid[r][c])
+#     solver.add(Distinct(col))
+
+# Blocks
+solver.add([
+    Distinct([
+        grid[3 * r0 + r_offset][3 * c0 + c_offset]
+        for r_offset in range(3)
+        for c_offset in range(3)
+    ])
+    for r0 in range(3)
+    for c0 in range(3)
+])
+
+# # Equivalent, more verbose / explicit blocks
+# for r0 in range(3):
+#     for c0 in range(3):
+#         block_cells = []
+#         for r_offset in range(3):
+#             for c_offset in range(3):
+#                 block_cells.append(grid[3 * r0 + r_offset][3 * c0 + c_offset])
+#         solver.add(Distinct(block_cells))
+
+if solver.check() == sat:
+    m = solver.model()
+    # Extract model into a grid of strings
+    str_grid = [[str(m[grid[r][c]]) for c in range(9)] for r in range(9)]
+    # Print the grid as a compressed grid of numbers
+    print("\n".join(["".join(str_grid)]))
+
+    # Equivalent to:
+    for r in range(9):
+        row = []
+        for c in range(9):
+            row.append(str(m[grid[r][c]]))
+        print("".join(row))
+else:
+    print("No solution")

notes/z3py-intro-cont/z3py-intro-cont.md

 
 A common constraint that appears in puzzles is that a set of cells must be filled with numbers so that no two cells contain the same number.
 It is possible to create such a constraint by asserting inequality for every pair of cells.
-However, since this is such a common pattern, z3 actually provides a function to assert that each variable must take on a *Distinct* value. Let's look at this in the context of cryptarithms:
+However, since this is such a common pattern, z3 actually provides a function to assert that each variable must take on a *distinct* value. Let's look at this in the context of a [cryptarithm](https://en.wikipedia.org/wiki/Verbal_arithmetic):
 
 ```python
 # Solve the cryptarithm
 # SEND + MORE = MONEY
 
+# z3 dict pattern: Dict[str, ArithRef]
 letters = {c: Int(c) for c in set('SENDMOREMONEY')}
 s = Solver()
 
     print("No solution")
 ```
 
+You can find the complete code in [sudoku.py](sudoku.py).
+
 NOTE: I know that there are some occurences of repetition throughout this code.
 I wrote it this way to intentionally "separate" each "type" of condition from each other.
 If I had bugs in this, it is much easier to debug and tweak conditions when they are processed in separate blocks of code.
 Personally, a bit more boilerplate is much more preferable than code that is a pain to debug.
 
-### Modifying Your Solver
+### Modifying The Solver
 
 Now that we've written our solver, it's possible to *modify* it to solve sudoku variants as well (something you can't do with online solvers)!
 For example, Killer Sudoku has the additional constraint that some regions of cells must add up to a particular number.
 
 ## Pseudo Boolean Constraints
 
-<!-- TODO -->
\ No newline at end of file
+<!-- TODO -->
+
+ Phew! These were long notes, but with that, we've covered the relevant basic z3 features that we'll be using!
+ Future notes will focus on *representation*, or how we can use these base features to represent higher-level concepts.