A SAT-Based Approach for Solving Suguru Puzzles: Theory and Experiment

Source abstract

We discuss a SAT-based approach for solving Suguru puzzles---one-player puzzles similar to Sudoku that were confirmed NP-complete in 2022. We first discuss the formal rules of the puzzles and provide a rigorous technique to translate such rules into propositional formulas in conjunctive normal form (CNF). The resulting formulas form what is called a SAT encoding, and we prove that the number of clauses and variables in our encoding is polynomially proportional to the puzzle's dimension. This encoding allows one to reduce Suguru puzzles to SAT problems, and we use this encoding to construct a declarative SAT-based program without any search algorithm in C++ for solving general Suguru puzzles. We perform experiments involving 230 test cases for Suguru instances of size n \times n where 6 \leq n \leq 15. Finally, we derive some empirical results from these experiments and argue that, in terms of running time, our SAT-based approach outperforms the previously proposed backtracking technique in solving larger puzzles.