Constraint solvers and unsat cores, explained

The kind of question a solver answers

A constraint solver answers questions of the form: given these facts and these rules, does a valid assignment exist? Assign technicians to jobs such that every certification requirement, every SLA window and every working-time limit is respected. The solver's answer is one of two words:

• SAT (satisfiable) — yes, and here is an assignment that works.
• UNSAT (unsatisfiable) — no, and it is provably impossible, not merely hard to find.

Modern SMT solvers — Z3, developed at Microsoft Research, is the best known — answer these questions over rich domains: numbers, time intervals, sets, logical combinations of all of them. They are the workhorses behind chip verification and program analysis, fields where "probably correct" is not a category that exists.

Why a solver's answer is different in kind from an LLM's

A language model asked "can technician T-103 take this job?" produces the most plausible continuation of the conversation. A solver produces a theorem. The difference shows up in three properties:

1. Determinism. Same facts, same rules, same answer. Every time, on any machine.
2. Exhaustiveness. The solver checks the plan against every active rule, not the ones that happened to be salient in a context window.
3. Provability. UNSAT means a proof of impossibility exists — not "I couldn't find one."

The unsat core

The most operationally useful object a solver produces is the unsat core: when a plan is impossible, the solver can extract a minimal subset of the constraints that is already contradictory. Minimal means: remove any single element and the contradiction disappears.

This is precisely the answer to the question a dispatcher actually asks, which is never "is this plan valid?" but "why not, and what would I have to change?" If the core says {rule R4 driver-hours, stop 3's delivery window}, you know that relaxing either one — splitting the route, or calling the customer at stop 3 — unlocks the plan. The proof of impossibility doubles as a repair manual.

The catch — and how it's handled

Solvers only consume formal constraints. Nobody dispatches trucks in first-order logic, which is why solvers stayed locked inside engineering tools for decades. The modern move — the one systems like Vera are built on — is to use a language model as the translator from human rules to formal constraints, with schema validation and human confirmation in between, and let the solver do all of the deciding. Each component does the one thing it is provably good at.