Tighten StaffScheduling and SWRTD QUBO size bounds

docs/paper/reductions.typ

@@ -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))$.
 ]
 

src/models/misc/sequencing_with_release_times_and_deadlines.rs

@@ -137,6 +137,25 @@ impl SequencingWithReleaseTimesAndDeadlines {
         self.lengths.len()
     }
 
+    /// Returns the largest number of in-window start times of any task.
+    pub fn max_start_slots(&self) -> u64 {
+        self.lengths
+            .iter()
+            .zip(&self.release_times)
+            .zip(&self.deadlines)
+            .map(|((&length, &release), &deadline)| {
+                // Nonnegative inputs keep `deadline - release` and the slack in range.
+                let slack = deadline - release;
+                if slack < length {
+                    0
+                } else {
+                    (slack - length).unsigned_abs() + 1
+                }
+            })
+            .max()
+            .unwrap_or(0)
+    }
+
     /// Returns the time horizon (maximum deadline).
     pub fn time_horizon(&self) -> i64 {
         self.deadlines.iter().copied().max().unwrap_or(0)
@@ -154,6 +173,7 @@ impl Problem for SequencingWithReleaseTimesAndDeadlines {
     type Value = crate::types::Or;
 
     crate::problem_parameters![
+        ("max_start_slots", max_start_slots),
         ("num_tasks", num_tasks),
         ("time_horizon", time_horizon),
         ("time_horizon_bits", time_horizon_bits),

src/models/misc/staff_scheduling.rs

@@ -163,6 +163,11 @@ impl StaffScheduling {
         self.num_workers
     }
 
+    /// Magnitude bits of the worker budget, with at least one bit.
+    pub fn num_workers_bits(&self) -> u64 {
+        crate::types::max_numeric_magnitude_bits([self.num_workers])
+    }
+
     /// Get the number of schedule patterns.
     pub fn num_schedules(&self) -> usize {
         self.schedules.len()
@@ -232,6 +237,7 @@ impl Problem for StaffScheduling {
         ("num_periods", num_periods),
         ("num_schedules", num_schedules),
         ("num_workers", num_workers),
+        ("num_workers_bits", num_workers_bits),
     ];
 
     fn evaluate(

src/rules/exactcoverby3sets_staffscheduling.rs

@@ -52,10 +52,14 @@ impl ReductionResult for ReductionXC3SToStaffScheduling {
 impl crate::rules::AggregateReductionResult for ReductionXC3SToStaffScheduling {}
 
 #[reduction(
-    transform = exact {
-        num_periods = "universe_size",
-        num_schedules = "num_subsets",
-        num_workers = "universe_size / 3",
+    transform = {
+        exact {
+            num_periods = "universe_size",
+            num_schedules = "num_subsets",
+            num_workers = "universe_size / 3",
+        },
+        // Transforms have no logarithm; q = universe_size / 3 has at most q + 1 bits.
+        upper_bound { num_workers_bits = "universe_size / 3 + 1", },
     }
 )]
 impl ReduceTo<StaffScheduling> for ExactCoverBy3Sets {

src/rules/sequencingwithreleasetimesanddeadlines_qubo.rs

@@ -35,7 +35,7 @@ impl crate::rules::AggregateReductionResult
     for ReductionSequencingWithReleaseTimesAndDeadlinesToQUBO
 {
 }
-#[crate::reduction(transform = upper_bound { num_vars = "num_tasks * (time_horizon + 1)", num_quadratic_terms = "(num_tasks * (time_horizon + 1))^2" })]
+#[crate::reduction(transform = upper_bound { num_vars = "num_tasks * max_start_slots", num_quadratic_terms = "num_tasks * max_start_slots * (num_tasks * max_start_slots - 1) / 2" })]
 impl ReduceTo<Decision<QUBO<i64>>> for SequencingWithReleaseTimesAndDeadlines {
     type Result = ReductionSequencingWithReleaseTimesAndDeadlinesToQUBO;
     fn reduce_to(&self) -> Result<Self::Result, ReductionError> {

src/rules/staffscheduling_qubo.rs

@@ -48,8 +48,8 @@ impl ReductionResult for ReductionStaffSchedulingToQUBO {
 impl crate::rules::AggregateReductionResult for ReductionStaffSchedulingToQUBO {}
 
 #[crate::reduction(transform = upper_bound {
-    num_vars = "63 * (num_schedules + num_periods + 1)",
-    num_quadratic_terms = "63 * (num_schedules + 1) * (63 * (num_schedules + 1) - 1) / 2 + num_periods * (3969 * num_schedules + 1953)",
+    num_vars = "num_workers_bits * (num_schedules + num_periods + 1)",
+    num_quadratic_terms = "num_workers_bits * (num_schedules + 1) * (num_workers_bits * (num_schedules + 1) - 1) / 2 + num_periods * num_workers_bits * (num_workers_bits * num_schedules + (num_workers_bits - 1) / 2)",
 })]
 impl ReduceTo<Decision<QUBO<i64>>> for StaffScheduling {
     type Result = ReductionStaffSchedulingToQUBO;

src/rules/threepartition_sequencingwithreleasetimesanddeadlines.rs

@@ -101,7 +101,11 @@ impl crate::rules::AggregateReductionResult for ReductionThreePartitionToSRTD {}
             num_tasks = "num_elements + num_groups - 1",
             time_horizon = "num_groups * (bound + 1) - 1",
         },
-        upper_bound { time_horizon_bits = "max_numeric_magnitude_bits + num_groups + 1", },
+        // Each task's start window lies within [0, time_horizon].
+        upper_bound {
+            time_horizon_bits = "max_numeric_magnitude_bits + num_groups + 1",
+            max_start_slots = "num_groups * (bound + 1)",
+        },
     },
 )]
 impl ReduceTo<SequencingWithReleaseTimesAndDeadlines> for ThreePartition {

src/unit_tests/models/misc/sequencing_with_release_times_and_deadlines.rs

@@ -39,6 +39,8 @@ fn test_sequencing_rtd_basic() {
     assert_eq!(problem.release_times(), &[0, 1, 5, 0, 8]);
     assert_eq!(problem.deadlines(), &[5, 6, 10, 3, 12]);
     assert_eq!(problem.time_horizon(), 12);
+    // Start windows hold [3, 4, 2, 3, 3] start times.
+    assert_eq!(problem.max_start_slots(), 4);
     // Lehmer code dims: [5, 4, 3, 2, 1]
     assert_eq!(problem.dimensions(), vec![5, 4, 3, 2, 1]);
     assert_eq!(
@@ -97,6 +99,7 @@ fn test_sequencing_rtd_empty_instance() {
     let problem = SequencingWithReleaseTimesAndDeadlines::new(vec![], vec![], vec![]);
     assert_eq!(problem.num_tasks(), 0);
     assert_eq!(problem.time_horizon(), 0);
+    assert_eq!(problem.max_start_slots(), 0);
     assert_eq!(problem.dimensions(), Vec::<usize>::new());
     assert!(problem.evaluate(&vec![]).unwrap());
 }
@@ -172,3 +175,17 @@ fn test_sequencing_rtd_invalid_task_index() {
         Err(crate::traits::EvaluationError::InvalidConfiguration(_))
     ));
 }
+
+#[test]
+fn test_sequencing_rtd_max_start_slots_extremes() {
+    // A release after the deadline or a task longer than its window has no start.
+    let closed = SequencingWithReleaseTimesAndDeadlines::new(vec![0, 3], vec![5, 0], vec![4, 2]);
+    assert_eq!(closed.max_start_slots(), 0);
+    // The widest window, [0, i64::MAX] with length 0, has 2^63 starts.
+    let widest = SequencingWithReleaseTimesAndDeadlines::new(
+        vec![0, i64::MAX],
+        vec![0, i64::MAX],
+        vec![i64::MAX, 0],
+    );
+    assert_eq!(widest.max_start_slots(), 1 << 63);
+}

src/unit_tests/models/misc/staff_scheduling.rs

@@ -62,6 +62,7 @@ fn test_staff_scheduling_creation() {
     assert_eq!(problem.num_schedules(), 5);
     assert_eq!(problem.requirements(), &[2, 2, 2, 3, 3, 2, 1]);
     assert_eq!(problem.num_workers(), 4);
+    assert_eq!(problem.num_workers_bits(), 3);
     assert_eq!(problem.dimensions(), vec![5; 5]);
 }
 
@@ -149,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);
+}

src/unit_tests/parameter_formula_validation.rs

@@ -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.