ScheduleProof

Upload exams, rooms, enrollment, and human requirements; ScheduleProof produces an optimized conflict-free timetable in seconds, explains why no valid timetable exists, and suggests a repair.

Comment

Inspiration

I am a professor at Florida State University (https://www.cs.fsu.edu/~grigory/). Scheduling is my everyday pain and not an abstract optimization problem. At the university level, it is the kind of problem that appears every semester and quickly becomes difficult once real constraints are added: room capacities, instructor availability, student conflicts, accessibility needs, preferred dates, and last-minute changes.

What interested me most was not only generating a timetable, but making the result balanced, trustworthy, and also achieving it fast. A scheduling system should be able to explain why a schedule works, why a conflict has no solution, and what would need to change to make it solvable.

That led to ScheduleProof: a scheduling application that combines natural-language input with formal constraint solving and independent validation.

What it does

ScheduleProof accepts structured institutional data such as exams, rooms, capacities, time periods, instructor availability, and conflict information.

A user can also enter additional requirements in ordinary language, for example:

  • “Professor Ibrahim can only supervise on Friday.”
  • “Calculus I must be Monday morning.”
  • “Move Probability to Tuesday while changing as little as possible.”

A language model translates the sentence into one of the application’s supported formal rule types. The user can review the interpretation before activating it. The language model does not create the timetable itself.

The confirmed rules are translated into logical formulas and sent to Z3 (https://github.com/z3prover/z3), an automated theorem prover (solver). If the constraints are satisfiable, the solver returns a model from which the timetable is extracted. A separate Python validator then checks the completed schedule independently.

When the requirements are inconsistent, ScheduleProof does more than display an error. It identifies a small conflicting set and searches for low-cost relaxations. This allows the user to see which rules are causing the problem and review a possible repair before applying it.

The repair objective also tries to preserve the existing timetable, so a local change does not unnecessarily move unrelated exams.

How I built it

I began by discussing a detailed specification with GPT 5.6 before implementing the application. This was important because the main risk was not calling Z3 incorrectly; it was expressing the scheduling problem incorrectly.

The backend is written in Python with FastAPI. The scheduling model uses Z3 for feasibility, optimization, unsatisfiable-core analysis, and repair generation. The frontend is built with React and TypeScript.

The architecture deliberately separates three responsibilities:

  1. The language model translates.
    GPT-5.6 maps natural-language requests into a typed rule catalog.

  2. Z3 schedules.
    The solver reasons over the formal constraints and optimization objectives.

  3. Python verifies.
    An independent validator checks the resulting timetable without relying on the solver’s internal model.

I also created minimal datasets for the individual table-to-formula translations and for every supported human rule. These examples are documented with LaTeX formulas and can be executed through the application. This made it possible to compare the intended mathematical rule, the generated solver expression, and the observable result.

The project also includes automated backend tests, browser-level Selenium workflows, import fixtures, solver benchmarks, privacy controls, Docker configuration, and release-validation scripts.

I used GPT-5.6 during the early design and implementation stages, especially for turning rough ideas into a structured specification. I then used Codex extensively and exclusively while refining the codebase, writing tests, finding integration problems, and reviewing the repository from several perspectives. I kept separate workstreams for the formal backend, the runtime experience, and the final integration so that one part of the project could challenge the assumptions made in another.

Challenges I faced

The hardest part was establishing confidence in the encoding.

A solver can correctly prove that a formula is satisfiable or unsatisfiable, but that does not prove that the formula accurately represents the university’s policy. Small details matter. For example, “at least one slot between two exams” is not the same as an ordinal distance of one, and “on different days” is not always the same as requiring a full empty day between exams.

I spent a significant amount of time creating small examples that isolate one behavior at a time. This work was less visually impressive than the frontend, but it was the most important part of the project.

Another challenge was keeping solver state and interface state consistent. A timetable may exist while becoming stale after a new rule is added. A repair may be generated but not yet approved. A problem may be unsatisfiable, while most exams still have useful tentative assignments. These states required careful UI design so that the application did not hide the timetable or imply that a repair had already been applied.

Privacy was another major concern. University scheduling data may contain sensitive operational information even when it contains no student names. I added tenant-scoped project access, short-lived retention modes, deletion controls, pseudonymization support, privacy-safe logging, and an option to keep external language-model processing disabled. The displayed university identity is explicitly fictional unless the application is deployed behind a real institutional authentication proxy.

What I learned

I learned that formal methods become much more useful when they are presented as part of a complete workflow rather than as an isolated solver demonstration.

Users generally do not want to see a large Boolean formula. They want to know:

  • whether a timetable exists;
  • which requirement caused the conflict;
  • what would change under a repair;
  • whether the final result was independently checked.

I also learned that “minimal repair” needs to be explained carefully. A repair is minimal relative to the configured costs and priorities. It is not a universal definition of what is least inconvenient for a university. Those weights remain a policy decision.

The project also reinforced the value of adversarial review. Several important issues were found not while adding features, but while asking separate review sessions to break the workflow, challenge the solver semantics, inspect privacy assumptions, and follow the README exactly as a judge would.

Current limitations

The current prototype does not yet cover every real scheduling situation.

It assumes that an exam is assigned to one room rather than being split across several rooms. It does not create individualized schedules for students requiring extra time or separate accommodations. Detailed cross-campus travel, multiple simultaneous resource requirements, and uncertain future enrollment are also outside the current model.

Natural-language requirements must map to the supported formal rule catalog. The system should reject an unsupported or ambiguous policy rather than inventing an interpretation. There are many symmetries to be broken in the rules formulation.

Finally, SMT solving is effective for many practical instances, but the underlying problem remains computationally difficult. Very large or unusually dense combinations of constraints may require specialized encodings or additional decomposition techniques.

What is next

The next stage is to improve solver performance through more specialized encodings, especially for dense spacing and room-turnaround constraints.

I would also like to add split-room examinations, richer accommodation support, cross-campus travel models, and scenario-based scheduling for uncertain enrollment or room availability.

Beyond education, the same architecture could be applied to conference planning, workforce scheduling, laboratory allocation, healthcare rostering, and other domains where decisions need to be optimized, explained, and independently verified.

ScheduleProof began as an exam-timetabling project, but the broader idea is simple and powerful: use language models to help people express requirements, use formal solvers to reason about them, and use independent validation to keep the result trustworthy.

Built With

Share this project:

Updates