Is any sudoku solver an SAT solver?

Question

I have recently created a sudoku solver using C#, which outputs the solution to a sudoku after a reasonable amount of time in many cases. I have used the basic sudoku SAT-reduction (i.e. x111 meaning this is true if column 1, row 1 is filled by 1). The method I have done this does not take in a large clause of variables, but implicitly solves a large proposition (which can be generated) for each puzzle.

Due to the lack of universality, that it can't take in any clause for any other np-complete puzzle, does this still count as an SAT solver? And are there multiple ways of reducing sudoku into SAT (i.e. could you have many different ways of having that large proposition)?

Edit: the way I have created the sudoku solver is by representing each cell by 9 variables, which are classes in the solution. The program converts the user's input into a Boolean proposition made specifically for sudoku (i.e. obeying all sudoku constraints). It then solves the proposition. Due to the fact that sudoku has been reduced to SAT and solved, I'm wondering if the program counts as an SAT solver (to which I believe the answer is no, because it won't take any propositional formula and solve it). However, I also want to know of the 'uniqueness' of sudoku is in a way lost when converted to SAT, because 'real' sudoku problems only have one solution, but as far as I know, SAT only wants to know if there is a possible solution or not.

Answer 1

Your program is not a SAT solver. A SAT solver takes as input a SAT formula and outputs whether it is satisfiable or not. Your program doesn't take as input a SAT formula, so it isn't a SAT solver.

Yes, there are multiple ways of reducing Sudoku to SAT.

With standard Sudoku puzzles, we are promised that there exists exactly one valid solution. With SAT, there might be 0, 1, 2, or more satisfying assignments, and we are asked to determine whether there exists 0 satisfying assignments or 1+ satisfying assignments. Valiant and Vazirani considered the following problem: given a SAT formula with the promise that it has either 0 or 1 satisfying assignments (not more than 1), determine whether it has 0 satisfying assignments or 1 satisfying assignments. They showed a randomized polynomial-time reduction showing that this problem is at least as hard as SAT (specifically, there is no polynomial-time algorithm for this problem either, unless NP=RP).

More generally, we could ask about the following problem: given a SAT formula with a promise that it has exactly 1 satisfying assignment, find the satisfying assignment. This problem is the analogue of Sudoku (where we're given a Sudoku puzzle with the promise that it has exactly 1 valid solution, and we're asked to find that solution). It follows from Valiant and Vazirani's result that this problem is at least as hard as SAT under randomized polynomial-time reductions; if you could solve this problem in polynomial time, you could solve SAT in (randomized) polynomial time. So, the promise that a SAT formula has exactly 1 valid solution doesn't make it any easier to find the solution.

Further reading: UniqueSAT and UnambigousSAT at https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Extensions_of_SAT, https://en.wikipedia.org/wiki/Valiant%E2%80%93Vazirani_theorem, https://cstheory.stackexchange.com/q/1639/5038, Unique SAT complexity clarification, Proof of SAT is randomly reducible to UNIQUE-SAT, https://cstheory.stackexchange.com/q/22093/5038.

Answer 2

Its assumed you implemented a generalized Sudoku solver and not a 9x9 one. First you will need a parsimonious 1-to-1 reduction from 3SAT (SAT to 3SAT is easy) to Sudoku. This is because your sudoku solver may use assumptions of a unique solution. This leads into the another solution problem (ASP) but parsimoniety covers this. There are known reductions from 3SAT to the triangulation problem or finding a tripartite graph division problem. Latin squares also directly reduce to the tripartite graph problem. From there you can map from the Latin square problem to Sudoku with a careful mapping. I suggest seeking out the already published results in this area.

I've never seen a tool which takes a unique SAT equation and generates a Sudoku instance whose unique solution represents the original unique SAT. Note we are talking about the generalized sudoku so the grid could presumably be very large, likely absurdly and impractically large. Going from Sudoku to SAT is easier and many resources are available for this direction yet by the sheer large size of the constant in the polynomial reduction in both directions, likely much larger from SAT to Sudoku unless a very efficient, even more so than what is known is used to convert the Latin square to Sudoku process is used. Just consider reasonable 9x9 SAT instances of classic sudoku have hundreds of variables and thousands of clauses. So the other direction is probably incomprehensibly big and visualizing it would be mere novelty.