1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – D.W. Jul 26 '18 at 7:30
  • $\begingroup$ 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? $\endgroup$ – Schmetterling Jul 26 '18 at 7:39
  • 1
    $\begingroup$ 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. $\endgroup$ – ttnick Jul 26 '18 at 9:27
  • $\begingroup$ 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. $\endgroup$ – D.W. Jul 26 '18 at 18:23
  • $\begingroup$ I've edited the post. $\endgroup$ – Schmetterling Jul 26 '18 at 18:44
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.