Evaluating SAT Solver Metrics as Predictors of Human-Perceived Nonogram Difficulty
2026-08-24 • Human-Computer Interaction
Human-Computer InteractionArtificial Intelligence
AI summaryⓘ
The authors studied Nonograms, a type of puzzle, to see if computers solving them take the same amount of work as humans think it takes. They used special computer programs called SAT solvers to solve these puzzles and compared that to how humans played and said how hard the puzzles were. They found that what the computer measures as difficult doesn’t match well with what people feel or do, except for experts where there is some connection. They also noticed people use certain strategies that are different from how the computers solve the puzzles.
NonogramsSAT solversconstraint satisfaction problempuzzle difficultyhuman solving strategiesbehavioral signalsalgorithmic solverexpertise moderationpropagation
Authors
Changdao He, Yibing Ju, Jonathan Calver, Alice Gao
Abstract
Algorithmic solver effort is often assumed to align with perceived puzzle difficulty, but this assumption is rarely tested against human solving data. We evaluate this assumption for Nonograms, a popular logic puzzle similar to Sudoku in which numeric clues along each row and column determine a unique solution grid. We formulate Nonograms as a constraint satisfaction problem and solve them using existing SAT solvers. We then conduct a user study in which we collect data on both participant interactions and reported difficulty. We find that neither participants' reported difficulty nor their behavioural signals correlate meaningfully with SAT solver metrics; however, we find evidence that expertise moderates the relationship between solver metrics and reported difficulty. In this process, we uncover distinct, recurring solving strategies that indicate human preference for complex propagation, diverging from solver-measured complexity.