5 ms·

From Sudoku Solver to Program Synthesis

48 points by saurabh20n 8y ago

x11 8y ago
Just how long more should I leave my solver running ?
sevensor 8y ago
So is this meant to be an advertisement for their product, or are they trying to recruit? Why are they trying to filter for people who can write a sudoku solver?
- deleted 8y ago
  [deleted]
- saurabh20n 8y ago
  We are looking for people who want to play around with constraint solvers. As others in this thread have mentioned, the vanilla Sudoku is not hard to really need constraint solvers; a generalized version would. We don't expect people to have backgrounds in program synthesis, but constraint solving is a start. That said, it is just a fun problem. PTime specialized solutions are even more intriguing.
yazr 8y ago
TLDR : we use a solver to go from a formal constraint specification to an Ethereum smart contract So 1. the initial specification is still a formal constraint 2. the domain complexity is low 3. Use well known solvers to generate code in a DSL
- saurabh20n 8y ago
  This page was just a fun exercise; seems to have missed communicating fully how we use synthesis. My bad. You are right about about "2." and part of "3.". For "2." yes, the smart contracts are indeed simpler (small code, gas limits, closed systems). So we can skip some major hurdles that more general techniques need -- case in point the FB abstract interpretation framework Sparta here yesterday. For "3." we use Z3 (as should everybody :)!) but the target language for synthesis is Solidity. [ Hope you didn't mean Solidity is a DSL, coz that would be a generous interpretation of that word. ] The initial spec is another smart contract (call it IN), so code and not a formal constraint. We synthesize another smart contract (call it OUT), such that the combination (IN + OUT) behaves well. See work on synthesizing program inverters for the background ideas (http://saurabh-srivastava.com/pubs/pldi11-pins.pdf http://saurabh-srivastava.com/pubs/pldi11-pins.pdf)
  - yazr 8y ago
    Thanks for the explanation. Program synthesis is HARD, and we may never solve it, so any progress on this is great to read about. Good luck with this.
Isamu 8y ago
When I wrote a Sudoku solver I was disappointed to find that backtracking worked maybe too well; that is, I coded in the minimum constraints to follow the rules of the game and then added backtracking and voila, it found solutions quickly enough. Why was I disappointed? Because initially I wanted to write a solver that inferred more, that used the inferences that I made when solving Sudoku. Sadly once the solver worked, I kinda lost interest. I hate backtracking myself and it should only be necessary at a certain Sudoku hardness level - every puzzle below that level of hardness should be solvable without backtracking.
- deleted 8y ago
  [deleted]
- saurabh20n 8y ago
  You are absolutely right. Punching "extra holes" in puzzles of certain hardness should make backtracking not as viable. But we'll loose the unique solution property. Might make it more interesting? And maybe even bias it towards human-abilities. I think intuitively we're better at solving when the possibilities are more than 1 (just a conjecture.)
  - wiredfool 8y ago
    My soduku solver from ca~10 years back ran the "hardest" soduku puzzles in < 10 seconds on a netbook atom processor. IIRC, the hardest one that I ever threw at it had 7 levels of backtracking. It's just not that hard of a problem compared to the speed of computers.
- daxfohl 8y ago
  You can make it harder by using 16x16, 25x25, 36x36 etc boards, and see how fast you can make it. There are lots of known patterns to allow for elimination of options http://www.sudokuwiki.org/Getting_Started http://www.sudokuwiki.org/Getting_Started, of different computation complexity relative to each other, and all faster than regular backtracking. So the goal is to find the order at which to apply them for maximum speed and minimal need to backtrack. You can also try to multithread and use GPU, or FPGA if you're nuts. All that said, it's all still pretty mechanical. So if you're looking for something more inferential, then another game would be better.
Avery3R 8y ago
Don't hijack scrolling.
- saurabh20n 8y ago
  We don't. Which browser/OS are you seeing this on?
  - Avery3R 8y ago
    Yes, you do. Any browser on any os. https://synthetic-minds.com/smoothscroll.js https://synthetic-minds.com/smoothscroll.js hijacks scrolling and messes with the native scrolling behavior
    - saurabh20n 8y ago
      Removed! We are not front-end people :) and it wasn't an active choice. Let me know if you see anything else. Sincerely appreciate the help.
sigstoat 8y ago
now that my solver has been chugging along for awhile, and i'm sort of bored of fiddling around with the supporting bits, i find myself wondering: since there's a politely-requested limit on submission rate, isn't the person who solves the most basically just the one who wrote an automatic solver fastest and/or leaves it running the longest?
- sigstoat 8y ago
  well, you guys were sneakier than i initially expected, and clearly more clever than me, as i can't figure out the pattern. oh well.

48 points by saurabh20n 8y ago

x11 8y ago

Just how long more should I leave my solver running ?

So is this meant to be an advertisement for their product, or are they trying to recruit? Why are they trying to filter for people who can write a sudoku solver?

deleted 8y ago
[deleted]
saurabh20n 8y ago
We are looking for people who want to play around with constraint solvers. As others in this thread have mentioned, the vanilla Sudoku is not hard to really need constraint solvers; a generalized version would. We don't expect people to have backgrounds in program synthesis, but constraint solving is a start. That said, it is just a fun problem. PTime specialized solutions are even more intriguing.

yazr 8y ago

TLDR : we use a solver to go from a formal constraint specification to an Ethereum smart contract So 1. the initial specification is still a formal constraint 2. the domain complexity is low 3. Use well known solvers to generate code in a DSL

saurabh20n 8y ago
This page was just a fun exercise; seems to have missed communicating fully how we use synthesis. My bad. You are right about about "2." and part of "3.". For "2." yes, the smart contracts are indeed simpler (small code, gas limits, closed systems). So we can skip some major hurdles that more general techniques need -- case in point the FB abstract interpretation framework Sparta here yesterday. For "3." we use Z3 (as should everybody :)!) but the target language for synthesis is Solidity. [ Hope you didn't mean Solidity is a DSL, coz that would be a generous interpretation of that word. ] The initial spec is another smart contract (call it IN), so code and not a formal constraint. We synthesize another smart contract (call it OUT), such that the combination (IN + OUT) behaves well. See work on synthesizing program inverters for the background ideas (http://saurabh-srivastava.com/pubs/pldi11-pins.pdf http://saurabh-srivastava.com/pubs/pldi11-pins.pdf)
- yazr 8y ago
  Thanks for the explanation. Program synthesis is HARD, and we may never solve it, so any progress on this is great to read about. Good luck with this.

Isamu 8y ago

When I wrote a Sudoku solver I was disappointed to find that backtracking worked maybe too well; that is, I coded in the minimum constraints to follow the rules of the game and then added backtracking and voila, it found solutions quickly enough. Why was I disappointed? Because initially I wanted to write a solver that inferred more, that used the inferences that I made when solving Sudoku. Sadly once the solver worked, I kinda lost interest. I hate backtracking myself and it should only be necessary at a certain Sudoku hardness level - every puzzle below that level of hardness should be solvable without backtracking.

deleted 8y ago
[deleted]
saurabh20n 8y ago
You are absolutely right. Punching "extra holes" in puzzles of certain hardness should make backtracking not as viable. But we'll loose the unique solution property. Might make it more interesting? And maybe even bias it towards human-abilities. I think intuitively we're better at solving when the possibilities are more than 1 (just a conjecture.)
- wiredfool 8y ago
  My soduku solver from ca~10 years back ran the "hardest" soduku puzzles in < 10 seconds on a netbook atom processor. IIRC, the hardest one that I ever threw at it had 7 levels of backtracking. It's just not that hard of a problem compared to the speed of computers.
daxfohl 8y ago
You can make it harder by using 16x16, 25x25, 36x36 etc boards, and see how fast you can make it. There are lots of known patterns to allow for elimination of options http://www.sudokuwiki.org/Getting_Started http://www.sudokuwiki.org/Getting_Started, of different computation complexity relative to each other, and all faster than regular backtracking. So the goal is to find the order at which to apply them for maximum speed and minimal need to backtrack. You can also try to multithread and use GPU, or FPGA if you're nuts. All that said, it's all still pretty mechanical. So if you're looking for something more inferential, then another game would be better.

Avery3R 8y ago

Don't hijack scrolling.

saurabh20n 8y ago
We don't. Which browser/OS are you seeing this on?
- Avery3R 8y ago
  Yes, you do. Any browser on any os. https://synthetic-minds.com/smoothscroll.js https://synthetic-minds.com/smoothscroll.js hijacks scrolling and messes with the native scrolling behavior
  - saurabh20n 8y ago
    Removed! We are not front-end people :) and it wasn't an active choice. Let me know if you see anything else. Sincerely appreciate the help.

sigstoat 8y ago

now that my solver has been chugging along for awhile, and i'm sort of bored of fiddling around with the supporting bits, i find myself wondering: since there's a politely-requested limit on submission rate, isn't the person who solves the most basically just the one who wrote an automatic solver fastest and/or leaves it running the longest?

sigstoat 8y ago
well, you guys were sneakier than i initially expected, and clearly more clever than me, as i can't figure out the pattern. oh well.