SAT BASED ALGORITHMICAPPROACH FOR SUDOKU PUZZLE

In theoretical computer science, Sudoku puzzle has always grappled its importance since it is an NP-complete problem. Most of the existing algorithms are exponential for large instances of Sudoku puzzle. In this paper, we present an efficient approach for Sudoku puzzle in which constraints of Sudoku puzzle are encoded into SAT clauses and subsequently encoded into 3-SAT clauses. 3-SAT formulation of Sudoku puzzle (n × n) is very advantageous to obtain the solution of Sudoku puzzle using SAT solver. In this way, we design two algorithms SP2SAT and SP23SAT that generate SAT clauses and 3-SAT clauses respectively in polynomial time. Algorithm I: SP2SAT generates total [ * (3n2 – 3n + 2) + m] SAT clauses corresponding to Sudoku puzzle of size (n × n). On the other hand, Algorithm II: SP23SAT creates total [ * (3n2 – n – 4) + m] 3-SAT clauses corresponding to SAT clauses. Our approach provides an efficient way to obtain the solution of Sudoku puzzle as it produces fewer number of 3-SAT clauses than existing approach.