diff --git a/docs/plans/2026-03-22-counting-problem-trait-design.md b/docs/plans/2026-03-22-counting-problem-trait-design.md new file mode 100644 index 00000000..5aa94a2d --- /dev/null +++ b/docs/plans/2026-03-22-counting-problem-trait-design.md @@ -0,0 +1,244 @@ +# CountingProblem Trait — Supporting #P and PP-Complete Problems + +**Date:** 2026-03-22 +**Status:** Approved design, pending implementation + +## Problem + +The current trait hierarchy supports two problem families: + +- `OptimizationProblem` (`Metric = SolutionSize`) — find a config that maximizes/minimizes an objective +- `SatisfactionProblem` (`Metric = bool`) — find a config satisfying all constraints + +8 issues are blocked because they model problems where the answer depends on **aggregating over the entire configuration space** — counting feasible configs or summing weighted probabilities. These are #P-complete or PP-complete problems (not known to be in NP) that don't fit either existing trait. + +### Blocked issues + +**Models:** #235 NetworkReliability, #237 NetworkSurvivability, #404 KthLargestSubset, #405 KthLargestMTuple + +**Rules (blocked on models above):** #256 SteinerTree → NetworkReliability, #257 VertexCover → NetworkSurvivability, #394 SubsetSum → KthLargestSubset, #395 SubsetSum → KthLargestMTuple + +## Design + +### New type: `Weight` + +A newtype wrapper for per-configuration weights, parallel to `SolutionSize` for optimization problems. Infeasible configs have weight zero — no separate `Infeasible` variant needed (unlike `SolutionSize::Invalid`) because a zero-weight config contributes nothing to the sum. + +```rust +// src/types.rs +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +pub struct Weight(pub W); +``` + +### New trait: `CountingProblem` + +A marker trait parallel to `SatisfactionProblem`, binding `Metric = Weight`: + +```rust +// src/traits.rs +pub trait CountingProblem: Problem> { + /// The inner weight type (e.g., `u64` for unweighted counting, `f64` for probabilities). + type Value: Clone + AddAssign + Zero + PartialOrd + fmt::Debug + Serialize + DeserializeOwned; +} +``` + +The `evaluate(config) -> Weight` method (inherited from `Problem`) returns the weight of a single configuration. The "answer" to the problem is the sum of weights over all configurations. This is computed by the solver, not by `evaluate`. + +### Trait hierarchy (updated) + +``` +Problem (Metric: Clone) +├── OptimizationProblem (Metric = SolutionSize) — existing, unchanged +├── SatisfactionProblem (Metric = bool) — existing, unchanged +└── CountingProblem (Metric = Weight) — NEW +``` + +### Solver extension + +Add a separate `CountingSolver` trait (parallel to how problem families have distinct traits) rather than extending the existing `Solver` trait. This avoids forcing `ILPSolver` to implement a meaningless `count` method: + +```rust +// src/solvers/mod.rs (existing Solver trait unchanged) + +/// Solver trait for counting problems. +pub trait CountingSolver { + /// Compute the total weight (sum of evaluate over all configs). + fn count(&self, problem: &P) -> P::Value; +} + +// src/solvers/brute_force.rs +impl CountingSolver for BruteForce { + fn count(&self, problem: &P) -> P::Value { + let mut total = P::Value::zero(); + for config in DimsIterator::new(problem.dims()) { + total += problem.evaluate(&config).0; + } + total + } +} +``` + +`BruteForce` also gets a convenience method for testing: +```rust +/// Return all feasible configs and their weights alongside the total count. +pub fn count_with_configs(&self, problem: &P) + -> (P::Value, Vec<(Vec, P::Value)>); +``` + +### Reduction support + +Counting reductions preserve aggregate counts, not individual solutions. New traits parallel to `ReductionResult` / `ReduceTo`: + +```rust +// src/rules/traits.rs + +pub trait CountingReductionResult { + type Source: CountingProblem; + type Target: CountingProblem; + + /// Get a reference to the target problem. + fn target_problem(&self) -> &Self::Target; + + /// Transform the target's aggregate count back to the source's count. + /// + /// For parsimonious reductions (1-to-1 config mapping), this is identity. + /// For non-parsimonious reductions, this applies a correction factor + /// (e.g., divide by 2 if the reduction doubles feasible configs). + fn extract_count( + &self, + target_count: ::Value, + ) -> ::Value; +} + +pub trait ReduceToCount: CountingProblem { + type Result: CountingReductionResult; + fn reduce_to_count(&self) -> Self::Result; +} +``` + +### Registry and CLI integration + +#### `declare_variants!` macro + +Gets a new `count` keyword. The macro generates a `CountSolveFn` (instead of `SolveFn`) that calls `BruteForce::count()` and formats the result: + +```rust +crate::declare_variants! { + default count NetworkReliability => "2^num_edges * num_vertices", +} +``` + +The `count` keyword generates: +- A new `SolverKind::Count` variant in the proc macro's internal `SolverKind` enum (alongside existing `Opt` and `Sat`) +- A `solver_kind` field on `VariantEntry` to distinguish problem families at runtime (enum with `Optimization`, `Satisfaction`, `Counting` variants) +- A `count_fn: Option` field on `VariantEntry` where `CountSolveFn = fn(&dyn Any) -> String` +- The generated function downcasts `&dyn Any` to the concrete type, calls `BruteForce.count(&problem)`, and formats the result +- The existing `ProblemType` struct (which holds problem metadata, not a classification enum) is unchanged + +#### `LoadedDynProblem` + +Gets a new method: +```rust +pub fn solve_counting(&self) -> Option { + (self.count_fn?)(self.inner.as_any()) +} +``` + +The existing `solve_brute_force` remains unchanged for opt/sat problems. + +#### `pred solve` CLI + +The solve command checks `VariantEntry::solver_kind` to determine the dispatch path: +- `SolverKind::Optimization` / `SolverKind::Satisfaction` → existing `solve_brute_force()` +- `SolverKind::Counting` → new `solve_counting()`, displays `Total weight: ` + +#### `#[reduction]` proc macro + +The existing macro hardcodes `ReduceTo` trait detection. It must be extended to also recognize `ReduceToCount`: + +- When the macro sees `impl ReduceToCount for Source`, it generates a `reduce_count_fn` field on `ReductionEntry` +- The generated function returns a `Box` (new type-erased trait for counting reductions) +- `overhead` attribute works identically — overhead expressions are about problem size, not about solution type + +#### `ReductionEntry` changes + +`ReductionEntry` (in `src/rules/registry.rs`) gains new optional fields for counting reductions. A given entry has either `reduce_fn` (opt/sat) or `reduce_count_fn` (counting), never both: + +```rust +pub struct ReductionEntry { + // ... existing fields unchanged ... + pub reduce_fn: Option, // existing: opt/sat reductions + pub reduce_count_fn: Option, // NEW: counting reductions +} +``` + +Where `CountReduceFn = fn(&dyn Any) -> Box`. + +#### Reduction graph integration + +Counting edges and opt/sat edges coexist in the same `ReductionGraph`. The graph is about problem reachability — edge type doesn't affect pathfinding. The distinction matters only at solve time: + +- `ReductionEdgeData` gains an `edge_kind: EdgeKind` field (`enum EdgeKind { Standard, Counting }`) +- `reduce_along_path` checks edge kinds: a path must be homogeneous (all-standard or all-counting); mixed paths are invalid +- For all-counting paths, the runtime builds a `CountingReductionChain` instead of a `ReductionChain` + +#### Counting reduction chains + +For multi-hop counting paths (A →count→ B →count→ C): + +```rust +pub trait DynCountingReductionResult { + fn target_problem_any(&self) -> &dyn Any; + /// Transform target count to source count using serde_json::Value for type erasure. + fn extract_count_dyn(&self, target_count: serde_json::Value) -> serde_json::Value; +} +``` + +`CountingReductionChain` composes these: reduce A→B→C, solve C to get count as `serde_json::Value`, then call `extract_count_dyn` backwards through the chain. This parallels `ReductionChain` for opt/sat reductions. + +**Note on cross-type reductions:** When source and target have different `Value` types (e.g., `u64` → `f64`), the `extract_count` implementation is responsible for the type conversion. The `serde_json::Value` type erasure in `DynCountingReductionResult` handles this naturally at the runtime dispatch level. + +#### Exports + +Add to prelude and `lib.rs`: +- `CountingProblem`, `Weight`, `CountingSolver` traits/types +- `ReduceToCount`, `CountingReductionResult` traits + +### Concrete models + +All models store **only the counting problem data** — no decision thresholds (`k`, `q`). The threshold is part of the GJ decision formulation but not part of the counting problem we model. + +| Model | Value type | Fields | evaluate returns | +|---|---|---|---| +| `NetworkReliability` | `f64` | `graph`, `terminals`, `failure_probs` | `Weight(Π p_e^{x_e} · (1-p_e)^{1-x_e})` if terminals connected, else `Weight(0.0)` | +| `NetworkSurvivability` | `f64` | `graph`, `terminals`, `failure_probs` | Same pattern for survivability | +| `KthLargestSubset` | `u64` | `sizes`, `bound` | `Weight(1)` if subset sum ≤ bound, else `Weight(0)` | +| `KthLargestMTuple` | `u64` | `sizes`, `bound` | `Weight(1)` if m-tuple condition met, else `Weight(0)` | + +### `Weight` utility impls + +For ergonomics, `Weight` implements: +- `PartialOrd` where `W: PartialOrd` — delegates to inner value +- `Eq` where `W: Eq`, `Hash` where `W: Hash` — conditional impls (works for `u64`, not `f64`) +- `Add>` and `std::iter::Sum` where `W: Add` — enables `configs.map(evaluate).sum()` +- `Display` where `W: Display` — prints the inner value directly (e.g., `0.9832` not `Weight(0.9832)`) + +### What is NOT changed + +- `OptimizationProblem`, `SatisfactionProblem` — untouched +- `ReduceTo`, `ReductionResult` — untouched +- All existing models and rules — untouched +- Existing `Solver` trait — untouched (new `CountingSolver` is separate) + +## Alternatives considered + +1. **Generalized metric aggregation** (#737) — replace all three leaf traits with a single `Aggregation` enum. Elegant but large breaking refactor with no immediate payoff. Filed for future consideration. + +2. **Two-level trait** (`is_feasible` + `weight` methods) — more explicit but adds unnecessary surface area and boilerplate for unweighted counting. + +3. **`Metric = f64` without wrapper** — works but loses type safety. `Weight` follows the `SolutionSize` pattern and makes intent explicit. + +## Related issues + +- #737 — Generalized metric aggregation (future architecture) +- #748 — DefaultSolver per problem (future architecture) diff --git a/docs/plans/2026-03-22-generalized-aggregation-design.md b/docs/plans/2026-03-22-generalized-aggregation-design.md new file mode 100644 index 00000000..b69209d3 --- /dev/null +++ b/docs/plans/2026-03-22-generalized-aggregation-design.md @@ -0,0 +1,360 @@ +# Generalized Aggregation — Unified Problem Trait Hierarchy + +**Date:** 2026-03-22 +**Status:** Approved design, pending implementation +**Supersedes:** `2026-03-22-counting-problem-trait-design.md` (the minimal CountingProblem extension) + +## Problem + +The current trait hierarchy has three parallel leaf traits: + +- `OptimizationProblem` (`Metric = SolutionSize`, `direction()` method) +- `SatisfactionProblem` (`Metric = bool`, marker trait) +- (Proposed) `CountingProblem` (`Metric = Weight`) + +Each requires its own solver method, macro keyword, registry dispatch, and reduction trait. The aggregation strategy is implicit — `SolutionSize` "happens to" mean optimize, `bool` "happens to" mean exists. Adding each new problem family (counting, tautology checking, etc.) multiplies this surface area. + +### Blocked issues (counting/probability problems) + +**Models:** #235 NetworkReliability, #237 NetworkSurvivability, #404 KthLargestSubset, #405 KthLargestMTuple + +**Rules:** #256 SteinerTree -> NetworkReliability, #257 VertexCover -> NetworkSurvivability, #394 SubsetSum -> KthLargestSubset, #395 SubsetSum -> KthLargestMTuple + +## Design + +### Core idea + +The aggregation strategy IS the data type. Instead of separate leaf traits, each problem declares `type Value: Aggregate` where the value type encodes how to combine evaluations across the configuration space. + +### `Aggregate` trait + +A monoid: an identity element and an associative combining operation. + +```rust +// src/types.rs + +/// Trait for values that know how to aggregate across a configuration space. +/// +/// Each type encodes both the per-config evaluation result and the +/// combining strategy (monoid: identity + associative binary operation). +pub trait Aggregate: Clone + fmt::Debug + Serialize + DeserializeOwned { + /// Neutral element: combine(identity(), x) == x + fn identity() -> Self; + /// Associative combining operation. + fn combine(self, other: Self) -> Self; +} +``` + +### Aggregation types + +Five concrete types, each implementing `Aggregate`: + +```rust +// src/types.rs + +/// Optimization: keep the maximum value. None = infeasible. +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +pub struct Max(pub Option); + +/// Optimization: keep the minimum value. None = infeasible. +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +pub struct Min(pub Option); + +/// Counting: sum all weights. Zero = infeasible. +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +pub struct Sum(pub W); + +/// Satisfaction (existential): true if any config satisfies. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct Or(pub bool); + +/// Satisfaction (universal): true if all configs satisfy. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct And(pub bool); +``` + +| Type | Identity | Operation | Replaces | +|------|----------|-----------|----------| +| `Max` | `Max(None)` | keep larger `Some` | `SolutionSize` + `Direction::Maximize` | +| `Min` | `Min(None)` | keep smaller `Some` | `SolutionSize` + `Direction::Minimize` | +| `Sum` | `Sum(W::zero())` | add | (new, for #P/PP-complete) | +| `Or` | `Or(false)` | logical or | `bool` + `SatisfactionProblem` | +| `And` | `And(true)` | logical and | (new, for tautology checking) | + +Utility impls per type: +- `Max`, `Min`: `PartialOrd` delegating to inner; conditional `Eq`/`Hash` where `V: Eq`/`Hash` +- `Sum`: `Add`, `std::iter::Sum`, `PartialOrd`; conditional `Eq`/`Hash` where `W: Eq`/`Hash` +- All types: `Display` with descriptive formatting (e.g., `Max(Some(42))` displays as `"Maximum: 42"`) + +### Unified `Problem` trait + +```rust +// src/traits.rs + +pub trait Problem: Clone { + const NAME: &'static str; + /// The evaluation/aggregation type. + type Value: Aggregate; + /// Configuration space dimensions. + fn dims(&self) -> Vec; + /// Evaluate the problem on a configuration. + fn evaluate(&self, config: &[usize]) -> Self::Value; + /// Number of variables (derived from dims). + fn num_variables(&self) -> usize { self.dims().len() } + /// Variant attributes derived from type parameters. + fn variant() -> Vec<(&'static str, &'static str)>; + /// Look up this problem's catalog entry. + fn problem_type() -> crate::registry::ProblemType { + crate::registry::find_problem_type(Self::NAME) + .unwrap_or_else(|| panic!("no catalog entry for Problem::NAME = {:?}", Self::NAME)) + } +} +``` + +**What disappears:** +- `OptimizationProblem` trait +- `SatisfactionProblem` trait +- `DeclaredVariant` trait — unchanged, still generated by `declare_variants!` +- `direction()` method — encoded in `Max` vs `Min` +- `type Metric` — renamed to `type Value` +- `SolutionSize` enum +- `Direction` enum + +### Unified Solver + +```rust +// src/solvers/mod.rs + +pub trait Solver { + fn solve(&self, problem: &P) -> P::Value; +} + +// src/solvers/brute_force.rs + +impl Solver for BruteForce { + fn solve(&self, problem: &P) -> P::Value { + DimsIterator::new(problem.dims()) + .map(|config| problem.evaluate(&config)) + .fold(P::Value::identity(), P::Value::combine) + } +} +``` + +One method, works for all five aggregation types via monoid fold. + +Config-returning convenience methods stay on `BruteForce` (not on `Solver`): + +```rust +impl BruteForce { + /// Find all configs that achieve the optimal aggregate value. + /// For Max/Min: all configs with the best value. + /// For Or: all satisfying configs. + /// For Sum: all configs with nonzero weight. + pub fn solve_all(&self, problem: &P) -> Vec>; + + /// Solve and return the aggregate value alongside the contributing configs. + pub fn solve_with_configs(&self, problem: &P) + -> (P::Value, Vec<(Vec, P::Value)>); +} +``` + +**What disappears:** +- `find_best`, `find_all_best` +- `find_satisfying`, `find_all_satisfying` + +### Reductions + +Two reduction traits. The existing `ReduceTo` for config-mapping reductions (opt/sat). A new `ReduceToAggregate` for value-mapping reductions (counting): + +```rust +// src/rules/traits.rs + +// Unchanged — maps individual configs between source and target +pub trait ReductionResult { + type Source: Problem; + type Target: Problem; + fn target_problem(&self) -> &Self::Target; + fn extract_solution(&self, target_solution: &[usize]) -> Vec; +} + +pub trait ReduceTo: Problem { + type Result: ReductionResult; + fn reduce_to(&self) -> Self::Result; +} + +// NEW — maps aggregate values between source and target +pub trait AggregateReductionResult { + type Source: Problem; + type Target: Problem; + fn target_problem(&self) -> &Self::Target; + fn extract_value( + &self, + target_value: ::Value, + ) -> ::Value; +} + +pub trait ReduceToAggregate: Problem { + type Result: AggregateReductionResult; + fn reduce_to_aggregate(&self) -> Self::Result; +} +``` + +**`ReductionAutoCast`** — unchanged, still used for natural subtype edges. + +**`DynReductionResult`** — unchanged for config-mapping reductions. New `DynAggregateReductionResult` for value-mapping: + +```rust +pub trait DynAggregateReductionResult { + fn target_problem_any(&self) -> &dyn Any; + fn extract_value_dyn(&self, target_value: serde_json::Value) -> serde_json::Value; +} +``` + +### `#[reduction]` proc macro + +Extended to recognize both `ReduceTo` and `ReduceToAggregate`: + +- For `impl ReduceTo for Source`: generates `reduce_fn` on `ReductionEntry` (unchanged) +- For `impl ReduceToAggregate for Source`: generates `reduce_aggregate_fn` on `ReductionEntry` +- `overhead` attribute works identically for both — overhead expressions describe problem size, not solution type + +### `ReductionEntry` and reduction graph + +```rust +// src/rules/registry.rs +pub struct ReductionEntry { + // ... existing fields unchanged ... + pub reduce_fn: Option, // existing: config-mapping + pub reduce_aggregate_fn: Option, // NEW: value-mapping +} +``` + +Both edge kinds coexist in the same `ReductionGraph`. Pathfinding is shared — the graph is about reachability. At solve time, a path must be homogeneous (all config-mapping or all value-mapping). For all-aggregate paths, the runtime builds an `AggregateReductionChain` that composes `extract_value_dyn` calls backwards. + +### `declare_variants!` macro + +The `opt`/`sat` keywords are removed. The macro no longer needs to generate different `SolveFn` closures: + +```rust +// Before: +crate::declare_variants! { + default opt MaximumIndependentSet => "1.1996^num_vertices", + default sat Satisfiability => "2^num_variables", +} + +// After: +crate::declare_variants! { + default MaximumIndependentSet => "1.1996^num_vertices", + default Satisfiability => "2^num_variables", + default NetworkReliability => "2^num_edges * num_vertices", +} +``` + +The generated `SolveFn` always calls `Solver::solve()` — one code path. `SolverKind` enum disappears. + +### Registry and CLI integration + +**`DynProblem`:** No changes needed. `evaluate_dyn`/`evaluate_json` work as-is since `Aggregate` requires `Debug + Serialize`. + +**`LoadedDynProblem`:** `solve_brute_force` simplifies to one `SolveFn` signature, one code path. + +**`pred solve` CLI:** No longer needs to know the problem kind. Calls `solve_brute_force()` and prints the result. Aggregate types format via `Display`: +- `Max(Some(42))` -> `"Maximum: 42"` +- `Min(Some(7))` -> `"Minimum: 7"` +- `Or(true)` -> `"Satisfiable: true"` +- `And(false)` -> `"Tautology: false"` +- `Sum(0.9832)` -> `"Sum: 0.9832"` + +**Reduction graph export:** Edge data gains an `edge_kind` field in JSON to distinguish standard from aggregate reductions. + +**Prelude exports:** +- Remove: `OptimizationProblem`, `SatisfactionProblem`, `SolutionSize`, `Direction` +- Add: `Aggregate`, `Max`, `Min`, `Sum`, `Or`, `And`, `ReduceToAggregate`, `AggregateReductionResult` + +### Model migration examples + +**Optimization:** +```rust +// Before: +impl Problem for MaximumIndependentSet { + type Metric = SolutionSize; + fn evaluate(&self, config: &[usize]) -> SolutionSize { + if invalid { SolutionSize::Invalid } else { SolutionSize::Valid(size) } + } +} +impl OptimizationProblem for MaximumIndependentSet { + type Value = W::Sum; + fn direction(&self) -> Direction { Direction::Maximize } +} + +// After: +impl Problem for MaximumIndependentSet { + type Value = Max; + fn evaluate(&self, config: &[usize]) -> Max { + if invalid { Max(None) } else { Max(Some(size)) } + } +} +``` + +**Satisfaction:** +```rust +// Before: +impl Problem for Satisfiability { + type Metric = bool; + fn evaluate(&self, config: &[usize]) -> bool { satisfies } +} +impl SatisfactionProblem for Satisfiability {} + +// After: +impl Problem for Satisfiability { + type Value = Or; + fn evaluate(&self, config: &[usize]) -> Or { Or(satisfies) } +} +``` + +**Counting (new):** +```rust +impl Problem for NetworkReliability { + type Value = Sum; + fn evaluate(&self, config: &[usize]) -> Sum { + if terminals_connected { Sum(probability_weight) } else { Sum(0.0) } + } +} +``` + +### Migration scope + +| Area | Change type | Scope | +|------|-------------|-------| +| ~80 model files | Mechanical find-and-replace | `type Metric` -> `type Value`, `SolutionSize` -> `Max`/`Min`, remove `impl OptimizationProblem`/`SatisfactionProblem` blocks | +| ~100 test files | Mechanical | Update assertions, `find_best` -> `solve`, `SolutionSize::Valid(x)` -> `Max(Some(x))` | +| `src/traits.rs` | Rewrite | Remove leaf traits, rename `Metric` to `Value`, add `Aggregate` bound | +| `src/types.rs` | Rewrite | Replace `SolutionSize`/`Direction` with `Max`/`Min`/`Sum`/`Or`/`And` + `Aggregate` trait | +| `src/solvers/` | Rewrite | Single `solve` method via fold | +| `src/rules/traits.rs` | Extend | Add `ReduceToAggregate` / `AggregateReductionResult` | +| `problemreductions-macros/` | Simplify | Remove `SolverKind`, single codegen path, extend `#[reduction]` for `ReduceToAggregate` | +| Reduction graph / CLI | Minor | Edge kind field, simplified solve dispatch | +| Paper (`docs/paper/`) | None | Unaffected | + +## What is NOT changed + +- Reduction graph traversal logic +- Problem name/variant/alias system +- CLI command structure +- Paper (docs/paper/reductions.typ) +- `DeclaredVariant` marker trait + +## Alternatives considered + +1. **Minimal CountingProblem extension** (previous spec) — adds a third parallel leaf trait. Simpler but grows the parallel branching. Superseded by this design. + +2. **Fully unified reductions** — push unification into reductions too via associated types on `Aggregate`. Over-engineers: config-mapping and value-mapping reductions are genuinely different operations. + +3. **`Metric = f64` for counting** — no wrapper type, loses type safety. The aggregation-type-as-data-type design makes intent explicit everywhere. + +## Related issues + +- #737 — Original issue tracking this design +- #748 — DefaultSolver per problem (future, orthogonal) +- #235, #237, #404, #405 — Counting models unblocked by this design +- #256, #257, #394, #395 — Counting rules unblocked by this design