research: preserve solver experiments and reproducible benchmarks

exp/README.md

@@ -0,0 +1,44 @@
+# Slime Reverse Search Experiment
+
+This folder is for experiments that search "backwards" from a desired slime
+chunk pattern instead of scanning every `(seed, x, z)` tuple directly.
+
+## SMT Bit-Vector Prototype
+
+`slime_reverse_smt.py` emits an SMT-LIB query with these variables:
+
+- `seed48`: the low 48 bits of the world seed
+- `chunkX`, `chunkZ`: the top-left chunk coordinate, unless fixed with `--x/--z`
+
+It uses the approximate predicate:
+
+```text
+((LCG48(seed48 + coordTerm(x, z)) >> 17) % 10) == 0
+```
+
+That removes Java `nextInt(10)`'s extremely rare rejection-loop branch.  Models
+from this query are candidates and should be verified with the exact predicate.
+
+Examples:
+
+```bash
+# Generate a 4x4 query with variable coordinates in [-64, 64].
+python3 exp/slime_reverse_smt.py -n 4 -r 64 -o /tmp/slime4.smt2
+z3 /tmp/slime4.smt2
+
+# Fix the top-left coordinate and solve only for seed48.
+python3 exp/slime_reverse_smt.py -n 4 --x 0 --z 0 --run --verify
+
+# Start with a cheaper partial query before asking for all cells.
+python3 exp/slime_reverse_smt.py -n 5 -r 128 --cells border --run --verify
+python3 exp/slime_reverse_smt.py -n 5 -r 128 --cells corners --run
+```
+
+Notes:
+
+- Variable `chunkX/chunkZ` introduce bit-vector multiplication, so large-radius
+  full 5x5 queries may be very hard for a solver.
+- Fixed-coordinate queries are much cleaner and are useful for testing whether a
+  solver can handle many seed constraints.
+- Exact verification is included because the SMT predicate intentionally ignores
+  Java's rejection retry.