@@ -12318,7 +12318,7 @@ _Solution extraction and bounds._ Copy the subset bits; aggregate recovery is id
 
  _Correctness._ $arrow.r.double$: a feasible staffing vector has unused budget $z=W-sum_j c_j$ and nonnegative coverage surplus at most $W-r_t$, so all squares vanish. $arrow.l.double$: a target witness meeting the bound has $H<=0$. Every square is nonnegative, so the budget and coverage equations hold exactly. All decoded counts are nonnegative, their sum is at most $W$, and every positive requirement is met. Nonpositive requirements hold automatically. Unit penalties suffice because this endpoint is feasibility, with no competing objective.
 
- _Solution extraction and bounds._ Validate target feasibility, then sum each schedule's weighted bits. Aggregate `Or` recovery is identity, including NO results and the existing ExactCoverBy3Sets incoming route. With $b(B)=ceil(log_2(B+1))$, the exact variable count outside the early NO case is $(s+1)b(W)+sum_(t:r_t>0)b(W-r_t)$. For `i64` budgets this is at most $N=63(s+p+1)$, with at most $binom(63(s+1),2)+p(3969s+1953)$ registered couplings. The budget row already contains every count-count pair and every count-budget pair. Each period adds only count-surplus pairs (at most $63^2 s$) and within-surplus pairs (at most $binom(63,2)$); different periods' surplus blocks never interact. The coupling bound is therefore $O(s^2+s p+p)$, linear in periods for fixed schedule count. Construction performs $O((p+1)(s+1)^2+s+p)$ coefficient updates and row bookkeeping under the fixed 63-bit bound, since each coverage square may revisit count-count coefficients; ordered-map updates add a logarithmic factor. Bit counts grow logarithmically with the budget. Before expansion, check $s W$ to protect the source's count and coverage folds. Dimension arithmetic, expanded coefficients, omitted constant, and separate positive and negative coefficient sums are checked independently; an unrepresentable construction returns a typed overflow error. The conservative guard can reject representable special cases.
+ _Solution extraction and bounds._ Validate target feasibility, then sum each schedule's weighted bits. Aggregate `Or` recovery is identity, including NO results and the existing ExactCoverBy3Sets incoming route. With $b(B)=ceil(log_2(B+1))$, the exact variable count outside the early NO case is $(s+1)b(W)+sum_(t:r_t>0)b(W-r_t)$. With $beta$ the magnitude bits of $W$ (so $b(W-r_t)<=b(W)<=beta$), this is at most $N=beta(s+p+1)$, with at most $binom(beta(s+1),2)+p(beta^2 s+binom(beta,2))$ registered couplings. The budget row already contains every count-count pair and every count-budget pair. Each period adds only count-surplus pairs (at most $beta^2 s$) and within-surplus pairs (at most $binom(beta,2)$); different periods' surplus blocks never interact. The coupling bound is therefore $O(s^2+s p+p)$, linear in periods for fixed schedule count. Construction performs $O((p+1)(s+1)^2+s+p)$ coefficient updates and row bookkeeping for fixed $beta$, since each coverage square may revisit count-count coefficients; ordered-map updates add a logarithmic factor. Bit counts grow logarithmically with the budget. Before expansion, check $s W$ to protect the source's count and coverage folds. Dimension arithmetic, expanded coefficients, omitted constant, and separate positive and negative coefficient sums are checked independently; an unrepresentable construction returns a typed overflow error. The conservative guard can reject representable special cases.
 
  *Example.* #let ex = load-example("StaffScheduling", "DecisionQUBO")
  The canonical source assigns #repr(ex.solutions.at(0).source_config) workers across its #ex.source.instance.schedules.len() patterns, with budget #ex.source.instance.num_workers. The required coverages are #repr(ex.source.instance.requirements). The count blocks, unused-budget block and coverage-surplus blocks produce the displayed target; its canonical bits make every residual zero.
@@ -13141,7 +13141,7 @@ These constructions use the checked sparse penalty and extraction contracts abov
 ][
   _Construction._ First check that $max_i r_i+sum_i p_i$ fits the source integer type, bounding finish additions for every source order. Task $i$ chooses $t=r_i,dots,d_i-p_i$. An impossible window gives an empty row. Add squared one-hot rows and a unit pair penalty whenever neither selected task finishes before the other starts. Store the nonconstant energy with bound equal to the negative omitted constant.
   _Correctness._ ($arrow.r.double$) Earliest execution of a feasible source order gives valid choices without conflicts. ($arrow.l.double$) Zero-penalty choices are sorted by start, duration and index, placing zero-duration tasks first at a shared start. Inductively, earliest execution of that order starts no later than each selected start and finishes by its deadline. Source finish additions on recovered witnesses are bounded by these deadlines. Empty rows enforce NO and touching intervals are allowed.
-  _Extraction and size._ Decode and sort after target validation; completed feasibility maps identically. For $T=max_i d_i$, $S=sum_i max(0,d_i-p_i-r_i+1)<=n(T+1)$, with at most $S(S-1)/2$ couplings and $O(S^2)$ candidate pairs. This grid is pseudopolynomial in $T$, and can be much larger than the existing bounded-start route.
+  _Extraction and size._ Decode and sort after target validation; completed feasibility maps identically. For $T=max_i d_i$, $S=sum_i max(0,d_i-p_i-r_i+1)<=n w$, where $w<=T+1$ is the largest single start window, with at most $S(S-1)/2$ couplings and $O(S^2)$ candidate pairs. This grid is pseudopolynomial in $T$, and can be much larger than the existing bounded-start route.
 
  *Example.* #let ex = load-example("SequencingWithReleaseTimesAndDeadlines", "DecisionQUBO")
  The canonical source witness #repr(ex.solutions.at(0).source_config) maps to a target with #ex.target.instance.inner.num_vars variables; the exact source and target configurations are shown below.
@@ -17903,6 +17903,8 @@ The following table shows concrete target-variable counts for example instances,
 
   _Correctness._ ($arrow.r.double$) An exact cover $I$ with $|I| = q$ assigns one worker per selected schedule, covering each period exactly once. ($arrow.l.double$) A feasible assignment with $sum_j w_j = q$ and each period covered exactly once gives pairwise-disjoint schedules covering all of $X$.
 
+  _Size._ The budget $q$ has at most $q+1$ magnitude bits; transforms carry no logarithm, so the declared bound is linear in $|X|/3$.
+
   _Solution extraction._ Map $w in NN^m$ to $c in {0,1}^m$ by $c[j] = 1$ if $w[j] > 0$.
 ]
 
@@ -19912,6 +19914,8 @@ The following table shows concrete target-variable counts for example instances,
 
   _Correctness._ ($arrow.r.double$) A valid 3-partition fills each slot of width $B$ with exactly 3 elements; fillers are placed in their tight windows. ($arrow.l.double$) Fillers pinned to unit windows create $m$ slots of width $B$; total element work $m B$ fills all slots exactly; size constraints force 3 elements per slot.
 
+  _Size._ Every release time and deadline lies in $[0, m(B+1)-1]$, so no task has more than $m(B+1)$ start times.
+
   _Solution extraction._ Decode the Lehmer code, simulate the schedule tracking start times; assign elements to groups by $floor("start" / (B+1))$.
 ]
 
 
@@ -150,3 +150,9 @@ fn test_staff_scheduling_problem_name_and_variant() {
     assert_eq!(<StaffScheduling as Problem>::NAME, "StaffScheduling");
     assert!(<StaffScheduling as Problem>::variant().is_empty());
 }
+
+#[test]
+fn test_staff_scheduling_zero_workers_use_one_bit() {
+    let problem = StaffScheduling::new(1, vec![vec![true]], vec![0], 0);
+    assert_eq!(problem.num_workers_bits(), 1);
+}
@@ -417,7 +417,8 @@ fn direct_qubo_sparse_support_bounds_avoid_dense_cliques() {
     use crate::models::algebraic::QUBO;
     use crate::models::graph::OptimalLinearArrangement;
     use crate::models::misc::{
-        CyclicOrdering, ShortestCommonSuperstring, StackerCrane, StaffScheduling, ThreePartition,
+        CyclicOrdering, SequencingWithReleaseTimesAndDeadlines, ShortestCommonSuperstring,
+        StackerCrane, StaffScheduling, ThreePartition,
     };
     use crate::models::Decision;
     use crate::rules::{ReduceTo, ReductionResult};
@@ -452,7 +453,8 @@ fn direct_qubo_sparse_support_bounds_avoid_dense_cliques() {
             S::NAME
         );
     }
-    // Budget clique plus separate per-period surplus blocks, at most 63 bits per integer.
+    // Budget clique plus separate per-period surplus blocks, two bits for W = 3:
+    // binom(8, 2) + 3 * (2^2 * 3 + binom(2, 2)).
     check::<_, Decision<QUBO<i64>>>(
         StaffScheduling::new(
             2,
@@ -464,7 +466,12 @@ fn direct_qubo_sparse_support_bounds_avoid_dense_cliques() {
             vec![2, 2, 2],
             3,
         ),
-        73_206,
+        67,
+    );
+    // Three tasks with at most three start times each: binom(9, 2) couplings.
+    check::<_, Decision<QUBO<i64>>>(
+        SequencingWithReleaseTimesAndDeadlines::new(vec![1, 2, 1], vec![0, 0, 2], vec![3, 3, 4]),
+        36,
     );
     // Triangle terms, path/cycle transitions, and eligible value-triple multiplicities.
     // Vanishing factors must remain nonnegative and valid on empty/singleton inputs.