SAT-Based Class Scheduling Solver

A Java implementation of a constraint-based class scheduling solver using the Sat4J SAT solver.

The project was originally developed as part of a university logic course and demonstrates how a real-world allocation problem can be translated into a logical formula and solved using an external SAT solver.

Technologies used

• Java
• Sat4J SAT Solver
• Maven
• File parsing and output generation
• Boolean satisfiability modelling
• Constraint programming concepts

Problem description

The input describes:

• the number of courses;
• the number of teachers;
• the number of rooms;
• the number of timeslots;
• the teacher assigned to each course.

The goal is to assign every course to one room and one timeslot while ensuring that:

• a teacher is not assigned to teach two courses at the same time;
• two courses do not take place in the same room at the same time.

Example input

3 2 2 4
1 2 1

This means:

• 3 courses;
• 2 teachers;
• 2 rooms;
• 4 timeslots;
• course 1 is taught by teacher 1;
• course 2 is taught by teacher 2;
• course 3 is taught by teacher 1.

Example output

1 1 1 1
2 2 2 1
3 1 1 2

Each row represents:

course teacher room timeslot

How it works

The solver creates Boolean variables representing possible assignments of a course to a room and a timeslot. It then builds SAT clauses to represent the scheduling constraints.

For example:

• each course must be assigned to at least one room-timeslot combination;
• a course should not be scheduled multiple times;
• conflicting assignments are forbidden through negative clauses;
• Sat4J determines whether the resulting formula is satisfiable.

If the formula is satisfiable, the model returned by the solver is decoded and written to an output file.

Running the project

Build the project with Maven:

mvn package

Run the solver:

mvn exec:java -Dexec.mainClass="Main" -Dexec.args="data.in data.out"

Where:

• data.in is the input file;
• data.out is the generated schedule.

What I learned

Through this project, I practiced:

• modelling a real-world allocation problem using formal logic;
• translating constraints into SAT clauses;
• using an external Java solver library;
• working with Maven-based Java projects;
• reading structured input files and generating solution files;
• thinking about correctness, satisfiability, and constraint design.

Author

Created by @Bortrex