Constraint Augmentation
Patient records are sometimes under-specified — a diagnosis documented at a coarser level than the trial requires. SatIR augments trial constraints with salience-based reasoning, expanding conditions along the ontology tree as OR clauses when the extra specificity is unlikely to have been recorded.
The salience assumption: any clinically salient fact about a patient will be documented in their medical record. SatIR uses targeted LLM queries to assess whether a specificity gap is meaningful — compiling explicit, auditable judgments rather than leaving them as opaque LLM decisions. Matching decisions remain transparent and open to expert review.
Medical records are sometimes under-specified: a patient may be documented with appendicitis when the more precise diagnosis is acute appendicitis. The ontology tree provides the parent–child edges that license candidate alternatives. For each trial condition, SatIR uses the LLM to assess the salience of the extra specificity relative to its parent in the ontology.
If the specificity is low-salience — meaning the finer distinction would not reliably be recorded separately — the trial condition is expanded in the formula to specific_condition OR parent_concept. This allows the patient's coarser record to satisfy the criterion. If the specificity is high-salience — as in Ruptured Suppurative Appendicitis, a distinction a clinician would always note — no OR branch is added, and the patient's coarser evidence does not satisfy the constraint.
Augmentation compiles into ORs. Rather than bending the matching logic at runtime, SatIR encodes salience decisions directly into the trial-side SMT formula as disjunctive clauses — so the solver handles them natively. When the extra specificity of a condition relative to its ontology parent is low-salience, the condition is expanded to condition OR parent_concept. The augmented formula remains a valid SMT formula, and the solver's guarantees are preserved.
specific_condition OR parent_concept — making the coarser evidence sufficient — or left as-is, requiring an exact match.