ADR 0017: Abstract Solver Adapters Before Concrete Engines

ADR 0017: Abstract Solver Adapters Before Concrete Engines

Status: Accepted for architectural direction.

Date: 2026-05-11.

Context

Several mature solver ecosystems could be useful for UWScrape.

SMT-LIB provides solver-language standards for SMT: SMT-LIB.

Z3 offers arithmetic and fixedpoint features: Z3 arithmetic, Z3 basic Datalog.

Souffle offers a Datalog implementation model: Souffle program documentation.

PySAT documents SAT cardinality encodings: PySAT cardinality encodings.

OR-Tools CP-SAT and MiniZinc are relevant CP references: OR-Tools CP-SAT, MiniZinc specification.

PubGrub is relevant for resolver-style incompatibility explanation: PubGrub solver overview.

Choosing libraries too early would blur the academic contract with dependency decisions.

Decision

Define abstract engine_adapter contracts before selecting concrete external solver libraries.

The adapter contract must include:

• supported problem kinds;
• supported requirement fragments;
• normalization input;
• prepared problem output;
• engine result output;
• explanation mapping;
• completeness reporting;
• status mapping;
• source-reference preservation;
• fixture requirements.

Concrete engines may be selected later by implementation specs or ADRs.

No concrete solver library is mandatory in the current architecture.

The direct evaluator is the only first-runtime engine decision.

Consequences

The project can design endpoint and result contracts without library lock-in.

The project can compare candidate libraries against fixture obligations.

The project can replace a solver library later if the adapter contract is preserved.

The architecture remains slightly abstract until implementation specs choose concrete dependencies.

That abstraction is intentional.

The academic contract must stabilize before external engine details.

Alternatives Considered

Alternative 1: Choose All Solver Libraries Now

This would make implementation planning feel concrete.

However, the backend API and academic result contract do not require immediate library selection.

Premature dependency choices would distract from semantics.

This alternative is rejected.

Alternative 2: Avoid External Engines Forever

The project could use only hand-written Go code.

This keeps deployment simple.

It also leaves bounded planning, numeric feasibility, and rich conflict search harder to implement and validate.

This alternative is rejected as a permanent policy.

Alternative 3: Let Each Adapter Define Its Own Contract

Each adapter could expose whatever its library naturally returns.

This would speed isolated experiments.

It would break stable frontend and backend contracts.

This alternative is rejected.

Follow-Up

Write an adapter interface spec after backend package boundaries are drafted.

Add library-selection ADRs only when concrete implementations are ready.

Build fixtures before benchmarking concrete engines.