SMT Programming & Examples
How SatIR transforms free-text eligibility criteria into solver-executable SMT programs through incremental orchestration — and a worked model-checking example.
Why incremental? Direct one-shot translation from free-text to a full SMT program is brittle: variables get redeclared inconsistently, qualifiers are dropped or attached to the wrong concept, polarity is inverted, and the result may be syntactically valid but semantically wrong. By translating one requirement at a time, failures are localized, and the current symbolic state guides future decisions.
The incremental driver separates five distinct subproblems for each requirement:
Age, sex, pregnancy status — standardized template variables.
Grounded to SNOMED CT with qualifiers — the ontology-aware backbone.
Clinically meaningful content that can't be canonicalized — conservative, open-world.
Validation as feedback. After each fragment is generated, SatIR checks it with the SMT solver immediately. If it introduces a parse error, sort mismatch, or contradiction, the fragment is rolled back and retried with feedback. A separate semantic verifier catches subtler errors like polarity inversions and dropped qualifiers. The solver becomes an active feedback source during synthesis, not just a final execution engine.