Commit f51dd7d5 authored by Skynet0's avatar Skynet0
Browse files

Add file with all sudoku code

parent 13c5a309
1 merge request!1Add second set of z3py notes
This commit is part of merge request !1. Comments created here will be created in the context of that merge request.
Showing with 107 additions and 3 deletions
+107 -3
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")
......@@ -60,12 +60,13 @@ Some common z3 patterns that use comprehensions include:
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()
......@@ -231,12 +232,14 @@ else:
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.
......@@ -277,4 +280,7 @@ This behavior is different from `cond == expr`.
## 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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment