Inspiration
Drug labels carry timing rules: take on an empty stomach, every 4 hours, at least 2 hours before or 6 hours after antacids. A patient on five medications can have a dozen of these interacting, and pharmacists work them out by hand. The published scheduling methods I found place one dose at a time and give up when they get stuck. When they give up on a regimen that could have been scheduled, a patient may be told to change a prescription they did not need to change.
What it does
You enter the medications and the patient's day (meals and sleep). LINNET gives one of three answers:
- Tier 0: it fits the day as it is. You get a 24-hour schedule.
- Tier 1: it fits with a small change. You get ranked options, such as moving lunch 30 minutes or dropping one as-needed dose.
- Tier 2: the prescriptions cannot be scheduled at all, even under the loosest reading of every label. You get the smallest set of label sentences that clash, each linked to DailyMed.
A real tier 2 found in the labels: nimodipine every 4 hours, together with colestipol's "other drugs at least one hour before or four hours after". No 24-hour day fits both.
LINNET makes no drug recommendations. It shows that a conflict exists and which sentences cause it; what to change is the prescriber's decision.
How I built it
- Rules come from public FDA labels. A language model (Claude Haiku 5.5) proposes rules and cites sentence ids. Code then checks each one: the sentence exists, every number in the rule appears in that sentence, and the rule fits the schema. The quote is copied by code, never by the model.
- The scheduler is a Z3 encoding written in C++. It models one repeating 24-hour day in exact fractions, so 23:00 and 01:00 are 2 hours apart, not 22.
- Everything shown is re-checked. An independent verifier re-checks every schedule in exact arithmetic, and every conflict is shrunk until each remaining rule is needed.
- Patient data stays in memory. The model reads only public labels and never sees patient data. The solver never calls a model.
- Python, FastAPI and a single-page UI. Solo build.
Results
- On 500 random regimens, a greedy one-dose-at-a-time heuristic gave up on 33% of the regimens LINNET could schedule (64 of 194). On real NHANES daily routines it was 34% (67 of 199).
- An exhaustive 15-minute grid search never disagreed with the solver (274 regimens searched).
- Every conflict shown was minimal (78 of 78, and 93 of 93 on NHANES days).
- A full check takes 35 ms at the median.
- Of 362 NHANES adults taking a product the library covers, 41 (11%) cannot follow their labels on their recorded day. Most are levothyroxine users who ate breakfast less than 30 minutes after waking.
Challenges
- Midnight. A naive encoding treats doses at 23:00 and 01:00 as 22 hours apart. Every gap is measured around the clock, with regression tests for it.
- Solver state. Z3 keeps state across solves, and late in a long sweep one regimen went from 0.04 s to over 40 s. Each check now runs in a fresh process with a hard time limit, and a check that times out is reported as undetermined, never as an answer.
- Getting rules out of labels reliably. For the last twelve labels, each label was read four separate times and a rule entered the library only when three or four readings produced the same rule. Five of the twelve labels failed that test and were left out.
What I learned
Most of the effort went into the rules, not the solver. A model reading a label will state a rule backwards with full confidence: two of four readings inverted risedronate's "30 minutes after" rule. The deterministic checks and the agreement test mattered more than the choice of model.
Limits
- No pharmacist has reviewed the rules. The sign-off step is designed for a person; in this submission it was done by Claude (an AI) and every decision is recorded that way.
- The library is small: 17 products.
- The output is a draft for a pharmacist to check, not an instruction to a patient. Not for clinical use.
