A Multi-Solver Model for Academic Planning Queries

Status: Draft academic foundation.

Date: 2026-05-11.

Audience: project maintainers, solver implementers, architecture reviewers, and future specification authors.

Abstract

UWScrape models academic planning as a finite, typed, source-referenced reasoning problem.

The underlying academic object is not a plain prerequisite graph.

It is a versioned collection of course identities, listings, credits, requirement expressions, student-state facts, and credential targets.

Some queries are simple evaluations.

Some queries are closure queries over derived relations.

Some queries are feasibility questions over alternatives.

Some queries are numeric questions over grades, units, averages, and progress thresholds.

Some queries are bounded planning searches over future terms.

Some queries are explanation requests for conflicts and blocked paths.

No single engine style is the most natural, most auditable, and most efficient representation for all of those query families.

This paper defines the academic contract that lets a direct evaluator, Datalog, SAT, SMT, CP, and package-resolver style search cooperate without making any one of them the truth model.

The central thesis is:

UWScrape should define academic planning as normalized finite evaluation and planning problems, then route fragments to specialized solver adapters whose results are normalized into a shared academic result with explicit explanations, unknowns, conflicts, assumptions, and source references.

The mathematical burden is therefore not to prove that one solver can express everything.

The burden is to prove that every adapter is sound for its declared fragment and that composition does not upgrade incomplete evidence into false confidence.

1. Source and Theory Context

Waterloo’s Kuali course requisite documentation lists rule types that include course completion, choices, grade thresholds, academic level, program restrictions, milestones, and antirequisites: Waterloo course requisite rules.

Waterloo’s Kuali plan requirement documentation describes plan requirement lists as grouped rule structures: Waterloo plan requirement lists.

Waterloo’s cross-listed course documentation motivates the distinction between course listings and shared credit identity: Waterloo cross-listed courses.

SMT-LIB provides a standard theory and language context for SMT encodings: SMT-LIB.

Z3’s arithmetic guide documents integer and real arithmetic support and also notes incompleteness for some harder arithmetic fragments: Z3 arithmetic.

Z3’s fixedpoint guide describes bottom-up Datalog over finite relations: Z3 basic Datalog.

Souffle’s documentation describes Datalog relation declarations, facts, rules, and directives: Souffle program documentation.

PySAT documents cardinality encodings for Boolean cardinality constraints: PySAT cardinality encodings.

OR-Tools documents CP-SAT as a constraint programming solver over variables and constraints: OR-Tools CP-SAT.

MiniZinc provides a solver-independent constraint modeling reference: MiniZinc specification.

PubGrub documents a package dependency solver built around incompatibilities, decisions, derivations, and conflict explanation: PubGrub solver overview.

These sources justify the architecture as an integration of known reasoning forms rather than an invented monolith.

2. Basic Sets

Let C be the finite set of course credit identities in a published index.

Let L be the finite set of course listings in that index.

Let G be the finite set of credential objects.

Let R be the finite set of requirement identifiers.

Let F be the finite set of source-derived facts.

Let P be the finite set of source references.

Let T be the finite set of academic terms represented by a planning horizon.

Let A be the finite set of student-state facts.

Let U be the academic universe:

U = (C, L, G, R, F, P)

A published index is a serialized representation of U.

A student state is a finite set or record structure over A.

The finiteness assumption is essential.

The undergraduate calendar snapshot contains finitely many courses, credentials, and requirements.

A bounded planning query introduces finitely many future term positions.

Therefore every query in this architecture is a finite problem after normalization.

3. Course Identity

A course listing is a user-visible subject and number in a calendar version.

A course credit identity is the internal identity used for credit equivalence and contribution.

There is a relation:

listing_credit: L -> C

The relation may be many-to-one.

Cross-listed courses motivate many listings sharing one credit identity.

There may also be equivalence and antirequisite relations:

equivalent_credit subset C x C
antirequisite_credit subset C x C

These relations are indexed facts with source references.

The solver must not replace L with C globally.

Some source requirements refer to listings.

Some credential contribution rules depend on credit identity.

Some display explanations must preserve listing language.

4. Requirement Expressions

A requirement expression is a finite rooted tree.

Internal nodes are requirement groups.

Leaf nodes are requirement conditions or opaque source fragments.

The group constructors are:

all_of(children)
any_of(children)
choose(minimum_count, maximum_count, children)

The leaf families include:

course completion;
credit completion;
grade threshold;
unit count;
average threshold;
level predicate;
academic progress predicate;
academic standing predicate;
program enrollment predicate;
milestone predicate;
antirequisite exclusion;
equivalence;
cross-listing;
opaque source text.

Each node has a requirement id in R.

Each source-derived node has at least one source reference in P.

Opaque source text is modeled as a leaf whose truth value cannot be safely computed by the current parser.

5. Three-Valued Evaluation

Let:

K = {true, false, unknown}

true means the supported structured evidence proves satisfaction under stated assumptions.

false means the supported structured evidence proves non-satisfaction under stated assumptions.

unknown means the current problem cannot decide the requirement from supported structured evidence.

The direct evaluator computes:

eval_U,S: R -> K

where U is the published universe and S is a student state or hypothetical state.

The backend maps K plus child evidence into academic statuses:

AcademicStatus =
  satisfied
  not_satisfied
  partial
  unknown
  conflict
  not_applicable

The three-valued core is deliberately smaller than the public status set.

partial, conflict, and not_applicable require additional explanation context.

6. Evaluation Problems

An evaluation_problem is a tuple:

E = (U, S, target, scope, assumptions, limits)

U is a published academic universe.

S is a student state.

target is a course, credential, requirement expression, or query target.

scope determines which catalog version and requirements apply.

assumptions records explicit hypothetical facts.

limits records runtime and completeness policy.

An evaluation problem has no existential future plan variables unless the query explicitly provides hypothetical changes.

The desired output is one academic_result.

7. Planning Problems

A planning_problem is a tuple:

P = (U, S0, target, horizon, decision_variables, constraints, objectives, assumptions, limits)

S0 is the starting student state.

horizon is a finite set of future term positions.

decision_variables may choose courses, terms, grades, program paths, or requirement alternatives.

constraints are academic and user-defined restrictions.

objectives are optional preferences such as minimizing terms, minimizing extra courses, or maximizing credential relevance.

The desired output is zero or more candidate future states, plus explanation.

A planning problem is not an evaluation problem.

It may use evaluation internally to validate candidate states.

It may also use SAT, SMT, CP, and resolver-style search.

8. Engine Encodings

An engine_encoding maps a normalized problem fragment into the input language of an engine.

Let M be an academic fragment.

Let Enc_e(M) be the encoding for engine e.

An adapter is sound for fragment M when:

if engine e returns a conclusive result for Enc_e(M),
then the corresponding academic claim about M is true under the stated assumptions.

Completeness is separate.

An adapter may be sound without being complete.

For example, an adapter may prove that one plan exists while not proving that no better plan exists.

9. Soundness Notions

satisfied soundness:

If an academic_result reports satisfied, every requirement needed for the target is satisfied in the academic model under stated assumptions.

not_satisfied soundness:

If an academic_result reports not_satisfied, the target is not satisfied in the academic model under stated assumptions, and no relevant unknown or incomplete route could change that conclusion.

partial soundness:

If an academic_result reports partial, every reported satisfied part is satisfied and every reported unsatisfied part is unsatisfied or explicitly incomplete under the provided explanation.

unknown soundness:

If an academic_result reports unknown, the system is not claiming either satisfaction or non-satisfaction.

conflict soundness:

If an academic_result reports conflict, the explanation contains at least one incompatible set of source facts, state facts, or assumptions.

Planning soundness:

If a candidate plan is returned, validating the resulting state against encoded constraints yields satisfaction for every constraint claimed to be satisfied.

10. Direct Evaluation Rules

For a supported leaf condition, the direct evaluator uses the published index and student state.

Examples:

a course completion leaf is true if the required credit identity is completed in S;
a grade threshold leaf is true if the relevant attempt exists and grade >= threshold;
a grade threshold leaf is unknown if the relevant attempt exists but the grade is missing;
an academic progress leaf is true if S.academic_progress satisfies the predicate;
an opaque source leaf is unknown unless applicability rules prove it irrelevant.

For all_of(children):

true if every applicable child is true;
false if at least one required child is false and no unknown can repair that child;
unknown if at least one required child is unknown and the group is not otherwise conclusively false.

For any_of(children):

true if at least one applicable child is true;
false if every applicable child is false;
unknown if no child is true and at least one child is unknown.

For choose(m, n, children):

Let t be the number of true children.

Let u be the number of unknown children.

Let f be the number of false children.

The lower bound is satisfiable when t + u >= m.

The lower bound is already satisfied when t >= m.

The upper bound is violated when an upper bound n exists and t > n.

The result is true when the lower bound is already satisfied and no upper-bound uncertainty can change validity.

The result is false when t + u < m.

The result is conflict or false when t > n, depending on whether the upper bound is a contribution conflict or a pure choice condition.

Otherwise the result is unknown.

11. Theorem: Direct Evaluation Soundness

Statement.

For every requirement expression made only of supported requirement groups and supported leaf conditions, the direct evaluator returns true only when the expression is satisfied by the academic semantics under the stated student state and assumptions.

Proof sketch.

Proceed by structural induction on the requirement expression.

For leaf nodes, soundness is the contract of each supported leaf evaluator.

Each leaf evaluator checks the exact indexed fact family it declares.

For all_of, the evaluator returns true only when every child returns true.

By the induction hypothesis, every child is semantically satisfied.

Therefore the conjunction is semantically satisfied.

For any_of, the evaluator returns true only when at least one child returns true.

By the induction hypothesis, that child is semantically satisfied.

Therefore the disjunction is semantically satisfied.

For choose, the evaluator returns true only when the count of children proven true satisfies the declared cardinality bounds.

By the induction hypothesis, each counted child is semantically satisfied.

Therefore the cardinality requirement is semantically satisfied.

Opaque leaves return unknown rather than true.

Thus unsupported source text cannot create an unsound true result.

12. Theorem: Conservative Unknown Propagation

Statement.

If a requirement fragment can affect the truth of a target and the system cannot evaluate that fragment, then the solver layer must not return a conclusive satisfied or not_satisfied result for the target unless another rule proves the fragment irrelevant.

Proof sketch.

An unevaluated relevant fragment has at least two possible completions: one in which it is satisfied and one in which it is not satisfied.

If those completions can lead to different target results, choosing a conclusive result would be unsound in at least one completion.

Therefore the only sound academic statuses are unknown, partial with visible unknowns, conflict if inconsistency is known, or not_applicable if applicability eliminates the fragment.

This is exactly the result policy for opaque source text, missing grades, missing academic progress, and unsupported requirement families.

13. Theorem: Finite Decidability for Bounded Problems

Statement.

Every normalized evaluation_problem over a published index is finite.

Every normalized planning_problem with finite horizon, finite course set, finite grade domain, and finite decision-variable domains is finite.

Proof sketch.

The published index contains finitely many indexed objects.

Student state contains finitely many facts.

An evaluation problem traverses finite requirement expressions and finite relation sets.

Therefore direct evaluation terminates when implemented as structural recursion with cycle guards over requirement ids.

For planning, each decision variable has a finite domain by assumption.

The product of finitely many finite domains is finite.

An exhaustive search would terminate, although it may be too expensive.

Specialized engines are introduced for efficiency and explanation, not for decidability of bounded finite instances.

14. Datalog Fragment

The Datalog fragment consists of finite relations and Horn-style derivation rules.

Examples:

requires(course_a, course_b)
requires(course_b, course_c)
requires_transitive(x, z) :- requires(x, y), requires_transitive(y, z)
requires_transitive(x, y) :- requires(x, y)

This style matches closure questions:

what does a course unlock;
what depends on a course;
which credential requirements mention a course;
which courses are in a requirement subtree;
what equivalence closure exists.

Souffle and Z3 fixedpoint are implementation references for finite relation derivation: Souffle program documentation, Z3 basic Datalog.

15. Proposition: Datalog Closure Soundness

Statement.

If the Datalog adapter encodes source relations exactly and uses only sound derivation rules, every derived relation fact returned by the adapter is entailed by the finite source relation system.

Proof sketch.

Datalog rules derive facts by repeated application of rules whose premises are already facts.

Base facts come from the index.

Induct on derivation length.

At length zero, every derived fact is a source fact.

At length k + 1, the fact is produced by a rule whose premises have derivations of length at most k.

By induction, those premises are entailed by the source relation system.

By soundness of the rule, the conclusion is entailed.

Therefore every returned derived relation is sound.

16. SAT Fragment

The SAT fragment consists of finite Boolean choices.

Examples:

choose at least one course from a finite list;
choose exactly two requirements from a finite group;
enforce that antirequisite choices do not coexist;
test whether a set of Boolean alternatives can satisfy a credential shell.

Cardinality constraints can be encoded into CNF using standard encodings.

PySAT documents multiple encodings for at-most, at-least, and equality cardinality forms: PySAT cardinality encodings.

The SAT fragment should not hide numeric thresholds by coarse Boolean approximations unless the approximation is explicitly marked.

17. Proposition: SAT Encoding Soundness

Statement.

For a finite Boolean requirement fragment, if the SAT adapter uses a truth-preserving encoding and the SAT solver returns satisfiable, then the extracted Boolean assignment satisfies the original Boolean fragment.

Proof sketch.

A truth-preserving encoding has the property that every model of the CNF maps to a valuation of original Boolean variables that satisfies the original formulas.

The adapter records the map from academic choices to Boolean variables.

If the solver returns satisfiable, it returns or implies a model of the CNF.

Applying the inverse map yields an academic choice valuation.

By truth preservation, that valuation satisfies the Boolean fragment.

If the solver returns unsatisfiable and the encoding is complete, no satisfying Boolean valuation exists for the fragment.

The complete condition is necessary for mapping unsatisfiability to academic non-satisfaction.

18. SMT Fragment

The SMT fragment consists of Boolean structure combined with numeric academic constraints.

Examples:

grade >= 70;
average over selected courses >= 65;
units from a group >= 1.5;
grade variables under hypothetical what-if assumptions;
mixed constraints over course choice and grade thresholds.

SMT-LIB provides standard theories and solver-language conventions: SMT-LIB.

Z3’s arithmetic guide documents integer and real sorts, arithmetic constraints, and cases where nonlinear or otherwise hard arithmetic can return unknown: Z3 arithmetic.

For UWScrape, grades and units should preferably be represented as exact scaled integers.

This avoids accidental floating point policy.

19. Proposition: SMT Numeric Soundness

Statement.

If grade, unit, and average rules are encoded as exact arithmetic constraints over domains matching the academic policy, then any model returned by an SMT solver corresponds to a numeric assignment satisfying those rules.

Proof sketch.

The adapter maps each numeric academic quantity to an SMT variable with a declared domain.

Each academic numeric rule is translated into an arithmetic formula.

Exact scaled integers preserve comparison and addition when scale factors are chosen consistently.

An SMT model satisfies all asserted formulas.

Therefore the decoded numeric assignment satisfies the corresponding academic numeric rules.

The statement does not claim completeness for all possible arithmetic fragments.

The adapter must report engine-native unknown or unsupported fragments separately.

20. CP Fragment

The CP fragment consists of bounded finite-domain planning.

Examples:

assign each planned course to one of n future terms;
enforce prerequisite order;
enforce maximum courses per term;
enforce that corequisites appear in the same term or earlier allowed term;
enforce credential completion by the final term;
search for one plan or several plans.

OR-Tools CP-SAT and MiniZinc are useful implementation references for this style of modeling: OR-Tools CP-SAT, MiniZinc specification.

The CP fragment is meaningful only with explicit horizon and assumptions.

Unbounded degree planning is not a v1 target.

21. Proposition: CP Plan Soundness

Statement.

If a CP adapter returns a candidate plan and every academic constraint claimed by the adapter is encoded exactly, then direct evaluation of the resulting planned state satisfies those encoded constraints.

Proof sketch.

The CP solver returns an assignment to decision variables.

The adapter decodes the assignment into a future planned student state.

Each encoded academic constraint is true under the assignment.

If the decoding preserves variable meaning, the corresponding academic constraint is true in the planned state.

Running the direct evaluator over the planned state is an independent validation step.

If validation fails, the adapter result must be rejected or marked conflict.

22. Package-Resolver Style Fragment

The package-resolver style fragment consists of decisions, incompatibilities, backtracking, and explanations.

It is most useful for alternative-path search.

PubGrub documents package solving through incompatibilities, derived incompatibilities, decisions, and conflict explanation: PubGrub solver overview.

For academic planning, an incompatibility might be:

a chosen course conflicts with a completed antirequisite;
two credential paths require mutually exclusive courses;
a course choice cannot satisfy a grade threshold with known grade;
a planned course cannot be taken before its prerequisite under the current horizon.

The adapter should treat conflict explanations as structured derivation summaries.

It should not treat package version ranges as a literal model for all academic semantics.

23. Proposition: Resolver Explanation Soundness

Statement.

A package-resolver style explanation is sound when every incompatibility in the explanation is either a source fact, a state fact, or a derived incompatibility justified by earlier incompatibilities.

Proof sketch.

This is an induction over the explanation derivation.

Base incompatibilities are checked against source facts or state facts.

Derived incompatibilities cite their premises.

If all premises are sound and the derivation rule is sound, the conclusion is sound.

Therefore the final conflict explanation is sound.

The proposition does not imply that the resolver found every possible alternative path.

It only validates the explanation it returned.

24. Safe Composition

The solver layer composes adapters through a result normalizer.

Let R_i be the result returned by adapter i.

Let A be the final academic_result.

Composition is safe when:

each adapter declares its supported fragment;
each adapter reports completeness for that fragment;
each adapter preserves source references;
the normalizer never treats incomplete evidence as conclusive evidence;
conflicts between routes are reported rather than suppressed.

25. Theorem: Safe Multi-Adapter Composition

Statement.

If every adapter result used by the normalizer is sound for its declared fragment, and the normalizer only emits conclusive academic statuses when the relevant fragments are complete and non-conflicting, then the final conclusive academic_result is sound.

Proof sketch.

Consider a final result with status satisfied.

By normalizer policy, every relevant fragment needed for satisfaction is covered by a complete, non-conflicting adapter result or by direct evaluation.

Each such result is sound for its fragment.

Therefore every needed academic condition is satisfied.

The argument for not_satisfied is similar but requires completeness for the negative claim.

The normalizer may emit unknown or partial when coverage is incomplete.

Those statuses make no false conclusive claim.

If adapter results conflict, the normalizer emits conflict rather than choosing an arbitrary winner.

Therefore no conclusive academic status is produced from inconsistent evidence.

26. Counterexample: Plain Prerequisite Graphs Are Lossy

Suppose course T requires:

all_of(
  any_of(A, B),
  any_of(C, D)
)

A plain directed graph usually draws:

A -> T
B -> T
C -> T
D -> T

That graph cannot distinguish this requirement from:

any_of(A, B, C, D)

It also cannot distinguish it from:

all_of(A, B, C, D)

All three expressions can yield the same four incoming edges.

Therefore the ordinary graph projection is not injective.

It loses requirement structure.

It cannot be the truth model.

27. Counterexample: Datalog Alone Is Not Enough

Datalog is excellent for finite relation closure.

However, a requirement such as:

average(best_three_courses_from_group) >= 70

is not naturally a monotone relation closure query.

Adding a new low grade can reduce an average depending on contribution rules.

Choosing best three courses introduces optimization-like selection.

Forcing this into Datalog either complicates the language with aggregates and policy-specific encodings or loses the numeric semantics.

Therefore Datalog should be a closure engine, not the entire solver layer.

28. Counterexample: SAT Alone Is Not Enough

SAT can encode finite choices.

However, a grade average over exact numeric values requires either:

a large Boolean encoding of every numeric possibility; or
an approximation; or
a separate arithmetic theory.

The first option can be inefficient and opaque.

The second is academically unsafe if not disclosed.

The third is SMT, not pure SAT.

Therefore SAT should handle Boolean alternatives and conflicts, while SMT should handle numeric constraints.

29. Counterexample: SMT Alone Is Not Enough

SMT can express many Boolean and numeric constraints.

However, recursive closure queries over a large finite graph are often more naturally expressed as Datalog relations.

A user asking “what does this course unlock transitively?” needs a relation result and derivation paths.

Encoding the whole closure problem as an SMT query is possible in bounded forms but is less direct and less explanation-friendly.

Therefore SMT should not replace Datalog for closure-heavy queries.

30. Counterexample: CP Alone Is Not Enough

CP can model bounded planning.

However, using CP for every current-state unlock query is unnecessary.

A direct evaluator can answer a fixed-state requirement tree deterministically and explain it structurally.

CP search adds overhead and may return engine-native incomplete statuses under time limits.

Therefore CP should be reserved for bounded planning and schedule-like constraints.

31. Counterexample: Package Resolver Alone Is Not Enough

Package dependency solvers are strong at alternative selection and conflict explanation.

Academic planning also needs:

grade thresholds;
averages;
unit totals;
academic progress;
cross-listed credit identities;
opaque source propagation;
credential contribution rules.

Those are not all natural package version constraints.

The package-resolver style is valuable as an explanation pattern, but it should not be the canonical academic model.

32. Counterexample: Direct Evaluator Alone Is Not Enough

The direct evaluator answers fixed-state questions.

It can evaluate:

Does the current state satisfy this requirement?

It does not naturally answer:

Is there some sequence of future courses over six terms that satisfies this credential while respecting prerequisites?

That question introduces existential decision variables.

The direct evaluator can validate a candidate plan after it is constructed.

It should not be the only planning search mechanism.

33. Academic Soundness for Course Unlock

A course unlock answer is sound when:

the target course identity is resolved;
all relevant prerequisites are evaluated or marked unknown;
relevant corequisites are distinguished from prerequisites;
antirequisite conflicts are reported;
grade thresholds are checked against known grades or marked unknown;
academic progress requirements are checked against academic progress, not academic standing;
source references are attached to every decisive requirement.

The answer should not say “unlocked” when an opaque source fragment could block enrollment.

The answer may say “partially unlocked” when known prerequisites are satisfied but one unknown remains.

34. Academic Soundness for Credential Progress

A credential progress answer is sound when:

the credential version is fixed;
requirement groups preserve cardinality;
course contribution uses credit identity rules;
cross-listed courses do not double-count unless policy permits it;
unit totals are exact under indexed unit values;
average thresholds are computed under declared policy;
unparsed credential rules remain unknown;
satisfied and unsatisfied requirement ids are visible.

The answer should separate:

completed courses that contribute;
completed courses that do not contribute;
completed courses whose contribution is unknown;
planned courses that might contribute.

35. Academic Soundness for What-If Queries

A what-if answer compares two states:

S_before
S_after = S_before + hypothetical_changes

The comparison is sound when both states are evaluated under the same index, same credential version, and same policy.

The result should report changed facts rather than only final status.

If adding a course introduces an antirequisite conflict, the result should not present only the new unlocks.

If adding a grade resolves an unknown threshold, the result should show which unknown was resolved.

36. Academic Soundness for Degree-CAD Feasibility

A degree-CAD feasibility result is sound when:

the planning horizon is explicit;
offering assumptions are explicit;
grade assumptions are explicit;
course load limits are explicit;
prerequisite timing is encoded;
corequisite timing is encoded;
credential requirements are validated on the final planned state;
every returned plan is checked by direct evaluation or equivalent validation;
non-existence claims are limited to the encoded horizon and assumptions.

A bounded infeasibility result is not a universal impossibility result.

It means no plan exists under the encoded bounds, if the encoding is complete and the engine result is conclusive.

37. Unknown Is Academically Meaningful

Academic unknown means the project refuses to guess.

It can arise from:

opaque source text;
missing grade data;
missing academic progress;
missing declared program state;
unsupported requirement condition;
source conflict;
engine incompleteness.

These reasons differ.

They should have different unknown_reason codes.

An engine-native UNKNOWN is only one possible source of academic unknown.

A timeout is not the same as an opaque source fragment.

An SMT unknown is not the same as missing student grade data.

The shared result contract keeps these distinctions visible.

38. Conflict Is Academically Meaningful

Academic conflict means the system found incompatible facts or assumptions.

Examples:

completed courses violate a contribution exclusion;
planned courses include antirequisites;
two source references disagree after patches;
a state migration produced incompatible catalog versions;
a user assumes two mutually exclusive program states.

Conflict is not ordinary non-satisfaction.

Conflict requires explanation.

The system should not choose one side silently.

39. Explanation Trees

An explanation tree is not necessarily a formal proof object.

It is a structured account of why an academic status was returned.

For direct evaluation, it should mirror requirement structure.

For Datalog, it may show derived relation paths.

For SAT, it may show chosen alternatives and unsatisfied alternatives.

For SMT, it may show numeric inequalities and values.

For CP, it may show planning assignments and violated constraints.

For resolver-style search, it may show incompatibility derivations.

Every explanation tree node should carry source references when it depends on source data.

40. Proof Review Checklist

The model avoids circularity because:

academic objects are defined before requirements;
requirements are defined before evaluation;
evaluation problems are defined before engine encodings;
engine encodings are defined before adapter soundness;
adapter soundness is defined before composition.

The model separates:

course listing from course credit identity;
course prerequisites from credential requirements;
academic progress from academic standing;
source unknown from engine incompleteness;
evaluation from planning.

The model admits incomplete parser coverage without pretending the data is complete.

The model admits multiple engines without allowing any engine to define academic truth alone.

41. Implementation Consequences

The backend should implement direct evaluation first.

The direct evaluator should be fixture-rich.

The direct evaluator should validate candidate plans returned by future planning engines.

Every future adapter should declare its supported fragment.

Every future adapter should provide fixture evidence.

Every future adapter should preserve source references.

Every future adapter should report completeness separately from academic status.

The result normalizer should be tested as aggressively as the adapters.

42. Conclusion

UWScrape needs multiple solvers because academic planning contains multiple mathematical shapes.

Requirement trees need deterministic evaluation.

Reachability needs relation closure.

Course alternatives need Boolean feasibility.

Grades and averages need numeric reasoning.

Term plans need bounded finite-domain search.

Blocked paths need conflict explanation.

The academically sound architecture is not a single engine.

It is a shared normalized problem contract, specialized adapter fragments, conservative status mapping, and explanation trees grounded in source references.

That architecture lets the site be visually rich without letting visualization become the truth model.