21–30 of 39 posts
Earlier quoted context omitted.
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.
That is true, indeed. It could be that the author is just massively unskilled at writing Z3 code.
Either one of the two statements is true, no other way around.
I remembered there was a trick to avoid popcount, but I didn't remember it. So I found https://stackoverflow.com/questions/51387998/count-bits-1-on...
That version counts, the 1 bit's but here we already know the number is not 0 and we want to know that the inverted number it has exactly 1 bit set, so instead of
popcnt(n) == 1
n & (n-1) == 0
n = 0b1111111111 - s
s | (s+1) == 0b1111111111For 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”?
It took 3 readings and a scan of some of the later words but I think this is the correct reading
So a naive program can just solve the puzzle repeatedly, differently, and ccmpute the GCD of the rows, and output the one with the highest result. There aren't infinitely many solutions to a sodoku style puzzle, so...?
Should look into Knuth’s DLX. My JS implementation solved this case in 1.8ms
Earlier quoted context omitted.
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.
(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.
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,…
Nitpick: that has two threes.
Also, what’s wrong with 109,738,654 from that argument’s view?
If the floating point trick worth it? When I was young, floating point operations were very slow and I still try to avoid them like the plague. I remembered there was a trick to avoid popcount, but I didn't remember it. So I found https://stackoverflow.com/questions/51387998/count-bits-1-on... That version counts, the 1 bit's but here we already know the number is not 0 and we want to know that the inverted number it…
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,…
The GCD search should start at 098,765,432 and then go down from there.
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.