Putting some of my comments into writing. This is less than an answer but too much for a comment. In the comments I had claimed to apply SMT to solve case 1 - this is false, I was mistaken. I have had cases 2 and 3 running SMT (boolector, Z3, CVC4, yices) for some time without success. The closest thing to success is the identification of seeds that produce matching output for the first ~96 bits. Past that point the solvers appear to take geometrically (or worse) more time matching seed per additional bit of matching output. The formulation is a naive use of Cryptol:
lcg : {n} (fin n) => [64] -> [64] -> [64] -> [64] -> [n][32]
lcg seed inc ex mult =
[rand | (_,rand) <- take`{n} (drop`{1} seq) ]
where
seq = [(seed,0)] # [(st * mult + inc, drop (((st * mult + inc) >> 32) ^ ex)) | (st,_) <- seq]
harderOutput : [4][32]
harderOutput = [0x5e3af925, 0x1b7f8e1a, 0x268c64d1, 0x4b614b92]
harderMult : [64]
harderMult = 0xc278c0d1c04a88d9
knownMult : [64]
knownMult = 0xc278c0d1c04a88d9
knownXor : [64]
knownXor = `0x0
knownOutput : [4][32]
knownOutput = [0x8c005b3e, 0x27e3338e, 0x1bb199bb, 0x46449299]
trivialMult : [64]
trivialMult = 0xc278c0d1c04a88d9
trivialOutput : [4][32]
trivialOutput = [0x8b1294a5, 0xae5cbf0d, 0x2da164bd, 0xcbe27c6d]
doneSeed : [64]
doneSeed = 0x35e647cfd3423fd0
doneMult : [64]
doneMult = 0xc278c0d1c04a88d9
doneOutput : [4][32]
doneOutput = [0x59502137, 0xb6152ece, 0xbbd2cb88, 0xef05249f]
// case 1:
// :sat \s -> lcg s zero zero trivialMult == trivialOutput
// case 2:
// :sat \s i -> lcg s i knownXor knownMult == knownOutput
// case 3:
// :sat \s i x -> lcg s i x harderMult == harderOutput
And an example, which terminates quite quickly, in which we find initial values producing an identical first 3 words (96 bits) includes:
Main> :sat \s i x -> lcg s i x harderMult == take `{3} harderOutput
(\s i x -> lcg s i x harderMult ==
take`{3} harderOutput) 0x897c9820380325ef 0xa75286c029abc35f
0x00000000dd1aa469 = True
Notice it is actually harder (well, slower) for this method to obtain a solution in which the only unknown is the seed:
Main> :sat \s -> lcg s zero zero trivialMult == take `{3} trivialOutput
... still waiting after many minutes ...
So contrary to my earlier comment it appears a @Charphacy's mental power plus Mathematica has done better on this problem than the typical SMTs.