Tighten sparse, geometric and cached construction overhead formulas - #1190
Conversation
Correct exactness claims, count sparse coefficients by construction block, reject negative flow capacities, and verify metadata using existing behavior inputs and real executors.
Derive upper bounds from conditional even padding and the set-packing endpoint universe. Preserve the exact edge-to-set count and verify the registered promises in existing parity and isolated-vertex tests.
Replace oversized formulations with compact constructions for partition, register, matrix, graph, and ordering problems. Add direct bounded ILP pipelines and reuse exact customized subset-sum and clique-cover solvers. Preserve signed weights and costs, avoid artificial partition-bound overflow, and align overhead contracts, rule targets, tests, and proofs with the resulting constructions. Validated with make check, make paper, independent reduction audits, and CLI solver and extraction round trips.
isPANN
changed the title
GiggleLiu
left a comment
GiggleLiu
left a comment
There was a problem hiding this comment.
Independent review covered all 49 changed files, including sparse construction counts, geometric CVP bounds, cached statistics and incoming parameter contracts. No material findings remain; policy audit PASS. The solver regression fixes from #1174 are included.
The merge from main preserves the already-reviewed combined tree exactly. On that tree, make check and make paper pass. CI is running on final head 76c7d3a; merge remains conditional on all checks passing. Historical construction-corpus measurements retain their original provenance and were not rerun for this review.
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1190 +/- ##
==========================================
+ Coverage 96.88% 96.90% +0.01%
==========================================
Files 1095 1095
Lines 144504 145109 +605
==========================================
+ Hits 140006 140621 +615
+ Misses 4498 4488 -10 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
2 participants
Dense variable×constraint, padded-grid-area and factorial magnitude bounds greatly overstate the targets actually built. This PR replaces them with counts of sparse construction blocks and geometric bit bounds. Compared with prerequisite
44537006, it changes 68 formulas across 37 rules, adds one explicitly unavailable incoming field, and supplies eight cheap/cached source statistics with their incoming contracts. Reduction targets, solving, extraction, public input formats and existing APIs retain their behavior; exact/composition engines and path selection are untouched.The three highlighted declarations now use these derivations:
An independently derived unequal-coordinate CVP test uses basis [[1,0,0],[3,1,0]] and target [0,0,1]. Its widths six and two require three and two bits: the real target has five variables and ten quadratic terms, while registered predictions are five and thirteen. A two-domino overlapping image has four rectangle-cell incidences and two budget terms, giving exactly six nonzeros. Tests failed before the corresponding implementation changes and cover degenerate/zero encodings, Gram cancellation, large cancelling determinant products, row swaps, normalized budgets and final rational ceiling. Real SubsetSum→DecisionCVP→CVP→QUBO intermediate targets and extracted solutions are checked.
All 16 initial proposals were reconciled with current source: four sparse-support candidates were already present, the remaining candidates are covered, and the PR also tightens ILP, timetable, macro and scheduling declarations. The other added statistics are NAE clause-variable memberships (expected O(L)), homologous pair count (O(1)) and capacity bits (O(m)), Partition's existing total sum (O(n)), and ThreePartition's existing bound (O(1)). Incoming SAT and 3D-matching contracts are updated. Five original unavailable raw numeric fields become available. LCS's exponential cross-frequency product and SubsetSum→Partition's arbitrary-precision raw total remain precisely unavailable; their schema/variable-exponent limitations are documented without expanding #1175 into engine redesign.
The test-only cleanup at 29d2373 reuses measured and predicted parameters from the existing contract check instead of constructing targets and evaluating predictions twice. All assertions remain. The 51 existing overhead tests pass, and
make checkandmake paperpass again at this follow-up. Production code is unchanged from 6f9dbe9; construction measurements and correctness records keep their original commit provenance.Fresh evidence at 6f9dbe9, built exclusively from this worktree:
44537006and previous dashboarda44a350c). Corpus remainsb9ae9e39; no instances or oracle values changed. The intermediate4e20d877run is also preserved with its own provenance.make check(format, all-feature clippy, workspace tests including ignored tests/docs) andmake paperpass. Changed production methods/closures have 98.14% instrumented-region coverage; the retained invariant-error closure is explicitly recorded as unexercised.Immediate improvement from the previous dashboard (
a44a350c) to this commit, using the same 100 inputs per field:num_quadratic_termsnum_edgesnum_nonzerosRatios exclude zero actuals. Equality and absolute excess include them; zero columns are both-zero/positive-for-zero counts. P95 interpolates at (n−1)×0.95. CVP still has 50 zero-actual cases with positive predictions: the geometric relaxation does not compute the concrete rounded residual or Gram cancellations. CVP and grid declarations remain proved bounds; observed equality is not a basis for exactness.
Other leading improvements against prerequisite 4453700
num_available_assignmentsnum_quadratic_termsnum_nonzero_requirementsnum_nonzerosnum_nonzerosnum_nonzerosnum_nonzerosnum_nonzerosnum_constraintsnum_nonzerosnum_nonzerosnum_nonzerosnum_nonzerosnum_nonzerosnum_nonzerosmax_constraint_magnitude_bitsThe unified private dashboard (version 8, source
49110a96) preserves its URL, Sites project and owner-only audience. The measured table and per-rule details retain correctness results, true numeric ratios, case evidence and run provenance. The overview axis ends at 64×; larger values show an overflow arrow and their true maximum. Local and hosted browser checks pass for filters, downloads, pagination, mobile layout and removal of the four supplementary sections. Underlying evidence files are retained unchanged, and the hosted snapshot matches the local artifact.The inventory retains 406 upper-bound fields with median ratio above one and 195 fields with same-complete-source-vector/different-target observations. This focused PR does not close the broader systematic-tightening issue merely because this batch passes.
Refs #1188. Prerequisite #1174 is squash-merged; this PR now targets
main. Related availability work: #1175.Review follow-up:
76c7d3acincludes the reviewed solver fixes from #1174, including budgeted quadratic preprocessing and large ensemble union chains, plus the current-Clippy compatibility fix. The branch incorporates the prerequisite squash merge with a regular merge commit, preserving published history. Its tree is identical to the combined head8c7fd591.make checkandmake paperboth pass on this combined tree. All nine CI and Codecov checks pass on final commit76c7d3ac. The original construction-corpus measurements above retain their recorded provenance; they were not rerun.