Sudoku and 2SAT

I've updated PADS, my Python algorithm implementation library, to include

• The condensation of a directed graph.

• A bit-parallel algorithm for testing reachability in a directed acyclic graph; after a linear number of bit-vector operations, one can test reachability between any pair of vertices in constant time.

• A 2-satisfiability solver that uses reachability in the condensation of an implication graph to determine which variables have values that are fixed to true or fixed to false in all solutions to a given 2SAT instance.

• An optional rule for my Sudoku solver that transforms the puzzle into a 2SAT instance with at least as many solutions, and uses the fixed variables of this instance to make inferences about the puzzle.

In more detail, a 2SAT instance is represented as a collection of implications, that if one variable or negated variable is true then so must be another. The 2SAT instance for a Sudoku puzzle has a variable for each combination of a cell and a digit. There are obvious 2SAT implications between these variables: if a digit is placed somewhere, no other digit can be placed there, and the same digit cannot be placed anywhere else in the same row, column, or square. But these aren't enough to get any useful information out of the 2SAT solver, because with only these implications the resulting 2SAT instance could be trivially solved by making all variables false. To get something nontrivial, we need to add some other implications: if a cell can only contain two possible digits, then if one digit is not placed in that cell the other digit must be placed there, and if a digit can only go in two cells within a row, column, or square, and if it is not placed in one of these cells it must be placed in the other. I also included implications whenever a placement of a digit in one cell eliminates all but one placement of the same digit in another row, column, or square.

The new smarter Sudoku solver still needs to backtrack on some puzzles, but many fewer of them than before. Here's one that it still finds difficult:

 ----------------------------------- 
| .   .   . | 9   .   2 | .   .   . |
|           |           |           |
| 8   .   . | .   4   . | .   .   3 |
|           |           |           |
| .   4   . | 7   .   . | 1   .   . |
|-----------------------------------|
| .   .   6 | .   .   9 | .   .   1 |
|           |           |           |
| .   2   . | .   .   . | .   7   . |
|           |           |           |
| 5   .   . | 3   .   . | 4   .   . |
|-----------------------------------|
| .   .   7 | .   .   3 | .   6   . |
|           |           |           |
| 6   .   . | .   1   . | .   .   5 |
|           |           |           |
| .   .   . | 2   .   6 | .   .   . |
 ----------------------------------- 

Comments: