# Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions

arXiv: https://arxiv.org/abs/2508.14294 · HTML: https://mlsanity.com/paper/2508.14294/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 8 of its 30 references that are in the map.
- First posted on arXiv 19 Aug 2025.

## Builds on (most cited first, 8 of 8)

- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Prompting](https://mlsanity.com/paper/2305.04388/) (2023)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Puzzle Solving using Reasoning of Large Language Models: A Survey](https://mlsanity.com/paper/2402.11291/) (2024)
- [Two Failures of Self-Consistency in the Multi-Step Reasoning of LLMs](https://mlsanity.com/paper/2305.14279/) (2023)
- [Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer](https://mlsanity.com/paper/1605.00723/) (2016)
- [Counterexample Explanation by Learning Small Strategies in Markov Decision Processes](https://mlsanity.com/paper/1502.02834/) (2015)

## Abstract (arXiv)

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.