## [Math][SAT] Project Euler 877 and 878: solving using SAT-solver

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.


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

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.

###### (the post first published at 20240718.)

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.