Of course, this is GF(2) math. XOR is addition and 'XOR-product' is multiplication. So it's in fact \( a^2 + 2ab + b^2 \) over GF(2). I tried to rewrite this equation to \( (a+b)^2 \), but my knowledge of GF(2) is so miserable, so I couln't.

GF(2) multiplication once was implemented by me, where it was used to factor numbers over GF(2). The very same code I can use here.

Now the equation is seemengly easy to solve:

\[ (a \otimes a) \oplus (2 \otimes a \otimes b) \oplus (b \otimes b) = 5 \]

And so I did: PE_877_ideal_world.py. But it would be only possible in an ideal world. Unfortunately, that works only for a under \( ~10^{6} \). \( log_2(10^{18}) = ~60 \) bits, this search space is too big.

% ./PE_877_ideal_world.py f() k=0x5 a_n=0x0, b_n=0x3, result_n=0x5 a_n=0x6, b_n=0xf, result_n=0x5 a_n=0x3, b_n=0x6, result_n=0x5 a_n=0x18000, b_n=0x3f303, result_n=0x5 a_n=0xf303, b_n=0x18000, result_n=0x5 a_n=0x6606, b_n=0xf303, result_n=0x5 a_n=0x3f0f, b_n=0x6606, result_n=0x5 a_n=0x1818, b_n=0x3f0f, result_n=0x5 a_n=0xf3f, b_n=0x1818, result_n=0x5 a_n=0x666, b_n=0xf3f, result_n=0x5 a_n=0x3f3, b_n=0x666, result_n=0x5 a_n=0x180, b_n=0x3f3, result_n=0x5 a_n=0xf3, b_n=0x180, result_n=0x5 a_n=0x66, b_n=0xf3, result_n=0x5 a_n=0x3f, b_n=0x66, result_n=0x5 a_n=0x18, b_n=0x3f, result_n=0x5 a_n=0xf, b_n=0x18, result_n=0x5 a_n=0x3f0f3f, b_n=0x660666, result_n=0x5 a_n=0x181818, b_n=0x3f0f3f, result_n=0x5 a_n=0xf3f0f, b_n=0x181818, result_n=0x5 a_n=0x66606, b_n=0xf3f0f, result_n=0x5 a_n=0x3f303, b_n=0x66606, result_n=0x5 solutions for k=0x5 = 22

However, the output exhibits some clearly visible patterns.

We see some symmetry. One value if used as a, is then used as b. Maybe like ladder.

First variables are 0 and 3 for a and b.

a_n=0x0, b_n=0x3, result_n=0x5 a_n=0x3, b_n=0x6, result_n=0x5 a_n=0x6, b_n=0xf, result_n=0x5 a_n=0x18, b_n=0x3f, result_n=0x5 a_n=0x3f, b_n=0x66, result_n=0x5 a_n=0x66, b_n=0xf3, result_n=0x5 a_n=0xf3, b_n=0x180, result_n=0x5 a_n=0x180, b_n=0x3f3, result_n=0x5 a_n=0x3f3, b_n=0x666, result_n=0x5 a_n=0x666, b_n=0xf3f, result_n=0x5 a_n=0xf3f, b_n=0x1818, result_n=0x5 a_n=0x1818, b_n=0x3f0f, result_n=0x5 a_n=0x3f0f, b_n=0x6606, result_n=0x5 a_n=0x6606, b_n=0xf303, result_n=0x5 a_n=0xf303, b_n=0x18000, result_n=0x5 a_n=0x18000, b_n=0x3f303, result_n=0x5 ...

We see that the following algorithm is manifests itself: find initial/seed pair of values, then try a value as a, and find corresponding b. Then use value of b as a, and find another b. And so on.

Step 1.

Find initial/seed pairs under a<0x1000 and b<0x1000.

Keep in mind, it's still possible to have solutions like:

x y x z

Add a,b and b,a pairs as blocking clause, collect all values.

Step 2.

Inf loop Set a to one of collected value (via assume()) Find all b's, add them to collected values. Add a to blocking clause.

List all solutions, also swap a and b. If a<=b, count that pair as a solution.

(See also: OEIS A000032: Lucas numbers.)

This algorithm is implemented in: PE_877_878.py.

And of course, there is some patterns in these values, but I couldn't crack it.

Now new version: PE_877.py. Result: PE_877_result.txt.

The result is correct.

Now PE 878. As k grows, patterns becomes less visible, if visible at all: k_0xf41fd.txt.

Enumerating all k under \( 10^6 \), this code worked for several days on 13 ARM CPU cores. Yes, painfully slow. But the result is correct. I managed to solve this problem after all, without any specific math knowledge about GF(2).

This is the coolness of SAT/SMT -- it's very helpful for prototyping work, experimenting.

Yes, I know about these lousy Disqus ads. Please use adblocker. I would consider to subscribe to 'pro' version of Disqus if the signal/noise ratio in comments would be good enough.