[moralestapia]

If anything, what a testament of the massive failure Z3 is.

[Jtsummers]

Unless I missed it, their Z3 solution wasn't even presented. So we can't comment on how good or bad Z3 is without seeing how good or bad their Z3 attempt was.

[moralestapia]

That is true, indeed.

It could be that the author is just massively unskilled at writing Z3 code.

[moralestapia]

Oh come on ...

Either one of the two statements is true, no other way around.

[AlexeyBelov]

Why did you bring such negativity to this thread? "Either one of my two rude statements is true!"

Who asked?

[moralestapia]

Who asked you, though?

It's a forum, people come here to discuss the submissions.

You should know this ...

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