ADR 0015: Solver Result and Explanation Contract

Status: Accepted for architectural direction.

Date: 2026-05-11.

Context

Different solver engines expose different native concepts.

SAT solvers may expose satisfiable or unsatisfiable results.

SMT solvers may expose satisfiable, unsatisfiable, or unknown results.

CP solvers may expose optimal, feasible, infeasible, or unknown results.

Datalog engines expose derived relations.

Package-resolver style solvers expose decisions, incompatibilities, and explanations.

The frontend should not depend on any of those native shapes.

Students need academic answers:

what is satisfied;
what is not satisfied;
what is partial;
what is unknown;
what conflicts;
what does not apply;
why.

Decision

Every solver route must return a shared academic_result after normalization.

Every academic_result must use one of these statuses:

satisfied;
not_satisfied;
partial;
unknown;
conflict;
not_applicable.

Every academic_result must include:

target;
status;
completeness;
explanation_tree;
source_reference entries;
unknowns with unknown_reason;
conflicts with conflict_reason;
assumptions;
warnings;
route summary.

The public explanation contract is semantic.

It must not expose raw solver clauses, internal variable names, Datalog table layouts, SMT model internals, or CP search logs as stable frontend API fields.

Debug references may exist for maintainers.

They are not the academic explanation contract.

Consequences

The frontend can render one result shape across all query families.

The backend can change concrete solver libraries without breaking the academic API.

Every adapter must preserve enough metadata for the result normalizer.

Every adapter must support explanation mapping.

Testing must assert explanation shape, not only status.

The result contract is more verbose than a boolean answer.

That verbosity is required for source-sensitive academic planning.

Alternatives Considered

Alternative 1: Expose Engine-Native Results

The backend could return SAT, SMT, CP, Datalog, or resolver-native result objects.

This might simplify early adapter development.

However, it would force the frontend to understand engine details.

It would also make library replacement difficult.

This alternative is rejected.

Alternative 2: Return Only Status and Message

The backend could return a status plus prose.

This is easy to display.

However, prose is not enough for graph highlighting, source inspection, unknown filtering, or fixture validation.

This alternative is rejected.

Alternative 3: Use One Explanation Format Per Endpoint

Each endpoint could define its own explanation format.

This would allow local optimization.

It would also duplicate unknown, conflict, and source-reference semantics.

This alternative is rejected.

Follow-Up

Define the exact JSON schema for academic_result.

Define the exact JSON schema for explanation_tree.

Define fixture assertions for unknowns, conflicts, and source references.