Answer: The decision problem is in \(\mathrm P\).
Lemma 1 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateConsider an WTPN S and the following inte- ger program: max xT cT (13) subject to AT x + M0 ∼h (14) All the integer solutions xmax to this IP represent the fir- ing count vectors of all the optimal solutions Jmax to the CMWOSP defined by ⟨∼, h⟩iffAT x + M0 represents all the reachable states R(S, M0).
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite good set \(G\), supplier types \(T\) with rational masses \(\mu_t\) summing to \(1\), each type’s finite XOR menu \(\mathcal B_t\) of priced packages \(D_b=\{(I_{bk},O_{bk})\}_k\), rational per-capita initial and required inventories \(u_{\mathrm{in}},u_{\mathrm{out}}\), and an acyclic network of all offered transformations, choose masses \(x_{tb}\ge 0\) to maximize \(\sum_{t,b}p_bx_{tb}\). Require \(\sum_{b\in\mathcal B_t}x_{tb}\le\mu_t\) for each type and \(u_{\mathrm{in}}(g)+\sum_{t,b}x_{tb}\sum_k(O_{bk}(g)-I_{bk}(g))\ge u_{\mathrm{out}}(g)\) for each good \(g\); every accepted package’s transformations must admit a finite execution schedule on their assigned mass.
Let \(G\) be a finite good set, with \(m=|G|\). A society is given by its support: the list of \(\tau\) supplier types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) counts listed types, not possible types.
Each type has an explicitly listed finite XOR menu \(\mathcal B_t\). Each package \(b\) has a signed binary-rational price \(p_{tb}\) and a nonempty finite multiset \(D_{tb}=\{(I_{tbk},O_{tbk})\}_k\), where \(I_{tbk},O_{tbk}\in\mathbb N^G\) have binary-encoded entries; positive prices are payments to the auctioneer. Initial and required per-capita inventories \(u_{\mathrm{in}},u_{\mathrm{out}}\in\mathbb Q_{\ge0}^G\) are binary encoded.
The directed bipartite graph containing good nodes and one node for each offered transformation occurrence, with arcs from positive input goods to transformations and from transformations to positive output goods, is acyclic.
Choose divisible masses \(x_{tb}\in\mathbb R_{\ge0}\) satisfying \(\sum_{b\in\mathcal B_t}x_{tb}\le\mu_t\). Different portions of a type may accept different packages, and the remaining mass may accept none.
A finite execution schedule starts at inventory \(M=u_{\mathrm{in}}\). A step applies an occurrence \((t,b,k)\) to mass \(\delta>0\), requires \(M\ge\delta I_{tbk}\), and replaces \(M\) by \(M+\delta(O_{tbk}-I_{tbk})\). For every occurrence, its step masses must sum to \(x_{tb}\); splitting and interleaving are allowed, every purchased transformation must be executed, and goods are pooled across types.
Require final inventory at least \(u_{\mathrm{out}}\), equivalently \(u_{\mathrm{in}}(g)+\sum_{t,b}x_{tb}\sum_k(O_{tbk}(g)-I_{tbk}(g))\ge u_{\mathrm{out}}(g)\) for every \(g\in G\). Surplus goods are permitted. Revenue is \(\sum_{t,b}p_{tb}x_{tb}\).
Given a binary-rational threshold \(R\), is deciding whether a feasible allocation with a finite execution schedule has revenue at least \(R\) in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard? State running times in \(m,\tau,B,K,L\), where \(B\) is the total menu size, \(K\) the total number of listed transformation occurrences, and \(L\) the total input bit length.
For discrete weighted Petri nets, maximum-weight feasible firing sequences have an exact integer-programming formulation when every admissible nonnegative integer firing vector is executable; acyclic nets satisfy this condition ([Giovannucci et al., 2007](https://doi.org/10.1145/1329125.1329253)).
Discrete XOR mixed-auction winner determination is \(\mathrm{NP}\)-complete ([Ottens and Endriss, 2008](https://eprints.illc.uva.nl/id/eprint/287/1/PP-2008-13.text.pdf)). Continuous Petri-net reachability is polynomial-time decidable ([Blondin et al., 2017](https://discovery.ucl.ac.uk/id/eprint/10088921/)); this concerns reachability rather than the package-constrained revenue problem above.
The decision problem is in \(\mathrm P\). Under the stated acyclicity assumption, the inventory balance inequalities are sufficient for a finite execution schedule. The allocation and revenue requirements therefore form an exact rational linear program.
Let \(T\) be the set of all listed transformation occurrences. For an occurrence \(v=(t,b,k)\), write \(I_v=I_{tbk}\), \(O_v=O_{tbk}\), and prescribe its total execution mass as \(y_v=x_{tb}\).
Lemma. Suppose \(y_v\ge 0\) for every occurrence and
\[
\text{}
\]
\(F:=u_{\mathrm{in}}+\sum_{v\in T}y_v(O_v-I_v)\ge 0\).
Then these masses have a valid execution schedule containing at most \(K\) steps.
Proof. Take a topological ordering of the given directed bipartite graph, and list its occurrence nodes in their induced order as \(v_1,\ldots,v_K\). We will execute each occurrence of positive prescribed mass once, with that entire mass.
Proceed by induction through this list. Immediately before occurrence \(v_j\), the inventory is
\(M_j=u_{\mathrm{in}}+\sum_{i<j}y_{v_i}(O_{v_i}-I_{v_i})\).
The induction hypothesis says that preceding executions were valid, so \(M_j\ge 0\).
Fix a good \(g\) with \(I_{v_j}(g)>0\). Every occurrence \(v_i\) producing \(g\) has a directed path
\(v_i\longrightarrow g\longrightarrow v_j\).
Consequently, every such producer precedes \(v_j\). In particular, no occurrence with index \(i\ge j\) produces \(g\). This also excludes production of \(g\) by \(v_j\) itself, which would create a directed cycle.
All production of \(g\) is therefore already included in \(M_j(g)\), giving
\(M_j(g)=u_{\mathrm{in}}(g)+\sum_{i=1}^{K}y_{v_i}O_{v_i}(g)-\sum_{i<j}y_{v_i}I_{v_i}(g)\)
\(=F(g)+\sum_{i\ge j}y_{v_i}I_{v_i}(g)\ge y_{v_j}I_{v_j}(g)\).
For a good with \(I_{v_j}(g)=0\), the required inequality follows from \(M_j(g)\ge 0\). Thus, whenever \(y_{v_j}>0\), the whole prescribed mass is enabled. Its execution leaves a nonnegative inventory because
\(M_j-y_{v_j}I_{v_j}+y_{v_j}O_{v_j}\ge 0\).
When \(y_{v_j}=0\), omit the step. This completes the induction. Every occurrence receives exactly its prescribed mass, and the final inventory is \(F\). There are at most \(K\) positive-mass steps. \(\square\)
Conversely, summing the inventory changes in any valid schedule gives exactly \(F\). Hence, because \(u_{\mathrm{out}}\ge 0\), prescribed masses admit a schedule with final inventory at least \(u_{\mathrm{out}}\) if and only if
\(u_{\mathrm{in}}+\sum_{v\in T}y_v(O_v-I_v)\ge u_{\mathrm{out}}\).
The lemma applies directly to real masses; no discretization or limiting argument is required.
For each package and good, define the integer coefficient
\(a_{g,tb}:=\sum_k\bigl(O_{tbk}(g)-I_{tbk}(g)\bigr)\).
Consider the following rational linear feasibility problem, with one variable \(x_{tb}\) per listed package:
This system has \(B\) variables and \(B+\tau+m+1\) inequalities, counting nonnegativity.
Exactness. Any allocation satisfying the original requirements satisfies these inequalities: the capacity and revenue inequalities are unchanged, and summing schedule updates gives the inventory inequalities.
Conversely, from any feasible point of this system, prescribe \(y_{tbk}=x_{tb}\) for every occurrence. The inventory inequalities and the lemma produce a valid finite schedule. Every occurrence of each purchased package executes exactly its required mass. The allocation also satisfies the type capacities and revenue threshold.
Thus the linear system is feasible exactly when the answer to the original decision problem is yes. Signed prices cause no difficulty: they are simply rational coefficients in the revenue inequality.
Set \(H=L+\lceil\log_2(K+2)\rceil\).
Each coefficient \(a_{g,tb}\) is a sum of at most \(K\) differences of binary-encoded integers, so its bit length is \(O(H)\). The rational right-hand sides, masses, prices, and threshold also have bit length \(O(H)\), including after the inventory subtraction.
A conservative dense encoding of the resulting linear system has length
\(N=O\bigl((B+m+\tau+1)(B+1)H\bigr)\).
The graph has \(m+K\) vertices and at most \(2mK\) arcs. Constructing and topologically sorting it takes \(O(m+K+mK)\) graph operations. Aggregating package coefficients takes \(O(mK)\) integer additions or subtractions on \(O(H)\)-bit integers. Including rational subtraction and encoding, a conservative preprocessing bound is
\(O\bigl((m+K+mK+\tau+B+1)H^2\bigr)\)
bit operations.
The standard rational linear-programming theorem decides feasibility exactly in time polynomial in the encoded system length, and can return a rational feasible point when one exists. Its hypotheses hold here: the system is finite, explicitly encoded, rational, and contains only non-strict linear inequalities. This includes feasibility on the exact revenue boundary. See [Khachiyan, *Polynomial algorithms in linear programming*](https://www.mathnet.ru/eng/zvmmf5239).
Consequently, the total decision time is bounded by
\(O\bigl((m+K+mK+\tau+B+1)H^2\bigr)+N^{O(1)}\),
and hence by
\((m+\tau+B+K+L+1)^{O(1)}\)
bit operations. A feasible allocation and a schedule of at most \(K\) steps can also be produced in polynomial time.
The discrete XOR model permits at most one whole package per bidder; this is the model whose winner determination is NP-complete in [Ottens and Endriss](https://eprints.illc.uva.nl/id/eprint/287/1/PP-2008-13.text.pdf).
Here, different portions of a type may accept different packages. Its allocation restriction is therefore the linear capacity inequality \(\sum_bx_{tb}\le\mu_t\). Package coupling is retained by using the same variable \(x_{tb}\) for every occurrence in that package. Acyclicity then supplies the schedule proved above. These two facts give the exact polynomial-time formulation.
⟨structured verdict parsed — rendered above⟩
Verdict: proved. The output resolves the assigned decision problem. The scheduling lemma is correct, the linear program is exact, and the stated bounds establish polynomial bit complexity in the requested parameters. No major or minor mathematical issues were found.
Occurrence indexing. Treating each listed occurrence as a separate node is correct, including repeated transformations within a multiset. Prescribing \(y_{tbk}=x_{tb}\) retains the requirement that every occurrence in a purchased package execute the same total mass.
Topological order. The acyclicity hypothesis guarantees the ordering used in the proof. If \(I_{v_j}(g)>0\), every producer of \(g\) precedes \(v_j\), because the graph contains the path \(v_i\to g\to v_j\). Production of \(g\) by \(v_j\) itself would create a directed cycle. Thus the assertion that no occurrence indexed \(i\ge j\) produces \(g\) is justified.
Inventory identity. The expression for \(M_j\) correctly records all earlier executions, including zero-mass occurrences, whose contributions vanish. For a consumed good, replacing earlier production by total production is valid by the preceding ordering argument. The resulting identity
\(M_j(g)=F(g)+\sum_{i\ge j}y_{v_i}I_{v_i}(g)\)
is algebraically correct.
Enabling inequality. Every summand on the right is nonnegative, and the sum includes the current occurrence’s input requirement. Consequently \(M_j(g)\ge y_{v_j}I_{v_j}(g)\). For goods not consumed by the current occurrence, the induction hypothesis supplies the required inequality.
Induction and termination. The base inventory is nonnegative by the task assumptions. Each enabled execution leaves a nonnegative inventory because both the remaining inventory after consumption and the output vector are nonnegative. Omitting zero-mass occurrences respects the requirement that actual steps have positive mass. Each positive-mass occurrence executes once, so the schedule has at most \(K\) steps and final inventory exactly \(F\).
The argument applies to arbitrary prescribed nonnegative real masses. It requires neither rationality nor a limiting construction.
The necessary direction is correct: summing all schedule updates yields the stated final inventory, since every occurrence’s executed masses sum to its prescribed mass.
The sufficient direction correctly uses \(F\ge u_{\mathrm{out}}\ge0\), which supplies the lemma’s hypothesis \(F\ge0\). The schedule produced by the lemma therefore satisfies the required final inventory.
No additional ordering restriction between occurrences of a package appears in the task. The proof consequently respects all stated execution requirements.
The coefficient \(a_{g,tb}\) correctly aggregates the net inventory change from all occurrences of one package.
Every constraint has the required interpretation:
There are exactly \(B\) variables and \(B+\tau+m+1\) inequalities under the stated counting convention.
Both directions of the claimed exactness follow from the scheduling equivalence already proved. Sharing one variable across a package’s occurrences preserves package coupling. Signed prices introduce no nonlinear or discrete condition.
Coefficient lengths. Each aggregated integer coefficient sums at most \(K\) differences of input integers. The asserted \(O(L+\log(K+2))=O(H)\) bit bound is valid. Subtracting the two rational inventory entries also yields an \(O(H)\)-bit rational coefficient.
System encoding. The dense bound
\(N=O((B+m+\tau+1)(B+1)H)\)
correctly accounts for all coefficient and right-hand-side positions. It is a conservative upper bound.
Graph and aggregation. The graph has \(m+K\) vertices and at most \(2mK\) arcs. Its construction and topological sorting have the stated graph-operation bound. Aggregation requires \(O(mK)\) additions or subtractions on \(O(H)\)-bit integers.
Preprocessing. The stated \(H^2\) allowance covers elementary exact rational subtraction and encoding. Dense initialization also fits this conservative bound: explicit listing gives \(B=O(L)\), so the dense encoding cost is absorbed by the displayed preprocessing expression.
LP theorem. The invoked theorem is stated with the relevant content: exact feasibility of explicitly encoded rational linear inequalities is decidable in polynomial bit time, and a rational feasible point can be returned. Its hypotheses hold here. There is no requirement that the feasible region have interior or that the revenue inequality hold strictly. The general polynomial-time feasibility result is corroborated by [MIT’s ellipsoid-method lecture notes](https://ocw.mit.edu/courses/15-083j-integer-programming-and-combinatorial-optimization-fall-2009/60dd52896e183e2c60bfe40e076d83d3_MIT15_083JF09_lec10.pdf).
The resulting total bound is polynomial in \(m,\tau,B,K,L\), as requested. A polynomial-size rational feasible allocation and its at-most-\(K\)-step schedule can likewise be produced.
Zero prescribed masses, zero input or output vectors, repeated occurrences, and empty menus cause no failure in the argument. If there are no packages, the displayed system reduces to constant feasibility checks and the execution schedule is empty. An empty good set also causes no difficulty.
The discussion of discrete XOR hardness is accurate. The cited paper defines mutually exclusive whole-package offers and states NP-completeness of the discrete winner-determination problem. The output correctly identifies divisibility as producing linear type capacities here. It does not use discrete hardness to infer continuous hardness. See [Ottens and Endriss, Sections 2–3](https://eprints.illc.uva.nl/id/eprint/287/1/PP-2008-13.text.pdf).
No mathematical repair or additional clarification is required. The empty display containing only a formatting command in the lemma statement is cosmetic and does not obscure any hypothesis.
⟨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.