Pen and paper puzzles like Sudoku, Futoshiki and Star Battle are hugely popular. Solving such puzzles can be a trivial task for modern AI systems. However, most AI systems solve problems using a form of backtracking, while people try to avoid backtracking as much as possible. This means that existing AI systems do not output explanations about their reasoning that are meaningful to people. We present Demystify, a tool which allows puzzles to be expressed in a high-level constraint programming language and uses MUSes to allow us to produce descriptions of steps in the puzzle solving. We give several improvements to the existing techniques for solving puzzles with MUSes, which allow us to solve a range of signi cantly more complex puzzles and give higher quality explanations. We demonstrate the e ectiveness and generality of Demystify by comparing its results to documented strategies for solving a range of pen and paper puzzles by hand, showing that our technique can nd many of the same explanations.
Puzzles like Sudoku, Futoshiki or Star Battle are designed to be solved on paper
and continue to be incredibly popular. New variants of these puzzles are created
almost weekly, and there are many websites and books dedicated to showing o
new problems. The increasing popularity of the YouTube channel `Cracking the
Cryptic' shows that people enjoy seeing explanations of pen and paper puzzles.
There exist specialised guides for solving many of these puzzles [
Most paper and pen puzzles can be trivially solved when using a constraint
solver [
Copyright © 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
(7,1) is 0, (7,2) is 0 and (7,3) is 0 because:
{ Column 7 must contain at most 1 star
{ Box 6 must contain at least 1 star
There are two main reasons to look at how humans solve puzzles { to advise
players on how to progress and to produce more accurate di culty measures
of puzzles. A common approach to explain how puzzles are solved is to create
custom solvers which use the same techniques as human players. For popular
puzzles this is easy, as the techniques which human players use are well
documented. SudokuWiki [
Our contribution is threefold. First, a novel MUS- nding algorithm optimised to nd individual small MUSes. Second, improved techniques for using MUSes to generate explanations designed for pen and paper puzzles. Finally, we provide a comparison of explanations generated via MUSes to real-world tutorials and puzzle solving, showing how our techniques closely match the explanations used by real players on a variety of puzzles and guides. 2
The puzzles we discuss in this paper are typically solved by keeping a list of
the values which are being considered for each cell of a grid, called the
candidates. Once every cell has only one candidate remaining, the puzzle is solved. We
consider puzzles with a single solution, which and are intended to be solved by
humans without guessing. We call these pen and paper puzzles. We consider
Bigiven grid: int
letting griddim be int(1..grid)
given starcount: int
$#VAR stars
find stars: matrix indexed by [griddim, griddim] of bool
$#CON rowup "at least {p[’starcount’]} star(s) in row ({a[0]})"
$#CON rowdown "at most {p[’starcount’]} star(s) in row ({a[0]})"
find rowup: matrix indexed by [griddim] of bool
find rowdown: matrix indexed by [griddim] of bool
forAll i: griddim. rowup[i] -> (sum(stars[i,..]) >= starcount),
forAll i: griddim. rowdown[i] -> (sum(stars[i,..]) <= starcount)
nairo, Futoshiki, Kakuro, Starbattle, Tents and Trees, Thermometer, Skyscrapers
and Sudoku (rules and examples of all these puzzles can be seen on [
An unsatis able set of an unsatis able constraint problem is any unsatis
able subset of the set of constraints of the problem. Traditionally, unsatis able
sets are de ned on the clauses of a conjunctive normal formula. In this paper,
we extend this de nition to general constraint problems. The hypothesis of our
work is that unsatis able sets closely align with how human players solve
puzzles. Unsatis able sets have many uses, such as on interactive applications or
model checking; see [
The rules for many well-known pen and paper puzzles can be expressed using constraints. For example a Sudoku is built from AllDi erent constraints, Kakuro rules have sums and Futoshiki has inequalities.
To be able to give explanations for each reasoning step, all constraints used
to model the rules of puzzles are half-rei ed. For each constraint c, SavileRow
outputs x ! c, where c is the constraint and x is a Boolean variable that
controls if the constraint is active. Each constraint is also associated with a
string, describing in natural language terms what the constraint is expressing.
We use SavileRow [
In problems such as Sudoku it is common for players to remove possible values for a cell one at a time until only one remains, commonly referred to as candidate elimination. In other puzzles such as Skyscrapers, Kakuro or Futoshiki it is common to only ll in a cell once the player knows its value. To support these two methods of playing, Demystify can either generate MUSes for both positive and negative assignments to Problem variables (allowing candidate elimination) or only for positive assignments to Problem variables. 4
Demystify1 generates explanations very similarly to [
Finally, choose the MUS which can be used to discard the most literals. 4. Assign any literals which can be deduced from the best MUS and iterate from step 2 until all variables are assigned.
There are several improvements we make when presenting MUSes to the user, which reduce information overload and allow us to solve the puzzles in fewer steps. Firstly, MUSes of size 1 are grouped together, as there can be many such MUSes and they are very simple to understand. Secondly, for each MUS we nd all literals which can be deduced using the MUS. This is generally very fast, as the MUS is already small and we only need to check literals contained in at least one of the constraints in the MUS. A single MUS can often be used to deduce many literals. This lets us deduce several literals in a single step. MUSes are displayed to the user by listing the English descriptions of the constraints. 5
As previously discussed, there are many existing MUS nding algorithms. We found existing state-of-the-art techniques for nding smallest MUSes either did 1 https://github.com/stacs-cp/demystify Algorithm 1 Basic MUS nding algorithm Algorithm 2 ManyChop Algorithm 1: procedure ManyChop(P; X; M axSize) 2: step = min(fn 2 Nj(1 21n )MaxSize 110 g); frac = 1 2s1tep 3: for i 2 [1::20] do 4: check = Shu e(X)[1::jXj frac] 5: if Solve(check) == False then return BasicMUS(check, M axSize) 6:
return Fail not nish in reasonable time or could only nd MUSes when each constraint is a single SAT clause. Furthermore, we do not wish to nd the smallest MUS for a single problem but to nd the globally smallest MUS for a set of problems { one for each remaining unassigned problem literal, where often most of these problems will have no small MUSes.
Demystify uses Glucose [
BasicMUS, a variant of the deletion-based algorithm of [
One major limitation of BasicMUS is the lack of variety in the MUSes it returns, as FindUnsatCore often returns the same unsat core. We mitigate this with the ManyChop algorithm (Algorithm 2), which starts by removing a random subset of X. ManyChop chooses a xed-size proportion of X to remove and keeps trying to remove that many elements of X and checking if the problem is still unsolvable, before using BasicMUS to nd a MUS. The intuition behind ManyChop is that, given a set X, if we remove some proportion p of the elements of X, the chance that any xed collection of n elements remains behind is approximately (1 p)n. In our experiments, we choose p such that there is at least a probability of 110 of nding a MUS of size M axSize, then search 20 times.
We nally nd the globally smallest MUS by searching over the problem variables (which represent the values these variables can take in the solution) in parallel using iterative deepening looking for larger and larger sizes of MUS. 6
We compare Demystify against a selection of published tutorials to show how
it lines up with human players. We wrote each of our puzzles in Essence' [
In problems which do not allow candidate elimination we imposed AllDifferent constraints as a single constraint. For problems which allow candidate elimination we decomposed the AllDi erent constraints into smaller pieces, requiring that each pair of variables take di erent values and each value occurs exactly once. This is because without candidates the deductions possible from a single AllDi erent are quite simple, while with candidate elimination the tutorial will decompose AllDi erent constraints into smaller simpler pieces.
Several puzzles (including Tents and Trees, Thermometers and Starbattle) require that there is a xed number of objects in rows, columns or regions. We split these equality constraints into and constraints, as this made the resulting MUSes easier to understand. In the Tents and Trees puzzle, there is a bijection between tents and trees. To express this bijection we assign each tree a unique number between 1 and n, then ll in cells with a number between 0 and n, where 0 represents empty and i > 0 represents that this is the tent for tree i. We require each non-zero number in the grid occurs exactly once. 6.1
Tutorials To show that MUS generation lines up with how players solve puzzles, we compared our techniques to the tutorials for ten di erent puzzles, seeing in each case if the MUS highlighted the same constraints as those given by the tutorial. For each step of each tutorial, we use ManyChop to get the smallest MUS for one of the deductions produced by that tutorial step. We do not use the globally smallest MUS, as in many cases there were smaller MUSes in di erent parts of the puzzle, unrelated to the logical rule the tutorial step was demonstrating. In some cases, a MUS may only deduce one, or a subset, of the deductions described in a single tutorial step, as many tutorial steps describe a general idea and then apply it in many places. We de ne a successful match by the MUS when it correctly captures the reasoning for the single deduction we chose. Where tutorials show several connected steps we consider each step individually, rather than running Demystify to solve the whole puzzle. There were two common issues we found with tutorials. In some cases the tutorial example had multiple answers, in this case Demystify can only deduce variables which take the same value in all solutions. Some tutorials had no solutions { we remove those instances.
We have taken instances from di erent online guides. For Sudoku, X-Sudoku
and Jigsaw Sudoku we used [
Our results on the classic Sudoku puzzle are not as impressive as for the other
puzzles. There are several reasons for this. One is that we often nd constraints
which represent a di erent Sudoku technique to the one in the tutorial. For
example, instead of the \Naked Triples" or \Hidden Triple" techniques we nd
\Pointing Pairs": the latter is sometimes considered as an easier technique, e.g.
by Sudoku Dragon's strategy guide [
Overall, we believe Table 1 gives strong evidence for the validity of using MUSes for solving unseen puzzles. With no signi cant tuning (other than deciding how to represent AllDi erent constraints) we have reproduced a signi cant number of the techniques from a varied set of puzzles.
We have presented a new algorithm to e ciently nd small MUSes. We
demonstrate its usefulness and generality by producing descriptions of steps for many
pen and paper puzzles. We also demonstrate that MUSes align very closely with
pre-existing research on how human players decide how to solve these puzzles.
This work, along with earlier work on Logic Grid Puzzles [
We believe the FORQES [