@@ -62,8 +62,6 @@ 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
...
...
@@ -274,11 +272,24 @@ Implies(cond, expr)
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`.
This behavior is different from `cond == expr`, which you can think of as "iff".
### Conditionals Example
TODO
```python
p=Bool('p')
q=Bool('q')
r=Bool('r')
x=Int('x')
# solve is a shortcut to creating a solver, checking, and getting the model
solve(
Implies(p,Not(q)),
r==Not(q),
Or(Not(p),r),
If(p,x==1,x==2),
)
# [q = True, p = False, x = 2, r = False]
```
## Pseudo-Boolean Constraints
...
...
@@ -291,19 +302,16 @@ When calling the function, the first argument is a list of 2-tuples, where the f
The second argument is the bound $`k`$.
Expressed in Python typing, `PbEq(args: List[Tuple[BoolRef, int]], k: int)`
Example problem and code to solve: $`2q + 2r \leq 2, 2u + 3r \geq 4$.
Example problem and code to solve: $`2q + 2r \leq 2, 2u + 3r \geq 4`$.