ADR 0018: Conservative Unknown and Engine Status Mapping
ADR 0018: Conservative Unknown and Engine Status Mapping
Status: Accepted for architectural direction.
Date: 2026-05-11.
Context
The project uses academic statuses:
satisfied;not_satisfied;partial;unknown;conflict;not_applicable.
External and internal engines use different native statuses.
SMT solvers may return unknown.
CP solvers may return statuses such as optimal, feasible, infeasible, or unknown; OR-Tools documents these as CP-SAT statuses: CpSolverStatus.
SAT solvers return satisfiable or unsatisfiable for a specific Boolean encoding.
Datalog engines derive or fail to derive finite relation facts.
Package-resolver style search may produce a conflict explanation, a candidate solution, or incomplete search.
Academic unknown also arises from source and state issues that are not engine statuses:
- unparsed requirements;
- missing grades;
- missing academic progress;
- missing program state;
- unsupported requirement condition;
- unresolved source conflict.
Conflating these categories would mislead users.
Decision
Keep academic unknown separate from engine-native UNKNOWN, timeout, incomplete search, and operational failure.
Use conservative mapping:
| Engine or source condition | Academic mapping |
|---|---|
| Complete direct evaluator true | satisfied |
| Complete direct evaluator false | not_satisfied or partial, depending on child evidence |
| Direct evaluator opaque relevant source | unknown or partial with unparsed_requirement |
| SAT satisfiable with complete encoding | candidate satisfaction evidence |
| SAT unsatisfiable with complete encoding | not_satisfied or bounded infeasible result |
| SAT unsatisfiable with incomplete encoding | unknown |
| SMT satisfiable with complete encoding | candidate numeric satisfaction evidence |
| SMT unsatisfiable with complete encoding | not_satisfied or bounded infeasible result |
| SMT unknown | unknown with engine_incomplete |
| CP feasible with validation | candidate plan evidence |
| CP infeasible with complete bounded encoding | bounded infeasible result |
| CP unknown or timeout | unknown with engine_incomplete or time_limit_reached |
| Datalog derived fact | relation evidence |
| Datalog missing derivation in complete closed-world relation | negative relation evidence for that relation only |
| Resolver conflict with valid derivation | conflict or blocked-path explanation |
| Resolver incomplete search | unknown or partial explanation |
| Operational adapter error | server error unless policy marks the route recoverable |
engine_unsat is not automatically academic not_satisfied.
engine_unknown is not automatically academic unknown without an unknown_reason.
Timeout is not academic evidence.
Incomplete search is not academic evidence.
A bounded infeasibility result must disclose its bounds.
Consequences
Users see honest uncertainty.
The frontend can distinguish missing academic data from engine limits.
The backend can add engines without weakening academic semantics.
Tests must cover status mapping directly.
The result normalizer must be deliberately conservative.
Some answers will be less decisive than a naive solver integration could make them.
That is acceptable because the tool is advisory and source-sensitive.
Alternatives Considered
Alternative 1: Map Any Solver Unknown to Academic Unknown Without Detail
This is simple.
It hides whether the uncertainty came from source text, missing student data, timeout, or solver incompleteness.
This alternative is rejected.
Alternative 2: Treat Solver Timeout as Not Satisfied
This would make the UI decisive.
It is mathematically unsound.
Timeout means the engine did not finish.
It does not mean the academic target is impossible.
This alternative is rejected.
Alternative 3: Treat SAT or SMT Unsatisfiable as Always Not Satisfied
Unsatisfiability applies to a specific encoding.
If the encoding omits relevant source fragments or assumptions, the negative academic conclusion is not justified.
This alternative is rejected.
Follow-Up
Define exact unknown_reason codes.
Define exact conflict_reason codes.
Add fixture tests for timeout, engine unknown, incomplete encoding, and opaque source text.