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);
			wordPath.push([pr,pc]);

			// enforce board boundaries on paths (coordinates zero-indexed)
			solver.require(Logic.lessThan(pr, const_numRows));
			solver.require(Logic.lessThan(pc, const_numCols));

			// adjacent letters in word must be adjacent on board
			if(i > 0){
				// x difference
				solver.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)));
				// y difference
				solver.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)));
			}
		}

		// path cannot overlap itself
		for(let i = 0; i < word.length; i++){
			for(let j = i+1; j < word.length; j++){
				solver.require(Logic.atMostOne(
					Logic.equalBits(wordPath[i][0],wordPath[j][0]),
					Logic.equalBits(wordPath[i][1],wordPath[j][1])
				));
			}
		}

		wordPaths.push(wordPath);
	}

	// 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
					solver.require(Logic.atMostOne(
						Logic.equalBits( wordPaths[w1][i][0], wordPaths[w2][j][0] ),
						Logic.equalBits( wordPaths[w1][i][1], wordPaths[w2][j][1] )
					));
				}
			}
		}
	}

	// find solution
	return {
		solution: solver.solve(),
		wordPaths: wordPaths
	};
}