What an unsat core tells a dispatcher

Vera 1.1 ships this week. The headline feature sounds small: better explanations. It was the hardest thing I've built this year.

When Z3 rejects a candidate plan, it can produce an unsat core — a minimal subset of the constraints that is already contradictory. Minimal is the magic word: remove any one element and the contradiction disappears. It is, mathematically, the exact reason the plan fails.

The problem is that a raw unsat core looks like this: a set of internal assertion labels referencing rule R2 and two fact atoms about technician T-103. Correct, minimal, and useless to a human under time pressure.

The obvious fix — and the wrong one — is to hand the core to the language model and ask for a friendly explanation. Tempting, fluent, and it reintroduces precisely the failure mode the architecture exists to prevent: the model might embellish. It might mention a plausible-sounding reason that isn't in the core. Then your compliance-grade explanation is fan fiction with a proof attached.

What 1.1 does instead is mechanical translation. Every rule already has its operator-confirmed plain-English source text. Every fact atom maps to a named entity and attribute. The explanation is assembled from those pieces with a template grammar — "R2 requires a certified technician for gas-boiler work; T-103 holds no gas certification." Every clause in the sentence is traceable to an element of the core. Nothing in the sentence is not in the core.

The model is allowed to smooth grammar. It is not allowed to add content, and the validator checks that: an explanation that references a rule or fact outside the core fails closed and ships as the raw structured form instead.

Dispatchers tell us the rejected options are now more useful than the accepted ones. "Plan C would work except for stop 3's window" is an instruction — call the customer, widen the window, unlock the better plan. A proof of impossibility, it turns out, is also a to-do list.