This project explores SAT solving as a method for generating crossword puzzles. Relationships between words, letters, and grid cell locations are defined to create crossword puzzles. A "quality" metric is defined based on the final state of the crossword puzzle and a heuristic is used to generate crossword puzzles of better "quality". A crossword grid size and a list of words can be specified and a crossword puzzle containing all the words present in the list can be generated. It is also possible to generate different crossword puzzle word arrangements for the same set of words in some cases.
Introduction
Introduction
This project formulates crossword puzzle generation into an instance of the Boolean Satisfiability problem (SAT) in computer science, which is the problem of determining whether there exists an assignment of truth values to variables that satisfies a given boolean formula. Tools that solve the Boolean Satisfiability problem are called SAT solvers. Readers familiar with propositional logic will find it easier to understand the various constraints and implications present in this project. Note:
◼
All logical operators and symbols used in this essay have their usual meanings.
◼
The function [] encompasses almost all the code of in project. It accepts a grid size and a list of words to build the crossword out of.
generateCrossword
The following line is the signature of the crossword generation function for reference. It is not to be evaluated.
generateCrossword[gridSize0_Integer, words0_List] := Module[{gridSize = gridSize0, words = words0}...
◼
Code in this essay is indexed starting from , apart from boolean representations.
1
0/1
◼
Rows are denoted by and are numbered from top to bottom. Columns are denoted by are are numbered from left to right.
x
y
◼
Statements like “placing a word at cell ” refer to the first letter of that word being placed at .
(x,y)
(x,y)
◼
Constraints and implications for horizontal word placement are identical to constraints and implications for vertical word placement. Hence, explanations are provided only for horizontal constraints and implications. Code is provided for both horizontal and vertical constraints and implications.
◼
It is assumed that words in the crossword will be at least 3 alphabets long.
◼
The example outputs in this essay are not generated by evaluating the code blocks in the "Constraints, SAT Solving" and "The Crossword" sections. See "How Can I Generate My Own Crosswords?"
The following variables are used throughout the essay:
numWords = Length[words];blankNum = 27;alphabetMap = AssociationThread[Alphabet[][[1 ;; blankNum - 1]], Range[blankNum - 1]];Append[alphabetMap, "blank" -> blankNum];satVariables = {};satConstraints = {};
◼
numWords
◼
blankNum
27
◼
alphabetMap
1
26
blankNum
◼
satVariables
◼
satConstraints
satVariables
satConstraints
True
Constraints, SAT Solving
Constraints, SAT Solving
Main Setup
Main Setup
◼
Let represent word being placed at in the crossword grid with representing horizontal placement and representing vertical placement.
wp
i,x,y,z
i
(x,y)
z0
z1
◼
Let represent alphabet being placed at in the crossword grid. is an integer value in the range . Values through represent characters from "a" through "z" while represents an empty character.
alpha
i,x,y
i
(x,y)
i
[1,27]
1
26
27
◼
Each word can only be placed at one position in the grid. This means that among all for a particular word, we require exactly one of those variables to be true.
wp
i
◼
Each cell in the grid can contain at most one letter. If it doesn't contain a letter, it will be empty. This means that for a particular location , among all , at most one variable can be true.
(x,y)
alpha
i,x,y
◼
Even though we define a value to denote a blank cell, we use the at most one constraint instead of the exactly one constraint because it is logically equivalent and its enforcement requires one clause less.
th
27
oneTrue[]
oneTrue
The Function
The Function
Function [] takes in a list of variables and generates constraints on those variables to enforce the exactly one or the at most one condition:
oneTrue
oneTrue[x0_List, atMost0_Integer] := Module[{variables = x0, atMost = atMost0}, res = {}; listSize = Length[variables]; prefFunc = "pref" <> ToString[Head@variables[[1]]]; prefVariables = prefFunc[#[[1]]] & /@ variables; prefConstraints = Table[ {Implies[variables[[i]], prefVariables[[i + 1]]], Implies[prefVariables[[i]], prefVariables[[i + 1]]], Implies[prefVariables[[i]], Not@variables[[i]]]}, {i, listSize - 1} ] // Flatten; AppendTo[prefConstraints, Implies[prefVariables[[listSize]], Not@variables[[listSize]]]]; If[atMost == 0, finalConstraints = Or @@ variables && And @@ prefConstraints, finalConstraints = And @@ prefConstraints]; finalVarList = Join[variables, prefVariables] // Flatten; Return[{finalVarList, finalConstraints}]; ];
For a list of size , [] creates additional variables. Let's denote the variable as for simplicity. is defined to be if there exists a () that is (the prefix of ). We have the following logical implications from this setup:
C
N
oneTrue
N
th
i
pref
i
pref
i
True
C
j
1≤j≤i-1
True
[1,i-1]
C
1
.If is then must be .
C
i
True
pref
i+1
True
2
.If is then must be .
pref
i
True
pref
i+1
True
3
.If is then must be .
pref
i
True
C
i
False
These constraints enforce the at most one condition. To enforce the exactly one condition, we simply add another clause which, if used alone, signifies that at least one value must be . A combination of at most one and at least one results in exactly one.
(⋁⋁⋁…)
C
1
C
2
C
3
C
N
True
Note: The additional variables created are present only to enforce our constraints. We do not care about their final truth values.
Its Application
Its Application
oneTrue
Generating exactly one constraints on word placements and at most one constraints on letter placements:
wordPlacementConstraints = Table[ oneTrue[Table[wp[{x, i, j, k}], {i, 1, gridSize}, {j, 1, gridSize}, {k, 0,1}] // Flatten, 0], {x, 1, numWords}];alphabetPlacementContraints = Flatten[Table[oneTrue[Table[alpha[{x, i, j}], {x, 1, blankNum}] // Flatten, 1], {i, 1, gridSize}, {j, 1, gridSize}], 1];AppendTo[satVariables, #[[1]]] & /@ wordPlacementConstraints;AppendTo[satConstraints, #[[2]]] & /@ wordPlacementConstraints;AppendTo[satVariables, #[[1]]] & /@ alphabetPlacementContraints;AppendTo[satConstraints, #[[2]]] & /@ alphabetPlacementContraints;satVariables = satVariables // Flatten;
Word - Letter Implications
Word - Letter Implications
What letter implications are created when a word is placed at a particular cell? Consider the word "wolfram" being placed horizontally at the position . If "wolfram" is the first word in our word list, in the definition of . So, we have representing "wolfram" being placed horizontally at . This has the following logical implication:
(1,1)
i1
wp
i,x,y,z
wp
1,1,1,0
(1,1)
wp
1,1,1,0
alpha
23,1,1
alpha
15,1,2
alpha
12,1,3
alpha
6,1,4
alpha
18,1,5
alpha
1,1,6
alpha
13,1,7
There's a slight issue with this approach. What if we have the words "wolfram" and "wolf"? Placing a single word "wolfram" could satisfy the boolean formula. Technically, the solver can place "wolf" inside "wolfram".
Fortunately, there’s an easy fix to this problem. We can force the cell right after the last letter of a word to be empty. The following constraint is added (a similar constraint is added for "wolf"):
wp
1,1,1,0
alpha
23,1,1
alpha
15,1,2
alpha
12,1,3
alpha
6,1,4
alpha
18,1,5
alpha
1,1,6
alpha
13,1,7
wp
1,1,1,0
alpha
27,1,8
Now, if the solver tries to place "wolf" inside "wolfram", it won't be able to do so because it will require the "r" character cell (location in our example) to be empty.
(1,5)
As mentioned earlier, vertical word placement is analogous to horizontal word placement, so it isn't discussed here.
Code
Invalid Placement Constraints
Invalid Placement Constraints
Out of Bounds Placements
Out of Bounds Placements
Even in an empty grid, it's just impossible to place some words in certain locations. If placing a word at a location causes its last letter to be placed outside the crossword grid, it's impossible to start the word at . For such words the following constraint is added which makes it impossible for the solver to place it there:
i
(x,y)
(x,y)
(
¬⋁¬
wp
i,x,y,z
wp
i,x,y,z
)
Generating constraints as described above:
horizontalConstraints = {Not@# || Not@#} & /@ Select[ Flatten[Table[wp[{x, i, j, 0}], {x, 1, numWords}, {i, 1, gridSize}, {j, 1, gridSize}], 2], StringLength[words[[#[[1]][[1]]]]] + #[[1]][[3]] - 1 > gridSize &] // Flatten;verticalConstraints = {Not@# || Not@#} & /@ Select[ Flatten[Table[wp[{x, i, j, 1}], {x, 1, numWords}, {i, 1, gridSize}, {j, 1, gridSize}], 2], StringLength[words[[#[[1]][[1]]]]] + #[[1]][[2]] - 1 > gridSize &] // Flatten;AppendTo[satConstraints, And @@ horizontalConstraints];AppendTo[satConstraints, And @@ verticalConstraints];
Invalid Starting Points
Invalid Starting Points
We want every word, whether it is horizontally or vertically formed, to correspond to an actual word in the English dictionary. Again, taking the example of horizontal words, if there is a letter to the right of a blank cell or if there is a letter in a cell in the first column, and another letter to the right of that cell, we want the horizontal word formed starting from the "middle" cell to be an actual word.
Assignment of Truth Values
Assignment of Truth Values
The following code finds an assignment of truth values for all the implications and constraints created:
The Crossword
The Crossword
Displaying The Crossword
Displaying The Crossword
Now that we have an assignment of truth values, we display the crossword generated.
Connected Components
Connected Components
The SAT solver has to only find a valid assignment of truth values. There can be multiple such assignments. It's possible for the solver to return an assignment in which all words in the crossword aren't "connected". In other words, the big crossword can be split up into smaller disjoint crosswords.
It's also possible that there is in fact no arrange of words that leads to a single connected crossword. Here, it may be worthwhile to explore constraints which choose a subset of words to place, which can possibly form a single connected component. However, our SAT solver cannot maximise or minimize any quantity. It can only find a valid assignment of truth values. When we allow it to choose what words to use, placing no words becomes a valid assignment. So, we can't allow that here.
The following code creates a graph of connected sub-crosswords:
The following code was present in the "Assignment of Truth Values" subsection:
Essentially, we randomly shuffle the list of constraints that we provide to our SAT solver. Many times, this leads to the solver finding a different assignment of truth values, resulting in a different arrangement of words (different crosswords are formed).
How Can I Generate My Own Crosswords?
How Can I Generate My Own Crosswords?
Display
Display
Enter a list of words or randomly generate one:
View the sum of sizes of words compared to the number of cells in the grid:
Generate a single crossword puzzle and calculate how much time (in seconds) the solver took to generate it:
Generate multiple crossword puzzles using the list "words":
The Future
The Future
A major limitation of this project is that it very rarely generates fully connected crosswords.
The next step would be to use a weighted MAX-SAT solver. A new quality metric can then be defined to choose a configuration of words that gives us a fully connected crossword puzzle, with the possibility of being able to maximise the number of words chosen in the subset.
Once fully connected crosswords can be generated, I would love to create a website which picks random words to generate a crossword every day, generates a crossword puzzle, generates hints, and then allows people to enter their solutions and gives them feedback.
References
References
◼
Wikipedia, Boolean satisfiability problem
◼
Wikipedia, Maximum satisfiability problem
◼
◼