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.