3 ms·

??? 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 cur

• gus_massa 2y ago
  [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.