3 ms·
If anything, what a testament of the massive failure Z3 is.
by moralestapia 2y ago
If anything, what a testament of the massive failure Z3 is.
- fn-mote 2y agoCan 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.
- Jtsummers 2y agoUnless 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 2y agoThat is true, indeed. It could be that the author is just massively unskilled at writing Z3 code.
- moralestapia 2y agoOh come on ... Either one of the two statements is true, no other way around.
- AlexeyBelov 2y agoWhy did you bring such negativity to this thread? "Either one of my two rude statements is true!" Who asked?
- moralestapia 2y agoWho asked you, though? It's a forum, people come here to discuss the submissions. You should know this ...