Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions

TL;DR

This paper introduces a neurosymbolic method combining decision procedures and Large Language Models to explain complex decision sequences, demonstrated through solving and explaining Hitori puzzles.

Contribution

It presents a novel neurosymbolic approach that integrates SAT solvers and LLMs for explaining puzzle solutions, with a practical tool and experimental validation.

Findings

Effective explanations for Hitori puzzle solutions

Successful integration of symbolic and neural methods

Tool assists humans in puzzle solving

Abstract

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.