[moralestapia]

(Way) worse than exhaustive brute force search ... you don't really have to say much more.

I think it's the first time I see such thing in the wild.

[gus_massa]

It's brute force after a complete rewrite of the problem.

[moralestapia]

???

No, I mean even the most naive brutal force code comes back after ~10 minutes, whereas the Z3 didn't finish even after "several hours".

I am now quite curious about writing a Z3 implementation of this myself and try to figure out why is it taking that much time.

[gus_massa]

[Sorry for my bad pseudo-python.] My guess is that the implementation in Z3 in he article was like

  max_gcd = 0
  for a1 in range(9):
    for b1 in range(9):
      ...
        *check_valid(a1, b1, ...)*
        n1 = to_number(a1, b1, ...)
        ...

        new_gcd = gcd(n1, n2, ...)
        max_gcd = max(max_gcd, new_gcd)

and the first brute force version was

  for gcd in range(111111111):
  for r1 in range(?):
    for r2 in range(?):
      ...
        a1, a2,... = split(r1*gcd)
        ...
        *check_valid(a1, b1, ...)*
        max_gcd = gcd

(I guess the author was checking earlier, but let's put only one check in may fake version.)

It's very difficult for a compiler to transform one into the other.