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]
From Sudoku Solver to Program Synthesis
11–20 of 25 posts
Re: From Sudoku Solver to Program Synthesis
#12When 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 work…
Yep, backtracking works fine. If you only want the solution, then you don't need complex rules. But, you really want more than just the solution.
Check out http://sudokuwiki.com/sudoku.htm
This solver (and the whole site) is the best one I know of, and it will solve a puzzle by using rules in order of difficulty, to guarantee it tries the simple rules you know before resorting to backtracking.
The benefits of this are that you can grade the difficulty of a sudoku board. You can also solve a puzzle up to the "crux" and then work on only the hard moves manually. I like doing that so I can skip the hours of boring stuff and practice doing the more tricky inferences. Andrew's site is a window into how big of a rabbit hole Sudoku can be...
Re: From Sudoku Solver to Program Synthesis
#13When 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 work…
Yep, backtracking works fine. If you only want the solution, then you don't need complex rules. But, you really want more than just the solution. Check out http://sudokuwiki.com/sudoku.htm This solver (and the whole site) is the best one I know of, and it will solve a puzzle by using rules in order of difficulty, to guarantee it tries the simple rules you know before resorting to backtracking. The benefits of this ar…
If you are interested in grading Sudokus by the difficulty of the human solving techniques required, you might want to check out the following two books:
- "Sudoku Programming with C" [https://www.apress.com/de/book/9781484209967] where a Sudoku solver and grader is implemented.
- "A to Z of Sudoku" [https://www.wiley.com/en-us/A+to+Z+of+Sudoku-p-9781847040008] where many human solving techniques are described and rated by their difficulty.
Re: From Sudoku Solver to Program Synthesis
#14Don't hijack scrolling.
Re: From Sudoku Solver to Program Synthesis
#15When 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 work…
this comment made me lose interested, too, even my interest in the article.
Re: From Sudoku Solver to Program Synthesis
#16TLDR : 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
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 (a…
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.
Re: From Sudoku Solver to Program Synthesis
#17So 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?
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.
Re: From Sudoku Solver to Program Synthesis
#18Don't hijack scrolling.
We don't. Which browser/OS are you seeing this on?
Re: From Sudoku Solver to Program Synthesis
#19When 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 work…
My first attempt did no backtracking at all. It would guess randomly, propagate constraints and continue. If it got stuck, it would just start again. The most it ever took to solve a puzzle was 2100 attempts. Sure it wasn't guaranteed to solve a puzzle in finite time, but it worked well enough for something written during one of those endless big-corp conference calls.
Technically, this is backtracking... to move 1.
Re: From Sudoku Solver to Program Synthesis
#20When 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 work…
Backtracking as a strategy definitely seems... underwhelming. But it does have its uses. I wrote a few solvers, and they all served a different purpose. One was based on Norvig's python post on the subject; I used that to generate many puzzles very quickly. Then I used a backtracker (using Knuth's Dancing Links) to reduce the set to puzzles with only a single solution. The last solver was a "human" solver that used various known strategies; this let me grade difficulty without having to manually attempt every puzzle (although I still found it useful in my app UI to tag puzzles as being too hard/easy). The human solver is incredibly inefficient, but the one with the most room for growth (new strats, etc).