[isPANN]

Summary

Adds the rule DecisionMinimumVertexCover<SimpleGraph, One> → MinimumCutIntoBoundedSets<SimpleGraph, i64>, with unit tests (closed loop, exhaustive small graphs, boundary and overflow cases, extraction rejections), a canonical example (the issue's graph, bound 3) and a paper entry with a worked YES and NO example and reproducible pred commands.

Target size: at most 2·num_vertices + 2 vertices and C(n,2) − num_edges + 3·num_vertices edges; the side bound is n + 1.

The construction differs from the one in the issue. The issue's weighted s/t construction cannot be used: every s–t cut in it contains the same constant term n·M, so the optimum does not depend on the graph. This PR uses a different construction on the complement graph. Vertices are 0..n, then s, t, then padding vertices attached to t. Edges are the complement pairs, {i,s} with weight 1, {i,t} with weight deg(i) + 2, and padding edges of weight M = Φ + 1 with Φ = 2|E| + 2n. With T = n − k clamped to 0..=n+1, the threshold is Φ − T². For a cut with p padding vertices on s's side and independent-side set I, the cut weight is Φ − 2e(I) − |I| + M·p. Because M > Φ, a cut within the threshold has p = 0. Then T² ≤ 2e(I) + |I| ≤ |I|² forces |I| ≥ T and e(I) = 0, so I is an independent set of size at least n − k, and its complement is a vertex cover of size at most k. The converse direction takes a vertex cover C of size at most k and I = V \ C. The bound T = n + 1 (negative k) is infeasible because |I| ≤ n. The extraction returns the vertices on s's side.

Library change outside the rule: MinimumCutIntoBoundedSets::try_new is made pub (behaviour unchanged), so the rule can build the target without panicking.

Outside this change: the paper's parameter-contract renderer prints every upper_bound formula as "unavailable" (it handles exact and bound-only only), which also affects existing rules. It is not changed here.

Fixes #250

[isPANN]

Verification certificate

Rule: DecisionMinimumVertexCover<SimpleGraph, One> → MinimumCutIntoBoundedSets<SimpleGraph, i64> (issue #250)
Verdict: PASS — the rule's own tests and the end-to-end round trips below all agree with exact brute force on the source.

Type resolution

• Source: Decision<MinimumVertexCover<SimpleGraph, One>>, value Or.
• Target: MinimumCutIntoBoundedSets<SimpleGraph, i64>, value Min<i64>.
• Witness-compatible (Or → Min). The Decision-to-optimization pattern is the one used by HamiltonianCircuit → TravelingSalesman: the target carries a threshold θ, extract_value returns Or(cut ≤ θ), and extract_solution rejects infeasible, wrong-length or above-threshold configurations.

Construction versus the issue

The construction differs from the one in the issue. The issue's weighted s/t construction contains the same term n·M in every cut, so its optimum does not depend on the graph and cannot decide vertex cover. The construction used here (details in the paper entry):

• Let n = |V|, m = |E|, Φ = 2m + 2n, M = Φ + 1, and T = clamp(n − k, 0, n + 1). The target has vertices 0..n, a source s, a sink t, and q = n − T padding vertices joined to t with weight M. Its edges are the complement pairs of G (weight 1), {i,s} (weight 1) and {i,t} (weight deg(i) + 2). Each side has at most n + 1 vertices, and the threshold is θ = Φ − T².
• For a feasible partition with p padding vertices on s's side and I the set of original vertices on t's side, the cut weight is Φ − 2·e_G(I) − |I| + M·p, where e_G(I) is the number of edges of G inside I.
• (⇒) A cut of weight at most θ < M forces p = 0. Then T² ≤ 2·e_G(I) + |I| ≤ |I|² gives |I| ≥ T, and equality in the second inequality forces e_G(I) = 0. So I is an independent set of size at least n − k, and V \ I is a vertex cover of size at most k. The case T = n + 1 (negative k) is infeasible because |I| ≤ n.
• (⇐) For a vertex cover C of size at most k, take I = V \ C (padded as needed). It has e_G(I) = 0 and |I| ≥ T, so the cut weight is at most Φ − T².
• Size: at most 2n + 2 vertices and C(n,2) − m + 3n edges; |θ| ≤ (n + 1)². Every size and weight is computed with checked arithmetic before allocation.

Rule unit tests (14, all passing, each under a second)

• The issue's graph (11 target vertices, 23 edges, Φ = 28, M = 29, θ = 19): closed loop at bound 3 (YES, optimum equals θ) and bound 2 (NO, optimum above θ).
• Exhaustive: every graph on at most 4 vertices × bounds i64::MIN, −1, i64::MAX and 0..=n + 1 × all target assignments, comparing extract_value with brute force on both sides.
• Special cases: n = 0; T = n; bounds n, 4, 100 and i64::MAX give the identical instance; negative bounds (−1, i64::MIN); an intermediate bound; edge order and orientation independence; the 5-cycle and the star K₁,₄.
• Every extraction rejection (wrong lengths, s/t on the wrong side, oversized side, padding on s's side, cut above threshold).
• Overflow boundaries of usize and i64 found by bisection against an independent u128 formula; the cases needing a 64-bit usize are gated by target_pointer_width.
• Overhead: the predicted num_vertices and num_edges bound the constructed target on edgeless, sparse, dense and complete graphs, with bounds below, inside and above 0..=n (added to parameter_formula_validation.rs).

End-to-end round trips (100 instances)

Each instance was reduced with pred reduce, the target solved, the solution mapped back, and the result compared with exact vertex-subset enumeration on the source: 100 / 100 correct, 68 with a solution (YES) and 32 without (NO).

• Instance range: n from 5 to 8 vertices, 0 to 21 edges, bounds k from 0 to 6.
• Families, 10 instances each: sparse, medium and dense G(n,p), G(n,m), trees/forests, bipartite, cycles/grids, block-community, and planted-witness graphs; plus 10 special cases (minimum legal size, no constraints, single element, obvious YES, obvious NO, bound equal to the optimum, bound adjacent to the optimum, several optima, ties, one extra boundary case).
• Additionally, on 9 hand-picked instances (the issue's graph at bounds 3 and 2, a path, one edge with k = −1, two isolated vertices, a star, n = 0, the 5-cycle with k = 10¹², K₄ plus an isolated vertex with k = −5), pred reduce produced exactly the target given by an independent evaluation of the construction: vertices, ordered edge lists, weights, terminals and side bound.

Other gates

cargo fmt --check, cargo clippy --workspace --all-targets --all-features -D warnings, the full make check suite and make paper pass. Coverage of the rule file: 100 % of lines and functions, 94.7 % of regions (the uncovered regions are ? arms on i64 conversions that cannot fail). The paper entry has the construction, both directions, the extraction, and a worked YES and NO example computed from the stored example.

[isPANN]

Agentic Review Report

Subject: rule DecisionMinimumVertexCover<SimpleGraph, One> → MinimumCutIntoBoundedSets<SimpleGraph, i64> (issue 250), uncommitted change on issue-250. Re-review after fixes.
Verdict: approve — no open findings. The four findings of the first review are resolved (see "Re-review" below).

Re-review

The diff since the first review touches exactly the four findings:

1. 32-bit bound (was Important) — fixed. construction_parameters now branches on bound < 0 (giving T = n + 1). Otherwise it computes n.saturating_sub(usize::try_from(bound).unwrap_or(usize::MAX)), since a non-negative bound beyond usize exceeds every vertex count. I compiled the new expression verbatim for wasm32-unknown-unknown (32-bit usize) and ran it under node. With n = 6, bounds i64::MIN, −1, 0, 3, 6, 100, 2³²−1, 2³² and i64::MAX give T = 7, 7, 6, 3, 0, 0, 0, 0, 0, which is min(max(n − k, 0), n + 1) in every case. Edge cases also agree: n = 0 gives T = 0 (bound 0) and T = 1 (bound −1), and n = 2³²−2 with bound 2³² gives T = 0. The ungated (i64::MAX, 0, 6) clamp case exercises the saturating path on 32-bit hosts.
2. 32-bit test literals (Minor) — fixed. The 1 << 63 / 1 << 32 overflow cases moved into …_parameters_64_bit_overflow. That test, total_weight and …_weight_boundary are all under #[cfg(target_pointer_width = "64")]. The remaining ungated shifts are below 1 << 11, plus usize::MAX cases that are portable.
3. Closed loop (Minor) — fixed. …_closed_loop calls assert_satisfaction_round_trip_from_optimization_target, which checks every optimal target witness extracts to a satisfying source solution. It keeps the Min(Some(19)), value-map and decoding assertions. Removing the inline source.evaluate check is fine because the helper now performs it.
4. Paper Step 3 (Minor) — fixed. The rendered text now reads "The sink's side has 7 vertices and the source's side has 4, both at most B = 7", computed from the fixture's target_config and the target's vertex count.

I re-ran formatting, clippy with -D warnings, the 14 rule tests and the full suite: all pass. make check and make paper pass on the final code. Rule-file coverage is unchanged (100% lines/functions, 94.7% regions). I repeated the pred feature test below on the rebuilt CLI with identical results.

Structural and semantic

• Files changed: the new rule, its unit tests, src/rules/mod.rs (module + canonical example), one new test in parameter_formula_validation.rs, the paper entry, and MinimumCutIntoBoundedSets::try_new made pub with a doc comment (behaviour unchanged; pub fn try_new is the convention in other graph models). No generated exports in the diff. No existing test loses a line.
• Registration: #[reduction(transform = upper_bound { num_vertices = "2 * num_vertices + 2", num_edges = "num_vertices * (num_vertices - 1) / 2 - num_edges + 3 * num_vertices" })] covers both target parameters. Counted by hand from reduce_to: vertices are n + 2 + q with q = n - T ≤ n; edges are C(n,2) - m + 2n + q (complement edges, {i,s}, {i,t}, padding). Both are sound upper bounds. pred path reports the same formulas.
• Result mapping: this is a Decision → optimization rule as in docs/src/design.md (the HamiltonianCircuit → TravelingSalesman row). extract_value returns Or(cut ≤ θ). extract_solution validates once through validate_target_witness using the same threshold predicate, then returns the original vertices on the source's side. Wrong lengths, infeasible partitions and cuts above θ return ExtractionError, and each rejection path is tested.
• Construction traced by hand on the issue's graph with k = 3 and on the path 0-1-2 with k = 1. Vertices 0..n, then s = n, t = n + 1, then padding. Edges: the complement pairs i < j in order of j then i, then {i,s} with weight 1, {i,t} with weight deg_H(i) + 2, and {t,p} with weight M = Φ + 1, where Φ = 2|E(H)| + 2n. Side bound n + 1, threshold θ = Φ − T², with T = n − k clamped to 0..=n+1. The target encodes the same question, and extraction inverts it.
• Errors and numerics: target construction goes through SimpleGraph::try_new and MinimumCutIntoBoundedSets::try_new, mapped with target_construction. Every size and weight is checked before allocation, and so is the total edge weight, which bounds every cut. The bound clamp is portable since the fix (re-review item 1).
• Paper: construction, cut-weight identity, both directions, extraction and numeric range. I checked every step: the identity cut = Φ − 2e_H(I) − |I| + M·p, the side sizes, the lower bound cut ≥ n + M·p, forcing p = 0, |I| ≤ T, T² ≤ 2e_H(I) + |I| ≤ |I|², and excluding T = n + 1. The worked YES and NO examples load the fixture. All four pred commands work when run by hand.
• Issue compliance: the issue's body proposes a weighted s/t construction. Its second comment shows that construction is wrong (every cut contains the constant n·M, so the optimum ignores the graph). This change implements a different, correct construction and does not claim to follow the issue's. The issue's example graph is the canonical example and appears in the tests, with the minimum cover size 3 confirmed by brute force (YES at bound 3, NO at bound 2).

Quality

• 14 unit tests, all fast (two of them run only with a 64-bit usize). They cover the issue's example at bounds 3 and 2; n = 0; T = n; k ≥ n (bounds n, 4, 100, i64::MAX give identical instances); negative bounds (-1, i64::MIN); an intermediate bound; edge-order independence; every extraction rejection; and every graph on up to 4 vertices × bounds × all target assignments, checking extract_value against brute force on both sides. They also cover the 5-cycle and the star K_{1,4}, every clamp boundary, and the usize/i64 overflow boundaries, the last found by bisection against an independent u128 formula.
• Coverage of the rule file: 100% lines, 100% functions, 94.7% regions. The uncovered regions are ? arms on i64 conversions that cannot fail.
• make check and make paper pass. Clippy passes with -D warnings.

Feature test

pred list --rules DecisionMinimumVertexCover lists the edge. I ran pred create --example DecisionMinimumVertexCover/SimpleGraph/One --to MinimumCutIntoBoundedSets, pred inspect, then pred path … -o paths.json with its first path as route.json, then pred reduce --via route.json, pred solve bundle.json and pred evaluate:

• The issue's example: 11 vertices, 23 edges, weights 1×14, 5,4,4,5,4,6, 29×3, B = 7. pred solve gives Or(true) with intermediate Min(19), which equals θ, and returns the cover {0,1,4} (a second minimum cover; the stored one is {1,2,4}).
• Eight more instances, reduced with pred reduce and compared with an independent evaluation of the construction: the path with k = 1, one edge with k = −1, two isolated vertices with k = 1, the star with k = 2, the issue's graph with k = 2, n = 0, the 5-cycle with k = 10¹², and K₄ plus a vertex with k = −5. The targets matched exactly: vertices, edge lists in order, weights, terminals, side bound. pred solve agreed with brute force on the source every time: YES instances had optimum = θ, NO instances returned status infeasible with optimum > θ.

Findings of the first review (all resolved)

1. Important — wrong answer on 32-bit usize targets. src/rules/decisionminimumvertexcover_minimumcutintoboundedsets.rs:119-122. match usize::try_from(bound) { Ok(b) => n.saturating_sub(b), Err(_) => n_plus_one } treats every failed conversion as a negative bound. With a 32-bit usize, a bound ≥ 2³² also fails, so T = n + 1: the construction's NO setting. The source is trivially YES (the whole vertex set is a cover of size n ≤ bound), but the reduction reports NO and extraction rejects every partition. Reproduced by compiling this exact expression for wasm32-unknown-unknown and running it under node: n = 6 with bound 4294967295 gives T = 0, but bound 4294967296 and i64::MAX give T = 7. Fix: branch on the sign explicitly, as the sibling multicenter_parameters does (bound < 0, then bound.min(n_i64)). For example: let independent_size = if bound < 0 { n_plus_one } else { usize::try_from(bound).map_or(0, |b| n.saturating_sub(b)) };, since a bound beyond usize::MAX exceeds n. A test that calls construction_parameters(6, 0, 1 << 32) and expects T = 0 covers it on any platform where the literal fits.
2. Minor — the unit tests do not compile or pass with a 32-bit usize. src/unit_tests/rules/decisionminimumvertexcover_minimumcutintoboundedsets.rs:402-404: the literals 1 << 63, 1 << 32 and (1 << 32) + 1 as usize trip the deny-by-default arithmetic_overflow lint (reproduced on wasm32-unknown-unknown). In …_weight_boundary (line 427 on), the bisection reaches n > 2³², so usize::try_from(low).unwrap() (line 441) would panic. Fix: gate these cases with #[cfg(target_pointer_width = "64")], as decisionminimumdominatingset_minmaxmulticenter.rs:178 and decisionmaximumindependentset_integralflowbundles.rs:146 do.
3. Minor — the closed-loop test hand-rolls the round trip. src/unit_tests/rules/decisionminimumvertexcover_minimumcutintoboundedsets.rs:83. The rule checklist asks closed-loop tests to use the shared assert_*_round_trip_* helpers, and the decision → optimization sibling hamiltoniancircuit_travelingsalesman.rs uses assert_satisfaction_round_trip_from_optimization_target. Fix: call assert_satisfaction_round_trip_from_optimization_target(&source, &reduction, "DecisionMinimumVertexCover -> MinimumCutIntoBoundedSets") in …_closed_loop, keeping the Min(Some(19)) and value-map assertions next to it.
4. Minor — one example fact in the paper is asserted, not computed. docs/paper/reductions.typ:11713, Step 3: "Both sides have at most $B$ vertices." is fixed text, while every other number in the example comes from the fixture. Fix: compute the two side sizes from target_config (4 on the source's side, 7 on the sink's side), print them against B = 7, and reuse the existing dmvc_mcibs_sink-side binding.

Outside this change, for a separate issue: format-parameter-contract (docs/paper/reductions.typ:642-648) handles exact and bound-only, but the graph export writes upper_bound. So every upper-bound field prints as "unavailable: " with an empty reason. That happens for both fields of this rule, for DecisionMinimumDominatingSet → DecisionMinimumSumMulticenter, and for num_transitions of MinimumVertexCover → LongestCommonSubsequence. The renderer predates this change, which should not fix it.

Open findings

None.

[codecov]

Codecov Report

❌ Patch coverage is 99.60239% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 97.20%. Comparing base (e7bacb3) to head (f489c3b).

Files with missing lines	Patch %	Lines
...ionminimumvertexcover_minimumcutintoboundedsets.rs	99.36%	2 Missing ⚠️

Additional details and impacted files

@@           Coverage Diff            @@
##             main    #1245    +/-   ##
========================================
  Coverage   97.19%   97.20%            
========================================
  Files        1146     1148     +2     
  Lines      151558   152060   +502     
========================================
+ Hits       147308   147808   +500     
- Misses       4250     4252     +2     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.