Search papers, labs, and topics across Lattice.
This study evaluates the correlation between SAT solver metrics and human-perceived difficulty in solving Nonograms, a type of logic puzzle. By formulating Nonograms as a constraint satisfaction problem and conducting a user study, the authors reveal that traditional solver metrics do not align with participants' reported difficulty or behavioral signals. Notably, they discover that expertise influences the relationship between solver metrics and perceived difficulty, highlighting distinct human solving strategies that prioritize complex propagation over solver-measured complexity.
SAT solver metrics fail to predict human difficulty in Nonograms, revealing a disconnect between algorithmic and human solving strategies.
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.
