ADR 0013: Multi-Engine Solver Layer

Status: Accepted for architectural direction.

Date: 2026-05-11.

Context

UWScrape must answer several different kinds of academic planning questions.

Some questions are fixed-state requirement evaluations.

Some questions are graph-like closure queries over prerequisites, reverse unlocks, and credential mentions.

Some questions are Boolean feasibility questions over finite alternatives.

Some questions involve grades, averages, units, and numeric thresholds.

Some questions involve bounded future-term planning.

Some questions require conflict explanation.

The existing mathematical model already treats the course universe as a typed finite constraint system projected into graphs for visualization.

The backend architecture already separates static index artifacts from runtime state.

The solver architecture now needs to decide whether one engine should own all academic reasoning.

Decision

Use a multi-engine solver layer behind a shared academic contract.

The solver layer will normalize:

published index + student state + query request
  -> normalized evaluation problem
  -> engine routing
  -> engine result
  -> academic result with explanation, unknowns, conflicts, and source references

The stable contract is academic_result.

The stable implementation boundary is engine_adapter.

The engine roles are:

direct evaluator for version 1 unlock, progress, and unknown propagation;
Datalog for reachability, closure, and derived relations;
SAT for Boolean alternatives, cardinality, coexistence, and conflicts;
SMT for grades, averages, units, and numeric thresholds;
CP for bounded term planning and schedule-like constraints;
package-resolver style search for alternative paths and conflict explanation.

No concrete solver library is mandatory in this ADR.

SMT-LIB, Z3, Souffle, PySAT, OR-Tools CP-SAT, MiniZinc, and PubGrub are cited as theory and implementation context, not as required dependencies.

See:

Consequences

The backend can route each query to the engine style that fits the query.

The frontend receives stable academic statuses rather than engine-specific outputs.

The project can start with a deterministic direct evaluator and add engines later.

Each engine must declare supported fragments.

Each engine must preserve source references.

Each engine must report completeness separately from academic status.

The result normalizer becomes critical infrastructure.

Testing must include adapter fixtures and cross-route status mapping.

Alternatives Considered

Alternative 1: One Universal Solver

The project could encode every query into one SMT, CP, or custom solver.

This would create one integration path.

However, it would make simple fixed-state queries harder to audit.

It would make relation closure and explanation depend on a general engine even when a specialized derivation is clearer.

It would also increase the risk that engine-native UNKNOWN or timeout leaks into academic semantics.

This alternative is rejected.

Alternative 2: Direct Evaluator Only

The project could implement only a direct evaluator.

This is enough for many version 1 evaluation queries.

It is not enough for bounded future planning, alternative-path search, rich closure queries, or numeric feasibility under hypothetical grades.

This alternative is rejected as a long-term architecture, but accepted as the first runtime slice in ADR 0014.

Alternative 3: Frontend-Owned Solving

The frontend could run most solver logic locally.

This may help visual responsiveness.

However, it would duplicate academic semantics, make source-reference guarantees weaker, and complicate state migration.

The frontend may compute visual highlighting.

The backend owns academic answers.

This alternative is rejected.

Follow-Up

Define exact Go interfaces for engine_adapter.

Define fixture formats for each engine fragment.

Define endpoint-specific query schemas after the solver contract stabilizes.