Keystone

A decision engine that pairs an LLM with a constraint solver

Keystone is a certified decision engine for operational planning: staff scheduling, assignment, allocation, selection and matching. A team describes the decision as data tables, plain-English rules and an objective, such as "minimize labor cost, then honor shift preferences." Keystone returns a plan with a certificate proving that it satisfies every hard rule and is optimal. If no valid plan exists, it returns proof of that instead.

We built it in two days for Track 3 of the AMD Developer Hackathon: ACT II. The hero domain is nurse shift scheduling, where a wrong answer is expensive and a merely plausible one is dangerous. The project is MIT-licensed and public on GitHub.

Why an LLM alone can't schedule staff

The bundled sample problem covers one week for 8 nurses across 10 shifts, which comes to 80 decision variables and 97 constraints, 95 of them hard. A raw-LLM plan for it costs 2,816. That's cheaper than Keystone's 2,936, but only because it breaks three skill-match rules. Keystone's plan is proven optimal, and all 95 hard constraints are re-checked independently.

That comparison is built into every run. The baseline plan goes through the same verifier as Keystone's, so its violations are shown, not just asserted.

Key features

Propose, decide, certify — the LLM only drafts the model. CP-SAT makes the decision, and a verifier that never trusts the solver's own report certifies it.
Proven infeasibility — when no plan can exist, Keystone returns the minimal set of conflicting rules. For example, if two ICU nurses are demanded on Monday morning and only one qualified nurse is on staff, it names exactly that coverage and skill pair.
Validate-and-repair loop — if the LLM proposes a malformed model, the model is checked and sent back with the errors for a configurable number of retries.
Natural-language re-solve — a request like "add a second nurse to Friday PM" changes the problem and re-runs the full pipeline. It returns a fresh certificate plus a diff against the previous plan.
Scope gate — open-ended questions that aren't optimization problems are declined with a suggestion for reframing them, instead of being forced into a fake model.
Decision pack — each run exports one self-contained JSON file with the problem, model, plan, certificate, baseline comparison and explanation, for whoever signs off.
Operator console — a single-file web UI streams the pipeline live and renders the roster, the certificate and the raw-LLM comparison.

Architecture and tech stack

Pipeline

A FastAPI service accepts a problem as JSON or as a CSV upload. An async worker runs it through six stages: received, modeling, solving, verifying, baseline and explaining. Progress streams over Server-Sent Events. Jobs and plans live in SQLite, which one environment variable can swap for Postgres.

Model, solver and verifier

The intermediate model uses linear integer constraints over bounded variables. That means it maps directly onto the CP-SAT constraint solver and can be re-checked with exact integers, with no floating-point tolerances. Soft preferences become weighted penalties.

The main solve uses multiple workers and a fixed seed, so certified results are reproducible. Conflict sets come from CP-SAT assumption cores. The solver is never mocked: the offline mock mode stubs only the LLM, so the guarantee still holds with zero API keys.

LLM routes and AMD compute

Gemma proposes the model through one OpenAI-compatible code path with three routes: Google AI Studio, Fireworks AI, or Gemma served by vLLM on an AMD Instinct MI300X.

The core feasibility check is also implemented in PyTorch as a batched float32 matrix multiply that runs on ROCm. Tests assert that it matches the CPU verifier bit for bit, and it drives a GPU-screened large-neighborhood search for very large rosters. A notebook scales the same solve-then-certify path to a roster with 10,080 variables and 31,179 hard constraints.

Quality

The repository ships 52 passing tests covering the model, solver, verifier, GPU evaluator, multi-domain builders, pipeline and REST API. They include regression tests from an adversarial review, which caught a variable-name collision that could have certified an understaffed schedule. Slim and ROCm Dockerfiles are included.

What we delivered

During the hackathon we shipped:

the full backend
four problem shapes that solve offline: assignment, allocation, selection and matching
the web console
a narrated demo video
a live demo that runs in mock mode with the real solver and verifier

The disclaimer ships with the product. A certificate proves that a plan satisfies the modeled constraints, not that the model captures every labor rule, so every plan is meant to be reviewed by a person.

Keystone is part of our AI integration and automation work. Other builds from the same hackathon are RecipeReel, Legible and Testify. For another system where the AI works inside strict verification steps, see Opus Magnum.