diff --git a/logic/README.md b/logic/README.md
index 03e0360..8af30be 100644
--- a/logic/README.md
+++ b/logic/README.md
@@ -10,3 +10,14 @@ mimicing a tiny subset of the [z3](https://github.com/Z3Prover/z3)
 library's interface. it exposes classes for high-level bitvectors and
 [unary-encoded integers.](https://en.wikipedia.org/wiki/Unary_numeral_system)
 (unary is sometimes more efficient to solve)
+
+`sugarcane4unary2.py` utilizes z0 to solve a (pretty arbitrary) problem
+relating to farming sugarcane in Minecraft. you will need to set
+the environment variable `SOLVER` to (the path of) an external SAT solver.
+[kissat](https://github.com/arminbiere/kissat) works well.
+
+`hex_problem.py` creates a hexagon grid with some colored numbers in it.
+it doesn't really a serve a purpose.
+
+`yices_solution.py` parses a solution from a SAT solver,
+given the original yices-generated CNF.