Commit 213c4137 authored by Skynet0's avatar Skynet0
Browse files

Draft notes for next week

parent 84cd98cd
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 255 additions and 0 deletions
+255 -0
notes/z3py-intro-cont/NotLikeDuck.png

18.1 KB

# z3py Introduction, Continued
## Sudoku
[Sudoku](https://en.wikipedia.org/wiki/Sudoku) is a well-known logic puzzle with simple rules.
Given some digits, the objective is to fill a 9x9 grid with one digit per cell so that each column, each row, and each of the nine 3x3 blocks contain every digit from 1-9.
This means that there cannot be any repeated digits in a block, row, or column.
Many Sudoku solvers exist online, but we're going to write our own!
### List Comprehensions
Before we start writing the solver, let's look at an incredibly useful Python feature - the list comprehension.
You're probably familiar with this method of creating a list based on the contents of an iterable:
```python
lst = []
for elem in iterable:
# f is an arbitrary function
lst.append(f(elem))
```
This can be replaced by a *list comprehension*:
```python
lst = [f(elem) for elem in iterable]
```
When solving logic puzzles, we will often want to work with grids.
List comprehensions are very useful concise tools for constructing groups of variables at once, or constructing many related conditions at once.
Another useful tool is the dictionary comprehension:
```python
dct = {}
for elem in iterable:
dct[f1(elem)] = f2(elem)
# Equivalent:
dct = {f1(elem): f2(elem) for elem in iterable}
```
We can also handle nested for loops that build a single list:
```python
lst = []
for e1 in iter1:
for e2 in iter2:
lst.append(f(e1, e2))
lst = [f(e1, e2) for e1 in iter1 for e2 in iter2]
Some common z3 patterns that use comprehensions include:
- Storing z3 variables in a list or 2D list
- Storing z3 variables in a dictionary that maps string identifiers to variables
- Asserting a common constraint that applies to each variable in an iterable (i.e. all cells must contain a number in a range)
### Distinct
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 cell must take on a *Distinct* value:
```python
# TODO
```
<!-- Mention that Distinct takes List or args -->
### The Solver
We'll work with input as a 2D list:
```python
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),
)
```
Since we are placing integers 1-9 in a 9x9 grid, we can use an `Int` to represent the value we will place in each cell.
We'll use a nested list comprehension to construct the grid.
```python
grid = [[Int(f'sudoku_{r}_{c}') for c in range(9)] for r in range(9)]
solver = Solver()
```
Note that the variable corresponding to each cell must have a unique z3 identifier, which we've ensured by using the row and column.
Then, we can only place digits from 1-9 in these cells.
```python
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)
```
We also need to make sure that our assignment agrees with the given values.
```python
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])
```
Next, each row and column and block must contain every value from 1-9.
There's two different ways that this can be expressed as a z3 expression.
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 the alternative expression.
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.
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.
While it's slightly contrived here, we'll see some more examples of this in other genres.
Now, the conditions:
```python
# Rows
solver.add([Distinct(grid[r]) for r in range(9)])
# Equivalent 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 columns
for c in range(9):
# Extract the cell at the current column for each row
col = [grid[r][c] for r in range(9)]
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))
```
We've added all the constraints that make up a Sudoku puzzle!
Now, we just need to run the solver and output the solution.
```python
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")
```
NOTE: I repeated the same loops over rows and columns 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
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.
This constraint has a direct SMT analogue!
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 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.
z3 provides functions to create conditional expressions:
```python
If(cond, then_expr, else_expr)
```
If `cond` evaluates to `True`, then `If` evaluates to `then_expr`.
Otherwise, `If` evalutes to `else_expr`.
This means that `then_expr` and `else_expr` must be of the same type.
```python
Implies(cond, expr)
```
`Implies` evalutes to true iff `If(cond, expr, True)`. evaluates to true.
Note that `expr` must evaluate to a `Boolean`.
WARNING: If `cond` evaluates to `False`, `expr` may take on any truth value, i.e. from a false proposition, anything can follow.
This behavior is different from `cond == expr`.
### Conditionals Example
<!-- TODO -->
## Pseudo Boolean Constraints
<!-- TODO -->
\ No newline at end of file
......@@ -181,6 +181,7 @@ The values in the "dictionary", however, are z3-specific types, which we usually
To cast integers, we use `model[var].as_long()`.
To cast booleans, you can directly cast the value: `bool(model[bool_var])`.
We can also directly cast z3 values to strings: `str(model[var])`.
We can also evaluate expressions in the context of the model; when `model.evaluate(expr)` is called with an expression, known variables are plugged in.
[Here is a helpful StackOverflow post](https://stackoverflow.com/questions/12598408/z3-python-getting-python-values-from-model/12600208) that describes how to get Python values from various z3 types.
......
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