This Sudoku solver reads values in from CSV or TXT files that have been formatted as a 3x3 grid, and proceeds to evaluate it as a complete Sudoku.

The algorithm relies on the fairly straightforward approach of representing a matrix as a tensor of varying lengths in the 3rd dimension, representing and narrowing down all potential values until it can be reduced to 3x3x1, or this is proven impossible.

We argue for termination in one of two cases – either a discovery that the Sudoku is unsolvable, or in a perfectly solved Sudoku.

Termination occurs in one of two scenarios:

1. A simple linear scan through the matrix reveals that all possible value tensors are reduced to exactly one layer.
2. A comparison between the two most recently updated matrices reveals no change, showing a cessation in updates.

This termination clause exists as per the defintion of a completed Sudoku. We can effectively flatten our tensor to a simple 3x3 matrix once the specified conditions have been met, and the algorithm terminates as per its own definiton.

We argue for termination in failure the following way: Assume that our algorithm is injective, meaning M1 = M2 -> eval(M1) = eval(M2). Let our previous matrix be M1 and our current matrix be M2. eval(M1) = M2 ∧ M1 = M2