[fn-mote]

Can you say more about this?

On the face of it this comment seems ridiculous to me. Z3 is fabulously successful in other domains. Perhaps the problem fit is not there, or the problem encoding chosen was not appropriate.

[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.