Optimize course schedules by leveraging our SAT solver's logical model
CISC-204 Modelling Project
The aim of this project is to create a logical model that allows a student to input a tentative course schedule and assess its feasibility. The model will consider various factors, including course prerequisites, and time conflicts. By applying principles of natural deduction, the model will attempt to evaluate a feasible solution satisfying all constraints and ensuring all necessary requirements are met.
- Student-Course Matching
- Conflict Resolution
- Prerequisite, Corequisite Tracking
- Course Exclusion
- Friendship Considerations
- Flexible Term Enrollment
- Time Conflict Avoidance
- Maximized Course Enrollment
Folders
documents
Contains both draft and final submissions.data
Contains both test and main data sets from qmulus.nextjs_app
Contains a Nextjs web app to view and interact with generated timetable solutions.
Files
run.py
General wrapper script to execute the sat solver.sat_solver.py
The Python SAT solver constraint and proposition models, as well as compile and solve functions.datalayer.py
Defines classes for representing Queens courses, departments, requirements, and sections, as well as collections of these elements.timetable.py
Defines timetable classes and JSON Serialization functions.webapp_api.py
Defines a Flask API for parsing requested SAT solver test cases.utils.py
Contains utility classes and functions for the timetable scheduling SAT solver.test.py
Submission requirements and theory size checks.
By far the most reliable way to get this project running is with Docker. This section runs through the steps.
- First, download Docker https://www.docker.com/get-started
- Navigate to your project folder on the command line.
- We have created a bash script
model.sh
to help you build and run the project given your desired preferences. (Web App and Console modes)
- This script is just a simple wrapper that executes commands in your docker containers to prevent blocking or terminal tie ups.
- This section outlines the steps without using
model.sh
.
-
Our script requires jq, a json processor. It can be installed by running
sudo apt install jq
in your console.If you would like to run the Python SAT Solver and use the Nextjs Web App for interaction with the Solver:
From the project folder run to following commands. a. Ensure the model.sh has execute permission.
chmod +x model.sh
b. Build both the Sat Solver and the Web App containers.
./model.sh --build
c. Start both the Sat Solver and the Web App
./model.sh --start
d. The Web App can be accessed at http://localhost:3000/ e. To stop both the Web App and the Sat Solver, you can
Ctrl+C
in the terminal to interrupt and shut down both containers. Running the following command is also an option if your terminal is not tied up../model.sh --shutdown
f. From the shutdown state both the Sat Solver and the Web APP containers can be restarted with
./model.sh --start
followed by./model.sh --run
to run both programs.If you would like to run the Python SAT Solver and use the Console for interaction:
From the project folder run to following commands.
a. Build the Sat Solver container*
./model.sh --build --console
b. Starts the Sat Solver
./model.sh --start --console
c. The Sat Solver can then be used through the terminal. d. To stop the Sat Solver, you can
Ctrl+C
in the terminal to interrupt and shut down the container. Running the following is also an option if your terminal is not tied up../model.sh --shutdown
e. From the shutdown state the Sat Solver container can be restarted with
./model.sh --start --console
followed by./model.sh --run --console
to run the program.Alternative Using Docker Compose
More complicated
-
Running
docker-compose up -d
will build the Python SAT Solver imagesat_solver_204
as well as the Nextjs Web Appweb_app_204
image as well as create and start both containers.Note that the -d option is important as it runs the command in the background to avoid tying up the terminal, preventing further commands from being run.
-
From there the two containers should be connected. Both containers share a local network
webapp_network
for HTTP communications. The SAT Solver container project directory is also linked to the local project folder so that everything you do in one automatically updates in the other. -
IMPORTANT You must ensure your desired preferences exist in the
config.json
file if using this method, otherwise the app may run in console mode as a background process, or vise versa. -
Web App Mode
- To start the Nextjs Web App you must run
docker exec -d $(docker-compose ps -q web_app_204) npm start
-
This executes npm start
in the web_app_204 container as a background process
- To start the Python Sat Solver you must run
docker exec -d $(docker-compose ps -q sat_solver_204) python3 run.py
This executes python3 run.py
in the sat_colver_204 container
- The Web App can be accessed at http://localhost:3000/
- To stop both the Web App and the Sat Solver, you must shutdown the containers using the Docker Desktop GUI or by running:
docker-compose stop $(docker-compose ps -q web_app_204)
stops the Web App
sh docker-compose stop $(docker-compose ps -q sat_solver_204)
stops the SAT Solver
-
Console Mode
- To start the Python Sat Solver you must run
docker exec -it $(docker-compose ps -q sat_solver_204) python3 run.py
This executes
python3 run.py)
in the sat_colver_204 container- To stop the Sat Solver, you can enter
e
as input, to shutdown the containers you can use the Docker Desktop GUI or run:
docker-compose stop $(docker-compose ps -q sat_solver_204)
stops the SAT Solver
Please read the configuration overview
Web App Mode
After running the project in the Web App Mode and visiting the home page http://localhost:3000/ you will be greeted with a blank page with no student data, as no tests have been ran.
Selecting the drop-down reveals pre-configured test cases, that can be selected and ran in the Sat Solver using the “Generate New Data button”.
After generating the solution the page will refresh and a table containing students and there enrolled terms will appear. A students term schedule can then be viewed using the “view” button located in the table.
A specific students time table may resemble the following
Console Mode
After running the project in Console Mode the following message will be displayed in the console
This prompt accepts user input for a test case id. After entering a case the solution is directed to the console.
The Console Mode remains in a while loop repeatedly asking for user input until the e
key is entered closing the program.
Please read the creating custom test cases overview
To remove all docker containers, volumes, and networks used by this project you can run
./model.sh —uninstall
if you wish to use our script OR
docker-compose down --volumes --rmi all