Sodoku
From Tractatus
I head of this game recently (August 2005) and so when I actually saw it in the Washington Post I decided to try it.
The puzzle is simple enough. Given a nine by nine grid assign a digit to each cell with the following restrictions:
- Some of the cells have already been filled in for you, to make sure there is only one solution.
- Every digit must appear in every row exactly once
- Every digit must appear in every column exactly once
- If the large box is divided into thee by three boxes, every digit must appear in box exactly once.
You can find some examples here.
I really like these puzzles. At their core, they are logic puzzles. They pose lots of interesting questions. But, the underlying logic is simple enough to be easily understand. A number of the sites providing 'strategies' were intesting because they showed high level reasoning about the puzzle, but usually without a basis in logic.
The interesting questions in my mind are:
- How many of these puzzles exist?
- Given a puzzle, categorize how difficult the puzzle is to solve.
- Given a completed grid, find a subset which uniquely determines the grid, in fact, find the hardest subset.
- Given a puzzle, find the solution in the least possible time.
- Given a puzzle, provide a proof showing that the solution is unique.
- Given a grid, and elements, provide a proof showing which, if any, or the provided elements a named cell is equal to.
Note that given a complete grid, it is trivial to check if it is a solution(extensions of this problem would be in NP). So, most of my questions that have to do with solutions involve the process used to generate the solution. Guessing is uninteresting. It is too easy.
I believe that a useful metric for saying that one puzzle is more difficult than another would be if the first puzzle requires longer proofs than the second.
Because the puzzles are so easy to verify, it is interesting then to start with a completed grid and produce from it the hardest puzzle.
to be continued.
Add logic of Sodoku
Logic
The grid is a failrly straight forward finite geometry. Each column, row, and square is a line. The normal rules of geometry do not apply. Some lines intersect normally, each column and row share exactly one cell. Some lines intersect each other in three cells, squares and columns. Some do not intersect at all, two squares.
The next important observations is that the problem does not actually require any digits at all. In order for the puzzle to be unique, at least eight digits must have been given to us(the last is implied). In stead of thinking of them as digits, think of them as 'equal to the first of the given cells,' 'equal to the second,' ... 'equal to the eighth,' 'not equal to any of the other cells.'
x = y is the same as
L_00 = {0,1,2,10,11,12,20,21,22} \forall L \forall x,y \in L. x!=y \forall L,M \exists x \in L \exists y \in M x=y