Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions
This work addresses the challenge of generating explanations for sequential decisions in puzzle-solving, which is an incremental improvement in neurosymbolic methods for a specific domain.
The authors tackled the problem of explaining complex decision sequences in Hitori puzzles by developing a neurosymbolic approach that combines SAT solvers and Large Language Models (LLMs), resulting in a tool that assists humans in solving these puzzles with demonstrated effectiveness.
We propose a neurosymbolic approach to the explanation of complex sequences of decisions that combines the strengths of decision procedures and Large Language Models (LLMs). We demonstrate this approach by producing explanations for the solutions of Hitori puzzles. The rules of Hitori include local constraints that are effectively explained by short resolution proofs. However, they also include a connectivity constraint that is more suitable for visual explanations. Hence, Hitori provides an excellent testing ground for a flexible combination of SAT solvers and LLMs. We have implemented a tool that assists humans in solving Hitori puzzles, and we present experimental evidence of its effectiveness.