Have you tried to apply the Z3 prover before?

[void4]

Your seedfinding explanations made me think of this. Z3 is a quite powerful theorem prover with Python bindings. It can find solutions for many systems and types of constraints, and can work with many datatypes, including floats and bit vectors! Here is an excellent talk about it: https://www.youtube.com/watch?v=56IIrBZy9Rc

Below I implemented a program which tries to find an initial_seed that, after ROUNDS iterations of an LCG, generates sequential values which each satisfy some constraints.

I haven't tested yet how well this works with other sets of constraints/larger numbers or rounds, but for this example it finds a solution even for 10000 LCG iterations within 2 seconds.

pip install z3

from z3 import *

java = (25214903917, 11, 48)#a,c,m

def ilcg(seed, params, repeat):
    """Computes *repeat* forward passes given a starting seed and LCG parameters"""
    for r in range(repeat):
        seed = (params[0]*seed+params[1])%2**params[2]
        print(f"LCG iteration:{str(r+1).rjust(5)}\tvalue:{str(seed).rjust(16)}")
    return seed

def create_expression(solver, seed, params, maxrounds=1000, constraints=None):
    """Creates expression with the initial *seed* BitVec variable, and adds constraints for the last passes, depending on the number of constraints"""
    ncs = []

    # reverse constraints order
    constraints = constraints[::-1]

    if constraints is None:
        constraints = []

    expr = seed

    for thisround in range(maxrounds):

        expr = (params[0]*expr+params[1])%2**params[2]

        if maxrounds-thisround-1 < len(constraints):
            nc = BitVec(f"nc_{maxrounds-thisround-1}", 48)
            ncs.append(nc)
            print("adding constraint", nc)

            c1 = nc==expr
            s.add(c1)
            #print(c1)

            c2 = constraints[maxrounds-thisround-1][0] <= nc
            print(c2)
            s.add(c2)

            c3 = nc <= constraints[maxrounds-thisround-1][1]
            s.add(c3)
            print(c3)

    return expr, ncs

# Number of rounds - constraints will be created matching the last rounds in reverse order
ROUNDS = 10

initial_seed = BitVec("initial_seed", 48)

# List constraints, structure: first_value <= value_at_iteration <= second_value
# last constraint is made to the last iteration, second last to the second last etc.
# In this case we want to find an initial_seed, that, after both 9 and 10 rounds has 0 <= value <= 1000
# here, it finds the 107048004364969 -> 0 -> 11 sequence
constraints = [(0, 1000), (0,1000)]#for some reason this doesn't work yet when using (0,2**48-1) somewhere, might have something to do with signed representations

s = Solver()

expr, ncs = create_expression(s, initial_seed, java, maxrounds=ROUNDS, constraints=constraints)

# Check whether the problem is satisfiable
ch = s.check()
if str(ch) == "unsat":
    print("unsatisfiable")
else:
    print("satisfiable")
    m = s.model()
    print("Model assignments", m)
    initial_seed = m[initial_seed].as_long()
    print("initial_seed:", initial_seed)

    for ci, constraint in enumerate(constraints):
        print("values vs constraints", m[ncs[ci]], constraint)

    check = ilcg(initial_seed, java, ROUNDS)
    print("forward pass check", check)

    if m[ncs[-1]].as_long() == check:
        print("forward pass check passed")
    else:
        print("final results do not agree")

Edit: found a video where someone applies it to a different generator: https://www.youtube.com/watch?v=-h_rj2-HP2E

[Earthcomputer]

It really depends on the situation whether it's more appropriate to use Z3 or the lattice method to crack an LCG. For 10 calls, the lattice method can optimally be on the order of microseconds, although LattiCG is still a bit less optimized than that.

[mjtb49]

Yes, we know about Z3. Your particular example is not very convincing as it is a problem which can be answered using only basic algebra, which Z3 is good at, while I am not aware of such methods working in the general case. It could be that Z3 is smart enough to use its MILP solver for the general case, in which case its performance should not be bad. One can replace our MILP code with Z3s and probably get something decent.

In general if you want to use some other software besides LattiCG (for example if you need to use a different language), an appropriate replacement is anything which can solve Mixed Integer Linear Programs (MILPs). In the past I have used gurobi for this.

[mjtb49]

Also, its just no fun!