What are SMT, OR-Tools, and CVC5 — and why do they belong next to an LLM?

Ask a language model whether a staffing schedule is optimal, or whether a policy can ever let the wrong role approve a payment, and it will give you a plausible answer with no way to check it. These are not language problems — they are search problems over a large but finite space, and there is a class of tools built to search that space exhaustively rather than plausibly. We use three of them, for different reasons.

SMT (satisfiability modulo theories) solvers answer one precise question: *does any assignment of values exist that violates this constraint?* Encode an organizational invariant — no non-finance role can approve a high-value expense, say — as a formula, ask the solver to satisfy its negation, and either it finds a concrete counterexample or it exhausts the search and reports none exists. Our fifth paper calls this *searched, not verified*, and insists on the distinction: an SMT result is a claim about an encoded model, checked by an unproven solver, which is real evidence and is not the same thing as a machine-checked proof. The discipline that matters most is refusing to let a timeout be recorded as if it were a clean "no violation found."

OR-Tools is Google's open-source optimization suite, and the piece we use most is CP-SAT — widely regarded as the strongest constraint-programming solver available, and the tool of choice for problems that mix logic and arithmetic: scheduling with optional intervals, job-shop sequencing, routing. Where an SMT solver asks *can this go wrong*, CP-SAT and its sibling HiGHS ask *what is the best possible answer, and can you prove it*. Our third paper reports what that buys concretely: a proven-optimal schedule that seats sixty of sixty tasks against a greedy heuristic's fifty-six, and a job-shop plan with a 48.8% shorter makespan than dispatching by hand — differences that are not academic once you multiply them across a real fleet or a real quarter.

CVC5 is the SMT solver we wrap. It is one of several strong open-source engines — not the permanent choice, but the first — and naming it specifically rather than hiding it behind an abstraction is part of the same discipline as everything else in this program: a claim of certainty should say exactly which piece of mathematics produced it.

None of these tools understands what a customer wants, or what a staffing request means in plain language. A language model does that translation well. What none of them can do alone is what all of them can do together: read the request, formulate the problem, and hand it to something that can either prove the answer or tell you precisely why it cannot.