← back to the atlas

d4-conf-ecai-2022-0007 (d4-conf-ecai-2022-0007)

Answer: \(\mathrm{NP}\text{-complete}\)

The anchor (named result in the paper)

Theorem 1 (NP-hardness) — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateOSAP is NP-hard. 1Note that, depending on the satellites orbits, time references of time-tagged requests might not be included in any reservation window.

statement extracted from the paper’s text layer; consult the paper for the exact wording

The continuous mirror question, as graded

Given a finite satellite set, a finite rational time grid, and a society supported on \(\tau\) request types with rational masses \(\mu_t\) summing to \(1\), each type specifies a complete OSAP request template. For each type \(t\), let \(Q_t\) be its valid single-client OSAP allocations. Given rational satellite-time capacities \(\kappa_{sj}\) per unit of population mass, choose allocation masses \(x_{tq}\ge 0\) summing to \(\mu_t\) for each type, subject to aggregate use of every satellite-time cell \((s,j)\) not exceeding \(\kappa_{sj}\). Compute the maximum aggregate mode utility, or decide whether it is at least a given threshold \(U\).

Packaged proof task (what the prover saw — nothing else)

Let \(S\) be a nonempty set of \(m\) satellites and \(g_0<\cdots<g_h\) an explicitly listed rational time grid, with \(h\ge1\). Windows and slots have grid endpoints and are half-open; durations are endpoint differences.
A society is given by its support: the list of \(\tau\) request types with positive binary-rational masses \(\mu_t\), with \(\sum_t\mu_t=1\). Here \(\tau\) counts supported types, not possible templates. Each template contains one request, described below; all numeric input is binary rational, and \(L\) is the total input bit length.
Each request has an explicitly listed set \(V_t\) of positive-length reservation windows, each on a specified satellite, a minimum slot duration \(d_t>0\), and a nonempty explicitly listed ordered mode list. A slot is a contiguous interval contained in its reservation window, of duration at least \(d_t\). Slots of one client on the same satellite must be disjoint.
A global request has modes with nonnegative, strictly increasing required durations \(D_{t,k}\). An allocation selects one mode and at most one slot per reservation window, with total slot duration at least \(D_{t,k}\); its mode utility is \(D_{t,k}\).
A time-tagged request has an explicitly listed reference set \(T_t\) and pairwise disjoint window subsets \(V_{t,a}\subseteq V_t\) for \(a\in T_t\). Its modes specify strictly nested subsets \(T_{t,k}\subseteq T_t\). An allocation selects one mode and exactly one slot in a window of \(V_{t,a}\) for each \(a\in T_{t,k}\), with no other slots; its mode utility is \(|T_{t,k}|d_t\).
Zero-duration global modes and empty-reference time-tagged modes are allowed but not required. Let \(Q_t\) be the finite set of all valid allocations for type \(t\), determined implicitly by its template and the grid, and let \(\Omega_{tq}\) be allocation \(q\)'s mode utility.
For cell \((s,j)\), corresponding to \([g_{j-1},g_j)\), let \(a_{tq,sj}\in\{0,1\}\) indicate whether allocation \(q\) occupies that cell. Given nonnegative capacities \(\kappa_{sj}\) per unit population mass and threshold \(U\in\mathbb Q\), ask whether there exist real masses \(x_{tq}\ge0\) satisfying \(\sum_{q\in Q_t}x_{tq}=\mu_t\), \(\sum_t\sum_{q\in Q_t}a_{tq,sj}x_{tq}\le\kappa_{sj}\), and \(\sum_t\sum_{q\in Q_t}\Omega_{tq}x_{tq}\ge U\). An infeasible instance has answer no.
Is this continuous OSAP decision problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,h,L\) and the total numbers of listed windows, modes, references, and reference-window memberships.
Discrete OSAP with mode utility maximization is NP-hard ([Maqrot et al., 2022](https://doi.org/10.3233/FAIA220061)). No complexity result for this exact mass-and-grid formulation was located in the literature search.

Modeling choices made when packaging the task

Prover output (gpt-6.1-sol / high, Bolzano prover prompt)

Result

The continuous OSAP decision problem is \(\mathrm{NP}\)-complete. Hardness holds even with one satellite, one supported type, two time-tagged modes, unit capacities, and reservation windows whose durations all equal the minimum slot duration.

The reduction includes an empty-reference mode, so the supported type always has a valid allocation. Thus hardness persists when individual feasibility is guaranteed.

Write \(W,K,R,B\) for the total numbers of listed windows, modes, references, and reference-window memberships, respectively.

1. An interval construction for a Boolean variable

All intervals below are half-open. Set the minimum slot duration to \(d=2\), and give every reservation window duration \(2\). Consequently, any slot in such a window must occupy the entire window.

Consider a Boolean variable with \(n\ge1\) literal occurrences. Introduce occurrence references \(a_1,\ldots,a_n\). Reference \(a_i\) has the two windows

\(L_i=[4i,4i+2),\qquad R_i=[4i+3,4i+5).\)

Introduce one additional guard reference with windows

\(E^-=[3,5),\qquad E^+=[4n+4,4n+6).\)

An allocation serving these references must select one window for every reference, with all selected intervals disjoint.

Lemma 1: Exactly two states are possible

The only feasible selections are:

Proof. If the guard selects \(E^-\), then it intersects \(L_1\), forcing selection of \(R_1\). For every \(i<n\),

\(R_i\cap L_{i+1}=[4i+4,4i+5).\)

Thus selection of \(R_i\) forces selection of \(R_{i+1}\). Induction forces every \(R_i\).

If the guard selects \(E^+\), then it intersects \(R_n\), forcing selection of \(L_n\). The same intersections, read backwards, show that selection of \(L_{i+1}\) forces selection of \(L_i\). Hence every \(L_i\) is selected.

Both resulting selections are feasible. Consecutive selected occurrence intervals have a gap of duration \(2\). In the first selection, the guard starts after the last occurrence interval; in the second, the guard ends before the first occurrence interval. ∎

Interpret the all-\(L\) state as true and the all-\(R\) state as false.

For occurrence \(i\), define two further candidate windows:

\(P_i=[4i+2,4i+4),\qquad N_i=[4i+5,4i+7).\)

These will represent positive and negative literals.

Lemma 2: Literal windows have the required availability

The window \(P_i\) is disjoint from the selected variable intervals exactly in the true state. The window \(N_i\) is disjoint from them exactly in the false state.

Proof.

In the true state, \(P_i\) lies between \(L_i\) and \(L_{i+1}\) when \(i<n\). For \(i=n\), it lies between \(L_n\) and \(E^+\). It is therefore disjoint from the selected intervals. In the false state,

\(P_i\cap R_i=[4i+3,4i+4),\)

so it is blocked.

In the false state, \(N_i\) lies between \(R_i\) and \(R_{i+1}\) when \(i<n\), and after \(R_n\) when \(i=n\). It is also disjoint from \(E^-\). In the true state, for \(i<n\),

\(N_i\cap L_{i+1}=[4i+5,4i+6).\)

For \(i=n\),

\(N_n\cap E^+=[4n+5,4n+6).\)

Thus it is blocked in the true state. ∎

For a fixed variable, the windows \(P_i\) are pairwise disjoint, as are the windows \(N_i\). This follows because consecutive starting points differ by \(4\), while each window has duration \(2\).

2. Reduction from satisfiability

Use the standard \(\mathrm{NP}\)-complete problem \(\mathrm{3SAT}\): satisfiability of a conjunction of clauses having three literal occurrences each. [Karp, *Reducibility among Combinatorial Problems*](https://link.springer.com/chapter/10.1007/978-1-4684-2001-2_9).

Let the formula have \(c\ge1\) clauses and \(v\) variables that actually occur. Let \(n_z\ge1\) count the occurrences of variable \(z\), and put

\(N=\sum_z n_z=3c.\)

Distinct occurrences, including repeated literals, receive distinct occurrence indices.

Grid and windows

Use one satellite. For each variable \(z\), construct the intervals from Section 1 in a separate time block of length \(4n_z+8\). Translate all of that variable’s intervals by the starting time of its block.

Every interval lies strictly inside its block: its earliest starting point is \(3\), and its latest possible endpoint is \(4n_z+7\). Hence intervals belonging to different variable blocks are disjoint.

Concatenate the blocks. Their total length is

\(H=\sum_z(4n_z+8)=4N+8v.\)

Use the explicitly listed integer grid

\(g_j=j,\qquad 0\le j\le H.\)

Thus \(h=H\).

One time-tagged request

Create one supported type with mass \(\mu=1\) and minimum slot duration \(d=2\).

Its reference set consists of:

The total number of references is

\(A=N+v+c.\)

Occurrence and guard references receive the windows specified in Section 1.

For each clause, its clause reference receives one window for each of its three literal occurrences. For an occurrence indexed \(i\) within variable \(z\), use the translated window \(P_i\) if the literal is positive, and the translated window \(N_i\) if it is negative.

Each listed window belongs to exactly one reference. In particular, a literal occurrence belongs to exactly one clause, so its literal window is assigned only to that clause reference. All listed windows are distinct; thus the required reference-window subsets are pairwise disjoint.

There are two ordered modes:

\(T_0=\varnothing,\qquad T_1=T.\)

Their utilities are \(0\) and \(2A\), respectively. Since \(A>0\), these subsets are strictly nested.

Set every cell capacity to \(1\), and set the threshold to

\(U=2A.\)

The empty allocation is always valid.

Lemma 3: The full mode is feasible exactly when the formula is satisfiable

Proof, forward direction. Suppose a full-mode allocation exists. Every window has duration \(d=2\), so every selected slot equals its reservation window.

Restrict the allocation to one variable’s occurrence and guard references. Lemma 1 gives either its true or its false state, defining a truth assignment.

Each clause reference selects one literal window. That window must be disjoint from the selected variable intervals. By Lemma 2, its corresponding literal is true. Consequently, every clause is satisfied.

Proof, reverse direction. Suppose a satisfying assignment exists. For each variable, select the corresponding state from Lemma 1. For each clause, choose one true literal and select its literal window.

Lemma 2 guarantees that every selected clause window is disjoint from the variable intervals. The clause windows are also mutually disjoint. Indeed, distinct clauses use distinct occurrences. For a fixed true variable, every chosen literal involving that variable is positive, and the relevant windows belong to the pairwise disjoint family \(\{P_i\}\). For a fixed false variable, they belong to the pairwise disjoint family \(\{N_i\}\). Different variable blocks are disjoint.

This serves every reference with exactly one slot and produces a valid full-mode allocation. ∎

Lemma 4: Fractional masses preserve the equivalence

Proof. Let \(\alpha\) be the total population mass assigned to full-mode allocations. The type’s mass equation gives \(0\le\alpha\le1\), and its total utility is \(2A\alpha\). Reaching the threshold \(2A\) therefore forces \(\alpha=1\).

Hence a yes-instance must contain at least one full-mode allocation. Conversely, if such an allocation exists, assign it mass \(1\). Its cell occupancy is at most \(1\) in every cell, so every capacity constraint holds, and its utility equals the threshold. ∎

Combining Lemmas 3 and 4 proves a polynomial-time many-one reduction from \(\mathrm{3SAT}\).

Reduction size

The constructed instance has

\(m=\tau=1,\qquad h=4N+8v,\qquad K=2,\)

\(R=N+v+c,\qquad W=B=3N+2v.\)

Here \(2N+2v\) windows serve the occurrence and guard references, and \(N\) windows serve clause references.

All endpoints and the threshold have binary length \(O(\log(N+v+c+2))\). Thus the output bit length is

\(O((N+v+c)\log(N+v+c+2)).\)

The construction takes polynomial time in the source bit length. Every reference has at most three windows, every reservation window has duration \(2\), and every capacity equals \(1\).

3. Membership in NP

Although the allocation sets are implicit, every yes-instance has a polynomial-size certificate.

Set

\(r=\tau+mh+1.\)

Introduce a nonnegative slack variable for every capacity inequality, and a nonnegative variable \(v\) for the utility surplus. The resulting equations are

\(\sum_q x_{tq}=\mu_t,\)

\(\sum_{t,q}a_{tq,sj}x_{tq}+u_{sj}=\kappa_{sj},\)

\(\sum_{t,q}\Omega_{tq}x_{tq}-v=U.\)

Together these form a finite rational system \(Az=b\), \(z\ge0\), with \(r\) rows.

Lemma 5: Sparse rational certificates exist

If this system is feasible over the reals, it has a rational solution with at most \(r\) positive coordinates. Each positive coordinate has numerator and denominator bit lengths

\(O(r(L+\log(R+r+2))).\)

Proof. Among all feasible nonnegative solutions, choose one with the smallest support. Such a support size exists because the number of columns is finite.

Its active columns must be linearly independent. Otherwise, let \(c\ne0\) be a dependence supported on those columns, choosing its sign so that some \(c_i>0\). Define

\(\varepsilon=\min_{c_i>0}z_i/c_i.\)

Then \(z-\varepsilon c\) is nonnegative, satisfies the same equations, and has strictly smaller support, a contradiction. There are therefore at most \(r\) active columns.

Let their number be \(k\). Their linear independence permits selection of \(k\) rows forming a nonsingular square matrix. These rows uniquely determine the active coordinates.

For the bit bound, multiply the system by the product of the denominators of all input rationals. This product has bit length at most \(L\). Every coefficient becomes integral: allocation coefficients are indicators or signs, global utilities are input rationals, and time-tagged utilities are integer multiples of an input duration. The resulting integer entries have bit length \(O(L+\log(R+1))\).

Cramer’s rule expresses each active coordinate as a ratio of determinants. If all matrix entries have absolute value at most \(M\), each relevant determinant has absolute value at most \(k!M^k\). Its bit length is therefore

\(O(k(L+\log(R+1)+\log(k+1))),\)

which gives the stated bound because \(k\le r\). ∎

A certificate lists the positively weighted allocations and their rational masses, omitting slack coordinates. Each allocation uses at most \(W\) slots and can be encoded by its type, mode, window indices, and grid endpoint indices.

A sufficient certificate-length bound is

\(O(rW\log(W+h+2)+r\log(K+1)+r^2(L+\log(R+r+2))).\)

The verifier checks window containment, minimum durations, disjointness, mode requirements, reference membership, and the mass, capacity, and utility constraints using exact rational arithmetic. These checks take

\(\operatorname{poly}(m,\tau,h,L,W,K,R,B)\)

bit operations.

Thus the problem belongs to \(\mathrm{NP}\). Together with the reduction, this proves \(\mathrm{NP}\)-completeness.

4. A deterministic running-time bound

For completeness, the following direct algorithm solves the general formulation.

The grid has

\(p=\binom{h+1}{2}=h(h+1)/2\)

possible positive-length intervals. If type \(t\) has \(W_t\) windows and \(K_t\) modes, enumerate a mode and, for every window, either no slot or one of these intervals. Reject candidates violating containment, duration, disjointness, or mode requirements.

This produces every valid allocation, with at most

\(E=\sum_t K_t(1+p)^{W_t}\le K(1+p)^W\)

candidates. Possible duplicate allocations are harmless because their columns are identical.

Construct the resulting explicit rational linear feasibility problem. It has at most \(E\) allocation variables and \(r\) constraints. Explicit rational linear feasibility is solvable in time polynomial in its binary encoding length. [Khachiyan, *Polynomial algorithms in linear programming*](https://www.mathnet.ru/eng/zvmmf5239).

Enumeration, validation, matrix construction, and linear feasibility therefore give the deterministic bit-operation bound

\(\bigl(K(1+h(h+1)/2)^W+m+\tau+mh+h+W+K+R+B+L\bigr)^{O(1)}.\)

Equivalently, this is

\(2^{O(W\log(h+1))}\operatorname{poly}(m,\tau,h,L,W,K,R,B).\)

The finite linear program provides this upper bound, but its implicit allocation columns cannot generally be handled in polynomial time unless \(\mathrm P=\mathrm{NP}\).

⟨structured verdict parsed — rendered above⟩

Adversarial review (gpt-6.1-sol / medium, Bolzano verifier prompt)

The prover’s claim is verified. The reduction establishes \(\mathrm{NP}\)-hardness for the stated restricted instances, and the sparse rational certificate argument establishes membership in \(\mathrm{NP}\). I found no mathematical errors or missing substantive steps.

The proof uses the grid-endpoint requirement correctly. With minimum duration \(d=2\) and reservation-window duration \(2\), every selected slot must equal its reservation window.

The construction satisfies the template requirements:

Thus the hardness construction respects the intended formulation and does not depend on an unintended degenerate interpretation.

The claimed forcing intersections are correct:

\[ E^-\cap L_1=[4,5),\qquad E^+\cap R_n=[4n+4,4n+5), \]

and, for \(i<n\),

\[ R_i\cap L_{i+1}=[4i+4,4i+5). \]

Selecting \(E^-\) therefore forces \(R_1\), and each selected \(R_i\) forces \(R_{i+1}\). Selecting \(E^+\) forces \(L_n\), and the same intersections force every preceding \(L_i\).

The two resulting selections are feasible. Consecutive \(L\)-windows, and consecutive \(R\)-windows, have gaps of duration \(2\). The selected guard is also separated from the occurrence windows.

The argument remains valid when \(n=1\): the guard directly forces the sole occurrence choice, and no induction step is needed. The “exactly two states” conclusion is established.

The positive-literal window \(P_i\) is available in the true state. For \(i<n\), it fits between \(L_i\) and \(L_{i+1}\); for \(i=n\), it fits between \(L_n\) and \(E^+\). Endpoint contact causes no overlap because the intervals are half-open.

In the false state, the stated blocking intersection is correct:

\[ P_i\cap R_i=[4i+3,4i+4). \]

The negative-literal window \(N_i\) is available in the false state, including the final occurrence and the guard boundary. In the true state, the blocking intersections are correctly computed:

\[ N_i\cap L_{i+1}=[4i+5,4i+6)\quad(i<n), \]

\[ N_n\cap E^+=[4n+5,4n+6). \]

These checks also cover \(n=1\).

The claimed pairwise disjointness within each family \(\{P_i\}\) and \(\{N_i\}\) is correct: consecutive starting points differ by \(4\), while every interval has length \(2\).

A variable block has length \(4n_z+8\). Its earliest interval starts at \(3\), and its latest possible endpoint is \(4n_z+7\). Consequently, all intervals lie strictly inside their blocks, and different blocks are disjoint.

The total grid length is correctly computed:

\[ H=4N+8v. \]

All listed windows are distinct. Within a block, occurrence windows, positive literal windows, and negative literal windows have different starting-point residues modulo \(4\). The two guard windows do not duplicate any listed occurrence or literal window. Different blocks cannot introduce duplicates.

Assigning distinct indices to distinct literal occurrences handles repeated literals and repeated variables within clauses. Each occurrence supplies exactly one clause window, so no window is assigned to two clause references.

The invoked source problem is the standard \(\mathrm{NP}\)-complete three-literal satisfiability problem; allowing repeated literal occurrences does not invalidate its use. The cited source is [Karp’s *Reducibility among Combinatorial Problems*](https://link.springer.com/chapter/10.1007/978-1-4684-2001-2_9). Restricting attention to formulas with at least one clause and omitting unused variables presents no hardness obstruction.

Forward direction. A full allocation serves every occurrence and guard reference. Its restriction to each variable gadget satisfies Lemma 1, producing a well-defined truth assignment. Each clause’s selected window is disjoint from all selected variable windows. Lemma 2 therefore makes its corresponding literal true. Every clause is satisfied.

Reverse direction. The proof checks both necessary forms of disjointness:

The second check is essential and is supplied correctly. For any fixed variable, chosen true literals all have the sign compatible with its assigned state, so their windows belong to one pairwise disjoint family. Different clauses use distinct occurrences, and different variables occupy disjoint blocks.

The resulting selection serves every reference exactly once and satisfies the request’s slot restrictions. Both directions are established.

Only the empty and full modes exist, with utilities \(0\) and \(2A\). If \(\alpha\) denotes total mass on full allocations, the type equation gives \(0\le\alpha\le1\), and total utility is exactly \(2A\alpha\).

Since \(A>0\), meeting \(U=2A\) forces \(\alpha=1\). The finite allocation set must therefore contain a full-mode allocation.

Conversely, assigning mass \(1\) to one full allocation satisfies every unit capacity: a valid allocation has cell indicators in \(\{0,1\}\). Its utility equals the threshold.

Thus fractional mixing cannot bypass the satisfiability condition. This establishes hardness for the continuous problem itself.

The parameter counts are correct:

\[ m=\tau=1,\qquad h=4N+8v,\qquad K=2, \]

\[ R=N+v+c,\qquad W=B=3N+2v. \]

There are \(2N\) occurrence windows, \(2v\) guard windows, and \(N\) clause windows. Each window contributes one reference-window membership.

The grid, capacities, windows, memberships, references, and full-mode reference list all have polynomial total size. Their indices and numerical values have logarithmic bit length in \(N+v+c+2\), supporting the stated output-length bound

\[ O((N+v+c)\log(N+v+c+2)). \]

The reduction is polynomial in the source encoding length.

Introducing capacity slacks and the utility surplus gives exactly the claimed finite rational equality system. The surplus sign is correct:

\[ \sum_{t,q}\Omega_{tq}x_{tq}-v=U,\qquad v\ge0. \]

The minimum-support argument is valid. A dependence among active columns permits the stated perturbation; coordinates with positive dependence coefficients decrease without becoming negative, while those with negative coefficients increase. At least one active coordinate becomes zero. This contradicts minimal support.

Hence the active columns are linearly independent and number at most

\[ r=\tau+mh+1. \]

Selecting a nonsingular row minor determines their coordinates uniquely. Since that square system is rational, the coordinates are rational.

The denominator-clearing argument covers all coefficients and right-hand sides. Global utilities are input rationals; time-tagged utilities are integer multiples of an input duration, with multiplier at most \(R\). The resulting integer-entry bound and the determinant estimate yield the claimed coordinate bit bound:

\[ O(r(L+\log(R+r+2))). \]

The positive input masses ensure that a feasible system has nonempty support, so no zero-dimensional determinant case is needed.

Every allocation uses at most \(W\) slots. Type, mode, window, and endpoint indices provide a polynomial encoding.

The displayed certificate-length bound is sufficient. Type identifiers are covered by the mode-index bound because the nonempty mode lists imply \(K\ge\tau\).

Omitting slack coordinates is legitimate: direct verification of the capacity and utility inequalities replaces their explicit inclusion. Exact rational arithmetic can verify the allocation rules and aggregate constraints in

\[ \operatorname{poly}(m,\tau,h,L,W,K,R,B) \]

bit operations.

Types with no valid allocations cannot receive their required positive mass, so infeasible individual templates are correctly rejected. The membership argument does not assume individual feasibility.

The number of positive-length grid intervals is correctly given by

\[ p=\binom{h+1}{2}. \]

Enumerating a mode and one interval-or-empty choice per window covers every valid allocation. Invalid candidates are filtered by the stated checks. Duplicate columns do not change feasibility.

The candidate bound

\[ E=\sum_tK_t(1+p)^{W_t}\le K(1+p)^W \]

is valid, including \(W=0\) and \(h=1\).

The invoked theorem is that feasibility of an explicitly encoded finite rational linear system is decidable in time polynomial in its binary encoding length. The constructed LP satisfies these hypotheses; neither boundedness nor individual request feasibility is required. This application is consistent with [Khachiyan’s polynomial linear-programming result](https://www.mathnet.ru/eng/zvmmf5239).

Enumeration, validation, matrix construction, and LP feasibility therefore support both displayed deterministic bounds, including

\[ 2^{O(W\log(h+1))} \operatorname{poly}(m,\tau,h,L,W,K,R,B). \]

The output fully resolves the assigned complexity question. No repair or additional clarification is required.

⟨structured verdict parsed — rendered above⟩

Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.