From constraint models to playable puzzle games

From constraint models to playable puzzle games

20 min read

For my paper Scaling Sudoku as a Constraint Problem, I generated a repository of 434,201 Sudoku instances at five sizes between 6×6 and 36×36. I used them in constraint-programming experiments to ask which propagation scheme solves a puzzle without branching, how that changes with size, and how many clues move an instance from one hardness category to another.

I also wanted to play a few of them.

That small wish grew sideways. I now have playable versions of Sudoku, Nonogram, Queens, Zip, Loopy, Tents, Patches, Wend, and its Swedish sibling Swend. They are collected on a games page.

Each game section below includes a small model written in MiniZinc, a constraint-modelling language, and explains one part of the corresponding generator. The models are explanatory sketches rather than the programs that build the packs. Most generation and solving code uses Gecode 6.4.0. Additional programs handle importing, rasterisation, exact cover, and pack assembly.

What all nine games have in common is that I start with a solution or source image. I then add, move, or remove information until the intended answer is unique, or discard a candidate that cannot be repaired cleanly. Some of the same deductions later classify difficulty and provide hints.

Generation and uniqueness checking happen offline. The browser receives static puzzles and stored solutions; it does not run a solver. Difficulty labels come from propagation, search, or deterministic deduction measurements. They provide a relative, mechanically derived ordering within each pack; they do not estimate how difficult players will find the puzzles.

The listings were checked with MiniZinc 2.10.0. To keep them focused, they leave out input validation, search annotations, and the outer loop that rejects a candidate when a second solution exists. Output is omitted except where it defines which decisions constitute a puzzle solution.

Sudoku: from corpus to game#

An in-progress 6 by 6 Sudoku board with pencil marks in the selected top-left cell
Pencil marks in a 6×6 Sudoku

The Scaling Sudoku corpus begins with 32,000 uniquely solvable base puzzles at sizes 6×6, 9×9, 16×16, 25×25, and 36×36. A generator first creates a complete grid, then removes clues while preserving uniqueness. Gecode classifies the resulting puzzles.

The classification extends the setup in Helmut Simonis’s 2005 paper Sudoku as a Constraint Problem. It tries an ordered family of propagation configurations. Val, Bnd, and Dom refer to value, bounds, and domain propagation; BS and DS add bounds or domain shaving.1 The weakest successful configuration becomes the puzzle’s hardness tag. If none finishes without branching, the tag is Search.

The basic Sudoku model is pleasantly short. The box dimensions are data, which lets the same model handle 6×6 boards with 2×3 boxes and the usual 9×9 boards with 3×3 boxes.

sudoku.mzn
include "globals.mzn";
int: n;
int: box_height;
int: box_width;
set of int: N = 1..n;
set of int: Values = 1..n;
set of int: BoxTopRows = {
row | row in N where (row - 1) mod box_height = 0
};
set of int: BoxLeftColumns = {
column | column in N where (column - 1) mod box_width = 0
};
array[N, N] of 0..n: clue;
array[N, N] of var Values: board;
constraint forall (row in N) (
all_different(board[row,..])
);
constraint forall (column in N) (
all_different(board[..,column])
);
constraint forall (top in BoxTopRows, left in BoxLeftColumns) (
all_different(board[
top..top+box_height-1,
left..left+box_width-1
])
);
constraint forall (row, column in N where clue[row,column] > 0) (
board[row,column] = clue[row,column]
);
solve satisfy;

The playable pack is a reproducible, fixed-seed sample of 500 base puzzles from a pinned corpus revision, limited to 6×6 and 9×9 boards. An offline importer turns the selected puzzles and their known solutions into a static pack.

Making Sudoku look more like Sudoku#

Generated puzzles do not automatically have the visual symmetry people tend to expect from a published Sudoku. I did not want to generate a separate collection merely for presentation, so I wrote an offline symmetrification pass for the selected puzzles.

There are two useful freedoms. First, rows and columns can be permuted in ways that preserve the box structure: rows within a band, columns within a stack, and the bands and stacks themselves. Second, a missing rotational partner can be filled with the value from the known solution. The latter only adds information, so it cannot introduce a second solution, but it may make the puzzle easier according to the propagation classifier.

The clue pattern starts out asymmetric.

First, columns 5 and 6 swap within the right stack.

Then the middle and lower two-row bands swap places.

The first new clue stays marked in green while its existing rotational partner pulses.

The second new clue is marked and its existing partner pulses.

The third marked clue completes the last pair.

The finished clue pattern has 180° rotational symmetry.

A small symmetrification run. The permutation reduces eleven missing partners to three before any clues are added. New clues remain green; each existing partner pulses as its match is added.

For each puzzle, the optimiser enumerates the distinct rotational pairings obtainable from box-preserving layouts and ranks them by how many clues would be needed for 180-degree rotational symmetry. It evaluates the three best-ranked layouts, first trying to complete the symmetry for each one. If that changes the hardness tag, it adds partner clues individually and keeps only additions for which Gecode reproduces the original tag. Finally, it chooses the resulting layout with the fewest asymmetric cells.

The pass made 228 of the 500 puzzles exactly rotationally symmetric and reduced the total number of asymmetric cells from 6,172 to 1,928.

Nonogram: back to regular#

An in-progress 10 by 10 Nonogram board with the top of a heart partly filled and known empty squares crossed out
The beginning of a 10×10 heart

In a Nonogram, the player fills cells so that the runs in every row and column match the given clues. The game also loops back to my early Gecode work. In 2005, I wrote the original Gecode nonogram example using Gilles Pesant’s regular constraint. Its model describes a line with runs of lengths a, b, ..., z by the regular expression

0* 1^a 0+ 1^b 0+ ... 0+ 1^z 0*

where 1 is a filled square and 0 is an empty one. Gecode turns the expression into a finite-state machine and constrains every row and column to follow it. The Gecode 6.4.0 example still uses the same compact idea.

Jan Wolter later included the example in his extensive survey of Paint-by-Number solvers. His assessment was rather nice: this small demonstration model performed surprisingly well alongside much larger, specialised solvers.

The MiniZinc model builds and applies the same automata directly. Its run clues are lists, so rows and columns can contain different numbers of runs without padding. The function line_regexp builds a regular-expression string from each list. MiniZinc compiles that string to a finite-state machine, and regular applies it to a row or column.

nonogram.mzn
include "globals.mzn";
enum CellStates = {Empty, Filled};
int: rows;
int: columns;
set of int: Rows = 1..rows;
set of int: Columns = 1..columns;
array[Rows] of list of int: row_runs;
array[Columns] of list of int: column_runs;
array[Rows, Columns] of var CellStates: board;
function string: line_regexp(list of int: runs) =
"Empty* " ++
join(" Empty+ ", [
"Filled{" ++ show(run) ++ "}" | run in runs
]) ++
" Empty*";
% Runs [3, 2] become
% "Empty* Filled{3} Empty+ Filled{2} Empty*"
constraint forall (row in Rows) (
regular(
board[row,..],
line_regexp(row_runs[row])
)
);
constraint forall (column in Columns) (
regular(
board[..,column],
line_regexp(column_runs[column])
)
);
solve satisfy;

A newer icon pack starts with SVGs from the pinned Heroicons 2.2.0 and Phosphor Icons 2.1.1 archives. An offline rasteriser renders each icon at high resolution, fits it to one of four board sizes, and thresholds the result into filled and empty cells.

Source iconHeroicons SVG

A magnified rasterization of the trash icon

Rasterize and trimmagnified preview

Resize and threshold10×10 puzzle bitmap

One accepted icon. The middle panel enlarges the raster preview so that its pixels are visible.

Each source icon is assigned to one board size, so the same image cannot reappear at several resolutions. The selector rejects rasters with extreme fill ratios, too many connected components, duplicate fingerprints, or badly balanced clues, then favours reviewed or more detailed silhouettes. The imported bitmap must satisfy the derived clues, and Gecode must find no second solution.

A deterministic replay records the initial line ambiguity and largest initial candidate set, then measures deduction rounds and unresolved cells. Together with Gecode’s search nodes and failures, these measurements rank the valid instances within each size.

Queens: grow regions around a solution#

An in-progress 9 by 9 Queens board showing black queens, a highlighted assumption square, and the pink Region 9
A failed assumption identifies Region 9 on a 9×9 Queens board

Queens is the one-star form of Star Battle: place one queen in every row, column, and coloured region, with no two queens touching. The generator starts with a valid no-touch queen permutation and grows one orthogonally connected region from each queen. It then perturbs non-queen cells along region boundaries while preserving connectivity.

The small example below starts with the base solution and then shows the proposed region boundaries grown around it. A second solution would be valid with those boundaries, making this an invalid puzzle instance. Moving the cell marked M into the neighbouring region removes that alternative, so one boundary-cell move makes the intended solution unique. The real generator repeats this sort of change while checking region connectivity and stopping each solution count at two.

The base solution before regions are added.
The proposed region boundaries around the base solution.
A second solution would be valid in this configuration, making it an invalid puzzle instance.
One boundary cell move makes the intended solution unique.

One variable per row is enough for the puzzle model. Its value is the queen’s column. Distinct columns handle the column rule, while indexing the region matrix at each queen position handles all coloured regions at once.

queens.mzn
include "globals.mzn";
int: n;
set of int: N = 1..n;
enum Regions;
array[N, N] of Regions: region;
array[N] of var N: board;
% Each queen is in a different column
constraint all_different(board);
% Each queen is in a different region
constraint all_different (row in N) (
region[row, board[row]]
);
% Queens in neighbouring rows may not touch diagonally
constraint forall (row in 1..n-1) (
abs(board[row] - board[row+1]) > 1
);
solve satisfy;

Region relabellings and the eight rotations and reflections of a square board are reduced to one canonical fingerprint, preventing disguised copies of the same puzzle. The generator also limits tiny and dominant regions; I chose those limits after measuring published LinkedIn Queens boards. Difficulty uses the same propagation and shaving configurations as Scaling Sudoku, followed by Search when none solves the board without branching.

Zip: ask for a counterexample#

An in-progress 7 by 7 Zip board with a path drawn from clue one through clue three
Fourteen cells into a 7×7 Zip path

In Zip, the player draws one path through every cell while visiting numbered clues in order and avoiding hedges. The generator represents the path as a Gecode circuit: each board cell has a successor, and an extra return node connects the final clue back to clue 1. The circuit constraint rules out disconnected subtours, while inverse path and position views make the numbered ordering constraints explicit.

The model expresses orthogonal movement with row and column offsets. For each cell, it tries the four directions. MiniZinc’s default <> turns an out-of-bounds lookup into an absent cell; since an absent cell cannot equal the successor, directions outside the board disappear from the disjunction. This avoids a separate adjacency matrix.

zip.mzn
include "globals.mzn";
int: rows;
int: columns;
int: cells = rows * columns;
set of int: Rows = 1..rows;
set of int: Columns = 1..columns;
set of int: Cells = 1..cells;
set of int: Nodes = 1..cells + 1;
int: return_node = cells + 1;
enum Directions = {Up, Right, Down, Left};
array[Directions] of int: row_offset = [-1, 0, 1, 0];
array[Directions] of int: column_offset = [0, 1, 0, -1];
array[Rows, Columns] of Cells: board =
array2d(Rows, Columns, [cell | cell in Cells]);
array[Cells, Cells] of bool: hedge; % Symmetric
int: number_count;
array[1..number_count] of Cells: numbered_cell;
array[Nodes] of var Nodes: successor;
array[Cells] of var Cells: path;
array[Cells] of var Cells: position;
constraint circuit(successor);
constraint inverse(path, position);
constraint successor[return_node] = numbered_cell[1];
constraint successor[numbered_cell[number_count]] = return_node;
constraint forall (
row in Rows,
column in Columns
where board[row,column] != numbered_cell[number_count]
) (
let {Cells: cell = board[row,column]} in
exists (direction in Directions) (
successor[cell] =
(board[
row + row_offset[direction],
column + column_offset[direction]
] default <>)
) /\
not hedge[cell,successor[cell]]
);
constraint path[1] = numbered_cell[1];
constraint path[cells] = numbered_cell[number_count];
constraint forall (step in 1..cells-1) (
successor[path[step]] = path[step+1]
);
constraint forall (number in 1..number_count-1) (
position[numbered_cell[number]] < position[numbered_cell[number+1]]
);
solve satisfy;

To decide which numbers and hedges to show, the Zip generator begins with only the first and last numbers. It asks the solver for a second path, then studies that counterexample. The example below starts after one checkpoint has already been added. Both paths obey the visible clues 1, 2, and 3.

Intended path
Counterexample
Adding clue 3 rules out the counterexample.

The added clue says that the middle-left cell must occur after the top-middle one. That is true of the intended path, but not of the counterexample, so one ambiguity has disappeared. The generator repeats this: whenever possible it adds a numbered checkpoint whose position distinguishes the intended path from the alternative. Sometimes a pair of numbers is needed because the two paths visit those cells in opposite orders. A hedge is added only when numbers cannot separate the counterexample within the clue-density limit.

The process repeats until the intended path is the only solution. Number and hedge limits keep the board from filling with annotations.

Zip tries the same nine propagation and shaving configurations as Scaling Sudoku, followed by Search when none solves without branching. The interface maps the ten internal tags to relative labels from Gentle through Expert.

Loopy: hide clues from a finished loop#

An in-progress 5 by 5 Loopy board with most of its loop drawn
Most of a 5×5 Loopy loop

Loopy is played on the edges of a square grid. The aim is to draw one closed loop without branches or crossings. A number inside a cell tells how many of its four edges belong to the loop; a blank cell imposes no such count.

The generator begins with the loop. It grows a connected patch of cells while keeping the cells outside the patch connected as well, then rejects any boundary that is not one simple loop. Once that shape is fixed, the generator counts the four surrounding loop edges for every cell and obtains a fully clued puzzle.

The MiniZinc model assigns one successor variable to each grid vertex. A vertex outside the loop points to itself. The remaining successors form one directed cycle, which is exactly the structure captured by subcircuit. An undirected grid edge belongs to the loop when either endpoint chooses the other as its successor.

loopy.mzn
include "subcircuit.mzn";
enum Cells;
enum Vertices;
enum Edges;
enum Sides = {North, East, South, West};
array[Cells] of opt 0..3: clue;
array[Cells, Sides] of Edges: cell_edge;
array[Edges] of Vertices: edge_from;
array[Edges] of Vertices: edge_to;
array[Vertices] of set of Vertices: neighbour = [
{edge_to[edge] | edge in Edges where edge_from[edge] = vertex} union
{edge_from[edge] | edge in Edges where edge_to[edge] = vertex}
| vertex in Vertices
];
array[Vertices] of var Vertices: successor;
constraint forall (vertex in Vertices) (
successor[vertex] = vertex \/
successor[vertex] in neighbour[vertex]
);
constraint subcircuit(successor);
constraint exists (vertex in Vertices) (
successor[vertex] != vertex
);
% An undirected edge cannot be traversed in both directions.
constraint forall (edge in Edges) (
not (
successor[edge_from[edge]] = edge_to[edge] /\
successor[edge_to[edge]] = edge_from[edge]
)
);
array[Edges] of var bool: in_loop = [
successor[edge_from[edge]] = edge_to[edge] \/
successor[edge_to[edge]] = edge_from[edge]
| edge in Edges
];
constraint forall (cell in Cells where occurs(clue[cell])) (
sum (side in Sides) (in_loop[cell_edge[cell, side]]) =
deopt(clue[cell])
);
solve satisfy;
% Puzzle solutions are undirected edge sets, not cycle orientations.
output [show(in_loop)];

The additional edge constraint rules out a directed two-cycle between adjacent vertices, which would otherwise collapse to a single undirected edge rather than a loop. The output records only in_loop, and the omitted uniqueness loop blocks each discovered edge set. It therefore treats the two directed orientations as the same puzzle solution.

The fully clued board is a useful starting point but a poor puzzle. The generator therefore tries hiding clues one at a time. A clue stays hidden only if the intended loop remains unique. For an Easy or Medium candidate, the local deduction engine also keeps the puzzle within the requested band as clues disappear.

Difficulty is measured by replaying two families of local deductions. A satisfied clue excludes its remaining edges, while a clue that needs every undecided edge forces all of them into the loop. At a grid vertex, two loop edges exclude the other incident edges; one loop edge with only one undecided incident edge forces that edge into the loop; and no selected loop edges with only one undecided incident edge forces that edge out. The bands record how many deduction rounds are needed; every selected puzzle can be completed by these rules without search.

Tents: move the trees against an alternative#

In Tents, the player places one orthogonally adjacent tent for each tree. No two tents may touch, even diagonally, and the row and column clues give the number of tents in each line. The generator starts from those tents, assigns each one a distinct orthogonally adjacent tree, and derives the counts. Those clues often admit another tent set.

The useful counterexample is the alternative set together with its possible tree matching. When the intended answer is not unique, the generator moves one tree to another square beside its intended tent, choosing a square that prevents the alternative tents from matching every tree. The tent set and line counts stay fixed. The generator recounts solutions after each move and stops when only the intended tent set remains. In the example below, dashed lines show one matching between trees and tents; M marks the moved tree.

The intended tent set under the initial tree positions.
A second tent set satisfies the same clues and still matches every tree.
Moving one tree keeps the intended answer and prevents the alternative matching.

The MiniZinc sketch does not need a decision variable for every board cell. A Coordinate record keeps a row and column together, and every tree owns one such decision record for its tent. Whole-array field projections such as tents.row then let global_cardinality count the chosen rows and columns directly. The rest of the listing uses optional lookups at board edges, imaginary 2×2 squares to enforce tent spacing, and sorted output to identify a solution by its tent set rather than a particular tree-to-tent matching.

tents.mzn
include "globals.mzn";
int: rows;
int: columns;
set of int: Rows = 1..rows;
set of int: Columns = 1..columns;
set of int: Cells = 1..(rows * columns);
enum Trees;
type Coordinate = record(Rows: row, Columns: column);
array[Trees] of Coordinate: trees;
array[Rows] of 0..columns: row_count;
array[Columns] of 0..rows: column_count;
array[Rows, Columns] of Cells: cell_id =
array2d(Rows, Columns, [cell | cell in Cells]);
array[Trees] of var Coordinate: tents;
array[Trees] of var Cells: tent_cells = [
cell_id[tents[tree].row, tents[tree].column]
| tree in Trees
];
% Each tree chooses an orthogonally adjacent cell that is not a tree.
constraint forall (tree in Trees) (
not (tents[tree] in trees) /\
exists (
row_offset, column_offset in -1..1
where abs(row_offset) + abs(column_offset) = 1
) (
tent_cells[tree] =
(cell_id[
trees[tree].row + row_offset,
trees[tree].column + column_offset
] default <>)
)
);
% diffn also makes the cells distinct, but the explicit all_different
% gives the tree-to-tent matching its own Hall-style propagator.
constraint all_different(tent_cells);
% Count the tent rows and columns directly.
constraint global_cardinality(
tents.row,
[row: row | row in Rows],
row_count
);
constraint global_cardinality(
tents.column,
[column: column | column in Columns],
column_count
);
% Two 2 by 2 squares overlap exactly when their anchor cells touch.
constraint diffn(
tents.row,
tents.column,
[tree: 2 | tree in Trees],
[tree: 2 | tree in Trees]
);
solve satisfy;
% Puzzle solutions are tent sets, not particular tree/tent matchings.
output [show(sort(tent_cells))];

The parameter array cell_id is only a coordinate lookup. The adjacency constraint uses the same default <> boundary idiom as Zip. Strict equality cannot match the absent value returned outside the board, so the four offsets need no edge cases.

diffn normally keeps rectangles from overlapping. Here each tent is the anchor of an imaginary 2×2 square. Two such squares overlap exactly when their anchor cells coincide or touch along an edge or corner, so one global replaces the eight-neighbour decomposition. It also implies that the tent cells are distinct. The explicit all_different is logically redundant, but it keeps the one-to-one matching visible to a dedicated matching propagator. The imaginary squares may extend past the board; without a container constraint, diffn only constrains them relative to each other.

The sorted output is deliberate. Since tents is indexed by tree, one tent set can admit several tree-to-tent matchings. The omitted uniqueness loop blocks the sorted cell identifiers, so it counts player-visible tent sets rather than matching witnesses. The native generator uses the same identity when it asks whether a second solution exists.

The player-facing Easy, Medium, and Hard labels come from replaying the deterministic deductions used by the hint engine. Easy puzzles need line-count and tent-spacing deductions, grass marks for cells without an adjacent tree, and trees with a single remaining position. Medium puzzles add locked tree sets and one-to-one matching deductions. Hard puzzles require a short failed assumption: try a tent or grass mark, propagate, and reject the assumption when it reaches a contradiction.

Empty lines are useful clues, but too many produce striped boards with large inactive areas. The generator therefore sets separate limits on empty rows and empty columns.

Patches: remove information from a tiling#

An in-progress 5 by 5 Patches board with two rectangles placed
Two patches placed on a 5×5 board

Patches asks the player to divide the board into rectangles, one per coloured clue, while respecting any given area or shape. The generator starts from a complete tiling. A bounded depth-first search tiles a square board with rectangles of area at least two, then places one clue in a corner of each rectangle. Initially, every clue gives both the rectangle’s area and its shape: square, wide, or tall.

That fully described tiling is usually too easy. The generator shuffles the clue fields and tries removing an area or shape. After every removal, an exact-cover solver counts rectangle tilings up to two; the field stays absent only when the puzzle remains unique.

The corresponding model uses one record for each clue and another for the placement variables of its rectangle. The Boolean covers view is redundant, but it expresses the exact-cover constraint clearly and gives useful propagation from cells back to rectangles. Corner placement is a convention for the generated answer, not a player rule: an alternative rectangle only has to contain its clue.

patches.mzn
enum Shapes = {Unspecified, Square, Wide, Tall};
int: rows;
int: columns;
set of int: Rows = 1..rows;
set of int: Columns = 1..columns;
int: patch_count;
set of int: Patches = 1..patch_count;
type PatchClue = record(
Rows: row,
Columns: column,
0..rows*columns: area, % 0 means absent
Shapes: shape
);
array[Patches] of PatchClue: clue;
type PatchPlacement = record(
var Rows: top,
var Columns: left,
var 1..rows: height,
var 1..columns: width
);
array[Patches] of PatchPlacement: placement;
array[Patches, Rows, Columns] of var bool: covers;
constraint forall (patch in Patches) (
placement[patch].top + placement[patch].height - 1 <= rows /\
placement[patch].left + placement[patch].width - 1 <= columns /\
placement[patch].width * placement[patch].height >= 2
);
constraint forall (patch in Patches, row in Rows, column in Columns) (
covers[patch,row,column] <->
row >= placement[patch].top /\
row < placement[patch].top + placement[patch].height /\
column >= placement[patch].left /\
column < placement[patch].left + placement[patch].width
);
constraint forall (patch in Patches) (
covers[patch,clue[patch].row,clue[patch].column]
);
constraint forall (patch, other in Patches where patch != other) (
not covers[patch,clue[other].row,clue[other].column]
);
constraint forall (row in Rows, column in Columns) (
sum (patch in Patches) (covers[patch,row,column]) = 1
);
constraint forall (patch in Patches where clue[patch].area > 0) (
placement[patch].width * placement[patch].height = clue[patch].area
);
constraint forall (patch in Patches) (
clue[patch].shape = Unspecified \/
(clue[patch].shape = Square /\
placement[patch].width = placement[patch].height) \/
(clue[patch].shape = Wide /\
placement[patch].width > placement[patch].height) \/
(clue[patch].shape = Tall /\
placement[patch].width < placement[patch].height)
);
solve satisfy;

Patches classifies difficulty by giving each clue a domain of candidate rectangles. It uses three custom propagation tiers, named Val, Bnd, and Dom to match the other games. Val removes rectangles that overlap an assigned patch. Bnd also uses cell coverage: if only one clue can still cover a cell, that clue’s domain is restricted accordingly. Dom adds a local support check for the remaining uncovered cells. Bounds- and domain-shaving variants complete the set, followed by Search.

Wend and Swend: fill a path cover with words#

An in-progress 5 by 5 Wend board with HERBS traced through the letter grid
Tracing HERBS in Wend

Wend and its Swedish sibling Swend ask the player to divide the letter grid into words of the given lengths. Every open cell belongs to one orthogonally connected word path. The two games use the same path and exact-cover models with language-specific word tables.

Generation runs that process backwards. It chooses a symmetric block mask and a path through every open cell, cuts the path into lengths between three and ten, and fills the pieces with words.

The first MiniZinc sketch models the geometric part of generation directly. The open cells are nodes in an undirected grid graph. Requiring MiniZinc’s path constraint to include every open node gives one Hamiltonian path from start to finish.

wend-paths.mzn
include "globals.mzn";
int: rows;
int: columns;
set of int: Rows = 1..rows;
set of int: Columns = 1..columns;
enum Cells;
array[Rows, Columns] of opt Cells: board; % <> marks a block
type Offset = record(int: row, int: column);
array[1..2] of Offset: forward = [
(row: 0, column: 1),
(row: 1, column: 0),
];
function opt Cells: neighbour(Rows: row, Columns: column, Offset: offset) =
board[
row + offset.row,
column + offset.column
] default <>;
type Edge = record(Cells: from, Cells: to);
array[int] of Edge: edge = [
(
from: deopt(board[row,column]),
to: deopt(neighbour(row, column, offset))
)
| row in Rows, column in Columns, offset in forward
where occurs(board[row,column]) /\
occurs(neighbour(row, column, offset))
];
set of int: Edges = index_set(edge);
var Cells: start;
var Cells: finish;
array[Edges] of var bool: used_edge;
constraint path(
from: edge.from,
to: edge.to,
source: start,
sink: finish,
ns: [cell: true | cell in Cells],
es: used_edge
);
% A path and its reverse are equivalent.
constraint start < finish;
solve satisfy;

The optional board values describe both the cell identities and the graph boundary. A block contains <>, and the default <> expression gives an out-of-range lookup the same absent value. The occurs tests therefore reject both blocks and positions beyond the board. Only rightward and downward offsets are needed because path treats the edges as undirected.

path returns selected edges rather than an ordered cell array. Walking those edges from start to finish recovers the sequence. The native generator constructs that sequence directly, cuts it into the required lengths, may reverse and reorder the pieces, and fills them with words.

The published 5×5 instance below shows those three steps directly.

1. Make a path

24 open cells

Choose one path through every open cell.

2. Cut into slots

Cut it into the required word lengths.

3. Fill with words

Choose words and write them along the slots.

Those chosen words do not by themselves make a valid puzzle. The same letters may form other dictionary words, and those candidates may admit a second path cover. A trie finds every dictionary word that can be traced without reusing a cell; the second model checks whether those candidate paths have another exact cover. Every cell must occur once, and the selected paths must have the advertised lengths.

wend-cover.mzn
set of int: OpenCells;
set of int: Lengths = 3..10;
enum Candidates;
array[Candidates] of set of OpenCells: candidate_cells;
array[Candidates] of Lengths: candidate_length;
array[Lengths] of int: required_count;
array[Candidates] of var bool: selected;
constraint forall (cell in OpenCells) (
sum (candidate in Candidates
where cell in candidate_cells[candidate]
) (selected[candidate]) = 1
);
constraint forall (length in Lengths) (
sum (candidate in Candidates
where candidate_length[candidate] = length
) (selected[candidate]) = required_count[length]
);
solve satisfy;

The Gecode checker stops after finding two covers and accepts only a unique decomposition.

Swend’s lexicon starts from SAOL 14 and keeps words supported by the Swedish Kelly list or NyLLex, together with reviewed additions. Wend instead uses a filtered, pinned version of the English Speller Database. Both importers remove palindromes and reversal pairs because a path can be read in either direction.

An in-progress 5 by 5 Swend board with ONT traced through the letter grid
Tracing ONT in Swend

Generated boards must contain turns and straight segments, use all four directions, and survive deduplication under rotations and reflections. Within each board size, the generator ranks them by the number of traceable dictionary candidates, followed by Gecode search nodes and failures. The lower, middle, and upper thirds receive the relative labels Easy, Medium, and Hard. Within each third, the generator favours boards with more mirrored letter pairs and a balanced selection of block masks.

Hints as small propagation systems#

Some of the local deductions used to classify generated puzzles can also explain the next move to a player. Once a puzzle has a known solution, the easiest hint system is still to reveal part of it. I wanted the hint button to make a deduction when the current state supports one, and to be explicit when it falls back to a reveal.

Sudoku and Queens have explainable hints backed by a small, puzzle-neutral deduction engine. It knows about exact-one groups, capacity-one groups, conflicts, Hall sets,2 and failed-literal reasoning, which uses the same assumption-propagation-failure test as shaving. It runs rules in teaching order and keeps a shown hint active until its target has been handled. The game adapters give those ideas their concrete meaning: cells and values for Sudoku; rows, columns, regions, and attacks for Queens.

Sudoku first reports an incorrect entry. It then tries naked singles, a value with only one place in a row, column, or box, Hall sets of up to four cells,2 and finally a small negative-reasoning step: assume a candidate, propagate forced placements, and reject it if propagation reaches a conflict. Only when none of those rules applies does it reveal a value from the stored solution.

Queens follows a similar teaching order. It reports attacking or incorrect queens and a cross that hides a solution square. It marks cells directly attacked by placed queens, finds rows, columns, or regions with one candidate left, and uses locked sets when a collection of regions is confined to the same number of rows or columns. Failed-literal reasoning handles the remaining case by tentatively placing a queen and propagating until two forced queens attack or some group loses its last candidate.

The first two examples below are direct deductions. A marks squares that the deduction allows the player to cross out. In the locked-set example, R marks the candidates that justify those actions.

A placed queen attacks the outlined squares.
The outlined square is the first row's only candidate.
Two regions lock columns 5 and 6.

Nonogram uses the same line model for solving and for hints, but keeps the hint implementation local. It first reports a marked square that conflicts with the stored picture. Otherwise it enumerates all line patterns compatible with the current marks and the run clues. If every remaining pattern for a row or column agrees on an unknown square, that square is forced. Only when no line has such a deduction does the hint reveal a square from the stored solution.

The other games use narrower hint finders. Patches recomputes live rectangle domains, and Tents replays its line, matching, and failed-assumption deductions. Loopy reasons about clue saturation, vertex degree, and premature closed subloops. Zip identifies the first wrong turn or continues the known path, while Wend and Swend progressively reveal a word. When no deduction applies, the hint says that it is revealing part of the stored solution.

That keeps the distinction visible: a deduction follows from the current state, while a reveal merely helps the player resume.

Summary#

Across these games, constraints do three related jobs. They describe valid solutions, detect alternatives during generation, and support deductions for hints. The generators use uniqueness in different ways: Nonogram retains source images that pass a uniqueness check; Sudoku, Loopy, and Patches remove information while preserving a unique answer; Queens, Zip, and Tents repair counterexamples; Wend and Swend reject alternative covers.

I started with a large Sudoku corpus and wanted to play a few instances. I ended up with nine playable games (so far).

Footnotes#

  1. Shaving temporarily assigns a value and propagates to a fixpoint. If that assumption fails, the value can be removed without committing to a branch. Bounds shaving tests the current smallest and largest values of a domain; domain shaving tests every remaining value. I described the corresponding MiniZinc preprocessing modes in the LinkedIn Queens benchmarking post.

  2. Hall’s theorem gives the matching condition behind all_different: any set of k variables must collectively have at least k possible values. If it has exactly k, those values are reserved for those variables and can be removed from every other domain; fewer than k proves failure. Régin’s matching-based propagator uses the general form of this argument to establish domain consistency. Puget’s bounds propagator looks for the cheaper restricted form given by Hall intervals. 2