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.
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.