31–39 of 39 posts
Earlier quoted context omitted.
We know that the GCD is divisible by 9 because the sum of the digits for every row is 45.
Not necessarily. The sum of the digits ranges from 36-45, there are 10 possible digits of which 9 will be used. If, say, 5 were the unused number then it would not be divisible by 9.
I don't think it would make a large difference in runtime, but the bounds aren't quite right. The largest possible value isn't 999,999,999, because that's not a legal value. The largest value is 987,654,321 Dividing that by 9, you get 109,739,369, but that's not a legal value either, you'd want to start with 109,738,365 for the gcd as it's a valid possible row. I don't know that all gcds would need to be a valid row,…
> you'd want to start with 109,738,365 for the gcd as it's a valid possible row Nitpick: that has two threes. Also, what’s wrong with 109,738,654 from that argument’s view?
Earlier quoted context omitted.
That is true, indeed. It could be that the author is just massively unskilled at writing Z3 code.
Oh come on ... Either one of the two statements is true, no other way around.
Who asked?
This is why choosing the right tool for the job matters. Z3 is hilariously overkill for such a problem (not to undermine how interesting and useful Z3 is, and not to accuse the author of doing anything wrong).
Z3 is only one class of solver; a finite domain constraint solver is much more suited to these sorts of tasks.
https://gist.github.com/Qix-/3580f268e2725848971703e74f6b26b...
$ time node sudoku.js
1 2 7 6 8 5 4 3 9
5 9 4 1 3 7 8 2 6
8 3 6 4 2 9 5 7 1
3 6 1 8 5 4 2 9 7
7 4 5 2 9 1 3 6 8
2 8 9 3 7 6 1 5 4
6 5 3 9 1 8 7 4 2
4 1 2 7 6 3 9 8 5
9 7 8 5 4 2 6 1 3
0:00.08elapsed> My first attempt when solving this puzzle was to encode the constraints as an SMT optimization problem, and using Z3 to find the solution. This is why choosing the right tool for the job matters. Z3 is hilariously overkill for such a problem (not to undermine how interesting and useful Z3 is, and not to accuse the author of doing anything wrong). Z3 is only one class of solver; a finite domain constraint solver is…
GCD(127685439, 594137826, 836429571, ...) = 9
but the author finds one GCD with 8 digits.
Also, for this reason it's important in this version to keep the "0" as "0" instead of mapping it to "1".
Earlier quoted context omitted.
(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.
It's brute force after a complete rewrite of the problem.
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.
Earlier quoted context omitted.
Oh come on ... Either one of the two statements is true, no other way around.
Why did you bring such negativity to this thread? "Either one of my two rude statements is true!" Who asked?
It's a forum, people come here to discuss the submissions.
You should know this ...
Earlier quoted context omitted.
It's brute force after a complete rewrite of the problem.
??? 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.
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)
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
It's very difficult for a compiler to transform one into the other.
The last time I saw a puzzle like this it led me to https://www.kakurokokoro.com