# Is any sudoku solver an SAT solver?

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.

• I don't understand your question. "Uses a SAT solver" / "Reduces Sudoku to SAT" is not the same as "Counts as a SAT solver" / "Reduces SAT to Sudoku". Which are you asking about? – D.W. Jul 26 '18 at 7:30
• It is converted to SAT, then solved using true/false values. So it is the first one - does this then mean the answer to the question is yes? – Schmetterling Jul 26 '18 at 7:39
• Your question is still not well stated. You have a "sudoku solver" that takes a sudoku instance and transforms it into a propositional logic formula, which is solved by a SAT solver, right? In this case, your sudoku solver should not be called a SAT solver, as you cannot input any pl formula, even if it allows arbitrary larger sudoku grids. – ttnick Jul 26 '18 at 9:27
• The answer to what question? As I said before, I don't understand what your question is, so I don't know how I can tell whether the answer is yes or no. I think I do understand how your Sudoku solver works, but I don't understand what your question is. – D.W. Jul 26 '18 at 18:23
• I've edited the post. – Schmetterling Jul 26 '18 at 18:44