[isPANN]

Summary

46 ILP rules declared num_nonzeros <= num_constraints * num_vars, which is the bound for a dense matrix. Against pred-validation-corpus, 55 rules never reached even half of that prediction. Each rule now sums the terms contributed by each constraint family in its reduce_to.

Verification

• scripts/verify_parameters.py (corpus) re-run on those 55 rules, 100 instances each: 0 violations. 47 fields now reach 0.83–1.0 of their prediction (before: ≤ 0.48).
• cargo test --workspace, cargo fmt --check and clippy all pass. The one clippy warning, in ksatisfiability_bicliquecover.rs, was already there.

Still loose, and not changed here: MinimumHittingSet (its parameters can't express the incidence count), CircuitSAT, HighlyConnectedDeletion, MinimumCodeGenerationUnlimitedRegisters, SequencingWithReleaseTimesAndDeadlines, SequencingWithinIntervals, TwoDimensionalConsecutiveSets.

Stacked on #1218 (feat/binary-ilp-to-sat).

🤖 Generated with Claude Code

[isPANN]

Agentic Review Report

Scope: 46 src/rules/*_ilp.rs files, metadata-only (num_nonzeros in transform blocks). Base feat/binary-ilp-to-sat. No code paths, tests, or generated exports changed.

Structural

• Only num_nonzeros formulas changed. No blacklisted or generated files, no unrelated edits.
• Every formula uses only declared source parameters (accepted by the compile-time parser).
• ILP::num_nonzeros() sums terms.len() after normalize_constraint, which merges duplicate variables and drops zero coefficients. So per-family term counts are always valid upper bounds, even where a rule pushes the same variable twice (MCP balance rows, self-loop flow rows, IFWM multiplier rows) or where a coefficient is 0 (position p = 0, cap = 0).

Semantic: hand derivation of every formula

I traced each reduce_to constraint family by family, including early returns, conditional rows, and loops over data-dependent sizes. All 46 formulas are valid upper bounds for every accepted input.

Data-dependent loops checked:

• Degree sums (Steiner, LongestCircuit, OCST, DCP, MLST, LongestPath, SWCP, MCP, UFLB, U2CIF, IFWM): every per-vertex incidence loop sums to ≤ 2·|E| per family. Source/sink skips only remove terms.
• Deadlines and windows: SWID's assignment row plus its unused-slot row together give exactly n·max_deadline; precedence rows give ≤ 2·max_deadline. ClosestSubstring's per-string window rows sum to total_num_windows. RCS caps d = min(deadline, n).
• Matrix and graph density: COS, CBM, Clustering, DHP, KClique, MaxClique, SubIso, Domatic and NMTS are bounded by the dense case.
• Partition and clauses: MCB's partition is validated to cover each arc exactly once (≤ m terms). Max2SAT clauses are validated to have exactly 2 literals (serde goes through try_new).
• Prefix rows: STMMCC, STMTTW, MTS<i64>, SWDST, SMWCT and FSS were summed in closed form; each matches the formula exactly or bounds it from above.

Exact matches (derivation equals the formula on the dense worst case): COS, Steiner, STMMCC, STMTTW, STMWT, SMWCT, FSS, MTS (both), DHP, OCST, SubIso, MinMaxMulticenter, MGB, OLA, LongestPath, SWCP, MLST, U2CIF, UFLB, and the others with linear families.

Loose but valid (≤ 1.2× slack):

• MCP: the derivation gives 22·num_arcs; the formula declares 26·num_arcs.
• LongestCircuit: the derivation gives 5·num_vertices; the formula declares 6·num_vertices.
• SWDST: switch plus linearization rows total n(n-1)(3n+5); the formula declares n(n-1)(3n+7).

Spot measurement with pred path ConsecutiveOnesSubmatrix ILP on a dense 3×4 all-ones matrix, K=4: predicted 436, measured 430. The 6-term gap is the p = 0 order coefficients that normalization drops.

Quality

• cargo test --lib --features example-db parameter_formula_validation: 6/6 pass (canonical-example coverage of every upper_bound field).
• No new tests pin the tightened bounds on adversarial (dense or worst-case) instances. The PR relies on the external pred-validation-corpus run. Canonical examples are small and sparse, so a future regression that adds a constraint family would only fail if it pushed a sparse example over the bound.

Feature test

• Built pred from the branch. pred path ConsecutiveOnesSubmatrix ILP shows the new formula. Executing it on a dense instance measured 430 ≤ 436 predicted.
• No CI checks are reported on this stacked PR.

Findings

Critical: none.

Important: none.

Minor

1. src/rules/mixedchinesepostman_ilp.rs:49: 26 * num_arcs can be tightened to 22 * num_arcs. Per-arc contributions: g/y bounds 2, balance 2, use-indicator 4, linking 4, z-cover 2, flow bounds 4, two conservation families 4.
2. src/rules/longestcircuit_ilp.rs:66,220: 6 * num_vertices can be 5 * num_vertices. Non-commodity rows give 4n; commodity rows give n·(n+1), which is already counted as num_vertices^2 + num_vertices.
3. src/rules/sequencingwithdeadlinesandsetuptimes_ilp.rs: 3 * num_tasks^2 * (num_tasks - 1) + 7 * num_tasks * (num_tasks - 1) can be 3 * num_tasks * (num_tasks - 1)^2 + 8 * num_tasks * (num_tasks - 1), i.e. n(n-1)(3n+5).
4. Optional: add a dense-instance assertion to sparse_ilp_predictions_use_construction_counts (src/unit_tests/parameter_formula_validation.rs) for one or two rules whose formulas are exactly tight, such as COS with an all-ones matrix, or DHP with no arcs. A missed constraint family would then fail in-repo rather than only in the external corpus.

Verdict: correct. All 46 num_nonzeros formulas are sound upper bounds. Mergeable as is; the minor items are optional tightening.

[GiggleLiu]

Agentic Review Report

PR #1222: Tighten ILP num_nonzeros bounds to per-constraint counts

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

Verdict: No new blocking finding in this diff. Hold stack integration until prerequisite fixes land.

Structural and semantic review

Reviewed all 46 changed ILP num_nonzeros declarations and their reduce_to construction bodies, the dense-source regression, and affected manual text against exact #1218. Each expression is an upper bound, so coefficient normalization may merge duplicates or drop zeros without invalidating it. No change to the optimization semantics is introduced.

Independent representative term counts: BinPacking has n² assignment terms plus n(n+1) capacity terms, giving 2n²+n. DirectedHamiltonianPath contributes 3n² plus 2n²(n−1), giving n²+2n³. Directed two-commodity paths contribute 4km flow terms plus 2km shared-capacity terms. Kernel/Clique-like and domination formulas count graph degrees before adding per-vertex terms. Scheduling formulas count one-hot rows, period capacities, and ordered precedence contributions separately rather than multiplying all rows by all variables. ResourceConstrainedScheduling uses the compressed horizon D <= n. SteinerTree's n−1 term is safe because construction requires a nonempty terminal set and thus n >= 1.

Checked degenerate zero-variable or empty-edge cases and early infeasible targets; each bound remains nonnegative or safely overestimates the constructed target. The changed multiway, flow, longest-path/circuit, tree, matching, assignment, scheduling, and subgraph-isomorphism bounds were traced to actual add_constraint calls. No undercount was identified.

Quality review

The new dense-source regression complements existing canonical sparse examples; a sparse canonical instance alone would not justify a tighter worst-case formula. Hand counts were used to assess all changed formulas. Material examples include 6km for directed commodity paths, 22m for undirected two-commodity flow, n+2precedences for partially ordered knapsack, and pattern_verticeshost_vertices plus 2pattern_edgeshost_vertices² for subgraph isomorphism. Normalization only decreases these upper bounds.

Feature tests and verification limits

No native exact #1222 metadata test or full build was run by this reviewer. The shared build slot was used for #1218 tests/CLI, then the exact #1224 numeric probe. That probe compiles the #1224 descendant, which includes these declarations, but compilation does not validate their counts. The author-reported tightness corpus and parameter regression results were read and are not counted as reviewer execution.

Executed own-base git diff --check successfully. Source/target optimization behavior is unchanged by this PR. Current GitHub CI results were not visible in the collected stack metadata. Parent should run current integrated parameter tests before merge.

Findings (severity order)

No new blocking finding. All changed count expressions were independently checked as upper bounds. The inherited #1214 reduction panic is outside this diff and should be resolved before integrating its dependency chain.

GitHub PR Audit — #1222

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]

Agentic Review Report: stack consolidation

Approved current head 5cab940eee60588875f3b21162df8881a0ff10e2 for merging into feat/binary-ilp-to-sat 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.