Repository navigation
Fix SimultaneousIncongruences complexity to include the search period - #1212
Conversation
…ucture' into fix/simultaneous-incongruences-complexity
Agentic Review ReportScope: six-file diff against StructuralNo critical or important findings. The new parameter reaches the model, complexity registration, incoming reduction, tests, and paper. No generated exports or unrelated changes are included. QualityThe arithmetic is sound: Feature testThe independent reviewer inspected the tests and manually checked the arithmetic. The existing standalone CLI binary was stale, so it was not used as evidence for this revision. Workspace library, integration, and CLI tests have passed; the remaining local gates will be recorded in the PR description. FindingsNone requiring changes. Coverage and a separate fresh standalone CLI walkthrough were not run. Better general exact bounds remain explicitly unverified, as documented. Please kindly check the following items (PR #1212):
Join the discussion on Zulip — feel free to ask questions or leave feedback there. |
Each ILP rule's num_nonzeros upper bound was num_constraints * num_vars, a dense-matrix bound that the corpus measured at under half of its prediction on 55 rules. Derive the bound from each reduce_to's constraint families instead, summing the terms each family contributes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Canonical examples are sparse, so a constraint family missing from a per-family nonzero count can go unnoticed. Reduce dense instances of five rules with the most constraint families and require the measured count to stay within the declared bound. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
StaffScheduling -> DecisionQUBO assumed 63 bits per worker count, and SequencingWithReleaseTimesAndDeadlines -> DecisionQUBO assumed every task may start anywhere in [0, time_horizon]. Neither source exposed the quantity the construction actually depends on, so the bounds ran three to four orders of magnitude above the corpus measurements. Add num_workers_bits to StaffScheduling and max_start_slots to SequencingWithReleaseTimesAndDeadlines, state both QUBO bounds in them, and declare the new fields in the two rules that target these models. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The sparse-support test kept the 63-bit StaffScheduling budget, so a regression to the old formula would still pass. Tighten it to the new prediction, add an SWRTD case, and restate both proofs' size bounds in the new parameters, including the two incoming rules that declare them. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The bound K counts selected columns, but try_new accepted any negative value. Such an instance panicked in parameters(), whose bound must fit u64, and its ILP reduction cast the bound with `as usize`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The corpus measured 81 non-trivial upper-bound fields at exactly their prediction on every instance. Of those, 46 fields in 30 rules are exact by construction: every row family and variable block is emitted unconditionally, the source invariants (simple graphs, exactly-K clauses, n divisible by 3, 1 <= k <= n) rule out merged or dropped terms, and no early return builds a different target. The rest stay upper bounds: degenerate-input shortcuts, data-dependent zero coefficients or cancelled literals, and QUBO entries where penalty and objective terms can cancel. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
KSatisfiability<K3>::new_allow_less admits clauses with fewer than three literals, so 3SAT -> KClique num_vertices and 3SAT -> DecisionMVC num_edges shrink below their formulas. Return both to upper_bound, pin the relations with short-clause instances, and lay out the transform declarations by nesting depth. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The exact claims for HamiltonianCircuit, MaximalIS, MinimumDominatingSet, MaximumMatching, Kernel, PartitionIntoPathsOfLength2, PartitionIntoPerfectMatchings and PartitionIntoCliques were checked only on canonical examples. Pin them on empty, path and complete graphs with up to three vertices, k = 1 and k = n, and antiparallel arcs. Also promote MinimumVertexCover -> EnsembleComputation num_subsets, one subset per edge, and convert the ConsecutiveOnesSubmatrix bound with try_from now that construction keeps it nonnegative. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
MaxCut<SimpleGraph, i64> accepts negative weights, but the rule rejected
them, so every planned path through it (for example Max2SAT -> MaxCut ->
MinimumMatrixCover) failed on ordinary inputs. Replace each negative edge
{u, v} by an auxiliary vertex joined to v with |w| + 1 and to u with |w|:
every maximum cut separates the auxiliary vertex from v, so the gadget
shifts the cut by the constant 2|w| + 1 and preserves maximum cuts.
Extraction drops the auxiliary bits; num_rows becomes an upper bound.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- ConsecutiveOnesSubmatrix stores its column-count bound as usize, so serde and the CLI reject negatives by type and the model and ILP rule drop their conversions. - The MaxCut -> MinimumMatrixCover gadget computes |w| + 1 as 1 - w with one checked subtraction; module docs and the paper's duplicate extraction paragraph now describe the auxiliary vertices. - The PartitionIntoPathsOfLength2 comment states why its counts are exact. - The degenerate-graph test covers every valid k; transform layouts are consistent. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
KSatisfiability<KN> was Satisfiability under another name: it checked no clause width and its only edges were identity casts into and out of it. Every path from K2 or K3 paid an extra hop through it. - Drop the KN variant; K2 and K3 now reduce directly to Satisfiability and K3 is the default variant. - Remove new_allow_less/try_new_allow_less. K2 and K3 always hold exactly K literals per clause, matching what serde and the CLI already enforced. - Delete the short- and empty-clause branches these constructors forced on 3-SAT rules, and declare 3SAT -> KClique num_vertices and 3SAT -> DecisionMVC num_edges exact again. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…e text SAT -> NAE turns every three-literal clause into a four-literal one, so the MonochromaticTriangle vertex, edge and triangle counts are equalities and its two-literal branch was dead. Also remove leftover short- and empty-clause wording and dead padding in OneInThree, QuadraticCongruences and Kernel. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
- Add a FixedK sub-trait implemented by K1..K5, and bound KSatisfiability and the SAT/K-SAT results by it, so KSatisfiability<KN> no longer type-checks instead of failing at construction. - Register each K-SAT aggregate mapping inside the macro that registers its witness edge, and take the SAT -> K-SAT clause width from the type. - Allocate CyclicOrdering's fresh padding variables with allocate_many. - Drop leftover braces in two tests and a stale QuadraticCongruences note. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Removing the KSatisfiability KN variant does not need a new variant trait. Keep KSatisfiability bounded by KValue with the runtime width check. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
GiggleLiu
left a comment
GiggleLiu
left a comment
There was a problem hiding this comment.
Agentic Review Report
PR #1212. Reviewed head 55823fbc894647fa83cfc70b7c60bca6bcba673e against own base 25ac12740957c303ed1c863c0eaa1ac16bfaeb86 (feat/graph-explorer-overhead-structure). Read-only review; no tracked edits, pushes, PR comments or merges.
Verdict
No new correctness blocker found. The change is reasonable to merge after its base stack is corrected and integrated. It is currently dependency-blocked by #1211/#1196, not rejected on the LCM-bound arithmetic.
Structural
Reviewed the model, incoming 3-SAT reduction, changed tests and relevant paper text against the PR's own base. Every incoming target-field contract now includes lcm_bits. lcm_moduli() is safe under the existing construction/serde range check. lcm_bits=floor(log2 L)+1 is correct for every positive supported L, including L=1 for empty input and i64::MAX.
Quality
The metadata regression distinguishes identical pair counts with different periods. Tests cover power-of-two boundaries, shared factors, empty input and the maximum supported integer. The integration test composes the target solving cost and asserts nonpolynomial growth rather than merely checking the target parameter.
The bound is sound: each variable prime appears as a modulus and every clause modulus divides their product, so L is exactly the product of the variable primes. With p_i≤2(n+1)^2≤2^(2n+1), bitlength(L)≤n(2n+1)+1. For n=0 the RHS is 1. Exhausting one period costs O((num_pairs+1)2^lcm_bits), within a constant factor of the candidate count under the documented fixed-width operation model.
Feature test
Parent reviewer reports the full 6,319 library tests passed on exact #1218 head, which contains byte-identical model and reduction files from this PR. This reviewer independently traced the constructor, bound, target period and extraction but did not run a separate exact-head CLI walkthrough. git diff --check BASE...HEAD passed.
Findings / uncertainty
- Advisory: the repository defines catalog complexity as the best known exact algorithm, while this PR deliberately registers a documented exhaustive-search bound and says the best general bound is not independently verified. That disclosure is honest, and the new bound fixes a false polynomial claim. The literature-best question remains open rather than being established by this review. Keep that limitation visible or complete the literature verification before advertising it as best-known.
- No new Critical/Important implementation finding.
GitHub PR policy audit
GATE: PASS. This is the harm-signals gate only; it does not override the correctness verdict above.
- harm.secrets (
security.no-secrets): OK. No obvious credential/private-key/token addition detected in the own-base diff. - harm.dangerous-files (
git.harm-signals): OK. No conflict markers, unexplained archives or local scratch/config artifacts detected. - harm.generated-artifacts (
code.generated-artifacts): OK. No blacklisted generated graph/schema/example exports or build targets added. Test oracle fixtures are intentional test inputs; small browser contracts/fonts are intentional source assets. - harm.cache (
code.generated-cache): OK. No cache directories added. - harm.debug-leftovers (
code.debug-leftovers): OK. No debugger, breakpoint or temporary debug print addition detected. Browser performance marks are deliberate verification instrumentation. - pr.description-quality (
github.pr-description-quality): OK. Purpose, changes, validation and limitations are described. - pr.traceable (
github.prs-traceable): OK. The PR states its purpose and own stack context.
Policy evidence: own-base name/status, numstat and patch inspection; added-line secret/conflict/debug scan; git diff --check; gh-axi pr view 1212 --full --comments --reviews. No claim of exhaustive secret scanning. The parent reviewer owns the final head/base recheck before any merge.
Add SetSplitting → NAE-SAT clause-per-subset reduction
[Critical] Remove KSatisfiability KN variant and short-clause constructors
Declare exact parameter counts that constructions always produce
Tighten ILP num_nonzeros bounds to per-constraint counts
Tighten StaffScheduling and SWRTD QUBO size bounds
Add binary decision ILP to SAT and fix solution validators
Add staff-scheduling QUBO and tighten direct-reduction bounds
Add Phase 3 conditional direct QUBO reductions
Add Phase 2 direct QUBO reductions
Add Phase 1 direct QUBO encodings for scheduling and assignment
GiggleLiu
left a comment
GiggleLiu
left a comment
There was a problem hiding this comment.
Agentic Review Report: integration follow-up
The LCM-period arithmetic and incoming parameter bound passed independent review. The documented exhaustive-search bound fixes the previous false polynomial cost; a literature-best bound is still not established.
The semantic source tree is 0cf54de5aa06ad17aae5a480e77ad62747ef308c. Backend child PRs retain their merge records. The previously reviewed integration resolutions and this PR's original source are preserved; the GitHub ancestry merges have identical trees. #1219, #1220, and #1221 remain excluded.
Validation: the combined Rust 2024 integration passed 7,194 native tests, formatting, all-target/all-feature Clippy, the paper build, and 23 pipeline tests. The subsequent website-only changes do not alter native sources. The production verifier passed 336 browser cases before the last visual fix; that fix passes focused Chromium/Firefox/WebKit dark/light tests and independent review. Its fresh complete website run and final main CI are pending and remain required before merging the aggregate into main. This approval is for folding into the feature parent only.
Rechecked PR comments, inline comments, reviews, linked conversation, and coverage feedback. No new material concern. The independent quality and harm-signal gates passed. The previously documented compatibility breaks were accepted by the maintainer.
Stacked on #1211; base:
feat/graph-explorer-overhead-structure. Merge the parent first.The catalog previously assigned
SimultaneousIncongruencesa cost ofnum_pairs, omitting the search over an entire LCM period and making the target appear polynomial-time. This change exposeslcm_bitsand uses(num_pairs + 1) * 2^lcm_bitsfor exhaustive search. The 3-SAT reduction supplies a polynomial upper bound on the new parameter, so composing its transform with target solving preserves the exponential cost.Adds model and parameter-bound regressions, extends the closed-loop reduction test, and documents the bound and its limitations in the paper. The literature's best general exact bound has not been independently verified.
Validation:
make check(formatting, workspace Clippy with all features, workspace tests including ignored tests and documentation tests),make paper, andgit diff --checkall pass. Independent review found no issues requiring changes. Working tree is clean.GitHub reports no CI checks for this stacked branch. Coverage and a separate fresh standalone CLI walkthrough were not run.