Large language models are famously bad at following strict logical rules — they hallucinate, they drift, they forget constraints halfway through. Amazon thinks it has a fix: make the LLM work alongside a formal math solver instead of going it alone. Amazon's patent US 2026/0127386 A1 (published May 7, 2026) describes a hybrid architecture called an LLM-enhanced SMT solver — pairing a language model with a SAT/SMT solver so the LLM never has to enforce logical consistency on its own. The problem Ask an AI assistant to plan a lunch menu with three rules — no red meat, the entrée and side balanced, heavy entrée means light side — and a regular chatbot will happily give you a confident answer that violates one of those rules without noticing. This is well-known: LLMs are bad at constraint satisfaction. They drift. They forget rules halfway through a complex query. For most consumer use cases, that's annoying. For enterprise AI agents handling procurement, compliance, or scheduling, it's a non-starter.…