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

Title of the Paper

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

Paper Information

• Field of Study: Human-Computer Interaction, focusing on optimizing academic scheduling processes through automation technologies
• Keywords: Constraint solving, decision making, student scheduling, human-computer interaction design, Boolean satisfiability, cognitive load, SAT solvers

Research Background and Problem Statement

• Identified Problems:

  1. Creating academic schedules manually requires handling numerous complex and conflicting constraints, which can lead to cognitive overload.
  2. Cognitive load negatively impacts decision quality, such as missing course information or scheduling conflicts.

• Importance of the Problem:
  Academic schedule creation is not only a common task but also directly affects students' time management, quality of life, and academic progress. Reducing cognitive burden and improving decision-making quality are crucial for enhancing student experience and time management.

• Research Motivation and Related Work:

  1. Traditional manual methods are considered cumbersome, necessitating an automated solution to alleviate cognitive load.
  2. SAT solvers have proven effective in solving constraint satisfaction problems, but their application in personalized scheduling remains underexplored.
  3. Existing tools primarily emphasize scheduling speed without adequately addressing user experience and human-computer collaboration.

Proposed Solution

• Proposed Method:
  Design a semi-automated academic scheduling system based on Boolean satisfiability solvers (SAT Solver), which assists individuals in creating schedules and supports collaborative scheduling among small groups.

• Innovative Features:

  1. Introducing SAT solvers to address specific academic scheduling problems, meeting individual customization needs.
  2. The system supports collaborative work, allowing users to dynamically adjust schedules based on personal and group preferences.
  3. Balancing automation with user control to optimize interaction experience.

• Implementation Steps and Key Technologies:

  1. Develop eight modules, including course viewing, schedule management, preference settings, schedule comparison, collaborative schedule generation, etc.
  2. Use SAT Solver for constraint encoding and decoding in the "Schedule Management" module, automatically handling cross-course conflicts.
  3. Provide a visual interface for users to manually confirm and modify automatically generated schedules, with color and formatting to distinguish course priorities.
  4. Introduce a "Friend Collaboration" feature to enable group members to share and synchronize schedules.

Research Outcomes

• Specific Results:

  1. Experiments show that the system significantly reduces users' cognitive load and stress.
  2. Students using the system completed schedule design faster and reported higher satisfaction with their final decisions.
  3. Reduced manual scheduling errors, such as time conflicts or missed courses.

• Advantages Comparison:
  Compared to traditional methods:

  1. Alleviated cognitive burden caused by manual data handling.
  2. Improved decision quality and scheduling efficiency.
  3. Supported collaborative scheduling, enhancing coordination within groups.

• Experimental Results:

  1. The experimental group's NASA-TLX cognitive load score was significantly lower (17.04 vs. 26.52, p < 0.001).
  2. Exceptionally efficient task completion time: the experimental group averaged 40.35 minutes, while the control group averaged 51.77 minutes.
  3. Higher user satisfaction in the experimental group, with users noting that schedule visualization and automated decision-making improved usability.

• Limitations and Future Directions:

  1. The system is suitable for small group collaboration (2-4 people); future studies could test its effectiveness in larger groups.
  2. The system's automation efficiency decreases with an increasing number of preferences; future research could compare other optimization algorithms like genetic algorithms or tabu search.
  3. Explore applying SAT solvers to other non-academic collaborative scheduling scenarios, such as employee shift planning or meeting coordination.
  4. Enhance system transparency by providing users with background feedback on automated decisions to reduce doubts about algorithmic outcomes.

Conclusion

This study investigates the effectiveness of a SAT Solver-based academic scheduling system in optimizing decision-making and reducing cognitive load. Through detailed analysis of user experience and cognitive burden, the paper offers valuable design recommendations, including balancing automation with manual control and improving result interpretation mechanisms. The findings provide significant insights for practical applications. Future research could further refine technical optimization and expand the system's application scope to achieve broader impacts.