将SAT求解器指标作为人类感知的Nonogram难度预测因子进行评估
Evaluating SAT Solver Metrics as Predictors of Human-Perceived Nonogram Difficulty
浏览论文内容
中文总结 AI 辅助
该研究针对Nonogram谜题验证算法求解器工作量与人类感知难度的关联，通过用户研究发现二者无显著关联，且专业知识会调节该关系，同时揭示人类求解偏好与SAT求解器测量的复杂性存在差异。
中文摘要 AI 辅助
算法求解器的工作量通常被认为与谜题的感知难度一致，但这一假设很少通过人类求解数据进行验证。我们针对Nonogram（一种类似数独的流行逻辑谜题，每行和每列的数字线索可确定唯一解网格）评估该假设。我们将Nonogram形式化为约束满足问题，并使用现有SAT求解器求解。随后开展用户研究，收集参与者的交互数据和报告的难度数据。我们发现，参与者报告的难度及其行为信号均未与SAT求解器指标产生有意义的关联；但有证据表明，专业知识会调节求解器指标与报告难度之间的关系。在此过程中，我们发现了独特且反复出现的求解策略，表明人类偏好复杂的传播过程，这与求解器测量的复杂性存在差异。
英文摘要
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.
发表机构
- University of Alberta（阿尔伯塔大学）
- University of Toronto（多伦多大学）
机构由 AI 辅助整理，请以论文原文为准。
