[Design] Classify reduction contracts by source and target aggregation semantics

[isPANN]

Classify rules by source/target aggregation semantics and clarify how each class uses witness and value recovery.

The snippets below illustrate existing interface shapes on main; setup, imports, and type annotations are omitted. Counting and universal examples are mathematical examples, not claims that these models/rules are registered.

1. Decision → decision (Or → Or)

Flow: transform → decide target → return the same YES/NO; recover a witness for YES when a witness mapping is supplied.

Example: SAT → NAE-SAT. For the satisfiable formula x ∨ y, solve the transformed NAE instance and recover a satisfying SAT assignment. If the transformed instance is proved unsatisfiable, the source is also unsatisfiable by this rule's equivalence.

let r = source.reduce_to()?; // target: NAESatisfiability
let source_witness = match BruteForce::new().solve(r.target_problem())? {
    Some(t) => Some(r.extract_solution(&t)?),
    None => None, // NO: justified by this rule's equivalence
};

A decision many-one reduction guarantees YES/NO equivalence; witness recovery is an additional requirement for this witness API.

2. Optimization → optimization (Min/Max/Extremum → Min/Max/Extremum)

Flow: transform → find a target optimum → map its witness back; evaluate the source witness for its objective.

Example: maximum independent set → minimum vertex cover on a three-vertex path. The minimum cover is the middle vertex; its complement is the maximum independent set containing both endpoints. Source optimum = 3 − target optimum = 2.

let r = source.reduce_to()?; // target: MinimumVertexCover
let t = BruteForce::new().solve(r.target_problem())?
    .expect("vertex cover always has a feasible solution");
let s = r.extract_solution(&t)?;
let source_optimum = source.evaluate(&s)?;

For other rules, target infeasibility may be propagated only if the rule guarantees that implication. Endpoint types alone do not guarantee optimality preservation.

3. Decision → optimization (Or → Min/Max/Extremum)

Flow: transform → find the target optimum → apply the rule's value test → return YES with a witness, or NO without one.

Example: does a triangle have a vertex cover of size ≤ 1? Its minimum cover has size 2, so the answer is NO. With bound 2, the answer is YES and the optimal cover is a witness.

let values = source.reduce_to_aggregate()?; // Decision<MVC> → MVC
let (optimum, witnesses) =
    BruteForce::new().solve_with_witnesses(values.target_problem())?;
let answer = values.extract_value(optimum); // Or(true) or Or(false)

let source_witness = if answer.0 {
    let mapping = source.reduce_to()?; // same deterministic MVC target
    Some(mapping.extract_solution(&witnesses[0])?)
} else {
    None // NO is a normal result, not an extraction failure
};

This uses existing APIs but constructs the reduction twice. Assess how to share the executed construction without replacing every rule interface. The value test belongs to the rule, not a solver-specific threshold check.

4. Counting → counting (Sum → Sum)

Flow: transform → compute the target count → map the count back. No representative witness is needed.

Example: #CircuitSAT → #SAT using a Tseitin encoding with equivalences for every gate and an asserted output. For the circuit x OR y, there are 3 satisfying input assignments. Each has exactly one extension to the gate variables, so the target count is also 3.

// Illustrative rule, not currently registered:
let r = source.reduce_to_aggregate()?;
let target_count = /* exact external count of r.target_problem() */;
let source_count = r.extract_value(target_count);

The mapping is identity for this parsimonious encoding; other counting reductions may require a different transformation. Do not use witness-returning BruteForce::solve as a counting API. Sum can also represent weighted sums, not only counts.

5. Universal aggregation (And)

Flow: transform → compute the target universal result → map that Boolean aggregate back. No single satisfying witness establishes a universal claim.

Example: rename variables in a tautology instance: x OR NOT x → y OR NOT y. Both universally evaluate to true; the aggregate mapping is identity.

// Illustrative rule, not currently registered:
let r = source.reduce_to_aggregate()?;
let target_value = /* exact universal evaluation of r.target_problem() */;
let source_value = r.extract_value(target_value); // And(true)

6. Other cross-category reductions

Specify the mathematical relationship individually.

Example: minimum vertex cover → decision vertex cover through repeated bound queries. Binary-searching the bound recovers the optimum size; recovering a witness may require additional queries.

API: no executable API is planned for this Turing procedure. Keep the relation as non-executable graph metadata; do not treat it as one ordinary reduce_to call.

Shared execution requirements

• Errors, timeout, and unknown results are not NO/infeasibility proofs. Numerical backend guarantees must support any conclusion returned.
• Multi-step recovery runs backward. After a step produces no witness, preceding steps must support recovery from that result; do not attempt witness extraction or silently infer an answer.
• Reuse existing extract_solution, extract_value, and completed-result types where possible. Identify concrete missing information before proposing API changes.

Related: #1148, #1151.