← back to the atlas

d4-conf-ijcai-2015-0508 (d4-conf-ijcai-2015-0508)

Answer: \(\mathrm{P}\): every valid instance admits a rational stable assignment.

The anchor (named result in the paper)

Theorem 1 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateIf µ and π are corresponding, then µ is stable if and only if π is satisfying.

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

The continuous mirror question, as graded

Given a finite set of programs \(P\), supported single-doctor types \(S\), couple types \(K\), rational type masses \(\alpha_s,\beta_k\), and rational per-capita quotas \(q_p\), decide whether there are rational assignment flows \(x_{s,p}\) and \(y_{k,(p_1,p_2)}\) that exhaust each type’s mass, respect quotas and individual acceptability, and admit no blocking deviation. Each type specifies its complete relevant preferences; programs rank doctor types, with members of a type sharing a priority. A blocking deviation is a positive mass of a type moving to a preferred option that the destination programs can accept under responsive choice, with both members accepted together when a couple chooses the same program. If such flows exist, produce one. Measure complexity in the number of programs \(m\), supported types \(\tau=|S|+|K|\), input bit length \(L\), and preference-list lengths.

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

Let \(P\) be a nonempty set of \(m\) programs, \(S\) single-doctor types, and \(K\) ordered couple types. A society is given by its support: the list of the \(\tau=|S|+|K|\) types with positive mass, each mass a binary rational; \(\tau\) counts supported types, not possible types. Normalize doctor mass by \(\sum_s\alpha_s+2\sum_k\beta_k=1\). Each program has a positive binary-rational per-capita quota \(q_p\).
Write \(P^+=P\cup\{\bot\}\), where \(\bot\) denotes unemployment. Singles strictly rank their listed acceptable options in \(P^+\); couples strictly rank listed ordered pairs in \((P^+)^2\). The options \(\bot\) and \((\bot,\bot)\), respectively, are always listed last; pairs with exactly one unemployed member may also be listed. Unlisted options are unacceptable.
Programs strictly rank acceptable doctor categories \(s\) and \((k,i)\), where \(i\in\{1,2\}\) identifies a couple member; all doctors within a category have equal priority. Assignment to a real program requires its acceptance of that category.
An assignment consists of nonnegative rational flows on acceptable options satisfying \(\sum_a x_{s,a}=\alpha_s\), \(\sum_{(a,b)}y_{k,(a,b)}=\beta_k\), and \(\sum_s x_{s,p}+\sum_k\sum_{(a,b)}(\mathbf1_{a=p}+\mathbf1_{b=p})y_{k,(a,b)}\le q_p\). Couple flow measures couples, so assigning both members to one program consumes twice that flow.
A blocking deviation selects a positive rational mass \(\delta\) from one type's flow at one current option and sends it to a strictly preferred listed option. Each destination applies responsive choice to its original incumbent doctor mass together with the arriving members, retaining acceptable mass up to quota in priority order. Equal-priority arrivals cannot displace incumbents; acceptance means some such selection retains every deviating member required at that destination. Members already there are counted once. Departures do not first free capacity in these acceptance tests; \(\bot\) accepts without limit.
For couples, both members must be accepted at their respective destinations, including when one stays in place; at a common destination both masses must be retained together. A stable assignment has no blocking deviation. Decide whether one exists and, if so, produce rational flows. State running times in \(m\), \(\tau\), total input bit length \(L\), and total preference-list length \(\ell\).

Is deciding whether a rational stable assignment exists in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?

Discrete: [Drummond, Perrault, and Bacchus](https://www.ijcai.org/Proceedings/15/Papers/079.pdf) establish a bijection between stable matchings and satisfying assignments of a SAT encoding.
Fractional: [Biró and Fleiner](https://real.mtak.hu/26264/7/BF16do_last.pdf) prove existence of stable allocations with contributions under their domination-based stability definition and discuss applications to couples.
Related complexity: [Ishizuka and Kamiyama](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2018.11) prove \(\mathrm{PPAD}\)-completeness of finding stable fractional hypergraph matchings even at maximum degree three; this concerns a different search problem.

Modeling choices made when packaging the task

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

1. Result

The existence decision problem is in \(\mathrm{P}\): every valid instance admits a rational stable assignment.

Rational flows can be constructed in time
\((2\tau+1)^m\operatorname{poly}(m,\tau,\ell,L)\).
Thus construction is polynomial-time for every fixed \(m\). This proof does not establish polynomial-time construction when both \(m\) and \(\tau\) vary.

The essential step is a refinement of the auxiliary program preferences used in the contribution-allocation theorem. It handles deviations in which a couple member stays at a program.

2. The existence theorem used

We use the following contribution-allocation theorem.

Let \(V\) be a finite vertex set and \(E\) a finite indexed collection of activities. Activity \(e\) has capacity \(c_e>0\) and positive contribution \(a_{ve}\) at each incident vertex \(v\). Vertex \(v\) has capacity \(b_v>0\) and strictly orders its incident activities. Then there exists an allocation \(z\) satisfying

\( 0\le z_e\le c_e, \qquad \sum_{e:\,v\in e}a_{ve}z_e\le b_v, \)

such that every activity \(e\) with \(z_e<c_e\) is dominated at some incident vertex \(v\), meaning

\( \sum_{f:\,v\in f,\ f\succeq_v e}a_{vf}z_f=b_v. \)

This is [Biró–Fleiner, Theorem 13](https://real.mtak.hu/26264/7/BF16do_last.pdf), with the domination definition in Section 3.3. Indexed activities may share incidence sets: the Scarf-matrix construction uses a separate column and capacity constraint for each activity and requires no distinct-incidence assumption.

We use only existence from this theorem. Rationality and an explicit running time will be proved separately.

3. Constructing the auxiliary instance

Write \(T\) for the supported single and couple types. Let \(\gamma_t\) denote their respective masses \(\alpha_s\) or \(\beta_k\).

First remove every listed option assigning a member to a program that does not accept that member’s category. Such an option cannot receive flow or be an accepted blocking destination. Unemployment remains available.

For each remaining option \(u\) of type \(t\), create an activity \(e=(t,u)\). Its incident vertices are \(t\) and the real programs used by \(u\). Set

\( b_t=\gamma_t,\qquad b_p=q_p,\qquad c_e=\gamma_t. \)

The contribution at the type vertex is \(a_{te}=1\). At a program vertex, \(a_{pe}\) is the number of members assigned there: either \(1\) or \(2\). Thus a common destination consumes twice the couple flow, exactly as required.

The unemployment activity is incident only with its type vertex. A partially unemployed couple activity has the type vertex and its one real destination.

At each type vertex, order activities by the given option preferences.

Auxiliary program preferences

For an activity \(e=(t,u)\) incident with program \(p\), define \(w_p(e)\) to be the worst-priority doctor category that \(u\) assigns to \(p\).

Order incident activities at \(p\) as follows:

The second rule is well-defined: a doctor category identifies its type. Consequently, two activities with the same worst category belong to the same type, whose option preferences are strict. These rules therefore give a strict order on all incident activities.

These auxiliary orders are a proof device. Stability will be checked using the original program priorities.

All vertex and activity capacities are positive, all incident contributions are positive, and the activity collection is finite. The theorem therefore applies.

4. Transferring domination to the stated blocking rule

Let \(z\) be an allocation supplied by the theorem.

Every type’s entire mass is assigned

Let \(e_t^\bot\) denote type \(t\)’s unemployment activity.

If \(z_{e_t^\bot}=\gamma_t\), the type capacity constraint implies that its total assigned mass is \(\gamma_t\).

Otherwise, \(e_t^\bot\) is unsaturated. Its only incident vertex is \(t\), so it must be dominated there. Since unemployment is last, every activity of \(t\) is weakly preferred to it. Domination gives

\( \sum_{e:\,t\in e}z_e=\gamma_t. \)

Thus all type equalities hold. Program capacity constraints also hold by construction, so \(z\) is a feasible assignment.

A preferred target cannot be dominated at its type

Suppose \(z_{(t,u)}>0\), and let \(v\) be a strictly preferred option of the same type.

Since total type flow is \(\gamma_t\),

\( z_{(t,v)} \le \gamma_t-z_{(t,u)} <\gamma_t=c_{(t,v)}. \)

Hence the target activity \((t,v)\) is unsaturated and must be dominated at some incident vertex.

It cannot be dominated at \(t\): the positive flow at the strictly worse option \(u\) is excluded from the domination sum, so that sum is strictly below \(\gamma_t\). Therefore the target is dominated at a real destination \(p\).

Domination at \(p\), together with its capacity constraint, implies both that its load is \(q_p\) and that every positive-flow activity incident with \(p\) is weakly preferred there to \((t,v)\). Indeed, any positive contribution from a strictly worse activity would make the domination sum strictly smaller than the total load.

The worst target member at the dominating program must be arriving

Let \(g=w_p((t,v))\).

Suppose the member of category \(g\) stays at \(p\) in the deviation from \(u\) to \(v\). Then \(u\) also assigns that member to \(p\). Consequently, \(w_p((t,u))\) has priority no higher than \(g\).

There are two cases.

Both contradict the domination consequence above, since \((t,u)\) has positive flow and is incident with \(p\).

Therefore the member of category \(g\) is genuinely arriving at \(p\).

That arriving member is rejected

Every positive-flow activity at \(p\) is weakly preferred in the auxiliary order to \((t,v)\). Its worst doctor category therefore has original priority at least as high as \(g\). Hence every incumbent doctor at \(p\) has priority at least as high as \(g\), and their total mass is \(q_p\).

Under the original responsive choice rule, these incumbents precede a new arrival of category \(g\): higher-priority incumbents have priority, and equal-priority incumbents precede equal-priority arrivals. They already fill the quota. Other arrivals cannot reduce the mass ordered ahead of the arriving category-\(g\) member.

Thus no positive mass of that arriving member can be retained. The proposed deviation fails.

This argument applies to singles, distinct couple destinations, common destinations, and partial unemployment. For a common destination, the arriving worst-priority member’s rejection prevents both members from being retained together.

Therefore \(z\) has no blocking deviation, even allowing real-valued deviations. In particular, it satisfies the stated rational-deviation stability condition.

5. An explicit algorithm producing rational flows

We now give a finite rational linear-programming construction.

Let \(N\) be the number of remaining options, including unemployment. Then

\( N\le \ell, \qquad N\le |S|(m+1)+|K|(m+1)^2 \le \tau(m+1)^2. \)

At program \(p\), retain only supported doctor categories in its acceptance list and number them from best to worst:

\( 1,\ldots,d_p, \qquad d_p\le |S|+2|K|\le 2\tau. \)

Enumerate one state \(h_p\) for each program:

For a fixed state vector, construct an LP with one variable \(z_{t,u}\) per option.

Include nonnegativity, all type mass equalities, and all program capacity inequalities. For every \(h_p=r\), additionally impose:

In this state, call an arriving category \(g\) at \(p\) certifiably rejected if

\( h_p=r\ne *, \qquad \operatorname{rank}_p(g)\ge r. \)

Indeed, all incumbent mass at \(p\) then has priority at least as high as \(g\), and it fills \(q_p\).

For each current option \(u\) and strictly preferred target \(v\), identify the members who genuinely enter real programs. A couple member \(i\) is entering if its target destination \(v_i=p\) is real and its current destination satisfies \(u_i\ne p\).

If none of these entering members is certifiably rejected, impose

\( z_{t,u}=0. \)

There are at most two entering members per comparison. If there are none, this rule also imposes zero flow.

Solve the resulting rational LP and return any feasible solution. Continue enumerating states until one is feasible.

Soundness

For a positive-flow current option \(u\), every strictly preferred target \(v\) must have a certifiably rejected entering member; otherwise the LP would have forced \(z_{t,u}=0\).

The certificate ensures rejection under the original responsive rule for every positive deviation mass. Consequently, every feasible LP solution is stable.

A feasible state exists

Take the real stable assignment constructed in Section 4.

At each full program, choose \(h_p\) to be the rank of its worst positive-mass incumbent category. At every other program choose \(h_p=*\). This assignment satisfies the state’s capacity and zero-flow restrictions.

Moreover, the Section 4 proof established something stronger than stability: for every positive-flow current option and every preferred target, some genuinely arriving category \(g\) faces a destination full of incumbents with priority at least as high as \(g\).

At that destination, the chosen worst-incumbent rank is no greater than \(\operatorname{rank}_p(g)\). Thus \(g\) is certifiably rejected. No additional zero-flow constraint excludes the assignment.

Therefore at least one enumerated LP is feasible.

Rationality and output size

Every candidate LP has rational right-hand sides and integer coefficients of absolute value at most \(2\). Its feasible set is bounded because every option flow is bounded by its type mass.

A nonempty candidate LP therefore has a rational vertex.

More quantitatively, let \(D\) be the product of the denominators of the input masses and quotas. Its binary length is \(O(L)\). At a vertex, choose \(N\) linearly independent active constraints. Their coefficient matrix \(B\) is integral, with entries of absolute value at most \(2\). Hadamard’s inequality gives

\( |\det B|\le (2\sqrt N)^N. \)

After multiplying the right-hand side by \(D\), Cramer’s rule bounds the numerator and denominator length of each flow by

\( O\!\left(L+N\log(N+1)\right). \)

Thus the algorithm produces an explicitly encoded rational stable assignment of polynomial total size.

6. Running times and scope of the conclusion

There are

\( \prod_{p\in P}(d_p+1)\le (2\tau+1)^m \)

state vectors.

For each state, checking all current/target preference comparisons takes \(O(\ell^2+m\tau)\) elementary operations. The resulting LP has \(N\le\ell\) variables, \(O(N+m+\tau)\) constraints, and polynomial encoding length. Rational LP feasibility and vertex extraction take polynomial bit time.

Consequently:

The decision classification follows from universal rational existence. The construction bound above is exponential in general; no polynomial-time search bound is claimed.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover’s claim is proved. The argument establishes universal rational existence, hence a polynomial-time existence decision on promised valid inputs. It also supplies a rational-flow construction with the stated exponential dependence on \(m\). It does not claim polynomial-time construction for unrestricted \(m\).

I found no major or minor mathematical issues requiring repair.

Step-by-step verification

1. The cited existence theorem

The theorem is stated with the relevant hypotheses and the correct conclusion: every unsaturated activity must have an incident vertex whose capacity is filled by activities weakly preferred to it, weighted by their contributions.

This matches the contribution-allocation definition and Theorem 13 in [Biró–Fleiner, Section 3.3](https://real.mtak.hu/26264/7/BF16do_last.pdf). The paper’s preceding matrix construction indexes edges individually and imposes a separate capacity constraint for each edge. Thus the prover’s use of distinct activities sharing an incidence set is legitimate.

The auxiliary instance meets the hypotheses:

The theorem supplies existence over the reals. The prover correctly postpones rationality to its separate LP argument.

2. Removing unacceptable options

The preprocessing is valid. An option involving a category unacceptable to its assigned real program cannot carry feasible assignment flow. It also cannot be an accepted blocking destination, because that destination must retain the unacceptable member.

Removing these options therefore preserves the existence question and all potentially successful blocking deviations. The unemployment option remains available.

3. Auxiliary activities and capacities

The construction reproduces the assignment constraints correctly:

The activity bound \(c_e=\gamma_t\) is consistent with the type-capacity bound. It introduces no restriction beyond the maximum possible flow for that option.

The auxiliary program order is well-defined and strict. A worst category uniquely identifies its type, including for the categories \((k,1)\) and \((k,2)\). Therefore activities with identical worst categories can be compared by that type’s strict option preferences. Activities with different worst categories are compared by strict program priority.

4. Every type’s full mass is assigned

The argument correctly separates the two possibilities for the unemployment activity.

If its flow equals \(\gamma_t\), nonnegativity and the type-capacity inequality force all other flows of that type to vanish.

Otherwise it is unsaturated. Its only incident vertex is its type, so domination must occur there. Because unemployment is last, the domination sum includes every activity of that type and gives total flow exactly \(\gamma_t\).

Thus the theorem’s allocation satisfies the required type equalities, as well as the program-capacity inequalities.

5. A preferred target is unsaturated and cannot be dominated at its type

For a current option \(u\) with positive flow and a strictly preferred target \(v\), the displayed inequality
\[ z_{(t,v)}\leq \gamma_t-z_{(t,u)}<\gamma_t \]
is correct. The target is therefore unsaturated.

At the type vertex, the domination sum excludes the positive flow at \(u\), because \(u\) is strictly worse than \(v\). Hence that sum is strictly below the type capacity.

Consequently, domination must occur at a real program incident with the target. If the target has no real destination, the preceding conclusions instead rule out positive flow at the current option. There is no missing unemployment exception.

6. Consequences of program domination

The prover correctly derives both consequences:

The domination sum is a sub-sum of total program load. It equals quota, while total load is at most quota. Thus the two sums coincide. Since incident contributions are positive, no strictly worse activity can have positive flow.

7. The worst target member must be arriving

This is the central transfer step, and it is valid.

Let \(g\) be the target’s worst category at the dominating program. If that member already occupies the program in the current option, the current activity is incident there and its worst category has priority no higher than \(g\).

The prover covers both possible comparisons:

Both contradict the consequence of domination, because the current activity has positive flow.

This reasoning respects member identities in ordered couples. It also applies when the target sends both members to the same program.

8. Rejection under the original responsive rule

The transfer from auxiliary activity preferences to original category priorities is sound.

Every positive-flow incumbent activity at the dominating program has worst category at least as highly ranked as \(g\). Therefore every incumbent doctor category there has priority at least as high as \(g\), and these incumbents already fill quota.

The member of category \(g\) is arriving. Higher-priority incumbents precede that arrival, and equal-priority arrivals cannot displace incumbents. Additional arrivals cannot create capacity for \(g\): higher-priority arrivals compete ahead of \(g\), and lower-priority arrivals cannot displace the incumbents ahead of it.

Thus no positive deviation mass of that member can be accepted. Rejection of this required member defeats the entire deviation, including at a common destination.

The argument uses original incumbent loads throughout, consistently with the rule that departures do not first free capacity. It establishes absence of real-valued deviations and therefore also absence of rational deviations.

9. LP construction: soundness

The rejection certificates are sufficient.

In state \(h_p=r\), the program is full and every incumbent category has rank at most \(r\). An arriving category with rank at least \(r\) therefore encounters a full quota of incumbents with weakly higher priority.

For each current/target comparison, the LP either provides such a certificate for an entering member or forces the current-option flow to zero. Hence every positive-flow current option is protected against every preferred target.

The treatment of comparisons with no entering members is sound: forcing their current-option flow to zero is a sufficient restriction. The prover does not assert that its certificates characterize every stable assignment.

10. At least one LP state is feasible

The witness is specifically the allocation obtained through domination, whose stronger rejection property was established in Section 4.

At every full program, the worst positive-mass incumbent category exists because quota is positive. Choosing its rank gives the required state restrictions. Nonfull programs use the unrestricted state.

For every positive-flow current option and preferred target, Section 4 supplies an entering member facing a full program whose incumbents all have weakly higher priority. That member satisfies the chosen state’s rejection certificate. Therefore none of the additional zero-flow constraints excludes the witness.

The enumeration consequently reaches a feasible LP.

11. Rationality and output size

Each candidate LP has rational right-hand sides and integer coefficients of absolute value at most two. Type equalities and nonnegativity bound every option flow by its type mass, so the feasible set is bounded.

A nonempty candidate LP has a rational vertex. At a vertex, choosing \(N\) independent active constraints gives a nonsingular integer matrix \(B\). The stated Hadamard bound
\[ |\det B|\leq (2\sqrt N)^N \]
is correct.

The product of input denominators has binary length \(O(L)\). Clearing denominators and applying Cramer’s rule yields the claimed per-coordinate bound
\[ O\!\left(L+N\log(N+1)\right). \]

The running-time section explicitly includes vertex extraction, so the algorithm can return a solution satisfying this size bound. Polynomial total output size follows from \(N\leq\ell\).

12. Running times and scope

The option and category bounds are correct:
\[ N\leq\ell,\qquad N\leq\tau(m+1)^2,\qquad d_p\leq2\tau. \]

There are at most
\[ \prod_{p\in P}(d_p+1)\leq(2\tau+1)^m \]
states.

Although there can be quadratically many current/target comparisons, every additional restriction is a zero constraint on an option variable. Repeated restrictions can be consolidated, giving the stated linear-order constraint count. Each state has polynomial construction and rational LP-solving cost.

Accordingly, the following claims stand:

The distinction between polynomial-time decision and the general construction bound is explicit and consistent with the task.

Required feedback

No repair is required. The output resolves the existence decision and provides a finite algorithm producing rational stable flows, with its computational scope accurately stated.

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