add-rule

name	add-rule
description	Use when adding a new reduction rule to the codebase, either from an issue or interactively

Add Rule

Step-by-step guide for adding a new reduction rule (A -> B) to the codebase. By default, every rule goes through mathematical verification (via /verify-reduction) before implementation. Pass --no-verify to skip verification for trivial reductions.

Invocation

/add-rule                     # interactive, with verification (default)
/add-rule --no-verify         # interactive, skip verification

When called from /issue-to-pr, the --no-verify flag is passed through if present.

Step 0: Gather Required Information

Before any implementation, collect all required information. If called from issue-to-pr, the issue should already provide these. If used standalone, brainstorm with the user to fill in every item below.

Required Information Checklist

#	Item	Description	Example
1	Source problem	The problem being reduced FROM (must already exist)	MinimumVertexCover<SimpleGraph, i32>
2	Target problem	The problem being reduced TO (must already exist)	MaximumIndependentSet<SimpleGraph, i32>
3	Reduction algorithm	How to transform source instance to target	"Copy graph and weights; IS on same graph as VC"
4	Solution extraction	How to map target solution back to source	"Complement: 1 - x for each variable"
5	Correctness argument	Why the reduction preserves optimality	"S is independent set iff V\S is vertex cover"
6	Size overhead	How target size relates to source size	num_vertices = "num_vertices", num_edges = "num_edges"
7	Concrete example	A small worked-out instance (tutorial style, clear intuition)	"Triangle graph: VC={0,1} -> IS={2}"
8	Solving strategy	How to solve the target problem	"BruteForce, or existing ILP reduction"
9	Reference	Paper, textbook, or URL for the reduction	URL or citation

If any item is missing, ask the user to provide it. Put a high standard on item 7 (concrete example): it must be in tutorial style with clear intuition and easy to understand. Do NOT proceed until the checklist is complete.

Step 0.5: Type Compatibility Gate

Check source/target Value types before any work:

grep "type Value = " src/models/*/<source_file>.rs src/models/*/<target_file>.rs

Compatible pairs for ReduceTo (witness-capable):

• Or->Or, Min->Min, Max->Max (same type)
• Or->Min, Or->Max (feasibility embeds into optimization)

Incompatible — STOP if any of these:

• Min->Or or Max->Or — optimization source has no threshold K; needs a decision-variant source model
• Max->Min or Min->Max — opposite optimization directions; needs ReduceToAggregate or a decision-variant wrapper
• Or->Sum or Min->Sum — Sum is aggregate-only; needs ReduceToAggregate
• Any pair involving And or Sum on the target side

If incompatible, STOP and comment on the issue explaining the type mismatch and options. Do NOT proceed.

Reference Implementations

Read these first to understand the patterns:

• Reduction rule: src/rules/minimumvertexcover_maximumindependentset.rs
• Reduction tests: src/unit_tests/rules/minimumvertexcover_maximumindependentset.rs
• Paper entry: search docs/paper/reductions.typ for MinimumVertexCover MaximumIndependentSet
• Traits: src/rules/traits.rs (ReduceTo<T>, ReduceToAggregate<T>, ReductionResult, AggregateReductionResult)

Step 1: Mathematical Verification (default, skip with --no-verify)

If --no-verify was passed, skip to Step 2.

Invoke the /verify-reduction skill to mathematically verify the reduction before writing Rust code. This runs the full verification pipeline: Typst proof, constructor Python script (>=5000 checks), adversary subagent (>=5000 independent checks), and cross-comparison.

All verification artifacts are ephemeral — they exist only in conversation context and temp files. Nothing is committed to the repository.

If verification FAILS: STOP. Report to user. Do NOT proceed to implementation.

If verification passes, the verified Python reduce() and extract_solution() functions, along with the YES/NO instances, carry forward in conversation context to inform Steps 2-5. Use them as the canonical spec for the Rust implementation.

Step 2: Implement the reduction

Create src/rules/<source>_<target>.rs (all lowercase, no underscores between words within a problem name):

// Required structure:
// 1. ReductionResult struct (holds the target problem + mapping state)
// 2. ReductionResult trait impl (target_problem + extract_solution)
// 3. #[reduction(overhead = { ... })] on ReduceTo impl
// 4. ReduceTo trait impl (reduce_to method)
// 5. #[cfg(test)] #[path = "..."] mod tests;

Key elements:

ReductionResult struct:

#[derive(Debug, Clone)]
pub struct ReductionXToY {
    target: TargetType,
    // any additional mapping state needed for extract_solution
}

ReductionResult trait impl:

impl ReductionResult for ReductionXToY {
    type Source = SourceType;
    type Target = TargetType;
    fn target_problem(&self) -> &Self::Target { &self.target }
    fn extract_solution(&self, target_solution: &[usize]) -> Vec<usize> {
        // Map target solution back to source solution
        // If Step 1 ran: translate the verified Python extract_solution() logic
    }
}

ReduceTo with #[reduction] macro (overhead is required):

#[reduction(overhead = {
    field_name = "source_field",
})]
impl ReduceTo<TargetType> for SourceType {
    type Result = ReductionXToY;
    fn reduce_to(&self) -> Self::Result {
        // If Step 1 ran: translate the verified Python reduce() logic
    }
}

Each primitive reduction is determined by the exact source/target variant pair. Keep one primitive registration per endpoint pair and use only the overhead form of #[reduction].

Aggregate-only reductions: when the rule preserves aggregate values but cannot recover a source witness from a target witness, implement AggregateReductionResult + ReduceToAggregate<T> instead of ReductionResult + ReduceTo<T>. Those edges are not auto-registered by #[reduction] yet; register them manually with ReductionEntry { reduce_aggregate_fn: ..., capabilities: EdgeCapabilities::aggregate_only(), ... }. See src/unit_tests/rules/traits.rs and src/unit_tests/rules/graph.rs for the reference pattern.

Step 3: Register in mod.rs

Add to src/rules/mod.rs:

• mod <source>_<target>;
• If feature-gated (e.g., ILP): wrap with #[cfg(feature = "ilp-solver")]

Step 4: Write unit tests

Create src/unit_tests/rules/<source>_<target>.rs:

Required: closed-loop test (test_<source>_to_<target>_closed_loop):

// 1. Create source problem instance
// 2. Reduce: let reduction = ReduceTo::<Target>::reduce_to(&source);
// 3. Solve target: solver.find_all_witnesses(reduction.target_problem())
// 4. Extract: reduction.extract_solution(&target_sol)
// 5. Verify: extracted solution is valid and optimal for source

If Step 1 ran, use the verified YES/NO instances from conversation context to construct test cases. Include both a feasible (closed-loop) and infeasible (no witnesses) test.

Additional recommended tests:

• Verify target problem structure (correct size, edges, constraints)
• Edge cases (empty graph, single vertex, etc.)
• Weight preservation (if applicable)

For aggregate-only reductions, replace the closed-loop witness test with value-chain tests:

• Solve the target with Solver::solve()
• Map the aggregate value back with extract_value()
• If testing a path, use ReductionGraph::reduce_aggregate_along_path(...)

Link via #[cfg(test)] #[path = "..."] mod tests; at the bottom of the rule file.

Step 5: Add canonical example to example_db

Add a builder function in src/example_db/rule_builders.rs that constructs a small, canonical instance for this reduction. Follow the existing patterns in that file. Register the builder in build_rule_examples().

Step 6: Document in paper (MANDATORY — DO NOT SKIP)

This step is NOT optional. Every reduction rule MUST have a corresponding reduction-rule entry in the paper. Skipping documentation is a blocking error — the PR will be rejected in review. Do not proceed to Step 6 until the paper entry is written and make paper compiles.

Write a reduction-rule entry in docs/paper/reductions.typ. Reference example: search for reduction-rule("KColoring", "QUBO" to see the gold-standard entry — use it as a template. For a minimal example, see MinimumVertexCover -> MaximumIndependentSet.

If Step 1 ran, adapt the verified Typst proof into the paper's macros. Do not rewrite the proof from scratch — reformat it.

6a. Write theorem body (rule statement)

#reduction-rule("Source", "Target",
  example: true,
  example-caption: [Description ($n = ...$, $|E| = ...$)],
)[
  This $O(...)$ reduction @citation constructs [target structure] ... ($n k$ variables indexed by ...).
]

Three parts: complexity with citation, construction summary, overhead hint.

6b. Write proof body

Use these subsections with italic labels:

][
  _Construction._ [Full mathematical construction — enough detail to reimplement]

  _Correctness._ ($arrow.r.double$) If ... ($arrow.l.double$) If ...

  _Variable mapping._ [Only if non-trivial mapping]

  _Solution extraction._ [How to convert target solution back to source]
]

Must be self-contained (all notation defined) and reproducible.

6c. Write worked example (extra block)

Step-by-step walkthrough with concrete numbers from JSON data. Required steps:

1. Show source instance (dimensions, structure, graph visualization if applicable)
2. Walk through construction with intermediate values
3. Verify a concrete solution end-to-end
4. Witness semantics: state that the fixture stores one canonical witness; if multiplicity matters mathematically, explain it from the construction rather than from solutions.len()

Use graph-colors, g-node(), g-edge() for graph visualization — see reference examples.

Reproducibility: The extra: block must start with a pred-commands() call showing the create/reduce/solve/evaluate pipeline. The source-side pred create --example ... spec must be derived from the loaded canonical example data via the helper pattern in write-rule-in-paper; do not hand-write a bare alias and assume the default variant matches.

6d. Build and verify

make paper     # Must compile without errors

Checklist: notation self-contained, complexity cited, overhead consistent, example uses JSON data (not hardcoded), solution verified end-to-end, witness semantics respected, paper compiles.

Step 7: Regenerate exports and verify

cargo run --example export_graph    # Generate reduction_graph.json for docs/paper builds
cargo run --example export_schemas  # Generate problem schemas for docs/paper builds
make regenerate-fixtures            # Regenerate example_db/fixtures/examples.json (slow, needs ILP)
make test clippy                    # Must pass

make regenerate-fixtures is required so the paper can load the new rule's example data from src/example_db/fixtures/examples.json. Without it, the reduction-rule entry in Step 6 will reference missing fixture data.

Structural and quality review is handled by the review-pipeline stage, not here. The run stage just needs to produce working code.

Solver Rules

• If the target problem already has a solver, use it directly.
• If the solving strategy requires ILP, implement the ILP reduction rule alongside (feature-gated under ilp-solver).
• A direct-to-ILP rule is a production reduction, not a stub. Match the completeness bar used by strong ILP reductions in this repo: exact overhead metadata, structure + closed-loop + extraction tests, weighted/infeasible/pathological regressions whenever the semantics require them, and ILP-enabled workspace verification.
• When this rule is the companion to a [Model] issue that explicitly claims ILP solvability, it belongs in the same PR as the model.
• If a custom solver is needed, implement in src/solvers/ and document.

CLI Impact

Adding a witness-preserving reduction rule does NOT require CLI changes -- the reduction graph is auto-generated from #[reduction] macros and the CLI discovers paths dynamically. However, both source and target models must already be fully registered through their model files (declare_variants!), aliases as needed in problem_name.rs, and pred create support where applicable (see add-model skill).

Aggregate-only reductions currently have a narrower CLI surface:

• pred solve <problem.json> can still compute direct aggregate values for aggregate-only problems
• pred reduce and pred solve bundle.json remain witness-only workflows and reject aggregate-only paths
• Manual aggregate-edge registration affects runtime graph search and internal value extraction, but not bundle solving

File Naming

• Rule file: src/rules/<sourcelower>_<targetlower>.rs -- no underscores within a problem name
  • e.g., maximumindependentset_qubo.rs, minimumvertexcover_maximumindependentset.rs
• Test file: src/unit_tests/rules/<sourcelower>_<targetlower>.rs
• Canonical example: builder function in src/example_db/rule_builders.rs

Common Mistakes

Mistake	Fix
Forgetting #[reduction(...)] macro	Required for compile-time registration in the reduction graph
Using #[reduction] for an aggregate-only rule	#[reduction] currently registers witness/config edges only; aggregate-only rules need manual ReductionEntry wiring with reduce_aggregate_fn
Wrong overhead expression	Must accurately reflect the size relationship
Adding extra reduction metadata or duplicate primitive endpoint registration	Keep one primitive registration per endpoint pair and use only the overhead form of #[reduction]
Missing extract_solution mapping state	Store any index maps needed in the ReductionResult struct
Not adding canonical example to example_db	Add builder in src/example_db/rule_builders.rs
Not regenerating reduction graph	Run cargo run --example export_graph after adding a rule
Skipping Step 5 (paper documentation)	Every rule MUST have a reduction-rule entry in the paper. This is mandatory, not optional. PRs without documentation will be rejected.
Source/target model not fully registered	Both problems must already have declare_variants!, aliases as needed, and CLI create support -- use add-model skill first
Treating a direct-to-ILP rule as a toy stub	Direct ILP reductions need exact overhead metadata and strong semantic regression tests, just like other production ILP rules
Skipping verification for complex reductions	Verification is default for a reason — --no-verify is for trivial identity/complement reductions only