Kemisolv #
A fast, high-performance exam scheduling system backed by Z3, with a SvelteKit frontend. Designed for small-medium sized schools.
Kemisolv generates a clash-free, optimised exam timetable in minutes. Compared to potentially days of manual scheduling, it's a game-changer for school administrators. Instead of timetabling by hand, potentially double-booking students, introducing conflicts, annoying teachers with weird unoptimised timetables, Kemisolv ensures a smooth, conflict-free exam timetable, taking into account student subject choices, teacher preferences, custom constraints, and availability.
Why Kemisolv? #
There is almost no other software that does what Kemisolv does. Most existing scheduling software is for daily scheduling, not exam timetabling. They also use heuristic-based algorithms, which can be slow and unreliable. The only real other solution is UniTime. It's genuinely awesome software, but it's:
- Old
- Started in 2001, making it over 20 years old
- Its age shows
- While that makes it mature, it also makes it hard to use for schools. Kemisolv is a focused tool built specifically for schools.
- Bloated
- Designed for universities, not schools
- Exam scheduling is just 1 part of it. It's not designed around it.
- Slow (runs on Java and needs multiple services running just to use)
- A hassle to set up
- Requires server administration experience
Kemisolv on the other hand is:
- Free for personal use and evaluation.
- A single executable. No other software installation required.
- Extremely fast, written in rust.
- Generates the optimal timetable, using a Z3-powered SAT solver
- Easy to use, with a simple interface that guides you through the process
Features #
- Intuitive, calendar-based timetable view
- Subject, Grade, and Exam management
- Set special requirements per-exam, such as specific availability and such
- Student management
- Import existing student data and map it into the system
- Set subjects they're taking for automatic clash detection and resolution
- This ensures no clashes are generated for the timetable
- A better-than-AI, mathematically optimal timetable generator
- Z3-powered SAT solver
- Mathematically sound
- Generates the optimal timetable, taking into account all constraints and preferences
- Diagnose why a timetable can't be built with specific errors and explanation
- Generate multiple timetables
- Streams in solutions as they're found
- Edit timetables after they're generated
- Intuitive, drag-and-drop interface
- Allows you to move exams around and see how they affect the timetable
- "Lock" specific slots and prevent them from being moved
- Regenerate a new optimal timetable, with these locks taken into account
- Save past timetable drafts to compare them
- Export timetables to PDF
- With embedded metadata, to use on the website to allow students and teachers to download and print their timetables
Commercial Use #
Kemisolv is free and open source for evaluation. Feel free to look at the code, and use it for your own projects.
However, for schools and actual organisations, the commercial option has:
- Whitelabeling, so your schools branding is on the timetables and software
- A simple hosted deployment option, so your servers can run it rather than a teachers laptop
- This ensures that, even if the teacher leaves, the timetable can still be generated
- And improves performance by running the solver on a dedicated server
- With no subscription lock-in. One-time license fee for the current version with a yearly maintenance subscription. Stop paying, you can still use the software.
You may also pay contract for any additional features your school requires, such as:
- Invigilation Timetables, so who invigilates when is solved automatically and fairly
- A Staff portal for collaboration
- Role-based access control
- Collaboration tools for staff
- A parent and student portal for viewing timetables and submitting feedback
- This feedback will be used to improve future timetables automatically
Please contact licensing@kemisolv.wobbl.co.za for more information and to book a real-time demo of how it works. Or try it for free on your real data. A website will be available soon!
Why the Name? #
Kemisolv is split up into two parts:
- Kemiso: It's Sesotho for scheduling
- Solve: It's a solver
Kemiso + solve = kemisolv
For a pronunciation guide:
- IPA: /kɛ.mi.sɔlv/
- Phonetic: ke-mee-sol-v
For Developers #
Feel free to contribute to the project or fork it! As long as it's not for commercial use, you're welcome to use it however you like.
If you want to contribute, note that this code will be used for my commercial version as well. I'll create a CLA specifically for contributors. I'll use contributions in the commercial version, but you retain ownership, credit, and I'll never take the repo down for commercial reasons. Your contributions will be put in the commercial version's credits page.
Architecture #
crates/solver: Z3-backed schedulercrates/backend: Data prep and solver wiringpackages/frontend: SvelteKit frontend for the main Tauri appcrates/app: Actual Tauri app and interfacepackages/website: SvelteKit client-side app for the website
How the Solver Works #
One part of the technical side I really want to yap about :p
The solver works on a very basic but extremely powerful numeric map:
- exam sessions are variables
- time slots are numbers
E.g. session_1 might be scheduled at 3 (i.e. the 3rd time slot).
The solver holds an internal map, which maps back from those variables to database-level session/time slot IDs,
and saves that mapping so the solver can translate back to a form to pass back to the client.
For an example of a constraint, here's how the solver translates a student into a Z3 constraint:
- Selects all subjects a student has
- Selects all exam sessions those subjects have
- Maps those session_ids into Z3 variables
- Adds a
distinctconstraint to ensure no two sessions are scheduled at the same time slot- Same number, same time slot. Distinct numbers, you get the idea.
For human-readable diagnoses, I actually wrap the Z3 solver in a custom diagnostic layer that translates back to human-readable session/time slot names. A constraint can take in a variable that gets filled with a number if it's constraint can't be met, so I simply check those values and map them to an error variant. These can either be programmatically handled or (as currently done) displayed to the user. Check the constraint_tracking.rs and diagnostics.rs files for more details.
All code lives inside of the solver crate. Check it out for more details! It's pretty well documented.
Contributing #
Please see the CONTRIBUTING.md file for more details.
AI Usage #
This project is not vibe-coded. Agents were used to do stuff I did not want to/did not have time to do myself or not absolutely critical to functionality. I don't like making error messages. All code with AI comments will eventually be reviewed. The CONTRIBUTING.md file contains more details on AI usage.