11–20 of 39 posts
If anything, what a testament of the massive failure Z3 is.
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.
I think it's the first time I see such thing in the wild.
Sigh. My friend did this problem on pen and paper and made me feel stupid. Their solution was so wildly clever! It relied on the observation that the sum of the rows of the sudoku board (given the digits in use) is a known fixed value, and went from there (I'll leave the rest as an exercise to the reader to avoid spoilers).
This isn't exactly a sudoku board, because they allow for 0.
If you use 1-9, sum is 45. For anything else, it's 45 - (the unused number).
Sigh. My friend did this problem on pen and paper and made me feel stupid. Their solution was so wildly clever! It relied on the observation that the sum of the rows of the sudoku board (given the digits in use) is a known fixed value, and went from there (I'll leave the rest as an exercise to the reader to avoid spoilers).
This isn't exactly a sudoku board, because they allow for 0.
If anything, what a testament of the massive failure Z3 is.
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.
It could be that the author is just massively unskilled at writing Z3 code.
For us slow kids in the back what does this mean, “[…] such that the nine 9-digit numbers formed by the rows of the grid has the highest-possible GCD over any such grid”?
Suppose the GCD was divisible by 2, then all rows would be even. Since the last digit of an even integer is in {0,2,4,6,8} and we need 9 unique numbers in the final column, we know that 4 or 5 of the row numbers must be odd. So the GCD can't be even.
Similarly, the GCD can't be divisible by 5. If it were, all rows numbers would need a 0 or 5 in the final digit.
Sigh. My friend did this problem on pen and paper and made me feel stupid. Their solution was so wildly clever! It relied on the observation that the sum of the rows of the sudoku board (given the digits in use) is a known fixed value, and went from there (I'll leave the rest as an exercise to the reader to avoid spoilers).
Since we're over-engineering here, one more optimization is to skip all potential GCDs that are divisible by 2 or 5. Suppose the GCD was divisible by 2, then all rows would be even. Since the last digit of an even integer is in {0,2,4,6,8} and we need 9 unique numbers in the final column, we know that 4 or 5 of the row numbers must be odd. So the GCD can't be even. Similarly, the GCD can't be divisible by 5. If it we…
Since we're over-engineering here, one more optimization is to skip all potential GCDs that are divisible by 2 or 5. Suppose the GCD was divisible by 2, then all rows would be even. Since the last digit of an even integer is in {0,2,4,6,8} and we need 9 unique numbers in the final column, we know that 4 or 5 of the row numbers must be odd. So the GCD can't be even. Similarly, the GCD can't be divisible by 5. If it we…
We know that the GCD is divisible by 9 because the sum of the digits for every row is 45.