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.

In this post, I'm going to build an example of artificial intelligence in the form of a Constraint Satisfaction Problem (or CSP), showing how much mathematics, logic skills, and computer science knowledge can help in the process. For this purpose, I took a puzzle game called Hitori on the popular logic puzzle website Nikoli. I didn't choose Hitori because it was convenient, I literally chose a random game precisely because it didn't matter what the game was for what I wanted to show. Let's begin by learning what a CSP actually is. CSPs are mathematical problems defined as a set of objects whose state must satisfy a number of constraints or limitations.