← back to the atlas

d4-conf-ecai-2025-0400 (d4-conf-ecai-2025-0400)

Answer: Exact computation of the aggregate cohort serial dictatorship outcome is polynomial-time solvable in \(m,\tau,L\).

The anchor (named result in the paper)

Proposition 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateConsider an instance with n workers and m firms, matched by SD according to the ranking r = (r1, . . . , rn+m). If the three tensors PW , PF , and R are defined as per Equations (3) and (4), then TSD outputs the matrix representation of the matching outcome determined by this SD. Assuming n ≥m, without loss of generality, this computation requires O(n4).

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

The continuous mirror question, as graded

Given worker types \(T_W\) and firm types \(T_F\), rational masses \(\mu_i\) and \(\nu_j\) on a common population scale, a strict preference order for each type over opposite-side types and \(\bot\), and a fixed order over \(T_W \cup T_F\), compute the aggregate matching produced by cohort serial dictatorship. At each type's turn, its remaining mass takes the highest-ranked available opposite-side mass in preference order, pairing up to the smaller residual mass; any remainder assigned to \(\bot\) leaves the process. Output the flows \(x_{ij}\) and unmatched masses, with running time polynomial in \(|T_W|+|T_F|\) and the input bit length.

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

Let \(T_W\) and \(T_F\) be disjoint, nonempty sets of worker and firm types, with \(n=|T_W|\), \(m=|T_F|\), and \(\tau=n+m\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each mass a binary rational; \(\tau\) is the support size, not the number of possible types. Worker masses \(\mu_i\) and firm masses \(\nu_j\) use a common population scale; neither normalization nor equality of the two total masses is required.
Each type has a strict total order over all opposite-side types and \(\bot\), the unmatched option. The input also specifies a total order over \(T_W\cup T_F\); let \(L\) be the total input bit length.
Cohort serial dictatorship starts with all mass available and processes each type once in the specified order. At its turn, a type repeatedly selects its highest-ranked available opposite-side type above \(\bot\), matching the smaller of their residual masses and removing that mass from both sides.
The selected partner's preferences impose no acceptance condition. If no available partner ranks above \(\bot\), all remaining mass of the acting type becomes permanently unmatched and unavailable; a type with no residual mass is skipped.
The output consists of exact rational flows \(x_{ij}\) and unmatched masses \(u_i,v_j\), satisfying \(\sum_j x_{ij}+u_i=\mu_i\) and \(\sum_i x_{ij}+v_j=\nu_j\).

Is exact computation of this aggregate cohort serial dictatorship outcome possible in time polynomial in \(m,\tau,L\), or is it NP-hard?

For finite one-to-one two-sided matching with a fixed agent order, tensor serial dictatorship exactly computes serial dictatorship in \(O(\max\{n,m\}^{4})\) arithmetic operations.
That discrete result does not establish the complexity of exact computation for rational-mass cohorts.

Modeling choices made when packaging the task

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

Result

Exact computation is polynomial-time solvable. The cohort procedure can be simulated directly using integers of polynomial bit length. No normalization, equality of total masses, or acceptance condition on the selected partner is needed.

1. Represent all masses on a common integer scale

Write the positive input masses as \(p_t/d_t\), where \(t\) ranges over the \(\tau\) supported types and \(p_t,d_t\) are positive integers encoded in binary. Define
\(D=\prod_t d_t\)
and
\(a_t=p_t(D/d_t)\).
Thus the mass of type \(t\) is exactly \(a_t/D\).

The bit length of \(D\) is at most one plus the sum of the input denominators’ bit lengths, hence is \(O(L)\). Each \(a_t\) also has bit length \(O(L)\), because
\(a_t\leq p_tD\)
and both factors have bit length \(O(L)\).

We will maintain integer residuals \(r_t\), initially \(r_t=a_t\). A positive residual means that the type remains available. A zero residual means that it is unavailable, whether its mass was matched or declared permanently unmatched.

Initialize integer flow entries \(X_{ij}=0\) and integer unmatched quantities \(U_i=V_j=0\).

2. Integer simulation

Process the supported types in the specified order. For an acting type \(t\):

Finally, output
\(x_{ij}=X_{ij}/D\),
\(u_i=U_i/D\), and
\(v_j=V_j/D\).

These fractions are exact; reducing them to lowest terms is unnecessary.

3. Correctness

We first justify why a single forward scan implements the repeated selection rule.

Residuals never increase. Consequently, a type skipped because its residual is zero can never become available later. Moreover, if the acting type still has positive residual after matching with \(s\), then \(s\) must have become exhausted: from
\(q=\min\{r_t,r_s\}\)
and \(r_t-q>0\), it follows that \(q=r_s\), so \(r_s-q=0\).

Therefore, whenever the acting type continues scanning, every previously examined opposite-side type is unavailable. The next positive-residual type encountered before \(\bot\) is exactly its highest-ranked available acceptable partner. If the scan reaches \(\bot\), no acceptable partner is available.

Now compare the integer simulation with the stated cohort procedure. Initially, the cohort residual mass of every type is \(r_t/D\). Suppose this correspondence holds immediately before a matching step. The cohort procedure transfers
\(\min\{r_t/D,r_s/D\}=\min\{r_t,r_s\}/D=q/D\).
The integer updates therefore preserve the correspondence for both residual masses and accumulated flows. Declaring residual mass permanently unmatched likewise transfers exactly \(r_t/D\) into the corresponding unmatched quantity and makes the type unavailable.

By induction over the ordered turns and their matching steps, the simulation produces precisely the specified outcome. The selected partner’s preferences are never consulted, as required.

For completeness, mass conservation follows from the invariants
\(a_i=r_i+\sum_jX_{ij}+U_i\)
for workers and
\(a_j=r_j+\sum_iX_{ij}+V_j\)
for firms. Every matching step and every unmatched declaration preserves these equalities. Each type finishes its own turn with zero residual, and residuals subsequently remain zero. Hence all residuals are zero at termination. Dividing the invariants by \(D\) gives the required output equalities.

4. Number of steps

Each worker scans at most \(m+1\) preference entries, including \(\bot\), and each firm scans at most \(n+1\). Thus the total number of examined entries is at most
\(n(m+1)+m(n+1)=2nm+\tau\).

There is also a stronger bound on positive matching steps. Every such step exhausts at least one currently available type, and no exhausted type becomes available again. If there are \(K>0\) matching steps, then immediately before the last one there are at most \(\tau-(K-1)\) available types. A matching step requires at least two available types, so
\(2\leq\tau-(K-1)\),
which implies
\(K\leq\tau-1\).
Unmatched declarations can only decrease availability further.

5. Bit complexity

All maintained residuals and unmatched quantities are bounded by their respective initial scaled masses. Every flow entry is also bounded by its worker’s initial scaled mass. Thus every maintained integer has \(O(L)\) bits.

Using ordinary binary arithmetic:

Including input reading, a valid overall bound is
\(O\bigl(L+\tau L^2+(nm+\tau)L\bigr)\).
Since \(n\leq\tau\), this is polynomial in \(m,\tau,L\).

The finite one-to-one tensor result is therefore unnecessary: the rational cohort problem admits its own direct polynomial-time algorithm, with an explicit bound on exact arithmetic sizes.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the assigned task. The direct simulation is correct, and its running-time bound accounts for exact rational arithmetic. No major or minor issues were found.

1. Common integer scale

The construction
\[ D=\prod_t d_t,\qquad a_t=p_t(D/d_t) \]
is valid: every denominator is positive and divides \(D\), so every \(a_t\) is an integer representing the original mass exactly.

The bit-length bounds are correct. The sum of the denominators’ encoded lengths is bounded by \(L\), so \(D\) has \(O(L)\) bits. Each numerator also has \(O(L)\) bits, and the stated inequality \(a_t\leq p_tD\) therefore gives \(O(L)\) bits for each scaled mass.

This construction requires neither normalized masses nor equal total masses.

2. Simulation of a turn

The forward scan correctly implements repeated selection of the highest-ranked available acceptable partner.

The simulation stops when the acting type is exhausted and never matches with a partner below \(\bot\). It imposes no acceptance condition based on the selected partner’s preferences.

3. Exact correspondence and conservation

The correspondence between integer residuals and cohort masses is preserved because division by the common positive denominator commutes with taking the minimum:
\[ \min\{r_t/D,r_s/D\}=\min\{r_t,r_s\}/D. \]

Matching updates and unmatched declarations therefore reproduce the prescribed mass transfers exactly. The induction over turns and matching steps is sufficient.

Both conservation invariants are correct. A matching step decreases each endpoint’s residual by precisely the amount added to its incident flow. An unmatched declaration transfers the remaining residual into the appropriate unmatched quantity.

Every type has zero residual after its own turn, including types skipped because they were already exhausted. Residuals never increase, so all residuals are zero at termination. The required output equalities follow by dividing the invariants by \(D\).

4. Operation counts

The preference-scan bound is correct:
\[ n(m+1)+m(n+1)=2nm+\tau. \]
Each preference list is scanned at most once, and only its prefix through \(\bot\) can be examined.

The stronger matching-step bound is also correct. Every positive matching step exhausts at least one previously available type. Before matching step \(K\), at most \(\tau-(K-1)\) types remain available; that step requires two available endpoints. Thus \(K\leq\tau-1\). Unmatched declarations only strengthen this bound. The case of zero matching steps is explicitly excluded from this argument and presents no problem.

5. Bit complexity and output size

The maintained-integer bounds hold:

The stated construction bound \(O(\tau L^2)\) is valid using schoolbook multiplication and long division on operands of \(O(L)\) bits. Each quotient \(D/d_t\) is exact.

The scan and update bound \(O((nm+\tau)L)\) is sufficient for comparisons, additions, subtractions, and preference processing. Writing all flow and unmatched fractions has the claimed \(O((nm+\tau)L)\) size bound. Unreduced fractions are permissible exact rational outputs.

Consequently, the overall bound
\[ O\bigl(L+\tau L^2+(nm+\tau)L\bigr) \]
is valid and polynomial in the requested parameters because \(n\leq\tau\).

6. Scope and verdict

The argument handles unequal total masses, arbitrary placement of \(\bot\), complete exhaustion before a type’s turn, and permanent removal of unmatched residual mass. It operates on the supported types and does not assume enumeration of additional possible types.

The discrete tensor result is not used, and no external theorem requires verification. The continuous rational-mass problem is established to admit exact polynomial-time computation. No additional clarification or repair is needed.

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