Skip to content

Commit 0dd7448

Browse files
committed
Add verified direct decision QUBO reduction for integer staff scheduling
1 parent 109985f commit 0dd7448

5 files changed

Lines changed: 306 additions & 1 deletion

File tree

‎docs/paper/reductions.typ‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12280,6 +12280,23 @@ _Solution extraction and bounds._ Copy the subset bits; aggregate recovery is id
1228012280
The canonical instance and target coefficients are shown below. Its source witness is #repr(ex.solutions.at(0).source_config); the displayed target witness decodes to it and meets the objective or feasibility certificate described above.
1228112281
]
1228212282

12283+
#reduction-rule("StaffScheduling", "DecisionQUBO", example: true,
12284+
extra: [#direct-qubo-commands("StaffScheduling", "DecisionQUBO")],
12285+
)[
12286+
Integer worker multiplicities reduce to bounded binary budget and coverage residuals, using the squared-equality construction of @lucas2014.
12287+
][
12288+
_Construction._ Let $s$ be the number of indexed schedule patterns, $p$ the number of periods, $W >= 0$ the worker budget, $a_(j t)$ the pattern incidence, and $r_t$ the signed requirement. Encode each count $c_j$ and unused budget $z$ in $[0,W]$ with bounded binary weights: successive powers of two and a final remainder, whose sum is exactly the upper bound. This represents every integer in the interval and no others. For each $r_t>0$, encode surplus $h_t$ in $[0,W-r_t]$. A requirement above $W$ instead emits the constant NO decision with no variables and bound $-1$. Otherwise expand
12289+
$ H=(sum_j c_j+z-W)^2 + sum_(t:r_t>0)(sum_j a_(j t)c_j-h_t-r_t)^2. $
12290+
Remove $C=W^2+sum_(t:r_t>0)r_t^2$ and use decision bound $-C$. Nonpositive requirements need no row, including the minimum signed integer; empty and duplicate patterns retain their source meaning.
12291+
12292+
_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.
12293+
12294+
_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 $N^2$ registered couplings and $O(s+p+(p+1)N^2)$ coefficient updates and row bookkeeping (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.
12295+
12296+
*Example.* #let ex = load-example("StaffScheduling", "DecisionQUBO")
12297+
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.
12298+
]
12299+
1228312300
#reduction-rule("ThreePartition", "DecisionQUBO", example: true,
1228412301
extra: [#direct-qubo-commands("ThreePartition", "DecisionQUBO")],
1228512302
)[

‎src/rules/ilp_i64_ilp_bool.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ fn overflow(operation: impl Into<String>) -> ReductionError {
1616
ReductionError::integer_overflow::<ILP<i64, i64, Bounded>, ILP<bool>>(operation)
1717
}
1818

19-
fn binary_weights(width: i64) -> Vec<i64> {
19+
pub(super) fn binary_weights(width: i64) -> Vec<i64> {
2020
if width == 0 {
2121
return Vec::new();
2222
}

‎src/rules/mod.rs‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -329,6 +329,7 @@ pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::Ru
329329
.extend(decisionminimumdominatingset_minimumsummulticenter::canonical_rule_example_specs());
330330
specs.extend(decisionminimumvertexcover_hamiltoniancircuit::canonical_rule_example_specs());
331331
specs.extend(exactcoverby3sets_staffscheduling::canonical_rule_example_specs());
332+
specs.extend(staffscheduling_qubo::canonical_rule_example_specs());
332333
specs.extend(closestvectorproblem_qubo::canonical_rule_example_specs());
333334
specs.extend(coloring_qubo::canonical_rule_example_specs());
334335
specs.extend(sequencingtominimizeweightedcompletiontime_qubo::canonical_rule_example_specs());
@@ -743,6 +744,12 @@ mod unit_schedule_qubo;
743744
#[path = "../unit_tests/rules/direct_qubo_conditional.rs"]
744745
mod direct_qubo_conditional_tests;
745746

747+
#[cfg(test)]
748+
#[path = "../unit_tests/rules/staffscheduling_qubo.rs"]
749+
mod staffscheduling_qubo_tests;
750+
751+
pub(crate) mod staffscheduling_qubo;
752+
746753
pub(crate) mod dynamicstorageallocation_qubo;
747754
pub(crate) mod minimumtardinesssequencingweighted_qubo;
748755
pub(crate) mod sequencingwithreleasetimesanddeadlines_qubo;

‎src/rules/staffscheduling_qubo.rs‎

Lines changed: 170 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,170 @@
1+
//! Bounded worker multiplicities with exact budget and coverage residuals.
2+
use crate::models::{algebraic::QUBO, misc::StaffScheduling, Decision};
3+
use crate::rules::ilp_i64_ilp_bool::binary_weights;
4+
use crate::rules::qubo_helpers::QuboBuilder;
5+
use crate::rules::traits::validate_target_witness;
6+
use crate::rules::{ExtractionResult, ReduceTo, ReductionError, ReductionResult};
7+
8+
#[derive(Debug, Clone)]
9+
pub struct ReductionStaffSchedulingToQUBO {
10+
target: Decision<QUBO<i64>>,
11+
weights: Vec<i64>,
12+
num_schedules: usize,
13+
}
14+
15+
impl ReductionResult for ReductionStaffSchedulingToQUBO {
16+
type Source = StaffScheduling;
17+
type Target = Decision<QUBO<i64>>;
18+
19+
fn target_problem(&self) -> &Self::Target {
20+
&self.target
21+
}
22+
23+
fn extract_solution(&self, bits: &Vec<bool>) -> ExtractionResult<Vec<usize>> {
24+
validate_target_witness(
25+
&self.target,
26+
bits,
27+
|value| value.0,
28+
"QUBO does not certify a staffing assignment",
29+
)?;
30+
(0..self.num_schedules)
31+
.map(|schedule| {
32+
let count: i64 = self
33+
.weights
34+
.iter()
35+
.enumerate()
36+
.filter(|(bit, _)| bits[schedule * self.weights.len() + bit])
37+
.map(|(_, &weight)| weight)
38+
.sum();
39+
usize::try_from(count).map_err(|_| {
40+
crate::rules::ExtractionError::invalid("worker count does not fit usize")
41+
})
42+
})
43+
.collect()
44+
}
45+
}
46+
47+
#[crate::aggregate_reduction(identity)]
48+
impl crate::rules::AggregateReductionResult for ReductionStaffSchedulingToQUBO {}
49+
50+
#[crate::reduction(transform = upper_bound {
51+
num_vars = "63 * (num_schedules + num_periods + 1)",
52+
num_quadratic_terms = "(63 * (num_schedules + num_periods + 1))^2",
53+
})]
54+
impl ReduceTo<Decision<QUBO<i64>>> for StaffScheduling {
55+
type Result = ReductionStaffSchedulingToQUBO;
56+
57+
fn reduce_to(&self) -> Result<Self::Result, ReductionError> {
58+
type Builder = QuboBuilder<StaffScheduling, Decision<QUBO<i64>>>;
59+
let overflow = Builder::overflow;
60+
let workers = self.num_workers();
61+
// Certify the source's count fold before any target coefficient cancellation.
62+
Self::exact_i64(self.num_schedules(), "counting schedule patterns")?
63+
.checked_mul(workers)
64+
.ok_or_else(overflow)?;
65+
if self
66+
.requirements()
67+
.iter()
68+
.any(|&required| required > workers)
69+
{
70+
let (target, _) = Builder::new(0).finish()?;
71+
return Ok(Self::Result {
72+
target: Decision::new(target, -1),
73+
weights: Vec::new(),
74+
num_schedules: self.num_schedules(),
75+
});
76+
}
77+
78+
let weights = binary_weights(workers);
79+
let count_bits = Builder::dimension(self.num_schedules(), weights.len())?;
80+
let mut num_vars = count_bits.checked_add(weights.len()).ok_or_else(overflow)?;
81+
let surpluses: Vec<_> = self
82+
.requirements()
83+
.iter()
84+
.enumerate()
85+
.filter(|(_, required)| **required > 0)
86+
.map(|(period, &required)| (period, required, binary_weights(workers - required)))
87+
.collect();
88+
for (_, _, surplus) in &surpluses {
89+
num_vars = num_vars.checked_add(surplus.len()).ok_or_else(overflow)?;
90+
}
91+
isize::try_from(Builder::dimension(
92+
num_vars,
93+
std::mem::size_of::<(usize, i64)>(),
94+
)?)
95+
.map_err(|_| overflow())?;
96+
97+
let mut q = Builder::new(num_vars);
98+
let mut budget = Vec::new();
99+
for schedule in 0..self.num_schedules() {
100+
budget.extend(
101+
weights
102+
.iter()
103+
.enumerate()
104+
.map(|(bit, &weight)| (schedule * weights.len() + bit, weight)),
105+
);
106+
}
107+
budget.extend(
108+
weights
109+
.iter()
110+
.enumerate()
111+
.map(|(bit, &weight)| (count_bits + bit, weight)),
112+
);
113+
q.affine_square(&budget, workers)?;
114+
let mut offset = count_bits + weights.len();
115+
for (period, required, surplus) in surpluses {
116+
let mut coverage = Vec::new();
117+
for (schedule, pattern) in self.schedules().iter().enumerate() {
118+
if pattern[period] {
119+
coverage.extend(
120+
weights
121+
.iter()
122+
.enumerate()
123+
.map(|(bit, &weight)| (schedule * weights.len() + bit, weight)),
124+
);
125+
}
126+
}
127+
coverage.extend(
128+
surplus
129+
.iter()
130+
.enumerate()
131+
.map(|(bit, &weight)| (offset + bit, -weight)),
132+
);
133+
q.affine_square(&coverage, required)?;
134+
offset += surplus.len();
135+
}
136+
let (target, constant) = q.finish()?;
137+
Ok(Self::Result {
138+
target: Decision::new(target, constant.checked_neg().ok_or_else(overflow)?),
139+
weights,
140+
num_schedules: self.num_schedules(),
141+
})
142+
}
143+
}
144+
145+
#[cfg(feature = "example-db")]
146+
pub(crate) fn canonical_rule_example_specs() -> Vec<crate::example_db::specs::RuleExampleSpec> {
147+
vec![crate::example_db::specs::RuleExampleSpec {
148+
id: "staffscheduling_qubo",
149+
build: || {
150+
crate::example_db::specs::rule_example_with_witness::<_, Decision<QUBO<i64>>>(
151+
StaffScheduling::new(
152+
2,
153+
vec![
154+
vec![true, true, false],
155+
vec![false, true, true],
156+
vec![true, false, true],
157+
],
158+
vec![2, 2, 2],
159+
3,
160+
),
161+
crate::export::SolutionPair {
162+
source_config: serde_json::json!([1, 1, 1]),
163+
target_config: serde_json::json!([
164+
true, false, true, false, true, false, false, false, false, false, false
165+
]),
166+
},
167+
)
168+
},
169+
}]
170+
}
Lines changed: 111 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
use crate::models::{algebraic::QUBO, misc::StaffScheduling, Decision};
2+
use crate::rules::direct_qubo_tests::{direct, feasible};
3+
use crate::rules::registry::reduction_entries;
4+
use crate::rules::ReductionError;
5+
use crate::Problem;
6+
7+
#[test]
8+
fn test_staffscheduling_to_qubo_closed_loop() {
9+
// A single pattern must receive two workers, not a Boolean selection.
10+
feasible(
11+
StaffScheduling::new(1, vec![vec![true]], vec![2], 2),
12+
true,
13+
4,
14+
);
15+
feasible(
16+
StaffScheduling::new(1, vec![vec![true], vec![true]], vec![2], 2),
17+
true,
18+
6,
19+
);
20+
// Three pair-covering patterns cannot cover six required shifts with two workers.
21+
feasible(
22+
StaffScheduling::new(
23+
2,
24+
vec![
25+
vec![true, true, false],
26+
vec![false, true, true],
27+
vec![true, false, true],
28+
],
29+
vec![2, 2, 2],
30+
2,
31+
),
32+
false,
33+
8,
34+
);
35+
// Coverage may exceed the requirement; the worker budget remains an inequality.
36+
feasible(
37+
StaffScheduling::new(1, vec![vec![true]], vec![1], 3),
38+
true,
39+
6,
40+
);
41+
}
42+
43+
#[test]
44+
fn test_staffscheduling_empty_signed_and_impossible_requirements() {
45+
feasible(
46+
StaffScheduling::new(0, vec![vec![], vec![]], vec![], 0),
47+
true,
48+
0,
49+
);
50+
feasible(StaffScheduling::new(9, vec![], vec![], 2), true, 2);
51+
feasible(StaffScheduling::new(1, vec![], vec![1], 2), false, 3);
52+
feasible(
53+
StaffScheduling::new(1, vec![vec![true]], vec![3], 2),
54+
false,
55+
0,
56+
);
57+
feasible(
58+
StaffScheduling::new(0, vec![vec![false]], vec![i64::MIN], 1),
59+
true,
60+
2,
61+
);
62+
feasible(
63+
StaffScheduling::new(1, vec![vec![true]], vec![0], 0),
64+
true,
65+
0,
66+
);
67+
}
68+
69+
#[test]
70+
fn test_staffscheduling_completed_decision_recovery() {
71+
let source = StaffScheduling::new(1, vec![vec![true]], vec![2], 2);
72+
let reduction = direct::<_, Decision<QUBO<i64>>>(&source);
73+
let recovered = reduction
74+
.extract_solution_dyn(&vec![true, true, false, false])
75+
.unwrap();
76+
assert_eq!(recovered.downcast_ref::<Vec<usize>>().unwrap(), &[2]);
77+
let entry = reduction_entries()
78+
.into_iter()
79+
.find(|entry| {
80+
entry.source_name == StaffScheduling::NAME && entry.target_name == "DecisionQUBO"
81+
})
82+
.unwrap();
83+
let aggregate = entry.reduce_aggregate_fn.unwrap()(&source).unwrap();
84+
for value in [false, true] {
85+
assert_eq!(
86+
aggregate
87+
.extract_value_dyn(serde_json::json!(value))
88+
.unwrap(),
89+
serde_json::json!(value)
90+
);
91+
}
92+
}
93+
94+
#[test]
95+
fn test_staffscheduling_rejects_unrepresentable_source_and_target_arithmetic() {
96+
let entry = reduction_entries()
97+
.into_iter()
98+
.find(|entry| {
99+
entry.source_name == StaffScheduling::NAME && entry.target_name == "DecisionQUBO"
100+
})
101+
.expect("staffing must have a direct decision QUBO route");
102+
for source in [
103+
StaffScheduling::new(0, vec![vec![], vec![]], vec![], i64::MAX),
104+
StaffScheduling::new(1, vec![vec![true]], vec![1], 1_i64 << 32),
105+
] {
106+
assert!(matches!(
107+
(entry.reduce_fn.unwrap())(&source),
108+
Err(ReductionError::IntegerOverflow { .. })
109+
));
110+
}
111+
}

0 commit comments

Comments
 (0)