# Unboggler

## Table of Contents

# Boggle

Boggle is a classic board game in which players search for words constructed by connecting adjacent tiles in a grid of letters. Letters can be used at most once, and are allowed to connect horizontally, vertically, or diagonally. Listing all words in a Boggle board is a common interview question, easily achieved by querying a trie data structure assembled from a list of dictionary words. Use the widget below to see it in action!

# Unboggle

Boggle was easy enough, so let's try **Unboggle**, or reverse boggle, where the goal is to reconstruct a Boggle board from a given list of words. There is no obvious way to divide-and-conquer the problem and no obvious greedy algorithm guaranteed to use all the words in the list. Instead, I encode Unboggle as a **boolean satisfiability** problem using `logic-solver.js`

, a convenient wrapper around the general-purpose `minisat`

solver, which has been compiled to JavaScript using `emscripten`

.

## The Unboggler

Try it out below! For a 4x4 grid and about 10 words, you can expect the Unboggle search to take about 30 seconds. Since the solver isn't designed to detect unsatisfiability, the Unboggler may hang for much longer if no satisfying board exists!

`<div class="spinner"></div>`

## SAT Solvers

SAT solvers search for a satisfying assignment of `true`

and `false`

values to a boolean formula containing literals, conjunction, disjunction, and negation. For example, the formula

$(x_1 \vee x_2 \vee \neg x_3) \wedge (\neg x_1 \vee x_2 \vee \neg x_4) \wedge (\neg x_3 \vee \neg x_4 \vee x_5)$

is satisfied by the assignment $x_1 = x_2 = \mathtt{true}$ and $x_3 = x_4 = \mathtt{false}$. Integer constraints like $y=11$ can be encoded as binary constraints on the individual binary digits $y = y_4 y_3 y_2 y_1$, like so:

$y_4 \wedge \neg y_3 \wedge y_2 \wedge y_1$

Thankfully, `logic-solver.js`

takes care of binary encodings for us and supports basic arithmetic constraints like $(=, <, >, \leq, \geq)$, together with addition and subtraction.

## SAT Encoding

To encode Unboggle as a satisfiability problem, suppose we wish to fit $m$ words on an $n \times n$ board. Assume an average word length $\ell$.

- For each letter of every word on the list, we use two integer variables to represent the letter's grid coordinates, requiring $L = 2 m \ell \lceil \log_2 n \rceil$ binary literals.
- When the board size is not a power of two, each coordinate needs an upper bound.
- Adjacent letters within the same word must be adjacent on the board.
- A word cannot overlap itself; its coordinate pairs must all be distinct.
- Two different words can only intersect at a common letter; that is, two different letters from distinct words cannot occupy the same space.

The number of constraints increases roughly quadratically with the number of words, so Unboggling more than ten words may take quite a while! The code below uses `logic-solver.js`

to represent these constraints:

```
function encode(numRows, numCols, words){
let solver = new Logic.Solver();
// dimensions
let numWords = words.length;
let numRowBits = Math.ceil(Math.log2(numRows));
let numColBits = Math.ceil(Math.log2(numCols));
// bit constants
let const_1 = Logic.constantBits(1);
let const_numRows = Logic.constantBits(numRows);
let const_numCols = Logic.constantBits(numCols);
// word constraints
let wordPaths = [];
for(let w = 0; w < numWords; w++){
// translate word
let word = words[w];
let wordPath = [];
for(let i = 0; i < word.length; i++){
// location of ith letter stored in variables:
// p_(w)_(i)_r and p_(w)_(i)_c
let pr = Logic.variableBits(`p_${w}_${i}_r`, numRowBits);
let pc = Logic.variableBits(`p_${w}_${i}_c`, numColBits);
.push([pr,pc]);
wordPath
// enforce board boundaries on paths (coordinates zero-indexed)
.require(Logic.lessThan(pr, const_numRows));
solver.require(Logic.lessThan(pc, const_numCols));
solver
// adjacent letters in word must be adjacent on board
if(i > 0){
// x difference
.require(Logic.lessThanOrEqual(wordPath[i-1][0], Logic.sum(wordPath[i][0], const_1)));
solver.require(Logic.lessThanOrEqual(wordPath[i][0], Logic.sum(wordPath[i-1][0], const_1)));
solver// y difference
.require(Logic.lessThanOrEqual(wordPath[i-1][1], Logic.sum(wordPath[i][1], const_1)));
solver.require(Logic.lessThanOrEqual(wordPath[i][1], Logic.sum(wordPath[i-1][1], const_1)));
solver
}
}
// path cannot overlap itself
for(let i = 0; i < word.length; i++){
for(let j = i+1; j < word.length; j++){
.require(Logic.atMostOne(
solver.equalBits(wordPath[i][0],wordPath[j][0]),
Logic.equalBits(wordPath[i][1],wordPath[j][1])
Logic;
))
}
}
.push(wordPath);
wordPaths
}
// now, ensure word paths are all compatible
for(let w1 = 0; w1 < numWords; w1++){
for(let w2 = w1+1; w2 < numWords; w2++){
let word1 = words[w1];
let word2 = words[w2];
for(let i = 0; i < word1.length; i++){
for(let j = 0; j < word2.length; j++){
// no constraint if words have letter in common
if(word1[i] == word2[j]){ continue; }
// prevent different letters from occupying same space
.require(Logic.atMostOne(
solver.equalBits( wordPaths[w1][i][0], wordPaths[w2][j][0] ),
Logic.equalBits( wordPaths[w1][i][1], wordPaths[w2][j][1] )
Logic;
))
}
}
}
}
// find solution
return {
solution: solver.solve(),
wordPaths: wordPaths
;
} }
```