[isPANN]

Summary

The corpus accuracy run (pred-validation-corpus/scripts/verify_parameters.py) found 81 non-trivial upper_bound fields that equal their prediction on every corpus instance. Matching on the corpus doesn't make a field exact: SpinGlass → MaxCut, for example, adds its ancilla vertex only conditionally. So I read each construction and promoted a field only when every input produces exactly that count.

Promoted, 45 fields in 29 rules. In each case:

• every variable block and row family is emitted unconditionally;
• the source invariants rule out merged or dropped terms: simple graphs with no loops or repeated edges, |V| divisible by 3 (PartitionIntoPathsOfLength2), and 1 ≤ k ≤ n (KClique);
• no early return builds a different target.

Kept as upper bounds:

Reason	Rules
Early return on degenerate input	AcyclicPartition, MixedChinesePostman, StackerCrane, RootedTreeStorageAssignment, MinimumInternalMacroDataCompression, Decision OpenShop, ExactCoverBy3Sets → BoundedDiameterSpanningTree, HamiltonianCircuit → Biconnectivity/StrongConnectivity augmentation, 3SAT → FeasibleRegisterAssignment, 3DM → ThreePartition
Terms that cancel or are filtered	NAESAT/1-in-3 ILP (x, ¬x in a clause), IntegerKnapsack (oversized items), PartitionIntoPerfectMatchings num_nonzeros (k = 1 zeroes a coefficient), MVC → MinimumWeightAndOrGraph, SAT → NAE / IntegralFlowHomologousArcs (repeated literals)
Clauses shorter than K (new_allow_less)	3SAT → KClique num_vertices, 3SAT → DecisionMVC num_edges (pinned by three_sat_contracts_cover_short_clauses)
QUBO num_quadratic_terms	Penalty and objective terms share entries and can cancel

Also in this PR

ConsecutiveOnesSubmatrix accepted a negative bound K. pred inspect then panicked, because bound must fit u64, and the ILP rule cast the bound with as usize. The model now rejects a negative bound at construction (8523caa).

MaxCut → MinimumMatrixCover with negative weights. MaxCut<SimpleGraph, i64> accepts negative weights, but the rule rejected them, so planned paths through it failed. The corpus path run found 44 failures, for example DecisionMax2SAT → MaxCut → MinimumMatrixCover.

• Each negative edge {u, v} now becomes an auxiliary vertex t, with weight |w| + 1 to v and |w| to u. Every maximum cut separates t from v, so the gadget shifts the cut by the constant 2|w| + 1 and preserves maximum cuts.
• Extraction drops the auxiliary bits, and num_rows becomes upper_bound num_vertices + num_edges.
• The paper proof is updated, and closed-loop tests cover mixed and all-negative weights plus the i64::MIN overflow. The previously failing paths now measure cleanly.

Verification

• cargo test --workspace passes, and so does clippy. Every exact field equals the measured value on the canonical examples (every_executable_parameter_formula_matches_a_constructed_target).
• A test had pinned KClique → BCBS num_vertices to UpperBound. That pin dates from before SimpleGraph rejected repeated edges (394f3df), so it now asserts Exact.
• Corpus: the 30 touched rules × 100 instances gave 0 violations.

Stacked on #1222.

🤖 Generated with Claude Code

[isPANN]

Agentic Review Report

Reviewed head b8867cfb (feat/exact-tight-bounds) against base fix/ilp-nonzeros-bounds. This is a generic PR: it changes rule parameter metadata (44 fields in 29 rules move from upper_bound to exact) and adds one model validation (ConsecutiveOnesSubmatrix now rejects a negative bound).

Structural

• No generated exports and no unrelated edits are in the diff. Every changed rule still declares each target parameter exactly once.
• ConsecutiveOnesSubmatrix::try_new is reached from both new and the serde try_from path, so the new 0 <= bound <= n check covers every constructor. The paper definition already states $0 <= K <= n$, and no other rule constructs this model.

Semantic: adversarial check of every promoted field

For each reduce_to, I traced the conditional pushes, early returns, edge filters and deduplication, and degenerate sizes. I also checked num_nonzeros after normalize_constraint, which merges repeated variables and drops zero coefficients. Each of the source invariants below is enforced by both the constructor and the serde path.

Rule	Promoted field(s)	Why it is exact
Kernel→ILP	num_nonzeros = 3a+n	SimpleDigraph rejects loops and parallel arcs, so no term merges. Antiparallel arcs produce separate rows.
MaximalIS→ILP	num_constraints, num_nonzeros	SimpleGraph has no loops or duplicate edges.
MaximumMatching→ILP	num_nonzeros = 2m	Each edge appears in exactly two vertex rows. Isolated vertices are filtered, but num_constraints remains an upper bound.
MinimumDominatingSet→ILP	num_nonzeros = 2m+n	Same reason as MaximalIS.
HamiltonianCircuit→ILP	num_vars, num_nonzeros = 10m	-capacity is zero only when n ≤ 1, and then m = 0. With n = 2 and one edge, capacity is 1 and the count is 10.
PartitionIntoPathsOfLength2→ILP	num_vars, num_constraints, num_nonzeros	n is divisible by 3 (enforced in try_new). Groups with no edges still push the empty ≥ 2 row. The McCormick product always yields 7 terms.
PartitionIntoPerfectMatchings→ILP	num_vars, num_constraints	When k = 1 the (same, k-1) term drops, but this affects only num_nonzeros, which stays an upper bound.
PartitionIntoCliques→Decision	num_vertices, num_edges	q = 2m. The side size is s = n+2m+1, giving edges s²+s+n+8m = (n+2m)²+4n+14m+2. No duplicate edges are pushed.
KClique→BCBS	all four	try_new, used by serde as well, requires 1 ≤ k ≤ n, so n-k and k(k-1)/2 are exact.
3-SAT→{KClique.k, DMVC.num_vertices, 1-in-3.num_clauses, SubsetSum.num_elements}	as listed	These counts do not depend on clause length, so they hold for new_allow_less clauses, including empty ones.
Max2SAT→MaxCut	num_vertices	The target is built with num_vars + 1 vertices directly.
MVC→EnsembleComputation	universe_size	try_new stores the universe size verbatim.
NMTS→ILP	num_constraints = 3m	One row per index, even when that row is empty.
num_vars promotions (Clustering, CBM, C1S, DHP, D2CIF, FlowShop, IST, MSMC, SCS, SMC, SubIso, UFLB, BiconnAug, StrongConnAug)	num_vars	Each is a closed-form layout computed from the same getters the parameters use. For C1S, k = bound is now guaranteed to be ≥ 0. For FlowShop, n(n-1)/2 evaluates to 0 at n = 0 under the exact rational arithmetic.

Empirical probe. I ran a temporary check_reduced_parameters probe (since removed) on degenerate instances: n ∈ {0,1,2,3} with a single edge or antiparallel arcs; KClique with k = n and k = 1; PIPL2 with 0 and 3 vertices, with and without edges; PIPM with k = 1; C1S with an empty matrix and with bound 0; CBM with an oversized bound; FlowShop with zero jobs; SCS with an empty string. Every exact field matched the measured target.

Tests run (-j 4, filtered): symbolic_parameter_contracts (27 passed), parameter_formula_validation (7 passed), consecutive_ones (33 passed).

Quality

• The 3-SAT short-clause test and the KClique→BCBS exactness test are well aimed.
• Of the ILP promotions, only the canonical example in every_executable_parameter_formula_matches_a_constructed_target checks equality. canonical_examples_satisfy_upper_bound_parameter_contracts (src/unit_tests/symbolic_parameter_contracts.rs:143) checks only >=, even for exact fields.

Feature test

I skipped make cli. The user's machine is under memory constraints, and the PR changes only symbolic metadata plus one constructor check, both of which are covered by the library tests above.

Findings

Critical: none. I found no accepted source instance that violates any promoted exact field.

Important

1. The degenerate-size boundaries are untested. The exactness of HamiltonianCircuit→ILP.num_nonzeros, PartitionIntoPathsOfLength2→ILP (all three), PartitionIntoPerfectMatchings→ILP, PartitionIntoCliques→MCBC, and the Kernel/MaximalIS/MinimumDominatingSet/MaximumMatching nonzero counts depends on edge cases: n ≤ 2 (the HC capacity term), empty edge sets, k = 1, and zero jobs. Only one canonical example checks each of them. Suggested fix: add a check_reduced_parameters(..., ParameterRelation::Exact) loop over n ∈ {0,1,2,3} (and k = 1, FlowShop with no jobs) in src/unit_tests/symbolic_parameter_contracts.rs, as was done for the 3-SAT rules, so a later change to a filter or a zero coefficient is caught.

Minor

1. src/unit_tests/symbolic_parameter_contracts.rs:143: canonical_examples_satisfy_upper_bound_parameter_contracts compares exact fields with >=. It could branch on transform.relation(field) and check equality for Exact.
2. src/rules/consecutiveonessubmatrix_ilp.rs:65: self.bound() as usize is now safe, but the numeric contract prefers usize::try_from(...) at range boundaries.
3. src/rules/minimumvertexcover_ensemblecomputation.rs:84: num_subsets = "num_edges" is also always exact (one subset per edge, and normalize_subset does not drop subsets), so it could be promoted. This is optional.

[isPANN]

Addressed the review in 0318bfd:

• Important: added exact_construction_counts_hold_on_degenerate_graphs. It runs:

  • empty, path and complete graphs with n ∈ {0..3};
  • k = 1 and k = n where the model accepts them;
  • Kernel on empty, single, antiparallel and 3-cycle arcs.

  It covers HamiltonianCircuit→ILP, MaximalIS / MinimumDominatingSet / MaximumMatching nonzeros, PartitionIntoPathsOfLength2→ILP, PartitionIntoPerfectMatchings→ILP and PartitionIntoCliques→Decision.

• Minor:

  • Promoted MinimumVertexCover→EnsembleComputation num_subsets, which builds one subset per edge.
  • The ConsecutiveOnesSubmatrix ILP now converts the bound with usize::try_from.
  • Not changed: canonical_examples_satisfy_upper_bound_parameter_contracts still checks only >=, matching its name. Exact equality on canonical examples is enforced by every_executable_parameter_formula_matches_a_constructed_target.

🤖 Generated with Claude Code

[GiggleLiu]

Agentic Review Report

PR #1224: Declare exact parameter counts that constructions always produce

Review date: 2026-10-29. Fresh-context read-only review of f95447ad2f1de5d37c020ad6ffc119460adebaff...ef18c7635bb68aa2bd36b41f995ed3c89c3db9db. Used the PR's own stack base, not origin/main. Local implementation evidence is diff-1224.patch; GitHub context is context-1224.txt in this directory.

Verdict: HOLD — newly accepted negative MaxCut weights can construct a target whose optimum cannot be evaluated.

Structural and semantic review

Reviewed all 45 promoted parameter fields across 29 rules, their constructor paths and degenerate cases, tests, and manual changes against exact #1222. Exact promotions are justified where the code allocates unconditional variable/constraint storage; fields affected by coefficient cancellation or optional terms remain upper bounds. SimpleGraph/SimpleDigraph invariants eliminate duplicate edges and loops where exact degree-count formulas require that property. Checked empty graphs, n=1 and n=2 cases, early infeasible targets, and k=1 partition parameters.

The ConsecutiveOnesSubmatrix bound changes from i64 to usize and rejects negative serde inputs, matching the nonnegative cardinality meaning. This is a public type change and should be disclosed separately from the user's acceptance of #1225's API break; that acceptance alone is not evidence of a decision on this constructor. No independent semantic error was found in this change.

The new MaxCut negative-edge gadget is algebraically sound over unbounded integers. For w<0, an auxiliary spin has a link of |w|+1 to one endpoint and |w| to the other; the stronger anchor forces it opposite the first endpoint in any optimum. Projecting source spins preserves max-cut optima up to a constant. However, representability of each link does not guarantee representability of the complete symmetric objective. The new supported negative-weight domain exposes the concrete failure below.

Quality review

Metadata promotions were traced to actual row/column construction rather than a finite tightness corpus. MaxCut tests include modest signed weights and reject weights whose anchor itself overflows, but omit signed weights whose links fit while the full matrix energy overflows. The added arithmetic guard only checks 1−w and therefore cannot establish the required target evaluation contract.

Feature tests and verification limits

Compiled and executed a standalone probe with problemreductions = { path = "/tmp/pr-review-1224", features = ["example-db"] } at exact head ef18c76. Build used two jobs, no debug info or incremental artifacts, and the shared local target directory. The probe uses the actual source/target constructors, ReduceTo implementation, evaluators, and BruteForce solver; it is not a reimplementation.

The source brute-force optimum is Ok(Max(Some(0))). Reduction succeeds. The target's mathematically optimal witness returns an IntegerOverflow evaluation error, and target brute-force solve also returns an evaluation error. Full output is numeric-probe.log; probe source is /tmp/pr-review-numeric-probe/src/main.rs.

Exact #1224 test-suite compilation was intentionally skipped after confirming the blocker so the shared build slot could validate an independent merge candidate. Own-base git diff --check passed. No current GitHub CI results were visible in the collected stack metadata.

Findings (severity order)

Critical — the negative-edge gadget can produce an unevaluable optimum

src/rules/maxcut_minimummatrixcover.rs:92-105 checks only the individual anchor coefficient and then returns the target without checking its aggregate arithmetic range.

Reproducer: MaxCut<SimpleGraph, i64> with 2 vertices, one edge (0,1), and weight -3000000000000000000. Every source configuration evaluates successfully, and source optimum is 0 when both endpoint bits agree. Reduction currently succeeds and constructs:

[[0, 0, 3000000000000000000],
 [0, 0, 3000000000000000001],
 [3000000000000000000, 3000000000000000001, 0]]

The target optimum has both endpoint spins equal and the auxiliary spin opposite, e.g. [true,true,false]. Its full symmetric quadratic form is -12000000000000000002, below i64::MIN. Row-major checked evaluation accumulates -3000000000000000000, -6000000000000000001, -9000000000000000001, then underflows. Native output:

maxcut source optimum [false, false] Ok(Max(Some(0)))
target optimum evaluate Err(IntegerOverflow("summing matrix-cover objective"))
target solve Err(Evaluation(IntegerOverflow("summing matrix-cover objective")))

Before this PR the reduction rejected negative weights, so this failure is newly introduced support, not merely an unrelated preexisting positive-weight edge case. Check complete target coefficient/prefix magnitude bounds in widened arithmetic and return a typed ReductionError when a safe i64 target cannot be represented (or normalize with a proved optimum-preserving construction). Add this signed single-edge regression. The inherited #1214 interval allocation panic also remains, but is not attributed to this diff.

GitHub PR Audit — #1224

GATE: PASS

Harm signals (blocking)

• harm.secrets (security.no-secrets): OK — inspected added text; no credential/key/token or private-data additions found.
• harm.dangerous-files (git.harm-signals): OK — changed files are scoped source, tests, and manual material; no conflict markers, unexplained binaries/archives, scratch files, or local configuration.
• harm.generated-artifacts (code.generated-artifacts): OK — no generated example/schema/reduction-graph exports or build/dependency outputs are committed.
• harm.cache (code.generated-cache): OK — no cache directories added.
• harm.debug-leftovers (code.debug-leftovers): OK — no debugger, debug print, temporary probe, or WIP instrumentation in added production code.

PR legibility (advisory)

• pr.description-quality (github.pr-description-quality): OK — body describes scope, purpose, validation, and limits; comments and reviews were read with gh-axi pr view --full --comments --reviews.
• pr.traceable (github.prs-traceable): OK — purpose and validation are stated and the series/issue context is identifiable.

Harm gate PASS does not clear correctness findings. No tracked file, commit, remote branch, PR comment, review, or merge was modified by this reviewer.

[GiggleLiu]

The objective-overflow blocker is fixed at 52bd171. Every constructed coefficient is nonnegative, so the complete coefficient sum is attained by an all-equal assignment and bounds every signed evaluation prefix. Checking that sum before construction gives the required i64 range guarantee. Independent review, all 15 MaxCut-to-matrix tests, make check (7,142 tests, formatting, and Clippy), and CLI regressions pass. The negative-weight reproducer now returns typed IntegerOverflow, while the largest safe positive and negative single-edge cases still round-trip. Fresh required CI will run on the combined stack against main.

[GiggleLiu]

Agentic Review Report: stack consolidation

Approved current head 3372d66b5b642ae6c99ccb42c61efd7e18477148 for merging into fix/ilp-nonzeros-bounds only. This contains the previously reviewed changes and, where applicable, the preceding recorded backend merges. The numeric blockers in #1214 and #1224 are fixed and reviewed at 2226ebec4 and 52bd171a0.

Rechecked inline comments, submitted reviews, PR conversation, linked-issue comments, and Codecov comments. No new unaddressed material issue. Harm gate remains PASS from the independent reviews. The old roadmap draft/hold instructions predate the user's current authorization; deferred rules and #1219/#1220/#1221 remain excluded.

The repaired aggregate passed 7,194 native tests, formatting, all-target/all-feature Clippy, and make paper at d96e7c8b8; the final website gate subsequently passed all 336 browser cases at 77774797e. These are aggregate gates, including the separately reviewed integration fixtures, not a claim that this branch head was independently retested unchanged. Required main-branch CI remains pending. This feature-branch merge preserves the individual PR record.