@@ -62,6 +62,8 @@ A common constraint that appears in puzzles is that a set of cells must be fille
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 a [cryptarithm](https://en.wikipedia.org/wiki/Verbal_arithmetic):
<!-- TODO: Magic Square instead? -->
```python
# Solve the cryptarithm
# SEND + MORE = MONEY
...
...
@@ -161,9 +163,9 @@ for r in range(9):
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.
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.
The form in which we express our constraints matters.
...
...
@@ -247,7 +249,7 @@ 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...
The annoying part of writing solvers for Sudoku variants is not writing the solver, but deciding what form the input should take...
...
...
@@ -276,11 +278,35 @@ This behavior is different from `cond == expr`.
### Conditionals Example
<!-- TODO -->
TODO
## Pseudo-Boolean Constraints
Another common constraint in puzzles is the condition "exactly K of these N cells must satisfy this condition".
More generally, consider the linear sums $`\sum_i a_i F_i \geq k`$, $`\sum_i a_i F_i \leq k`$, where $`a_i`$ and `k` are positive naturals and $`F_i`$ is a boolean expression.
This is called a Pseudo-Boolean constraint.
z3 exposes three functions for creating Pseudo-Boolean constraints: `PbGe`, `PbLe`, and `PbEq`.
## Pseudo Boolean Constraints
When calling the function, the first argument is a list of 2-tuples, where the first element of each tuple is $`F_i`$ and the second element is $`a_i`$.
The second argument is the bound $`k`$.
Expressed in Python typing, `PbEq(args: List[Tuple[BoolRef, int]], k: int)`
<!-- TODO -->
Example problem and code to solve: $`2q + 2r \leq 2, 2u + 3r \geq 4$.
```python
solver = Solver()
q = Bool('q')
u = Bool('u')
r = Bool('r')
solver.add(
PbLe([(q, 2), (r, 2)], 3),
PbGe([(u, 2), (r, 3)], 4),
)
solver.check()
print(solver.model())
# [q = False, u = True, r = True]
```
Phew! These were long notes, but with that, we've covered the relevant basic z3 features that we'll be using!
Phew!
These were long notes, but with that, we've covered the 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.
