Commit c503f373 authored by Skynet0's avatar Skynet0
Browse files

Typo fixes

parent 017c696c
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 13 additions and 16 deletions
+13 -16
......@@ -9,7 +9,7 @@ sudoku = (
(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)]
......@@ -86,13 +86,12 @@ if solver.check() == sat:
# 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")
......@@ -163,8 +163,7 @@ 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 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.
......@@ -219,9 +218,8 @@ 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)]))
# 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 = []
......@@ -234,7 +232,7 @@ else:
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.
......@@ -247,13 +245,13 @@ 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 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
......
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