slime/exp/README.md

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:

((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:

# 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.