Skip to content

GitLab

Error occurred when fetching sidebar data
Merged
Created by Ethan Ordentlich@eordentlOwner

Add second set of z3py notes

Viewing commit c503f373
Prev
Show latest version
2 files
+ 13
- 16
notes/z3py‎-intro-cont‎
sudo‎ku.py‎ +7 -8
z3py-intr‎o-cont.md‎ +6 -8
notes/z3py-intro-cont/sudoku.py
+ 7
- 8
Show all unchanged lines Show 20 lines
(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),
(0,6,0,0,8,0,1,3,0),
)
grid = [[Int(f'sudoku_{r}_{c}') for c in range(9)] for r in range(9)]
Show 20 lines Show all unchanged lines Show 20 lines
# 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)]))
print("\n".join(["".join(r) for r in 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))
# 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
+ 6
- 8
Show all unchanged lines Show 20 lines
We could take this condition literally, and assert that each value from 1-9 appears at least once in every row / column / block via an `And` of an `Or`s for each digit.
Alternatively, we could use z3's `Distinct` - there are 9 values and 9 cells, so if every cell takes on a distinct value, then every value must appear.
`Distinct` is much faster than most other choices.
If we used an `And` of `Or`s, z3 would have to rederive the "obvious" fact that no two cells in a group can have the same value; it's not an immediate logical conclusion.
`Distinct` is much faster, because if we used an `And` of `Or`s, z3 must rederive the "obvious" fact that no two cells in a group can have the same value; it's not an immediate logical conclusion.
The form in which we express our constraints matters.
Additionally, making some implicit constraints explicit can speed up the solver, by allowing it to apply its heuristics earlier.
Show 20 lines Show all unchanged lines Show 20 lines
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)]))
# Print the grid as a compressed grid of digits
print("\n".join(["".join(r) for r in str_grid]))
# Equivalent to:
for r in range(9):
row = []
Show 20 lines Show all unchanged lines Show 20 lines
You can find the complete code in [sudoku.py](sudoku.py).
NOTE: I know that there are some occurences of repetition throughout this code.
NOTE: I know that there are some instances 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.
Show 20 lines Show all unchanged lines Show 20 lines
You may also be familiar with [Cracking the Cryptic's](https://www.youtube.com/c/CrackingTheCryptic) YouTube channel.
Nearly *every* Sudoku variant they've presented (chess, thermometer, etc.) can be cleanly represented in an SMT framework.
The annoying part of writing solvers for Sudoku variants is not writing the solver, but deciding what form the input should take...
The annoying part of writing solvers for Sudoku variants is *not* writing the solver, but deciding what form the input should take...
![notlikeduck](NotLikeDuck.png)
## Conditionals
In logic puzzles, depending on what the contents of a cell, are different constraints may apply.
In logic puzzles, depending on what the contents of a cell are, different constraints will apply.
z3 provides functions to create conditional expressions:
```python
Show 20 lines Show all unchanged lines