Add second set of z3py notes

notes/z3py-intro-cont/z3py-intro-cont.md

 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
 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.
 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...
 
 ![notlikeduck](NotLikeDuck.png)
 
 
 ### 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.