[QUOTE=Blaster Master]
That would be difficult to prove. They only way you can say it has a unique solution is by running it through a Sudoku solver and verifying that, when the series of known Sudoku rules are applied iteratively, it produces a unique solution. That is, IF there is only a single solution, that information MUST be somehow within the puzzle, and so there must be some for of logic that can extract that information, otherwise, it wouldn’t dictate a single solution.
[/quote]
A sudoku site in the UK admitted a year or so ago that their algorithm for constructing puzzles had a bug, leading to some that required “guessing” - actually branching. I don’t know if anyone ever proved this, though.
By unsolvable is really unsolvable or unsolvable under a set of rules? The latter is clearly true, the former isn’t (assuming a legal configuration) since it would be fairly easy to resort to a recursive backtracking algorithm whenever no squares can be filled in by a given set of rules. Since the puzzle is finite the heuristic will terminate, and since there are a lot of constrained squares after a choice I suspect it would be reasonably efficient, given a decent set of rules.