You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Commit b84842c
Browse filesBrowse the repository at this point in the historyBrowse files
Copy file name to clipboardExpand all lines: docs/paper/reductions.typ
+6-2Lines changed: 6 additions & 2 deletions
Original file line number
Diff line number
Diff line change
@@ -12318,7 +12318,7 @@ _Solution extraction and bounds._ Copy the subset bits; aggregate recovery is id
12318
12318
12319
12319
_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.
12320
12320
12321
-
_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.
12321
+
_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.
12322
12322
12323
12323
*Example.* #let ex = load-example("StaffScheduling", "DecisionQUBO")
12324
12324
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
13141
13141
][
13142
13142
_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.
13143
13143
_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.
13144
-
_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.
13144
+
_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.
13145
13145
13146
13146
*Example.* #let ex = load-example("SequencingWithReleaseTimesAndDeadlines", "DecisionQUBO")
13147
13147
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.
@@ -17893,6 +17893,8 @@ The following table shows concrete target-variable counts for example instances,
17893
17893
17894
17894
_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$.
17895
17895
17896
+
_Size._ The budget $q$ has at most $q+1$ magnitude bits; transforms carry no logarithm, so the declared bound is linear in $|X|/3$.
17897
+
17896
17898
_Solution extraction._ Map $w in NN^m$ to $c in {0,1}^m$ by $c[j] = 1$ if $w[j] > 0$.
17897
17899
]
17898
17900
@@ -19902,6 +19904,8 @@ The following table shows concrete target-variable counts for example instances,
19902
19904
19903
19905
_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.
19904
19906
19907
+
_Size._ Every release time and deadline lies in $[0, m(B+1)-1]$, so no task has more than $m(B+1)$ start times.
19908
+
19905
19909
_Solution extraction._ Decode the Lehmer code, simulate the schedule tracking start times; assign elements to groups by $floor("start" / (B+1))$.
0 commit comments