CodingThrust
diff --git a/‎.claude/CLAUDE.md‎
Lines changed: 21 additions & 22 deletions b/‎.claude/CLAUDE.md‎
Lines changed: 21 additions & 22 deletions
diff --git a/‎.claude/skills/add-model/SKILL.md‎
Lines changed: 23 additions & 21 deletions b/‎.claude/skills/add-model/SKILL.md‎
Lines changed: 23 additions & 21 deletions
@@ -87,9 +87,9 @@ make release V=x.y.z  # Tag and push a new release (CI publishes to crates.io)
   - `misc/` - Unique input structures
   - Run `pred list` for the full catalog of problems, variants, and reductions; `pred show <name>` for details on a specific problem
 - `src/rules/` - Reduction rules + inventory registration
-- `src/solvers/` - BruteForce solver, ILP solver (feature-gated). To check if a problem supports ILP solving (via reduction path), run `pred path <ProblemName> ILP`
-- `src/traits.rs` - `Problem`, `OptimizationProblem`, `SatisfactionProblem` traits
-- `src/rules/traits.rs` - `ReduceTo<T>`, `ReductionResult` traits
+- `src/solvers/` - BruteForce solver for aggregate values plus witness recovery when supported, ILP solver (feature-gated, witness-only). To check if a problem supports ILP solving via a witness-capable reduction path, run `pred path <ProblemName> ILP`
+- `src/traits.rs` - `Problem` trait
+- `src/rules/traits.rs` - `ReduceTo<T>`, `ReduceToAggregate<T>`, `ReductionResult`, `AggregateReductionResult` traits
 - `src/registry/` - Compile-time reduction metadata collection
 - `problemreductions-cli/` - `pred` CLI tool (separate crate in workspace)
 - `src/unit_tests/` - Unit test files (mirroring `src/` structure, referenced via `#[path]`)
@@ -104,36 +104,33 @@ make release V=x.y.z  # Tag and push a new release (CI publishes to crates.io)
 Problem (core trait — all problems must implement)
 │
 ├── const NAME: &'static str           // e.g., "MaximumIndependentSet"
-├── type Metric: Clone                 // SolutionSize<W> for optimization, bool for satisfaction
+├── type Value: Clone                  // aggregate value: Max/Min/Sum/Or/And/Extremum/...
 ├── fn dims(&self) -> Vec<usize>       // config space: [2, 2, 2] for 3 binary variables
-├── fn evaluate(&self, config) -> Metric
+├── fn evaluate(&self, config) -> Value
 ├── fn variant() -> Vec<(&str, &str)>  // e.g., [("graph","SimpleGraph"), ("weight","i32")]
 ├── fn num_variables(&self) -> usize   // default: dims().len()
 └── fn problem_type() -> ProblemType   // catalog bridge: registry lookup by NAME
+```
 
-OptimizationProblem : Problem<Metric = SolutionSize<Self::Value>> (extension for optimization)
-│
-├── type Value: PartialOrd + Clone     // inner objective type (i32, f64, etc.)
-└── fn direction(&self) -> Direction   // Maximize or Minimize
+**Witness-capable objective problems** (e.g., `MaximumIndependentSet`) typically use `Value = Max<W::Sum>`, `Min<W::Sum>`, or `Extremum<W::Sum>`.
 
-SatisfactionProblem : Problem<Metric = bool> (marker trait for decision problems)
-```
+**Witness-capable feasibility problems** (e.g., `Satisfiability`) typically use `Value = Or`.
 
-**Satisfaction problems** (e.g., `Satisfiability`) use `Metric = bool` and implement `SatisfactionProblem`.
+**Aggregate-only problems** use fold values such as `Sum<W>` or `And`; these solve to a value but have no representative witness configuration.
 
-**Optimization problems** (e.g., `MaximumIndependentSet`) use `Metric = SolutionSize<W>` where:
+Common aggregate wrappers live in `src/types.rs`:
 ```rust
-enum SolutionSize<T> { Valid(T), Invalid }  // Invalid = infeasible config
-enum Direction { Maximize, Minimize }
+Max<V>, Min<V>, Sum<W>, Or, And, Extremum<V>, ExtremumSense
 ```
 
 ### Key Patterns
 - `variant_params!` macro implements `Problem::variant()` — e.g., `crate::variant_params![G, W]` for two type params, `crate::variant_params![]` for none (see `src/variant.rs`)
-- `declare_variants!` proc macro registers concrete type instantiations with best-known complexity and registry-backed dynamic dispatch metadata — every entry must specify `opt` or `sat`, and one entry per problem may be marked `default` (see `src/models/graph/maximum_independent_set.rs`). Variable names in complexity strings are validated at compile time against actual getter methods.
+- `declare_variants!` proc macro registers concrete type instantiations with best-known complexity and registry-backed load/serialize/value-solve/witness-solve metadata. One entry per problem may be marked `default`, and variable names in complexity strings are validated at compile time against actual getter methods.
 - Problems parameterized by graph type `G` and optionally weight type `W` (problem-dependent)
-- `ReductionResult` provides `target_problem()` and `extract_solution()`
-- `Solver::find_best()` → `Option<Vec<usize>>` for optimization problems; `Solver::find_satisfying()` → `Option<Vec<usize>>` for `Metric = bool`
-- `BruteForce::find_all_best()` / `find_all_satisfying()` return `Vec<Vec<usize>>` for all optimal/satisfying solutions
+- `Solver::solve()` computes the aggregate value for any `Problem` whose `Value` implements `Aggregate`
+- `BruteForce::find_witness()` / `find_all_witnesses()` recover witnesses only when `P::Value::supports_witnesses()`
+- `ReductionResult` provides `target_problem()` and `extract_solution()` for witness/config workflows; `AggregateReductionResult` provides `extract_value()` for aggregate/value workflows
+- CLI-facing dynamic formatting uses aggregate wrapper names directly (for example `Max(2)`, `Min(None)`, `Or(true)`, or `Sum(56)`)
 - Graph types: SimpleGraph, PlanarGraph, BipartiteGraph, UnitDiskGraph, KingsSubgraph, TriangularSubgraph
 - Weight types: `One` (unit weight marker), `i32`, `f64` — all implement `WeightElement` trait
 - `WeightElement` trait: `type Sum: NumericSize` + `fn to_sum(&self)` — converts weight to a summable numeric type
@@ -170,10 +167,12 @@ Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
 - Default variant ranking: `SimpleGraph`, `One`, `KN` are considered default values; variants with the most default values sort first
 - Nodes come exclusively from `#[reduction]` registrations; natural edges between same-name variants are inferred from the graph/weight subtype partial order
 - Each primitive reduction is determined by the exact `(source_variant, target_variant)` endpoint pair
-- `#[reduction]` accepts only `overhead = { ... }`
+- Reduction edges carry `EdgeCapabilities { witness, aggregate }`; graph search defaults to witness mode, and aggregate mode is available through `ReductionMode::Aggregate`
+- `#[reduction]` accepts only `overhead = { ... }` and currently registers witness/config reductions; aggregate-only edges require manual `ReductionEntry` registration with `reduce_aggregate_fn`
 
 ### Extension Points
 - New models register dynamic load/serialize/brute-force dispatch through `declare_variants!` in the model file, not by adding manual match arms in the CLI
+- Aggregate-only models are first-class in `declare_variants!`; aggregate-only reduction edges still need manual `ReductionEntry` wiring because `#[reduction]` only registers witness/config reductions today
 - Exact registry dispatch lives in `src/registry/`; alias resolution and partial/default variant resolution live in `problemreductions-cli/src/problem_name.rs`
 - `pred create` UX lives in `problemreductions-cli/src/commands/create.rs`
 - Canonical paper and CLI examples live in `src/example_db/model_builders.rs` and `src/example_db/rule_builders.rs`
@@ -199,8 +198,8 @@ Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
 **Reference implementations — read these first:**
 - **Reduction test:** `src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs` — closed-loop pattern
 - **Model test:** `src/unit_tests/models/graph/maximum_independent_set.rs` — evaluation, serialization
-- **Solver test:** `src/unit_tests/solvers/brute_force.rs` — `find_best` + `find_satisfying`
-- **Trait definitions:** `src/traits.rs` (`Problem`, `OptimizationProblem`), `src/solvers/mod.rs` (`Solver`)
+- **Solver test:** `src/unit_tests/solvers/brute_force.rs` — aggregate `solve()` plus witness recovery helpers
+- **Trait definitions:** `src/traits.rs` (`Problem`), `src/solvers/mod.rs` (`Solver`)
 
 ### Coverage
 
 
@@ -17,16 +17,16 @@ Before any implementation, collect all required information. If called from `iss
 |---|------|-------------|---------|
 | 1 | **Problem name** | Struct name with optimization prefix | `MaximumClique`, `MinimumDominatingSet` |
 | 2 | **Mathematical definition** | Formal definition with objective/constraints | "Given graph G=(V,E), find max-weight subset S where all pairs in S are adjacent" |
-| 3 | **Problem type** | Optimization (maximize/minimize) or satisfaction | Optimization (Maximize) |
+| 3 | **Problem type** | Objective (`Max`/`Min`), witness (`bool`), or aggregate-only (`Sum`/`And`/custom `Aggregate`) | Objective (Maximize) |
 | 4 | **Type parameters** | Graph type `G`, weight type `W`, or other | `G: Graph`, `W: WeightElement` |
 | 5 | **Struct fields** | What the struct holds | `graph: G`, `weights: Vec<W>` |
 | 6 | **Configuration space** | What `dims()` returns | `vec![2; num_vertices]` for binary vertex selection |
 | 7 | **Feasibility check** | How to validate a configuration | "All selected vertices must be pairwise adjacent" |
-| 8 | **Objective function** | How to compute the metric | "Sum of weights of selected vertices" |
+| 8 | **Per-configuration value** | How `evaluate()` computes the aggregate contribution | "Return `Max(Some(total_weight))` for feasible configs" |
 | 9 | **Best known exact algorithm** | Complexity with variable definitions | "O(1.1996^n) by Xiao & Nagamochi (2017), where n = \|V\|" |
 | 10 | **Solving strategy** | How it can be solved | "BruteForce works; ILP reduction available" |
 | 11 | **Category** | Which sub-module under `src/models/` | `graph`, `formula`, `set`, `algebraic`, `misc` |
-| 12 | **Expected outcome from the issue** | Concrete outcome for the issue's example instance | Optimization: one optimal solution + optimal value. Satisfaction: one valid/satisfying solution + why it is valid |
+| 12 | **Expected outcome from the issue** | Concrete outcome for the issue's example instance | Objective: one optimal solution + optimal value. Witness: one valid/satisfying solution + why it is valid. Aggregate-only: the final aggregate value and how it is derived |
 
 If any item is missing, ask the user to provide it. Do NOT proceed until the checklist is complete.
 
@@ -61,7 +61,7 @@ Read these first to understand the patterns:
 - **Optimization problem:** `src/models/graph/maximum_independent_set.rs`
 - **Satisfaction problem:** `src/models/formula/sat.rs`
 - **Model tests:** `src/unit_tests/models/graph/maximum_independent_set.rs`
-- **Trait definitions:** `src/traits.rs` (`Problem`, `OptimizationProblem`, `SatisfactionProblem`)
+- **Trait definitions / aggregate types:** `src/traits.rs` (`Problem`), `src/types.rs` (`Aggregate`, `Max`, `Min`, `Sum`, `Or`, `And`, `Extremum`)
 - **Registry dispatch boundary:** `src/registry/mod.rs`, `src/registry/variant.rs`
 - **CLI aliases:** `problemreductions-cli/src/problem_name.rs`
 - **CLI creation:** `problemreductions-cli/src/commands/create.rs`
@@ -71,7 +71,8 @@ Read these first to understand the patterns:
 
 Before implementing, make sure the plan explicitly covers these items that structural review checks later:
 - `ProblemSchemaEntry` metadata is complete for the current schema shape (`display_name`, `aliases`, `dimensions`, and constructor-facing `fields`)
-- `declare_variants!` is present with the correct `opt`/`sat` marker and exactly one `default` variant when multiple concrete variants exist
+- `Problem::Value` uses the correct aggregate wrapper and witness support is intentional
+- `declare_variants!` is present with exactly one `default` variant when multiple concrete variants exist
 - CLI discovery and `pred create <ProblemName>` support are included where applicable
 - A canonical model example is registered for example-db / `pred create --example`
 - `docs/paper/reductions.typ` adds both the display-name dictionary entry and the `problem-def(...)`
@@ -110,34 +111,32 @@ Create `src/models/<category>/<name>.rs`:
 // 1. inventory::submit! for ProblemSchemaEntry
 // 2. Struct definition with #[derive(Debug, Clone, Serialize, Deserialize)]
 // 3. Constructor (new) + accessor methods
-// 4. Problem trait impl (NAME, Metric, dims, evaluate, variant)
-// 5. OptimizationProblem or SatisfactionProblem impl
-// 6. #[cfg(test)] #[path = "..."] mod tests;
+// 4. Problem trait impl (NAME, Value, dims, evaluate, variant)
+// 5. #[cfg(test)] #[path = "..."] mod tests;
 ```
 
 Key decisions:
 - **Schema metadata:** `ProblemSchemaEntry` must reflect the current registry schema shape, including `display_name`, `aliases`, `dimensions`, and constructor-facing `fields`
-- **Optimization problems:** `type Metric = SolutionSize<W::Sum>`, implement `OptimizationProblem` with `direction()`
-- **Satisfaction problems:** `type Metric = bool`, implement `SatisfactionProblem` (marker trait)
+- **Objective problems:** use `type Value = Max<_>`, `Min<_>`, or `Extremum<_>` when the model should expose optimization-style witness helpers
+- **Witness problems:** use `type Value = Or` for existential feasibility problems
+- **Aggregate-only problems:** use a value-only aggregate such as `Sum<_>`, `And`, or a custom `Aggregate` when witnesses are not meaningful
 - **Weight management:** use inherent methods (`weights()`, `set_weights()`, `is_weighted()`), NOT traits
 - **`dims()`:** returns the configuration space dimensions (e.g., `vec![2; n]` for binary variables)
-- **`evaluate()`:** must check feasibility first, then compute objective
+- **`evaluate()`:** must return the per-configuration aggregate value. For models with invalid configs, check feasibility first and return the appropriate invalid/false contribution
 - **`variant()`:** use the `variant_params!` macro — e.g., `crate::variant_params![G, W]` for `Problem<G, W>`, or `crate::variant_params![]` for problems with no type parameters. Each type parameter must implement `VariantParam` (already done for standard types like `SimpleGraph`, `i32`, `One`). See `src/variant.rs`.
+- **Solve surface:** `Solver::solve()` always computes the aggregate value. `pred solve problem.json` prints a `Solution` only when a witness exists; `pred solve bundle.json` and `--solver ilp` remain witness-only workflows
 
 ## Step 2.5: Register variant complexity
 
 Add `declare_variants!` at the bottom of the model file (after the trait impls, before the test link). Each line declares a concrete type instantiation with its best-known worst-case complexity:
 
 ```rust
 crate::declare_variants! {
-    opt ProblemName<SimpleGraph, i32> => "1.1996^num_vertices",
-    default opt ProblemName<SimpleGraph, One> => "1.1996^num_vertices",
+    ProblemName<SimpleGraph, i32> => "1.1996^num_vertices",
+    default ProblemName<SimpleGraph, One> => "1.1996^num_vertices",
 }
 ```
 
-- Each entry must include an explicit solver kind:
-  - `opt` for optimization problems (`BruteForce::find_best`)
-  - `sat` for satisfaction problems (`BruteForce::find_satisfying`)
 - Mark exactly one concrete variant `default` when the problem has multiple registered variants
 - The complexity string references the getter method names from Step 1.5 (e.g., `num_vertices`) — variable names are validated at compile time against actual getters, so typos cause compile errors
 - One entry per supported `(graph, weight)` combination
@@ -146,6 +145,8 @@ crate::declare_variants! {
 - A compiled `complexity_eval_fn` plus registry-backed load/serialize/solve dispatch metadata are auto-generated alongside the symbolic expression
 - See `src/models/graph/maximum_independent_set.rs` for the reference pattern
 
+`declare_variants!` now handles objective, witness-capable, and aggregate-only models uniformly. Use manual `VariantEntry` wiring only for unusual dynamic-registration work, not for ordinary models.
+
 ## Step 3: Register the model
 
 Update these files to register the new problem type:
@@ -160,7 +161,6 @@ The CLI now loads, serializes, and brute-force solves problems through the core
 
 1. **Registry-backed dispatch comes from `declare_variants!`:**
    - Make sure every concrete variant you want the CLI to load is listed in `declare_variants!`
-   - Use the correct `opt`/`sat` marker per entry
    - Mark the intended default variant with `default` when applicable
 
 2. **`problemreductions-cli/src/problem_name.rs`:**
@@ -200,9 +200,9 @@ Create `src/unit_tests/models/<category>/<name>.rs`:
 Every model needs **at least 3 test functions** (the structural reviewer enforces this). Choose from the coverage areas below — pick whichever are relevant to the model:
 
 - **Creation/basic** — exercise constructor inputs, key accessors, `dims()` / `num_variables()`.
-- **Evaluation** — valid and invalid configs so the feasibility boundary is explicit.
-- **Direction** — verify optimization direction (optimization problems only).
-- **Solver** — brute-force solver finds correct solutions (when the model is small enough).
+- **Evaluation** — valid and invalid configs so the feasibility boundary or aggregate contribution is explicit.
+- **Direction / sense** — verify runtime optimization sense only for models that use `Extremum<_>`.
+- **Solver** — brute-force `solve()` returns the correct aggregate value; if witnesses are supported, verify `find_witness()` / `find_all_witnesses()` as well.
 - **Serialization** — round-trip serde (when the model is used in CLI/example-db flows).
 - **Paper example** — verify the worked example from the paper entry (see below).
 
@@ -280,9 +280,11 @@ Structural and quality review is handled by the `review-pipeline` stage, not her
 | Forgetting `inventory::submit!` | Every problem needs a `ProblemSchemaEntry` registration |
 | Missing `#[path]` test link | Add `#[cfg(test)] #[path = "..."] mod tests;` at file bottom |
 | Wrong `dims()` | Must match the actual configuration space (e.g., `vec![2; n]` for binary) |
+| Using the wrong aggregate wrapper | Objective models use `Max` / `Min` / `Extremum`, witness models use `bool`, aggregate-only models use a fold value like `Sum` / `And` |
 | Not registering in `mod.rs` | Must update both `<category>/mod.rs` and `models/mod.rs` |
 | Forgetting `declare_variants!` | Required for variant complexity metadata and registry-backed load/serialize/solve dispatch |
-| Wrong `declare_variants!` syntax | Every entry now needs `opt` or `sat`; one entry per problem may be marked `default` |
+| Wrong aggregate wrapper | Use `Max` / `Min` / `Extremum` for objective problems, `Or` for existential witness problems, and `Sum` / `And` (or a custom aggregate) for value-only folds |
+| Wrong `declare_variants!` syntax | Entries no longer use `opt` / `sat`; one entry per problem may be marked `default` |
 | Forgetting CLI alias | Must add lowercase entry in `problem_name.rs` `resolve_alias()` |
 | Inventing short aliases | Only use well-established literature abbreviations (MIS, SAT, TSP); do NOT invent new ones |
 | Forgetting CLI create | Must add creation handler in `commands/create.rs` and flags in `cli.rs` |