[isPANN]

Summary

The corpus accuracy report found these two direct QUBO rules to have the loosest bounds:

• StaffScheduling → DecisionQUBO assumed 63 bits per worker count.
• SequencingWithReleaseTimesAndDeadlines → DecisionQUBO assumed every task may start anywhere in [0, time_horizon].

Neither source model exposed the quantity the construction actually depends on, so this PR adds one parameter to each:

• StaffScheduling::num_workers_bits: the magnitude bits of the worker budget, the same convention as time_horizon_bits.
• SequencingWithReleaseTimesAndDeadlines::max_start_slots: the largest start window of any task. It always fits in u64 (at most 2^63), so the model accepts exactly the same inputs as before. A per-instance total, like SequencingWithinIntervals::num_start_slots, could exceed u64.

Both QUBO bounds are now stated in terms of these parameters. The two rules that target these models also declare the new fields:

• ExactCoverBy3Sets → StaffScheduling: num_workers_bits ≤ universe_size/3 + 1. Transforms have no logarithm, so this can't be tighter.
• ThreePartition → SWRTD: max_start_slots ≤ num_groups·(bound+1).

Corpus measurement (100 instances per rule, 0 violations)

Rule / field	max ratio before	after
StaffScheduling num_vars	0.044	0.93
StaffScheduling num_quadratic_terms	0.0016	0.75
SWRTD num_vars	0.10	1.0
SWRTD num_quadratic_terms	0.0007	0.15

SWRTD's quadratic count still depends on how much the start intervals overlap, which no parameter expresses.

Workspace tests, fmt and clippy pass. Stacked on #1218.

🤖 Generated with Claude Code

[isPANN]

Agentic Review Report

PR #1223: Tighten StaffScheduling and SWRTD QUBO size bounds. Reviewed head 4ce1d380 against feat/binary-ilp-to-sat (8 files).

Structural

• No generated exports, unrelated edits, or trait/macro changes. The new parameters are registered through problem_parameters!. Both incoming rules now declare every target field: ExactCoverBy3Sets→StaffScheduling adds num_workers_bits, and ThreePartition→SWRTD adds max_start_slots. Composition works. pred path ExactCoverBy3Sets DecisionQUBO renders the composed bound.
• max_start_slots: construction and serde both go through try_new, which rejects negative lengths, releases and deadlines. So deadline - release cannot overflow. When the window is open, slack - length lies in [0, i64::MAX] and +1 stays at most 2^63 in u64. This agrees exactly with StartChoices::encode's per-task choices.
• num_workers_bits = max_numeric_magnitude_bits([num_workers]) equals binary_weights(num_workers).len() for W ≥ 1, and is 1 instead of 0 when W = 0. Both directions are safe.

Semantic check of the formulas (by hand)

• StaffScheduling→DecisionQUBO. Let b = |weights| ≤ B and S = num_schedules. The variables are b·S count bits, b budget bits, and Σ_{r_t>0} |bw(W−r_t)| surplus bits. Since 0 ≤ W−r_t < W, each surplus block has at most B bits. That gives ≤ B(S+P+1) variables. QUBO::num_quadratic_terms counts only off-diagonal entries (i != j).
  • The budget square creates at most C(b(S+1), 2) pairs.
  • Each coverage square reuses count–count pairs that the budget row already holds. It adds only count×surplus pairs (≤ B·B·S) and surplus×surplus pairs (≤ C(B,2)). Surplus blocks of different periods are disjoint, so the per-period term B(BS + (B−1)/2) is valid.
  • The early-return path builds a 0-variable QUBO.
  • Periods with r_t ≤ 0 add nothing but are still counted in P.
  • Valid upper bound.
• SWRTD→DecisionQUBO. num_vars = Σ counts ≤ n·max_start_slots. Pairs ≤ C(num_vars, 2) ≤ C(n·M, 2), since x(x−1)/2 is monotone for x ≥ 0. Valid.
• ThreePartition→SWRTD. Every task has release ≥ 0 and deadline ≤ horizon = m(B+1)−1, so each window has at most m(B+1) starts. Fillers have exactly 1. Measured on the canonical example: 28 ≤ 32. Valid.
• XC3S→StaffScheduling. bits(⌊u/3⌋) ≤ ⌊u/3⌋+1 ≤ u/3+1. Valid.
• Adversarial measurements (pred path … instance.json against the formulas):
  • StaffScheduling with W ∈ {0, 1, 2, 3, 7, 8, 1023, 2^20}, signed, zero and maximal requirements, plus the early-return case: 0 violations. W=1023 meets both bounds exactly (50 vars, 1125 pairs).
  • 12 random SWRTD instances, including empty windows: 0 violations.

Quality

• cargo test --workspace: all pass. cargo fmt --check: clean.
• The model tests cover max_start_slots at 0, a typical value, and the 2^63 extreme. num_workers_bits gets one assertion, with no W=0 case.
• The sparse-support regression test still uses the old 63-bit budget (see findings).

Feature test

• make cli.
• pred show StaffScheduling / pred show SequencingWithReleaseTimesAndDeadlines list the new parameters and the restated bounds.
• pred path with instances measures sizes as listed above.

Findings

Critical: none.

Important

1. src/unit_tests/parameter_formula_validation.rs:455-467: the comment still says "at most 63 bits per integer". The budget 73_206 belongs to the old formula, so this test would not catch a regression back to it. For this instance (W=3, S=3, P=3) the new prediction is 28 + 39 = 67. Tighten the budget to 67 and fix the comment. Also add an SWRTD instance to the same test, so the max_start_slots bound is pinned.
2. docs/paper/reductions.typ:12321: the StaffScheduling→DecisionQUBO proof still derives N=63(s+p+1) and binom(63(s+1),2)+p(3969s+1953). The auto-rendered overhead now shows the num_workers_bits formula. Restate the size paragraph in terms of B = b(W): B(s+p+1) variables, and binom(B(s+1),2) + p·B(Bs+(B−1)/2) couplings. The per-period argument already in the text carries over unchanged.
3. docs/paper/reductions.typ:13144: the SWRTD→DecisionQUBO size paragraph still bounds S ≤ n(T+1). State S ≤ n·M, where M = max_i max(0, d_i−p_i−r_i+1) is max_start_slots, so the prose justifies the registered formula.

Minor
4. docs/paper/reductions.typ:17873 (XC3S→StaffScheduling) and :19887 (ThreePartition→SWRTD): neither proof mentions the newly declared target fields. Add one sentence each: bits(q) ≤ q+1, and windows ⊆ [0, m(B+1)−1].
5. src/rules/exactcoverby3sets_staffscheduling.rs:62: without log, the composed ExactCoverBy3Sets→StaffScheduling→DecisionQUBO bound now grows as (u/3+1)²·(s+u). The old bound used 63 bits and grew linearly in u. The new one is looser once q+1 > 63 (u ≥ ~186). The direct XC3S→DecisionQUBO edge dominates this path, so the impact is small, but mention the trade-off in the PR or the paper.
6. src/unit_tests/models/misc/staff_scheduling.rs:65: add a num_workers = 0 → num_workers_bits = 1 assertion to pin the floor.

[isPANN]

Addressed the review in 0801132:

• Important 1: the StaffScheduling sparse-support budget is now 67, the new prediction, so a regression to the 63-bit formula fails. Added an SWRTD case with budget binom(9,2) = 36.
• Important 2 and 3: the paper's StaffScheduling → DecisionQUBO proof now states its bounds in β = bits(W). The SWRTD size paragraph now uses S ≤ n·w, where w is the largest start window.
• Minor:
  • The ExactCoverBy3Sets → StaffScheduling and ThreePartition → SWRTD proofs now each have a Size line justifying the new fields.
  • Added a num_workers = 0 → num_workers_bits = 1 test.
  • The looser composed ExactCoverBy3Sets → StaffScheduling → QUBO bound is a known trade-off: transforms have no log. The direct ExactCoverBy3Sets → DecisionQUBO edge is tighter.

🤖 Generated with Claude Code

[GiggleLiu]

Agentic Review Report

PR #1223: Tighten StaffScheduling and SWRTD QUBO size bounds

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

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

Structural and semantic review

Reviewed both tightened direct-QUBO bounds, new model parameters, incoming reduction metadata, tests, and manual updates against exact #1218.

StaffScheduling uses B = magnitude bits of workers (minimum one), s schedules, and p periods. Count and slack domains require at most B bits each, giving N <= B(s+p+1). Budget terms form a clique of at most B(s+1) variables. Each period contributes at most B surplus variables, B²*s count/surplus pairs, and choose(B,2) surplus pairs. Summing yields the declared coupling bound. W=0 deliberately has B=1, an upper bound on the zero bits actually allocated.

SequencingWithReleaseTimesAndDeadlines computes max_start_slots from each task's release, deadline, and duration. All time fields are nonnegative i64, so deadline−release stays in i64. A negative available window yields zero slots; otherwise the nonnegative result plus one is widened before adding and fits u64 even at the i64 boundary. Total variables are at most n*max_start_slots, and all couplings are bounded by its complete graph.

Incoming X3C and ThreePartition reductions conservatively bound the newly required parameters. Checked that their source invariants imply the declared worker-bit/window bounds. No domain restriction, solver behavior, or extraction change is introduced.

Quality review

Regression expectations include W=0, workers requiring remainder bits, extreme windows, the staff coupling bound 67 on the selected 3-schedule/3-period instance, and the SWRTD bound 36 for three tasks with maximum window 3. The proof of the coupling bound counts actual interactions and does not rely on those example values.

Feature tests and verification limits

No exact #1223 compilation or metadata tests were run by this reviewer because the shared build slot was reserved for supported descendant tests, the #1224 numeric reproduction, and another independent PR. Source/target CLI behavior for the underlying StaffScheduling and SWRTD encodings was exercised on #1218 and passed, but that binary predates these metadata changes and does not validate these new formulas. This distinction is intentional.

Own-base git diff --check passed. Read the complete affected tests and construction code and independently derived both bounds. No current GitHub CI results were visible in the collected stack metadata. Parent should run current integrated parameter tests before merge.

Findings (severity order)

No new blocking finding. The numeric formula changes appear safe. The inherited #1214 allocation panic is outside this diff and should be fixed before integrating this dependency chain.

GitHub PR Audit — #1223

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 0801132969fd4e442b06526a0fbfbc4956dd9209 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.