6 ms·

Here's a solver in python with z3: https://gist.github.com/sielicki/fd86d68733133f654128519b3c4e12c2 https://gist.github.com/sielicki/fd86d68733133f654128519b3c

Here's a solver in python with z3: https://gist.github.com/sielicki/fd86d68733133f654128519b3c4e12c2 https://gist.github.com/sielicki/fd86d68733133f654128519b3c4... (note, most of the code coming from here, I just slopped together the additional constraints, https://ericpony.github.io/z3py-tutorial/guide-examples.htm https://ericpony.github.io/z3py-tutorial/guide-examples.htm ) $ time python3 game.py [[4, 8, 3, 7, 2, 6, 1, 5, 9], [7, 2, 6, 1, 5, 9, 4, 8, 3], [1, 5, 9, 4, 8, 3, 7, 2, 6], [8, 3, 7, 2, 6, 1, 5, 9, 4], [2, 6, 1, 5, 9, 4, 8, 3, 7], [5, 9, 4, 8, 3, 7, 2, 6, 1], [3, 7, 2, 6, 1, 5, 9, 4, 8], [6, 1, 5, 9, 4, 8, 3, 7, 2], [9, 4, 8, 3, 7, 2, 6, 1, 5]] python3 game.py 7.47s user 0.15s system 97% cpu 7.801 total

gabrielsroka 6y ago
Each row is a cycle [?] of 483 726 159. And even the cycles have a pattern: 665 665 66. That is, you can rotate the first row by 6 to get the second row, then rotate again by 6, then by 5, etc. The columns are almost as consistent, but not quite.
dreamer_soul 6y ago
I love how z3 code looks like magic! Seems like a good library to start getting the hang of
carapace 6y ago
FWIW, "Boring Sudoku" a solver in Prolog w/ CLP(FD): https://swish.swi-prolog.org/p/Boring%20Sudoku.swinb https://swish.swi-prolog.org/p/Boring%20Sudoku.swinb - - - - I don't mean this in a critical way, just an observation. To me the video was boring because watching a human do machine work is frustrating (to me). (As fast and as clever as that fellow is, he's still so slow compared to a computer.) However, designing elegant constraint rules to encode the special constraints of this puzzle is also a puzzle, and that puzzle seems interesting to me. (Although not very because it's not that challenging.) I have the same problem with most video games: after playing just a little while I get bored and want to reprogram the game itself instead of just playing it. Do y'all feel me, or am I just a freak?
- kryptn 6y ago
  > To me the video was boring because watching a human do machine work is frustrating (to me). I wouldn't think Sudoku is machine work. Yes, a machine can solve it, but it's not intended to be machine work.
  - carapace 6y ago
    It's intended as recreation, yeah, but to me watching that video was like watching someone carry large rocks without aid of a wheelbarrow. Or like digging a large ditch without aid of a backhoe. To me there is a clear hierarchy or graduation of puzzles. Metaphorically: 1. Ditch digging by hand. 2. Planning efficient ditch layouts to be dug by machines. 3. Designing new and better ditch digging machines. - - - - 1. Solving Sudoku puzzles. 2. Designing new Sudoku puzzles (with additional constraints even.) 3. Designing e.g. CLP(FD) programs to solve all sudoku puzzles everywhere. - - - - What I'm saying is, Why don't people move up that hierarchy? Why is level 1 so fascinating to people? I believe that anyone who can solve sudoku can program a computer, but they don't. Why not?
    - carapace 6y ago
      Futamura Projections
    - dEnigma 6y ago
      You can have fun at all those levels, jumping back and forth between them at your leisure. Just because you can program a computer to solve a sudoku doesn't mean that you can't enjoy solving one by hand from time to time. Digging a ditch can be fun too, as long as you don't have to do it all the time.
- nickysielicki 6y ago
  That's cool, but that doesn't solve this puzzle. It's just a normal solver unless I'm missing something.
  - carapace 6y ago
natrys 6y ago
I used Picat which provides a uniform API for many different flavour of solvers (e.g. smt module uses z3 underneath): https://gist.github.com/natrys/c19be79ac93578674540cdfa7a0dfcb4 https://gist.github.com/natrys/c19be79ac93578674540cdfa7a0df... I get instantaneous answer with apparently zero backtrack with both SAT and SMT module. Though I don't know how reliable this statistics is.

gabrielsroka 6y ago

Each row is a cycle [?] of 483 726 159. And even the cycles have a pattern: 665 665 66. That is, you can rotate the first row by 6 to get the second row, then rotate again by 6, then by 5, etc. The columns are almost as consistent, but not quite.

dreamer_soul 6y ago

I love how z3 code looks like magic! Seems like a good library to start getting the hang of

carapace 6y ago

FWIW, "Boring Sudoku" a solver in Prolog w/ CLP(FD): https://swish.swi-prolog.org/p/Boring%20Sudoku.swinb https://swish.swi-prolog.org/p/Boring%20Sudoku.swinb - - - - I don't mean this in a critical way, just an observation. To me the video was boring because watching a human do machine work is frustrating (to me). (As fast and as clever as that fellow is, he's still so slow compared to a computer.) However, designing elegant constraint rules to encode the special constraints of this puzzle is also a puzzle, and that puzzle seems interesting to me. (Although not very because it's not that challenging.) I have the same problem with most video games: after playing just a little while I get bored and want to reprogram the game itself instead of just playing it. Do y'all feel me, or am I just a freak?

kryptn 6y ago
> To me the video was boring because watching a human do machine work is frustrating (to me). I wouldn't think Sudoku is machine work. Yes, a machine can solve it, but it's not intended to be machine work.
- carapace 6y ago
  It's intended as recreation, yeah, but to me watching that video was like watching someone carry large rocks without aid of a wheelbarrow. Or like digging a large ditch without aid of a backhoe. To me there is a clear hierarchy or graduation of puzzles. Metaphorically: 1. Ditch digging by hand. 2. Planning efficient ditch layouts to be dug by machines. 3. Designing new and better ditch digging machines. - - - - 1. Solving Sudoku puzzles. 2. Designing new Sudoku puzzles (with additional constraints even.) 3. Designing e.g. CLP(FD) programs to solve all sudoku puzzles everywhere. - - - - What I'm saying is, Why don't people move up that hierarchy? Why is level 1 so fascinating to people? I believe that anyone who can solve sudoku can program a computer, but they don't. Why not?
  - carapace 6y ago
    Futamura Projections
  - dEnigma 6y ago
    You can have fun at all those levels, jumping back and forth between them at your leisure. Just because you can program a computer to solve a sudoku doesn't mean that you can't enjoy solving one by hand from time to time. Digging a ditch can be fun too, as long as you don't have to do it all the time.
nickysielicki 6y ago
That's cool, but that doesn't solve this puzzle. It's just a normal solver unless I'm missing something.
- carapace 6y ago

natrys 6y ago

I used Picat which provides a uniform API for many different flavour of solvers (e.g. smt module uses z3 underneath): https://gist.github.com/natrys/c19be79ac93578674540cdfa7a0dfcb4 https://gist.github.com/natrys/c19be79ac93578674540cdfa7a0df... I get instantaneous answer with apparently zero backtrack with both SAT and SMT module. Though I don't know how reliable this statistics is.