Skip to content
uwwoe docs

ADR 0024: Post-V1 Demo Solver Adapters

ADR 0024: Post-V1 Demo Solver Adapters

Status: accepted

Date: 2026-05-12

Context

ADR 0013 established that UWScrape needs multiple specialized solver shapes rather than one universal solver. ADR 0017 deliberately kept concrete adapters abstract until the runtime, state, query, graph, frontend, and beta gates existed.

Milestone 8 now requires concrete solver expansion after Milestone 7 passes. The project still needs to protect the direct evaluator as the academic validation oracle, avoid unreviewed external runtime dependencies, and keep engine-native unknown, timeout, incomplete search, and unsatisfiable results distinct from academic unknown or academic impossibility.

Decision

For the first post-V1 demo solver slice, UWScrape will implement concrete in-process Go adapters under internal/solver:

  • DatalogClosureAdapter for finite relation closure and reverse unlock derivation.
  • SATBooleanAdapter for small finite Boolean choice and cardinality fragments.
  • BoundedSMTAdapter for exact bounded scaled-integer numeric fragments.
  • BoundedCPAdapter for candidate finite-horizon planning scaffolds.
  • ResolverStyleAdapter for alternative selection and incompatibility explanation.

These adapters are concrete engines for fixture-backed experimentation. They are not public API endpoints, not authoritative academic truth, and not replacements for the direct evaluator. Any returned candidate plan or derived fact that becomes user-visible academic meaning must still be validated through the direct evaluator or a later explicitly specified normalizer.

Consequences

  • The repo gains runnable solver fixtures without requiring Z3, Souffle, OR-Tools, MiniZinc, PySAT, or another external engine in CI.
  • The adapter contracts are exercised before public planning endpoints exist.
  • The project can later replace an in-process adapter with an external engine by a new ADR and compatibility tests.
  • Engine-native statuses stay visible in EngineResult.NativeStatus and are not collapsed into endpoint academic statuses.
  • CP-style planning requires explicit finite max_terms and max_courses; missing horizons return an incomplete/not-supported engine result, not an academic impossibility claim.

Non-Decisions

  • This ADR does not expose degree-CAD planning endpoints.
  • This ADR does not claim full Datalog language support.
  • This ADR does not claim production SAT, SMT, CP, or PubGrub performance.
  • This ADR does not choose WebGPU, frontend geometry, or any visualization behavior.

Verification

  • make test-m8-solver runs the solver adapter fixture suite.
  • Tests cover Datalog transitive closure, Boolean cardinality, Boolean unsatisfiability, bounded integer numeric feasibility, engine-limit incompleteness, finite-horizon CP behavior, and resolver-style conflict explanation.