Source-linked AI summary
Evaluating SAT Solver Metrics as Predictors of Human-Perceived Nonogram Difficulty
Changdao He, Yibing Ju, Jonathan Calver, Alice Gao
TL;DR
The paper asks whether SAT-based solver effort predicts how difficult humans find Nonograms. It formulates puzzles as SAT instances and compares solver statistics with participant reports and behaviour. The study finds little alignment overall, with evidence that expertise moderates reported-difficulty relationships and that human propagation strategies are not directly captured.
Problem
Prior studies often use algorithmic solver metrics to measure puzzle difficulty, but most lack validation against human-reported difficulty and solving behaviour.
Method
The study encodes Nonograms as SAT instances, extracts solver statistics, and compares them with participant interactions, difficulty reports, expertise, and solving strategies.
Results
SAT solver metrics largely do not align with human-perceived Nonogram difficulty or behavioural signals, while expertise moderates some reported-difficulty relationships.
Takeaways & Limitations
Human and solver difficulty appear to arise from different underlying mechanisms, with recurring human propagation strategies not captured by the considered solver metrics.
Takeaways & Limitations
Puzzle-level correlation analyses are exploratory because only 6 puzzles were sampled and assignments were somewhat unbalanced at 28–43 participants.
Abstract
from arXiv · showhide
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.
1 Introduction
This paper tests whether SAT solver statistics predict human-perceived Nonogram difficulty and solving behaviour. It combines a SAT formulation with a behavioural study and finds little evidence of alignment, while identifying human strategies not directly represented by the measured statistics.
- Problem context: Nonograms require assigning filled cells so row and column clues specifying consecutive run lengths are satisfied simultaneously.A clue such as “1 3” specifies ordered filled runs separated by at least one empty cell, and the solution is unique.
- Research questions: Prior solver-based difficulty studies have often lacked validation against human data, motivating questions about reported difficulty and solving behaviour.The study asks whether SAT statistics correlate with participant-reported difficulty and with human behavioural signals.
- Approach: The study encodes Nonograms as SAT instances, extracts decisions, propagations, and conflicts from CDCL solvers, and records participant interactions and self-reported difficulty.The authors expected greater solver effort to correspond to higher reported difficulty and specific solver metrics to align with particular behaviours.
- Findings: The authors find little evidence that SAT solver statistics positively associate with reported difficulty or behavioural signals for the examined metrics, encoding, and puzzle sample.This is described as an exploratory result limited to the specific study configuration.
- Findings: Starting footholds and constraint-propagation chains may matter to human judgments but are not directly represented by the considered SAT statistics.The result points to recurring human solving strategies that diverge from solver-measured complexity.
2 Related Work
Related work spans algorithmic and constraint-based Nonogram solvers alongside research on puzzle difficulty. The paper distinguishes mathematical or computational difficulty from human-perceived difficulty and therefore measures behaviour as well as reported judgments.
- Algorithmic approaches: Existing Nonogram solvers include genetic algorithms, depth-first search with permutation generation, and heuristic methods combined with neural networks.
- Constraint formulations: Constraint-based approaches include 2-SAT, integer linear programming, and CSP decompositions that combine row and column reasoning.The paper instead uses a single CNF instance for the complete puzzle, as described in the supplied related-work passage.
- Difficulty concepts: Nonograms are NP-hard, while inference difficulty is co-NP-complete and substantially determined by filled-cell density.These are computational properties rather than direct measures of human-perceived difficulty.
- Human difficulty: Solve time and perceived difficulty have often been treated interchangeably, but recent work suggests they can decouple around insight moments.This motivates collecting both solving behaviour and reported difficulty for a more holistic view.
3.1 SAT Problem Formulation and Metrics
The paper encodes each Nonogram as a compact CNF model with explicit block placements and shared cell variables, then uses CDCL solver statistics as search-effort metrics. The encoding restricts feasible placements and is designed to strengthen propagation.
- SAT Problem Formulation: A Nonogram is represented on an R × C grid with ordered row and column clues describing contiguous filled-cell blocks.A valid solution is a binary matrix satisfying all row and column constraints.
- SAT Problem Formulation: The CNF encoding uses cell variables for filled status and block-start variables for feasible placements, with each block selecting exactly one start.
- SAT Problem Formulation: Feasible block starts are bounded using a packed configuration, remaining slack, and earliest and latest start positions before CNF construction.Restricting starts to the resulting interval removes structurally impossible placements.
- SAT Problem Formulation: The clauses enforce block placement, ordering, cell coverage, filled-cell justification, and global row-column consistency through shared cell variables.
- Complexity: Each line introduces O(kN) auxiliary variables and O(kN^2) worst-case clauses, while instances up to 10×10 remain compact and solve within milliseconds.
- Encoding choice: The block-start encoding is chosen because it exposes explicit placement decisions and provides stronger propagation than a purely cell-based formulation.
- Solver-Derived Difficulty Metrics: The study records decisions, propagations, and conflicts as solver search-effort measures, each corresponding respectively to heuristic choices, forced assignments, and falsified clauses.
3.2 Experimental Design
The experiment combines controlled Nonogram generation with web-based sessions that capture detailed interactions, subjective judgments, expertise, and solving strategies. Participants complete tutorials, warmups, three puzzles, and surveys while trajectories are timestamped for analysis.
- Experimental Design: The experiment was designed to collect fine-grained interaction data and subjective difficulty judgments while controlling for prior experience and learning effects.
- Participants and Recruitment: Eligible participants were students at a North American research university recruited between January 2026 and May 2026 through email outreach and university flyers.
- Participants and Recruitment: Most participants completed the approved study in person, while a smaller number participated remotely using the same platform and procedure.Demographic characteristics beyond age eligibility and academic program were not collected.
- Procedure: Each session included a tutorial, warmup, pre-survey, three experimental puzzles, and post-survey.
- Procedure: The tutorial introduced Nonogram rules and the interface, and warmup data were excluded from analysis.The warmup lasted a maximum of five minutes.
- Measures: The pre-survey measured Nonogram and logic-puzzle experience, exposure to puzzle sizes, play frequency, and self-rated skill on a 1–10 scale.
- Measures: Participants attempted three puzzles and could edit, undo, reset, request hints, submit for verification, or skip, then rated difficulty on a 1–5 scale.They also reported reliance on guessing rather than logical deduction.
- Measures: The post-survey allowed revised difficulty ratings and collected explanations, strategy descriptions, guessing reports, and optional comments.
4 Results
Across the results, SAT solver metrics did not significantly align with puzzle difficulty rankings or recorded participant behaviours. Expertise nevertheless moderated solver-metric sensitivity in reported difficulty, while higher expertise was associated with more efficient solving.
- Study and analysis: 67 participants contributed 201 puzzle attempts across three of six puzzles, with varied puzzle subsets and presentation orders.The study used 67 of 120 possible ordered selections and analyzed revised final difficulty ratings.
- Reported difficulty: No significant puzzle-level Spearman correlation was found between Bradley-Terry-adjusted reported-difficulty rankings and SAT solver metric rankings.Table 1 reports the comparison between participant-derived difficulty rankings and solver metrics.
- Expertise: Expertise significantly moderated the SAT-metric-to-difficulty relationship, with more expert participants becoming less sensitive to solver-measured puzzle difficulty.Expertise itself was not significantly related to mean final difficulty (ρ = −0.094, p = 0.451).
- Behavioural data: Higher expertise was associated with faster solving, fewer hints and pauses, and fewer errors.These relationships were assessed using participant-level mean behavioural outcomes.
- Behavioural data: No significant correlation emerged between any recorded participant behaviour and any SAT solver metric.Behavioural signals were evaluated with crossed-random-effects linear mixed models for each behaviour–metric pair.
- Survey responses: Constraint propagation was negatively associated with subjective difficulty, whereas ambiguity, guessing, and cognitive load were positively associated with it.The associations were estimated using rank-biserial correlations on coded difficulty and strategy themes.
5 Discussion
The study finds little evidence that SAT solver metrics predict human-perceived Nonogram difficulty or behavioural signals, while human difficulty themes and solving strategies diverge from solver-measured complexity. These exploratory puzzle-level findings are limited by the small, unbalanced puzzle sample.
- The puzzle-level correlation analysis is exploratory because only 6 puzzles were studied and assignments were unbalanced at 28–43.
- SAT solver metrics show no evidence of predicting human-perceived difficulty, whether difficulty is reported directly or proxied by behavioural signals.
- Humans may prioritize advanced strategies combining several constraints, while the basic SAT encoding restricts solvers to unit propagation on individual clauses.CDCL solvers can learn joint clause patterns after conflicts, but expert difficulty ratings diverge further from solver ratings than beginners’ ratings do.
6 Conclusion
The study concludes that SAT solver metrics largely do not align with how humans experience or solve Nonograms. It identifies recurring human strategies, evidence that expertise moderates the relationship with solver metrics, and directions for testing more expressive encodings and broader samples.
- SAT solver metrics largely do not align with human experiences and solving processes in Nonograms.
- Trajectory and survey analyses reveal recurring human solving strategies that solver metrics do not capture.
- Expertise appears to moderate the relationship between reported difficulty and solver metrics, possibly because participants develop advanced propagation strategies.
- Future work should test whether more expressive constraint-satisfaction encodings improve difficulty tracking and extend evaluation to larger samples and other logic puzzles.
A Detailed SAT Encoding
The SAT encoding introduces variables for filled cells and block starts, then constrains placements, ordering, coverage, and cell justification. These constraints connect row and column reasoning into a globally consistent Nonogram solution.
- The encoding introduces Boolean cell variables and block-start variables for each feasible starting position.
- Each block is constrained to have exactly one placement among its feasible start variables.
- Consecutive blocks are ordered so that the next block starts after the preceding block’s span and required separating cell.
- Selected block placements force every cell in their spans to be filled.
- Every filled cell must be covered by at least one selected block placement; cells with no possible covering placement are forced empty.
- Lines without blocks constrain all cells in those lines to be empty.
B Identifying Pauses
Interaction gaps are modeled with a three-component Gaussian mixture model to distinguish interface-driven dragging, smooth logic chaining, and longer reasoning pauses. The pause threshold is set at 2.36 seconds.
- A three-component Gaussian mixture model separates interaction gaps, improving fit by ΔBIC = 7387.1 against a one-component model.
- The first component has mean 0.01s and reflects consecutive cell filling enabled by interface dragging.
- The remaining components distinguish smooth logic chaining from blocks in reasoning or deliberation.
- The pause threshold is 2.36s, corresponding to the equal-posterior threshold between components.
C Codebook
Table 4 presents the qualitative-analysis codebook and strategy taxonomy for Nonogram difficulty, pairing themes and strategies with example participant responses. The codes cover cognitive and interface-related difficulty, confidence, and recurring solving approaches such as forced-line solving, cross-referencing, guessing, and hint use.
- Difficulty themes: Table 4 organizes the qualitative analysis into difficulty themes and strategy codes, each illustrated with an example response.The codebook includes categories such as cognitive load, time pressure, confidence or affect, and visual or spatial layout.
- Difficulty themes and strategies: Additional codes record combinatorial ambiguity, guessing, hint use, and participants’ experiences of confidence, being stuck, or managing filled cells.Examples include multiple intermediate possibilities, reliance on hints, misreading numbers, and difficulty tracking completed cells.
- Solving strategies: Participants described forced-line solving by prioritizing fixed lines and large number blocks.Examples include determining fixed lines first and locating the largest number block first.
- Solving strategies: Most-constrained-first ordering and row/column cross-referencing used clue relationships to narrow possible solutions.Participants compared values across rows and columns and connected known lines with remaining cells.
- Solving strategies: The taxonomy also captures edge or anchor exploitation, negative marking, and trial-and-error or contradiction-based solving.These strategies include using start or end positions, marking white cells, and applying logical deduction with trial and error.