Efficient SAT-Based Approach for Solving Juosan Puzzles

Juosan is a single-player paper-and-pencil puzzle introduced in 2014 and shown to be NP-complete in 2018. This NP-completeness implies that the Juosan puzzle is polynomial-time reducible to the Boolean satisfiability (SAT) problem, thereby allowing us to transform the puzzle into SAT problems. This paper introduces an efficient SAT-based approach for solving the Juosan puzzles. We first discuss the rules and derived properties of Juosan puzzles and translate them into Boolean formulas in Conjunctive Normal Forms (CNF). We show that the number of clauses and propositional variables used in the encoding is polynomially proportional to the puzzle’s size. Using this encoding, we successfully implement a declarative program with no search algorithm using MiniSAT in C++ to solve any Juosan puzzle with up to \(1350\) cells in less than one second on a standard personal computer. Experimental results show that our SAT-based approach outperforms the optimized backtracking algorithm for larger puzzles.