This program is a python program that is based on Time Table Scheduling to SAT reduction approach.
We first encode the problem in Propositional Logic and use 'z3 SAT Solver' to find if there can be a time table.
If there can be a time table the program will make an Excel Sheet and print it.
This program requires the following libraries
- z3 SAT Solver for Python
- XlsxWriter for python
pip install XlsxWriter
- copy
- json
- Make sure you have all the required libraries.
- Make sure you have the input JSON file in the correct format.
- Run the main.py file to check if there can exist a time table or not.
python main.py
- If there can exist a time table the program will create an Excel Worksheet with name TimeTable.xlsx and print the time table in that file.
Should have
- "Room Types" specifying all the sizes. e.g. ["small", "big"]
- "Classrooms" specifying all classes with sizes. e.g. [ ["T1", "small"], ["LH1", "big"] ]
- "Courses" list
"Courses" must specify:
- Course Name. e.g. "cs201"
- List of classroom sizes possible for that course. e.g. ["small", "big"]
- List of lectures time required for that course. e.g. [1.5, 1.5]
- List of Professors teaching that course. e.g. ["Amal", "Clint"]
- List of batches attending that course. e.g. ["cs btech 18"]
- If some course requires classroom size of small, big size classroom can also be used for that course if small size classroom is unavailable. Hence put ["small", "big"] instead of "small".
- If multiple batches are going to attend a course, put them in a list. e.g. ["cs btech 16", "ee btech 16", "me btech 16"]
We created this Time Table Scheduling Program as part of a programming assignment of CS 228: Logic in Computer Science taught at IIT Goa.
- Raj S. Jagtap
- Neeraj Khatri
- Ujjawal Tiwari
Any suggestions in improving are appreciated.