I need to find all triples of 16-bit numbers (x, y, z) (well, actually only bits which perfectly match up in different triples with bits on same positions), such that
y | x = 0x49ab
(y >> 2) ^ x = 0x530b
(z >> 1) & y = 0x0883
(x << 2) | z = 0x1787
Straight ahead tactics would require about 2 days on 8700K, which is too much (even if I'll use all PCs I have access (R5-3600, i3-2100, i7-8700K, R5-4500U, 3xRPi4, RPi0/W) it would take too much time).
If bit shift wasn't in equations then it would be trivial to do that, but with shifts it's too hard to do the same thing (or maybe even impossible).
So I came up to pretty interesting solution: parse equations into statements about bits of numbers (something like "3rd bit of x XOR 1st bit of y is equal 1") and with all these statements written in something like Prolog language (or just interpret them using truth tables of operations) executed all unambiguous bits would be found. This solution is pretty hard too: I have no idea how to write such parser and no experience in Prolog. (*)
So the question is: What would be the best way to do this? And if it's (*) then how to do that?
Edit: for easier coding here the binary pattern of the numbers:
0x49ab = 0b0100100110101011
0x530b = 0b0101001100001011
0x0883 = 0b0000100010000011
0x1787 = 0b0001011110000111
There are four solutions. In all of them, x = 0x4121, y = 0x48ab. There are four options for z (two of its bits are free to be 0 or 1), namely 0x1307, 0x1387, 0x1707, 0x1787.
This can be calculated by treating the variables are arrays of 16 bits and implementing the bitwise operations on them in terms of operations on booleans. That could probably be done in Prolog, or it could be done with a SAT solver or with binary decisions diagrams, I used this website which uses BDDs internally.