DEV Community

Arthur031221
Arthur031221

Posted on

A seating planner that names the rules that clash, with a SAT solver in TypeScript

When a teacher's seating requests can't all hold, most planners say "no solution". That's true and useless. I wanted a tool that names the few requests that clash, so I wrote SeatReason, a static web app that runs entirely in the browser.

A conflict in the example class, a repaired plan with changed seats outlined, then a hand-made move that breaks a fixed seat and is undone

The three requests

The room is a grid with optional blocked seats, up to 40 pupils and 48 seats. A request is one of three kinds: a fixed seat, a place in the first N rows, or two pupils who must not sit next to each other. That is deliberately small, so every request can be explained in one sentence.

How the clash is found

Fixed seats and front rows are a matching problem, so a Hall violator gives the clash quickly. Everything else goes to a CDCL SAT solver I wrote in TypeScript. Each request has a selector literal that guards its clauses. If the formula is unsatisfiable under all selectors, the failed assumptions are a conflict. A deletion pass then tries to drop each request from the set and keeps it only if the rest become satisfiable.

The result is a subset-minimal set: take away any one request and the others can hold. The page only says "minimal" after that pass finished. If the solver runs out of its budget, the answer is "inconclusive", never "impossible".

Repairs you can check

Under each request in the clash there is a preview. It plans again with that request off, keeping the current seats where it can, and checks every remaining request together. Changed seats are outlined. The plan is replaced only when you press the button, and Undo brings it back.

A separate checker that doesn't share the solver's encoding validates every plan. In the tests the solver is compared with an exhaustive search on small rooms.

Measurements

On an AMD Ryzen 5 7500F with Node 24.21, five runs of the bench gave a median of 18 to 32 ms to find a minimal clash that needs the SAT solver, with the slowest case at 0.38 s. Repair previews for those cases took a median of 0.26 to 0.49 s. The machine was busy during those runs, so the numbers moved.

Limits

Nine pupils who must all be kept apart in a 4 by 4 room run past the 8 second limit, and the page says so. Keep apart means orthogonal neighbours only. There is no gender balance, group seating or rotation.

The app has nine interface languages, a JSON backup and a printable chart. Try it at https://arthur031221.github.io/SeatReason/ or read the code at https://github.com/Arthur031221/SeatReason.

Top comments (0)