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

Manual schedule creation often involves satisfying numerous unique and conflicting constraints, which becomes more cognitively demanding when creating a common academic schedule with other individuals. Poor decision making caused by cognitive overload can result in unsuitable schedules. This study proposes the use of Boolean satisfiability (SAT) solvers in an academic scheduling system to help students balance scheduling preferences and satisfy necessary constraints. Based on the availability of courses and the scheduling preferences of users, the system automatically resolves conflicts and presents possible schedules. In a controlled experiment with 42 undergraduate students, cognitive demand was reduced by eliminating menial decisions, which significantly optimized the creation of a common schedule among peers. We found that human errors and emotional stress were diminished, and schedules created using the system were more satisfactory to participants. Finally, we present recommendations and design implications for future academic scheduling systems.