Pergunta

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.

Nenhuma solução correta

Licenciado em: CC-BY-SA com atribuição
Não afiliado a cs.stackexchange
scroll top