5 ms·
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 no
by fn-mote 2y ago
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 2y ago(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 2y agoIt's brute force after a complete rewrite of the problem.
- moralestapia 2y ago??? 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 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.