I noticed crossword puzzle books selling well on Amazon KDP and wanted to see if I could automate the whole thing from one command, grids and clues through page layout, cover, and a print-ready PDF. The main output is a CLI that writes a LaTeX book, and I've generated a few 100-puzzle books with it at 10x10 and 16x16. The browser demo came later and runs the same Rust crate compiled to WebAssembly.
Why a SAT solver
The open-source generators I looked at use backtracking: place a word, place another, undo when nothing fits. On small grids that works. On bigger ones the grids I got out had dead zones where nothing interlocked and filler words jammed into whatever gaps were left. Filling a grid from a dictionary is NP-complete (it is problem GP14 in Garey and Johnson), so I didn't expect a clever search of my own to fix that. Writing down every rule a finished grid has to obey and handing the lot to Varisat seemed like the better bet.
The encoding
The encoder is placement-based. There is one Boolean variable for each word, position, and orientation where the word fits, and one for each cell and letter. A placement variable being true forces its letters into the grid cells and forces the cell before and after the word to be empty. Each cell has pairwise at-most-one clauses over its letters, so two crossing words agree wherever they share a cell just by both writing into the same variable. Every word gets at most one placement.
Those rules alone would let letters appear from nowhere, so every cell-letter variable also implies that at least one placement covers it with that letter. And any two adjacent letters, with an empty cell or the grid edge before them, must be the start of some placement. That is what makes every run of two or more letters a real word rather than a coincidence.
Connectivity was the awkward one. I want one connected grid rather than islands. The encoder picks the first filled cell in reading order as a root, then unrolls a breadth-first search into variables meaning "this cell reaches the root within \(i\) steps", each implied by the cell being filled and a neighbor reaching the root in \(i-1\). Every filled cell must reach the root. I cap the unrolling at 20 steps because the full bound made the formula too big, so a long snaking grid that needs more than 20 steps gets rejected even though it's legal.
Density is a cardinality constraint, at least half the cells filled, through a hand-rolled sequential counter whose auxiliary variables mean "at least \(j\) of the first \(i\) cells are filled". The same counter forces at least three across and three down words. Neither the CLI's --density nor its --seed flag reaches the encoder, so the 50 percent minimum is fixed and puzzles aren't reproducible.
The word pool per puzzle is small, about 100 words at 16x16, drawn 60 percent short (3 to 5 letters), 30 percent medium, and 10 percent long. One run I measured came to 333,000 variables and 28 seconds. When a pool can't fill the grid, Varisat proves it and the CLI skips that puzzle with a warning instead of searching forever.
Words
An unfiltered dictionary gave me medical abbreviations, archaisms nobody would recognize, and occasionally offensive entries. The shipped allowlist is 47,327 words cut down from the WordSet dictionary. A word only qualifies if it's 3 to 15 letters, all ASCII, and has a definition between 10 and 200 characters that doesn't contain the word itself, because that definition becomes the clue. The CLI takes a custom allowlist for themed books.
The book
Each puzzle takes a two-page spread, grid on the left and clues on the right, with a wider inner margin for the binding. Before the puzzles there is a title page, a copyright page with ISBN and edition fields, an optional introduction, and a table of contents. Trim sizes are 5x8, 5.5x8.5, 6x9, 7x10, and 8x10 inches. The cover is an SVG template sized to the trim, with the spine width computed from the page count at KDP's published 0.002252 inches per page for black and white and 0.002347 for color. Puzzles are generated in parallel with rayon, one per core.