使用布尔可满足性求解器来帮助减少认知负荷并提高在创建通用学术时间表时的决策能力

文献标题

Using Boolean Satisfiability Solvers to Help Reduce Cognitive Load and Improve Decision Making when Creating Common Academic Schedules

文献信息

• 主题领域: 人机交互领域，专注于通过自动化技术优化学术排课流程
• 关键词: 约束求解，决策制定，学生排课，人机交互设计，布尔可满足性，认知负荷，SAT求解器

研究背景与问题

• 发现的问题:

  1. 学生手动创建学术课程表需要处理大量复杂和冲突的约束，容易导致认知过载。
  2. 认知负荷会削弱决策质量，如遗漏课程信息或冲突的时间安排。

• 问题重要性: 创建学术课程表不仅是一项常见任务，还直接影响学生的时间管理、生活质量以及学术进度。减少认知负担、优化决策质量对于提升学生体验和时间管理至关重要。

• 研究动机与相关工作:

  1. 传统手动方法被认为繁琐，因此需要一种能减轻认知负担的自动化解决方案。
  2. SAT求解器在解决约束满足问题方面已显成效，但其应用于个性化排课领域仍有开发潜力。
  3. 现有工具主要强调排课速度，却未充分考虑用户体验和人机协作。

解决方案

• 提出的方法: 设计一个基于布尔可满足性求解器（SAT Solver）的半自动化学术排课系统，该系统不仅能帮助个人创建课程表，还支持小群体间的协作式排课。

• 创新之处:

  1. 将SAT求解器引入用于解决具体的学术排课问题，满足个体定制需求。
  2. 系统支持协同工作，允许用户根据个人和朋友的偏好动态调整课程表。
  3. 平衡了自动化与用户控制，从而优化交互体验。

• 实施步骤与关键技术:

  1. 开发8个模块，包括课程查看、排课管理、偏好设置、课程表比较、协作课表生成等。
  2. 在"排课管理"模块中使用SAT Solver进行约束编码与解码，自动处理跨课程的冲突。
  3. 提供可视化界面，让用户手动确认和修改自动生成的课程表，同时通过颜色和格式区分课程优先级。
  4. 引入“好友协作”功能以便群体成员分享和同步课程表。

研究成果

• 具体成果:

  1. 实验表明，该系统显著降低了用户的认知负荷和压力。
  2. 使用该系统的学生能够更快地完成课程表设计，并对最终决策的满意度更高。
  3. 减少了手动排课错误，例如时间冲突或遗漏课程。

• 优势比较: 与传统方法相比：

  1. 减轻了因手动处理数据而带来的认知负担。
  2. 提高了决策质量和排课效率。
  3. 支持协作式排课，增强了群体间的协调能力。

• 实验结果:

  1. 实验组的NASA-TLX认知负荷评分显著较低（17.04 vs. 26.52，p < 0.001）。
  2. 异常高效的任务完成时间：实验组时间平均为40.35分钟，而对照组为51.77分钟。
  3. 实验组的用户满意度更高，认为课程表视觉化和自动化决策增强了决策过程的易用性。

• 局限性与未来方向:

  1. 系统适用于2-4人的小组合作，未来可测试更大规模群体的应用效果。
  2. 系统对偏好数量较多时的自动化效率有所下降，建议未来对比其他优化算法如遗传算法或禁忌搜索。
  3. 可以探索将SAT求解器应用到其他非学术性领域的协作式排程场景，如企业员工排班或会议协调。
  4. 提高系统透明度，向用户提供关于自动决策的背景反馈以减少对算法结果的疑虑。

总结

本文研究了基于SAT Solver的学术课程排课系统在优化决策和减轻认知压力方面的有效性，通过对用户体验和认知负荷的细致分析，提出了重要的设计建议，包括保持自动化与手动控制的平衡，以及改善结果解释机制，在实际应用领域里具有重要启示价值。未来研究可以进一步完善技术优化并扩展应用范围以实现更广泛的影响。