You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
feat: Decision wrapper for optimization→decision conversion (#1014)
* docs: add Decision wrapper design spec and implementation plan
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* feat: add OptimizationValue trait for Min/Max decision conversion
* feat: add Decision<P> generic wrapper with Problem impl
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* feat: add ReduceToAggregate<P> impl for Decision<P>
Implements the aggregate reduction from Decision<P> to P that
extracts the optimization value by comparing against the threshold.
This is Task 3 of the decision-wrapper plan.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* fix: extract_type_name handles Decision<T> nested generics
* feat: register Decision variants for MVC and MDS
* refactor: remove hand-written VertexCover, replaced by Decision<MinimumVertexCover>
* feat: add golden-section search solver via Decision queries
* docs: migrate VertexCover paper entry and example_db to DecisionMinimumVertexCover
* chore: integration fixups for Decision wrapper
* fix: address PR #1014 review comments and quality issues
- Add register_decision_variant! macro to reduce per-type boilerplate (~80 lines each for MVC/MDS)
- Add Decision<MinimumDominatingSet> behavioral tests (creation, evaluate, reduction, solver)
- Add boundary test for reduce_to_aggregate with infeasible bound
- Rename golden_section.rs to decision_search.rs (binary search, not golden section)
- Fix schema-driven CLI creation for Decision types (restructure flat JSON to nested {inner, bound})
- Add canonical rule example specs for Decision→Optimization aggregate edges
- Update example_db test to handle aggregate-only reduction paths
- Filter trivial Decision<P>↔P edges from paper completeness check
- Remove plan files
- Generalize DecisionProblemMeta to blanket impl per optimization model
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* fix: relax flaky kclique_ilp assertion (ILP may return larger valid clique)
The K4 graph with k=3 has both size-3 and size-4 valid cliques.
The ILP solver nondeterministically picks either, so assert >= k
instead of == k.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* feat: add Turing (multi-query) reduction edges for Optimization → Decision
Registers P → Decision<P> as a Turing reduction edge — representing
that solving an optimization problem via its decision version requires
multiple adaptive queries (binary search over the bound).
- Add `turing` field to EdgeCapabilities and ReductionMode::Turing
- Register reverse Turing edges in register_decision_variant! macro
- Export turing flag in JSON graph
- Turing edges excluded from rule example coverage (no single-shot demo)
- Add tests for MVC→DecisionMVC and MDS→DecisionMDS Turing edges
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* refactor: parameterize register_decision_variant! size fields
The macro previously hardcoded num_vertices/num_edges as size getters,
which only works for graph problems. Now accepts dims, fields, and
size_getters as parameters so non-graph Decision variants can specify
their own problem-size fields (e.g., num_vars/num_clauses for SAT).
Callers define inherent methods on Decision<P> before invoking the macro.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* docs: update CLAUDE.md and add-model skill for Decision wrapper
- Document Decision<P> wrapper, OptimizationValue trait, decision_search solver
- Document EdgeCapabilities.turing field and ReductionMode::Turing
- Document register_decision_variant! macro with dims/fields/size_getters params
- Document Decision↔P completeness filter in paper section
- Add anti-pattern entry in add-model skill: use Decision<P> not hand-written models
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* fix: CLI compat for Decision types (--k alias, MDS example)
- Map --k to --bound for Decision types in schema_field_flag_keys
so `pred create VC --k 2` works (backward compat with old VertexCover)
- Add canonical model example for DecisionMinimumDominatingSet
so `pred create --example DecisionMinimumDominatingSet` works
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* refactor: remove backward-compat aliases (VertexCover/VC/--k)
Breaking changes are allowed at this stage. Remove:
- VertexCover and VC aliases from DecisionMinimumVertexCover schema
- --k → --bound mapping for Decision types
- Replace with DMVC alias
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
* fix: Typst syntax errors in paper completeness filter
- Use if/else instead of `not ... and` (Typst precedence issue)
- Fix RR_ge → RR_(gt.eq 0) in DecisionMVC math notation
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
-`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/solvers/` - BruteForce solver for aggregate values plus witness recovery when supported, ILP solver (feature-gated, witness-only), decision search (binary search via Decision queries). To check if a problem supports ILP solving via a witness-capable reduction path, run `pred path <ProblemName> ILP`
@@ -122,14 +123,22 @@ Problem (core trait — all problems must implement)
122
123
123
124
**Aggregate-only problems** use fold values such as `Sum<W>` or `And`; these solve to a value but have no representative witness configuration.
124
125
126
+
**Decision problems** wrap an optimization problem with a bound: `Decision<P>` where `P::Value: OptimizationValue`. Evaluates to `Or(true)` when the inner objective meets the bound (≤ for Min, ≥ for Max).
`OptimizationValue` trait (in `src/types.rs`) enables generic Decision conversion:
134
+
-`Min<V>`: meets bound when value ≤ bound
135
+
-`Max<V>`: meets bound when value ≥ bound
136
+
130
137
### Key Patterns
131
138
-`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`)
132
139
-`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.
140
+
-`decision_problem_meta!` macro registers `DecisionProblemMeta` for a concrete inner type, providing the `DECISION_NAME` constant.
141
+
-`register_decision_variant!` macro generates `declare_variants!`, `ProblemSchemaEntry`, and both `ReductionEntry` submissions (aggregate Decision→Opt + Turing Opt→Decision) for a `Decision<P>` variant. Callers must define inherent getters (`num_vertices()`, `num_edges()`, `k()`) on `Decision<P>` before invoking. Accepts `dims`, `fields`, and `size_getters` parameters for problem-specific size fields.
133
142
- Problems parameterized by graph type `G` and optionally weight type `W` (problem-dependent)
134
143
-`Solver::solve()` computes the aggregate value for any `Problem` whose `Value` implements `Aggregate`
135
144
-`BruteForce::find_witness()` / `find_all_witnesses()` recover witnesses only when `P::Value::supports_witnesses()`
@@ -171,14 +180,16 @@ Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
171
180
- Default variant ranking: `SimpleGraph`, `One`, `KN` are considered default values; variants with the most default values sort first
172
181
- Nodes come exclusively from `#[reduction]` registrations; natural edges between same-name variants are inferred from the graph/weight subtype partial order
173
182
- Each primitive reduction is determined by the exact `(source_variant, target_variant)` endpoint pair
174
-
- Reduction edges carry `EdgeCapabilities { witness, aggregate }`; graph search defaults to witness mode, and aggregate mode is available through `ReductionMode::Aggregate`
175
-
-`#[reduction]` accepts only `overhead = { ... }` and currently registers witness/config reductions; aggregate-only edges require manual `ReductionEntry` registration with `reduce_aggregate_fn`
183
+
- Reduction edges carry `EdgeCapabilities { witness, aggregate, turing }`; graph search defaults to witness mode, aggregate mode is available through `ReductionMode::Aggregate`, and Turing (multi-query) mode via `ReductionMode::Turing`
184
+
-`#[reduction]` accepts only `overhead = { ... }` and currently registers witness/config reductions; aggregate-only and Turing edges require manual `ReductionEntry` registration
185
+
-`Decision<P> → P` is an aggregate-only edge (solve optimization, compare to bound); `P → Decision<P>` is a Turing edge (binary search over decision bound)
176
186
177
187
### Extension Points
178
188
- 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
179
189
-**CLI creation is schema-driven:**`pred create` automatically maps `ProblemSchemaEntry` fields to CLI flags via `snake_case → kebab-case` convention. New models need only: (1) matching CLI flags in `CreateArgs` + `flag_map()`, and (2) type parser support in `parse_field_value()` if using a new field type. No match arm in `create.rs` is needed.
180
190
-**CLI flag names must match schema field names.** The canonical name for a CLI flag is the schema field name in kebab-case (e.g., schema field `universe_size` → `--universe-size`, field `subsets` → `--subsets`). Old aliases (e.g., `--universe`, `--sets`) may exist as clap `alias` for backward compatibility at the clap level, but `flag_map()`, help text, error messages, and documentation must use the schema-derived name. Do not add new backward-compat aliases; if a field is renamed in the schema, update the CLI flag name to match.
181
-
- 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
191
+
-**Decision variants** of optimization problems use `Decision<P>` wrapper. Add via: (1) `decision_problem_meta!` for the inner type, (2) inherent methods on `Decision<Inner>`, (3) `register_decision_variant!` with `dims`, `fields`, `size_getters`. Schema-driven CLI creation auto-restructures flat JSON into `{inner: {...}, bound}`.
192
+
- Aggregate-only models are first-class in `declare_variants!`; aggregate-only and Turing reduction edges still need manual `ReductionEntry` wiring because `#[reduction]` only registers witness/config reductions today
182
193
- Exact registry dispatch lives in `src/registry/`; alias resolution and partial/default variant resolution live in `problemreductions-cli/src/problem_name.rs`
183
194
-`pred create` schema-driven dispatch lives in `problemreductions-cli/src/commands/create.rs` (`create_schema_driven()`)
184
195
- Canonical paper and CLI examples live in `src/example_db/model_builders.rs` and `src/example_db/rule_builders.rs`
@@ -195,8 +206,8 @@ Reduction graph nodes use variant key-value pairs from `Problem::variant()`:
195
206
### Paper (docs/paper/reductions.typ)
196
207
-`problem-def(name)[def][body]` — defines a problem with auto-generated schema, reductions list, and label `<def:ProblemName>`. Title comes from `display-name` dict.
197
208
-`reduction-rule(source, target, example: bool, ...)[rule][proof]` — generates a theorem with label `<thm:Source-to-Target>` and registers in `covered-rules` state. Overhead auto-derived from JSON edge data.
198
-
- Every directed reduction needs its own `reduction-rule` entry
199
-
- Completeness warnings auto-check that all JSON graph nodes/edges are covered in the paper
209
+
- Every directed reduction needs its own `reduction-rule` entry (except trivial Decision↔Optimization pairs which are auto-filtered)
210
+
- Completeness warnings auto-check that all JSON graph nodes/edges are covered in the paper; `Decision<P> ↔ P` edges are excluded since they are trivial solve-and-compare reductions
200
211
-`display-name` dict maps `ProblemName` to display text
Copy file name to clipboardExpand all lines: .claude/skills/add-model/SKILL.md
+1Lines changed: 1 addition & 0 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -311,6 +311,7 @@ Structural and quality review is handled by the `review-pipeline` stage, not her
311
311
| 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 |
312
312
| Wrong `declare_variants!` syntax | Entries no longer use `opt` / `sat`; one entry per problem may be marked `default`|
313
313
| Forgetting CLI alias | Must add lowercase entry in `problem_name.rs``resolve_alias()`|
314
+
| Adding a hand-written decision model | Use `Decision<P>` wrapper instead — see `decision_problem_meta!` + `register_decision_variant!` in `src/models/graph/minimum_vertex_cover.rs` for the pattern |
314
315
| Inventing short aliases | Only use well-established literature abbreviations (MIS, SAT, TSP); do NOT invent new ones |
315
316
| Forgetting CLI flags | Schema-driven create needs matching CLI flags in `CreateArgs` for each `ProblemSchemaEntry` field (snake_case → kebab-case). Also add to `flag_map()`. |
316
317
| Missing type parser | If the problem uses a new field type, add a handler in `parse_field_value()` in `create.rs`|
@@ -649,22 +659,23 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
649
659
}
650
660
651
661
#{
652
-
let x = load-model-example("VertexCover")
662
+
let x = load-model-example("DecisionMinimumVertexCover")
663
+
let inner = x.instance.inner
653
664
let nv = graph-num-vertices(x.instance)
654
665
let ne = graph-num-edges(x.instance)
655
-
let k = x.instance.k
666
+
let k = x.instance.bound
656
667
let sol = x.optimal_config
657
668
let cover = sol.enumerate().filter(((i, v)) => v == 1).map(((i, _)) => i)
658
669
[
659
-
#problem-def("VertexCover")[
660
-
Given an undirected graph $G = (V, E)$ and a positive integer $k <= |V|$, determine whether there exists a vertex cover of size at most $k$: a subset $V' subset.eq V$ with $|V'| <= k$ such that for each edge ${u, v} in E$, at least one of $u, v$ belongs to $V'$.
670
+
#problem-def("DecisionMinimumVertexCover")[
671
+
Given an undirected graph $G = (V, E)$ with vertex weights $w: V -> RR_(gt.eq 0)$ and an integer bound $k$, determine whether there exists a vertex cover $S subset.eq V$ with $sum_(v in S) w(v) <= k$ such that every edge has at least one endpoint in $S$.
661
672
][
662
-
Vertex Cover is one of Karp's 21 NP-complete problems @karp1972 and the decision version of Minimum Vertex Cover @garey1979. The best known exact algorithm runs in $O^*(1.1996^n)$ time (Chen, Kanj, and Xia, 2010).
673
+
Decision Minimum Vertex Cover is the decision version of Minimum Vertex Cover and one of Karp's 21 NP-complete problems @karp1972 @garey1979. It asks whether the optimization objective can be achieved within a prescribed budget rather than minimizing the cover weight directly.
663
674
664
-
*Example.* Consider a graph on $n = #nv$ vertices and $|E| = #ne$ edges with threshold $k = #k$. The cover $V' = {#cover.map(i => $v_#i$).join(", ")}$ with $|V'| = #cover.len() <= k$ is a valid vertex cover.
675
+
*Example.* Consider a graph on $n = #nv$ vertices and $|E| = #ne$ edges with threshold $k = #k$. The cover $S = {#cover.map(i => $v_#i$).join(", ")}$ has total weight $2 <= #k$ and therefore certifies a yes-instance.
0 commit comments