Modeling Path Puzzles as SAT Problems and How to Solve Them

This paper discusses a SAT-based approach for solving the Path Puzzles—one-player paper-and-pencil puzzles recently proven NP-complete in 2020. The properties and rules of Path Puzzles are encoded into propositional formulas in Conjunctive Normal Forms (CNF). We describe the step-by-step derivation for such formulas and analyze the number of clauses and variables used to express them. Experimental results show that our declarative SAT-based solver in PySAT outperforms the conventional imperative backtracking technique for solving larger puzzles.