44 lines
1.5 KiB
Markdown
44 lines
1.5 KiB
Markdown
# 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.
|