Satoku Matrix CSP Solver Statistics¶

Despite the name Satoku Matrix[1], it is not a special algorithm for sudoku, but a generic algorithm for structural analysis of CDF (generalized CNF)[2] problems.

The sudoku is therefore formulated as CSP problem and encoded as propositional clauses in conjunctive normal form (CNF). The codified problem is then mapped to a satoku matrix, where each alternative of a clause is represented as a state.

The matrix is then consolidated, i.e., the immediate consequences of conflicts between states are propagated throughout the matrix (0 consolidation). This step already determines the solution for most of the unsolvable sudokus.

In the next step, the satoku matrix is reduced, i.e., separate clauses are combined into a single clause, if that results in a smaller matrix (1 reduction).

Finally, the binary alternatives between states are expanded, which reveals the solution for the hardest sudokus (2 minor CCR check).

Currently, there are no known sudokus, which require further processing.

The HDP hardness and the satoku matrix hardness correlate quite nicely, at least a multitude better than e.g. straightforward depth first search (SDFS).