From what I can see on Wikipedia and the Internet at large, all sudoku solving algorithms (including human ones) employ some kind of EXPTIME backtracking search for some sudokus.
Are there any SAT solving algorithms that determine satisfiability in worst-case EXPTIME, which only require a worst-case POLYTIME subset of operations for sudokus on $n^2\times n^2$ grids of $n\times n$ blocks, with $n=3$ and a single solution (a subset of UNAMBIGUOUS SAT).
Would such an algorithm be a stepping stone to raise the lower bound for e.g., graph vertex coloring from k>2 to k>3. Or would it just be considered an oddity.
I am mostly interested in the extent of the POLYTIME subset of operations of such an algorithm and any actual proof that an algorithm indeed solves all instances of 3x3 sudokus, not just experimental evidence.
The papers I have come across so far, are somewhat lacking in the sample set (e.g., the assumption that the number of clues correlates to the hardness is simply unfounded). No analysis is given that correlates the hardness of a sudoku to identifiable structural properties (like the XOR loops that make some problems hard for CDCL).
CSP algorithms seem to be best suited for such questions, but do not provide much insight into the structure of a specific problem instance.
To illustrate the context of my question, here are two papers which explicitly identify POLYTIME subsets of the applied algorithm:
Helmut Simonis, Sudoku as a Constraint Problem, CP Workshop on Modeling and Reformulating Constraint Satisfaction Problems, 2005, pages 13-28. In this paper sudokus are categorized with regard to how many solutions were obtained "search free".
I. Lynce, J. Ouaknine, Sudoku as a SAT problem, in 9th International Symposium on Artificial Intelligence and Mathematics AIMATH'06, January 2006. However, the sample sudokus (only 17 clue sudokus) are very weak, which explains the result, that only polynomial operations were necessary.