Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions
Not on the map. Why?
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.
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
8 of 30 references.
References · 8
- 2020Retrieval-Augmented Generation for Knowledge-Intensive NLP Taskscited by 9,297
- 2023Language Models Don't Always Say What They Think: Unfaithful Explanations in Chain-of-Thought Promptingcited by 1,122
- 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
- 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
- 2024Puzzle Solving using Reasoning of Large Language Models: A Surveycited by 45
- 2023Two Failures of Self-Consistency in the Multi-Step Reasoning of LLMscited by 36
- 2016Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquercited by 23
- 2015Counterexample Explanation by Learning Small Strategies in Markov Decision Processescited by 10
Built on by
Not cited yet.