Commit 13c5a309 authored by Skynet0's avatar Skynet0
Browse files

Add cryptarithm for Distinct.

- Typo fixes
parent 213c4137
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 38 additions and 12 deletions
+38 -12
......@@ -11,7 +11,7 @@ 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:
Often, we will want to create a list after calling some function on each element of an iterable:
```python
lst = []
......@@ -20,7 +20,7 @@ for elem in iterable:
lst.append(f(elem))
```
This can be replaced by a *list comprehension*:
This can be replaced by a more concise *list comprehension*:
```python
lst = [f(elem) for elem in iterable]
......@@ -28,7 +28,6 @@ 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
......@@ -49,6 +48,7 @@ for e1 in iter1:
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:
......@@ -60,13 +60,38 @@ 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 cell must take on a *Distinct* value:
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:
```python
# TODO
# Solve the cryptarithm
# SEND + MORE = MONEY
letters = {c: Int(c) for c in set('SENDMOREMONEY')}
s = Solver()
# Each letter is a single digit
s.add([And(0 <= c, c <= 9) for c in letters.values()])
# The math must check out.
send = Sum([10 ** i * letters[c] for i, c in enumerate('SEND'[::-1])])
more = Sum([10 ** i * letters[c] for i, c in enumerate('MORE'[::-1])])
money = Sum([10 ** i * letters[c] for i, c in enumerate('MONEY'[::-1])])
s.add(send + more == money)
# Leading digits shouldn't be 0
s.add(letters['S'] != 0, letters['M'] != 0)
# DISTINCT
# Each letter must take on a distinct value
# .values() isn't actually a list, so it has to be cast :(
s.add(Distinct(list(letters.values())))
if s.check():
print(s.model())
# [D = 7, R = 8, N = 6, S = 9, O = 0, M = 1, E = 5, Y = 2]
```
<!-- Mention that Distinct takes List or args -->
Similar to `And` and `Or`, `Distinct` can accept any number of arguments, or a list of variables.
### The Solver
......@@ -99,7 +124,7 @@ Then, we can only place digits from 1-9 in these cells.
```python
solver.add([
And(1 <= grid[r][c], grid[r][c]) <= 9
And(1 <= grid[r][c], grid[r][c] <= 9)
for r in range(9)
for c in range(9)
])
......@@ -150,17 +175,18 @@ Now, the conditions:
# Rows
solver.add([Distinct(grid[r]) for r in range(9)])
# Equivalent rows
# 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 columns
# # Equivalent conditions for 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)]
col = []
for r in range(9):
col.append(grid[r][c])
solver.add(Distinct(col))
# Blocks
......@@ -205,7 +231,7 @@ else:
print("No solution")
```
NOTE: I repeated the same loops over rows and columns throughout this code.
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.
......
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