PaperlayerView exact revision on arXiv

Source-linked AI summary

Capacity Modification for Matching with Couples: An Integer Programming and Computational Study

Zexiao Wu, Genjiu Xu, Péter Biró

arXiv:2610.32793v1cs.GT

TL;DR

Capacity decisions can determine whether stable assignments exist in matching markets with couples. The paper develops integer programs and capacity-modification guarantees, then tests their performance and repair outcomes. Exact is modestly faster at fixed capacities, while Cutoff performs better in minimum repair; the experiments also report extensive restoration of stability through small capacity changes.

  • Problem

    In matching with couples, a stable matching may not exist, and the existence problem is NP-complete, while capacity decisions can affect whether stability is attainable.

    Source: §1 · p. 1

  • Method

    The paper develops equivalent Exact and Cutoff integer programs that jointly determine stable matchings and hospital capacities under three modification policies.

    Source: §1 · p. 2

  • Results

    Exact is modestly faster at fixed capacities, while Cutoff performs better in minimum repair and certifies more outcomes at scales up to 30,000 doctors; capacity changes repaired all 12,830 tested markets lacking an original stable matching.

    Source: §1 · p. 2, §8 · p. 18

  • Takeaways & Limitations

    The results suggest considering small capacity reallocations when total capacity is sufficient, then adding positions when necessary.

    Source: §1 · p. 3

    The experiments do not model adjustment costs, so they do not determine an economically optimal capacity policy or expansion budget.

    Source: §8 · p. 19

Abstract

from arXiv · show

We study capacity modification in the Hospitals/Residents problem with Couples, in which hospital capacities and a stable matching are jointly determined. Exact and Cutoff integer programming formulations are developed for the resulting problem. We assume that, for each couple, either both members are matched or neither is. For arbitrary strict preferences, every instance admits a stable matching after changing each hospital capacity by at most two. Total capacity increases by at most one, and this bound is tight. Under sub-responsive and sub-complete couple preferences, a stable matching exists after adding at most one position to each hospital. The total number of additions is at most the number of couples, and this bound is also tight. Computational experiments show that Exact formulations are modestly faster at fixed capacities, whereas Cutoff formulations perform substantially better in the minimum repair experiments and attain higher completion rates in markets with up to 30,000 doctors. Across 96,000 synthetic and reconstructed markets, small capacity changes restore existence whenever no stable matching exists at the original capacities.

1 Introduction

The paper asks whether changing hospital capacities can restore stability in matching markets with couples. It establishes existence guarantees under several capacity policies, develops equivalent Exact and Cutoff integer programs, and evaluates their computational performance.

1 Introduction

  • The study treats capacities as design choices because they can affect whether stability exists, and compares near-feasible, balanced, and unit-expansion policies.Near-feasible modification allows changes of up to two positions per hospital; balanced modification preserves total capacity with changes of at most one; unit expansion limits additions by a budget.Source: §1 · pp. 1–2
  • With jointly assigned or jointly unmatched couples, arbitrary strict preferences permit changes of at most two positions per hospital and a total capacity increase of at most one; the aggregate bound is tight.Balanced unit modification can fail even with a common master list and sub-responsive, sub-complete couple preferences.Source: §1 · p. 2
  • Under sub-responsive and sub-complete preferences, adding at most one position per hospital and at most one per couple suffices, with the aggregate bound tight.Source: §1 · p. 2
  • Exact and Cutoff formulations produce the same stable matchings and capacity vectors; Exact is modestly faster at fixed capacities, while Cutoff performs better in minimum-repair experiments.In scalability tests up to 30,000 doctors, Cutoff completed 93.4% of balanced-modification procedures and 95.4% of unit-expansion procedures, versus 71.4% and 72.2% for Exact.Source: §1 · p. 2
  • Unit expansion repaired all 12,830 markets without an original stable matching, while balanced modification repaired all but 19; allowing changes of up to two positions per hospital repaired the remaining cases.One added position sufficed in 96.4% of the unit-expansion repairs.Source: §1 · p. 2

2 Related work

Related work spans fixed-capacity matching with couples, computational methods for HRC, and capacity modification in matching markets. This paper extends that work by jointly optimizing capacities and stable assignments in HRC.

2 Related work

  • With fixed capacities, stability can be hard to obtain, though restricted preference domains offer guarantees; large random markets show high-probability existence when couples are sufficiently scarce.Source: §2 · p. 3
  • Computational HRC work includes heuristics, Scarf-based methods, and exact integer programs, but these approaches treat hospital capacities as fixed (Biró et al., 2011, 2016, 2014; Delorme et al., 2021).Source: §2 · p. 3
  • Near-feasibility results restore HRC stability through capacity changes, with later work reducing per-hospital changes to one under sub-responsive and sub-complete preferences.The cited guarantees differ in their stability notions and whether they bound aggregate capacity changes.Source: §2 · p. 3
  • Many-to-one capacity-modification studies address expansion, reduction, or implementation, but typically start from markets with an existing stable matching, unlike HRC where stability may fail initially.Source: §2 · p. 3

3 Matching markets with couples

The model assigns singles to acceptable hospitals and couples to acceptable hospital pairs, with each hospital subject to an integer capacity. Stability rules out blocking deviations by singles and couples.

3 Matching markets with couples

  • Each doctor has a strict order over acceptable hospitals, and each hospital has a strict priority order over doctors who find it acceptable.Source: §3 · p. 4
  • Couples rank acceptable ordered hospital pairs and are either jointly assigned to an acceptable pair or both unmatched; assigning only one member is excluded.This assumption models complementarity in joint employment and relocation decisions.Source: §3 · p. 4
  • A matching is feasible when no hospital exceeds its capacity, and stability means there is no blocking coalition under the paper's BIS-stability definition.BIS-stability distinguishes single-doctor deviations, couple deviations to two hospitals, and couple deviations to two positions at one hospital.Source: §3 · p. 4

4 Existence results

The existence results establish capacity-change guarantees for arbitrary strict preferences and for the more restricted sub-responsive, sub-complete domain. They also show that balanced unit modification can fail, while unit expansion has a tight worst-case budget.

4.1 A tight near feasibility guarantee

  • For arbitrary strict preferences with couples jointly assigned or jointly unmatched, changing each hospital's capacity by at most two and increasing total capacity by at most one guarantees stability; the aggregate bound is tight.The proof retains Scarf domination and rounding but replaces deletion of the aggregate capacity constraint; it is existential and does not assert a polynomial-time algorithm.Source: §4.1 · p. 5

4.2 Balanced capacity modification

  • Even with sub-responsive and sub-complete preferences, balanced unit modification may admit no stable matching, although allowing increases or reductions of one per hospital has an MM-stability guarantee.The two-hospital counterexample rules out stability for all three capacity vectors permitted by balanced modification.Source: §4.2 · pp. 5–6

4.3 Unit capacity expansion

  • For sub-responsive and sub-complete preferences, adding at most one position per hospital and a total of at most |C| positions guarantees stability.The preference restrictions require individual orders to govern pair rankings when one member's assignment changes, and every pair of individually acceptable hospitals must be acceptable to the couple.Source: §4.2 · p. 5, §4.3 · p. 6
  • The |C| expansion budget is tight: for every m ≥ 1, an instance with m couples requires a minimum budget of m.Source: §4.3 · p. 6

5 Integer programming formulations

The integer programming formulations encode assignments and stability, then extend the model to choose hospital capacities under three modification policies. Their feasibility characterizes stable matchings and capacity vectors allowed by each policy.

5 Integer programming formulations

  • The framework separates fixed-capacity stability testing from capacity-modification models for near-feasible, balanced, and unit-expansion policies.The capacity-modification formulation makes capacities decision variables and applies the three policies to the same core model.Source: §5 · p. 6, §5.2 · p. 8

5.1 IP with fixed capacities (IFC)

  • Binary variables represent doctor-hospital assignments and couple-pair assignments, with constraints linking a couple’s pair assignment to both members’ placements or leaving both unmatched.Hospital feasibility and stability constraints are added to these assignment constraints.Source: §5 · p. 6, §5.1 · p. 7
  • When a doctor has not obtained a hospital or a preferred one, the S1 constraints require that hospital to be full with doctors it ranks at least as highly.The formulation uses inequalities to exclude S1 blocks.Source: §5.1 · p. 7
  • For a couple preferring another pair, constraints keep at least one proposed hospital’s priority condition active, while a separate constraint excludes S3 blocks.For couples applying to the same hospital, the BIS constraint reduces to the cited fixed-capacity constraint under strict preferences.Source: §5.1 · p. 7
  • IFC is feasible exactly when a stable matching exists at the fixed capacities, and its objective selects one with the maximum number of matched doctors.The formulation specializes the fixed-capacity BIS formulation to strict preferences and couples that cannot be partially assigned.Source: §5.1 · p. 7

5.2 IP with capacity modification (ICM)

  • ICM adds integer variables for positions added and removed, uses modified capacities in the stability constraints, and linearizes bounded-capacity stability inequalities.The linearization extends the bounded-capacity approach to the three BIS blocking types.Source: §5.2 · p. 8

5.3 Capacity modification policies

  • ICM-BC preserves total capacity with at most one position gained or lost per hospital; ICM-UC allows additions only, while ICM-NF permits changes of up to two positions per hospital.The policies impose distinct capacity restrictions and objectives, including minimizing additions or determining whether total capacity must increase.Source: §5.3 · p. 9
  • Each policy formulation is feasible exactly when a stable matching exists under a capacity vector allowed by that policy; the cardinality objective maximizes matched doctors.The same equivalence holds for the general ICM formulation over unrestricted capacity vectors.Source: §5.3 · p. 9

6 Cutoff formulations

The cutoff formulations encode hospital priority thresholds and doctor preference prefixes to exclude blocking coalitions. They admit exactly the same matching and capacity vectors as the original formulations.

6 Cutoff formulations

  • Hospital priority scores define a cutoff variable and a binary indicator, with modified-capacity bounds set by the selected policy.A larger score means higher hospital priority, and scores are compared only within the same hospital.Source: §6 · p. 9
  • Assigned doctors must meet their hospital’s cutoff, while hospitals with unfilled positions cannot reject acceptable doctors through a positive cutoff.A zero-capacity hospital may retain a positive cutoff.Source: §6 · p. 9
  • Doctor preference-prefix variables mark whether a doctor receives a hospital or one they prefer, so a doctor lacking that outcome must exceed the hospital’s cutoff score.These constraints encode the single-doctor S1 condition.Source: §6 · pp. 9–10
  • For couples, assignment indicators and hospital cutoffs exclude proposed blocking pairs, while tail variables handle same-hospital S3 cases, including the partner-dependent case.The tail count combines unfilled positions with assignees ranked below the proposed member.Source: §6 · p. 10
  • The original and cutoff formulations admit exactly the same matching and capacity vector for each fixed-capacity or capacity-modification model.The result covers IFC, ICM-NF, ICM-BC, and ICM-UC.Source: §6 · p. 10

7 Computational study

The computational study evaluates the Exact and Cutoff formulations across stability, repair, and scalability problems in synthetic and reconstructed markets, reporting solver certification and repair outcomes. It also examines how capacity increases relate to matching cardinality and stability restoration in the tested markets.

7.1 Formulation comparison

  • IFC and IFC-CUT agree on optimal values for 484 feasible variants and prove 26 infeasible; IFC is modestly faster overall, with a paired geometric mean time ratio of 0.88.IFC-CUT averages 22.3% fewer variables and 1.9% fewer nonzero coefficients, but 9.9% more constraints.Source: §7.1 · p. 11, Table 2 · p. 12
  • Cutoff certifies minimum repairs in all 26 infeasible variants under both policies, while Exact certifies 25 balanced repairs and Enumeration certifies 24 under each policy.Exact-to-Cutoff mean PAR-2 time ratios are 5.43 for balanced modification and 1.33 for unit expansion; one balanced transfer suffices in every variant, while unit expansion needs one added position in 25 and two in one.Source: Table 3 · p. 12, §7.1 · p. 12

7.2 Existence and capacity modification across stability conditions

  • BIS and KPR admit stable matchings in 84 of 90 markets each, compared with 54 under MM and 53 under NV.All 30 master-list markets where couples accept only same-hospital assignments are stable under BIS and KPR but not MM or NV; the same six hospital-specific-priority markets are infeasible under all four notions.Source: Table 4 · p. 13, §7.2 · p. 13
  • Exact and Cutoff certify minimum repairs in all 170 problems, whereas Enumeration certifies 56; for MM and NV, Cutoff has the lowest mean PAR-2 times.For MM and NV, Exact-to-Cutoff time ratios are approximately 55 and 53 under balanced modification, and 46 and 41 under unit expansion. The minimum is one transfer and one added position in each selected BIS and KPR case; MM and NV means are 2.56 and 2.59 transfers, and 5.17 and 5.22 added positions, respectively.Source: §7.2 · pp. 13–14, Figure 1 · p. 14

7.3 Existence and capacity modification across market types

  • IFC-CUT finds stable matchings in 73,360 of 84,000 synthetic instances and proves nonexistence in 10,640; pooled nonexistence rises from 2.18% at 5% couples to 21.61% at 100%.At Q=100, nonexistence is 13.09% under master lists and 3.15% under hospital-specific priorities; the difference is smaller across random versus rank-sum couple preferences (9.28% versus 6.96%) and same-hospital assignments allowed versus excluded (8.43% versus 7.81%).Source: Table 5 · p. 15, §7.3 · p. 15
  • One balanced transfer repairs all 3,897 initially infeasible Q=100 instances, and unit expansion repairs all 10,640 infeasible instances with at most one added position per hospital.Balanced unit modification is infeasible in 19 instances, each of which needs only one added position; allowing each hospital to gain or lose up to two positions restores stability in all 10,640 while preserving total capacity.Source: §7.3 · p. 15

7.4 Existence and capacity modification across methods

  • In the 12,000 reconstructed data500 markets, 2,190 lack stability at original capacities, and both repair policies restore stability in all 2,190.The minimum balanced repair is one transfer in every case; unit expansion requires one added position in 2,096 markets, two in 93, and three in one. Nonexistence rises from 2.5% with 12 couples to 35.3% with 250 couples.Source: Table 6 · p. 16, §7.4 · p. 16

7.5 Matching cardinality with additional positions

  • The study examines how bounded capacity expansion changes maximum matching cardinality in markets that already have stable matchings, including 9,810 such markets.It defines cumulative gain as Δ_r(B)=m_r(B)−m_r(0) and marginal gain as d_r(B)=m_r(B)−m_r(B−1).Source: §7.5 · p. 16, Figure 2 · p. 17
  • The solver proves optimality in 97,999 runs, while 93 matching-cardinality values remain known only within certified bounds.There are 98,100 optimization runs; 101 reach the time limit, and mean and median running times are 7.61 and 0.60 seconds.Source: §7.5 · p. 17
  • At B=10, mean cumulative matching gains are 11.342–11.348 doctors, while pooled marginal gains fall from 1.881–1.882 at B=1 to 0.711–0.719 at B=10.At B=1, 63.9% of markets gain more than one matched doctor; expansion can also enable a different stable matching that fills previously unused positions at other hospitals, and average marginal gains diminish over the tested budgets.Source: §7.5 · p. 17

7.6 Scalability of the Exact and Cutoff formulations

  • At n=30,000, Cutoff completes 92% of balanced-modification cases and 96% of unit-expansion cases, versus 50% for Exact under either policy.Across all 500 markets, completion rates are 93.4% and 95.4% for Cutoff under balanced modification and unit expansion, respectively, versus 71.4% and 72.2% for Exact.Source: Figure 3 · p. 18, §7.6 · p. 18
  • Cutoff certifies maximum-cardinality stable matchings in 458 markets and infeasibility in 42, while Exact certifies maximum cardinality in 345, proves infeasibility in 18, and leaves 137 unresolved.Among markets entering repair, Cutoff certifies minimum repairs in 9 under BC and 19 under UC; Exact certifies 12 under BC and 16 under UC, but these repair results are not directly comparable because the procedures enter repair on different market sets with different remaining time.Source: §7.6 · p. 18

8 Conclusion

The paper establishes tight capacity-modification guarantees and compares integer-programming formulations, while its experiments show that small changes often restore stability in tested markets. The appendix distinguishes stability notions and describes the Exact and Cutoff formulations.

8 Conclusion

  • For arbitrary strict preferences, BIS-stability is guaranteed when each hospital changes capacity by at most two and total capacity is preserved or increases by one; the net bound is tight.Under sub-responsive and sub-complete preferences, additions alone suffice: at most one per hospital and at most as many additions as couples, with a tight aggregate bound.Source: §8 · p. 18
  • Cutoff outperforms Exact in paired minimum-repair experiments and certifies more outcomes at scales up to 30,000 doctors, while Exact is modestly faster at fixed capacities.The minimum-repair problem remains difficult at larger scales.Source: §8 · p. 18
  • Among 96,000 tested markets, all 6,087 fixed-capacity failures with total capacity equal to the doctor count were repaired by one balanced transfer.The paper notes that this pattern suggests considering reallocation before expansion in comparable markets, but is not a general existence guarantee.Source: §8 · p. 18
  • Because the experiments omit adjustment costs, they do not identify an economically optimal modification policy or expansion budget.Whether one-position changes suffice under arbitrary strict preferences, and whether one-position-per-hospital expansion suffices, remain open.Source: §8 · p. 19

A.1. Definitions and relationships

  • The appendix explains that KPR-stability, MM-stability, and NV-stability retain S1 and S2, differing only in the S3 condition; NV tests each couple member separately.Under NV, the same vacant position or displaced doctor may support both individual acceptance conditions, unlike MM.Source: §A.1 · p. 19

A.2. Exact and Cutoff formulations

  • The Exact formulations replace the S3 constraints for KPR, MM, and NV, while the Cutoff formulations use corresponding stability-specific constraints alongside shared constraints and recursions.The appendix gives the fixed- and variable-capacity replacements and specifies which additional constraint each Cutoff formulation uses.Source: §A.2 · p. 20

A.3. Proofs for NV and Cutoff

The appendix proves that Exact and Cutoff formulations represent the same stable matchings and capacity vectors for KPR, MM, and NV. It establishes this by comparing their S3 constraints after accounting for shared S1 and S2 conditions.

A.3. Proofs for NV and Cutoff

  • The NV constraint excludes an NV S3 block, and adding the capacity-policy constraints restricts feasible solutions to the permitted capacity vectors.The proof also shows that the Exact and Cutoff NV inequalities agree for every admissible capacity vector.Source: §A.3 · pp. 20–22
  • For KPR-stability, MM-stability, and NV, Exact and Cutoff formulations admit exactly the same matchings and capacity vectors.The proof combines the equivalence of shared S1 and S2 constraints with equivalence of the respective S3 constraints.Source: §A.3 · pp. 21–22
  • For a same-hospital couple option, the proof compares Exact and Cutoff S3 constraints using member priority ranks, prefix counts, and the capacity bound.When the couple does not receive the option, the MM inequalities reduce to a condition negating the need for two distinct admissible positions.Source: §A.3 · pp. 21–22

B.1. Proof of Theorem 4.2

The proof modifies iterative rounding to preserve domination while producing an integral assignment. Under the joint-assignment assumption for couples, it bounds each hospital’s capacity change by two and aggregate capacity increase by one.

B.1. Proof of Theorem 4.2

  • The modified rounding keeps active hospital constraints as equalities and changes how slack assignment constraints are handled when the aggregate capacity constraint is removed.It maximizes total assigned positions at each iteration, so the objective does not decrease.Source: §B.1 · pp. 22–23
  • The improvement relies on every acceptable couple assignment using exactly two hospital positions, an identity that need not hold if partial couple assignments are allowed.The construction treats each single or couple as one agent and uses assignment columns with one or two positions, respectively.Source: §B.1 · p. 23
  • When no hospital has at most three fractional variables, the proof groups at most two slack agent constraints before removing the aggregate constraint.The grouped row preserves individual assignment feasibility, and a token-counting argument establishes termination at an integral vector.Source: §B.1 · pp. 23–24
  • The rounding yields an integral assignment whose total assigned positions increase by at most one over the initial total.If the aggregate constraint is removed, the fractional agents’ final contribution can increase by at most one.Source: §B.1 · p. 24
  • Each hospital’s capacity changes by at most two, and the resulting matching is BIS-stable under the rounded capacity vector.The proof preserves domination during rounding and verifies BIS-stability by ruling out each type of blocking coalition.Source: §B.1 · pp. 24–25

B.2. Proof of Proposition 4.3

The appendix gives an instance with three hospitals and fixed initial capacities for which no capacity vector allowed by balanced modification admits a stable matching. The proof forces assignments and derives a blocking couple in every case.

B.2. Proof of Proposition 4.3

  • With three hospitals initially at capacity (3, 3, 3), four couples, and two single doctors, the construction rules out stability under every balanced-modification capacity vector.The instance’s preference lists and common hospital priority order specify the counterexample.Source: §B.2 · pp. 25–26
  • The proof enumerates the permitted capacity cases and uses successive rejection conditions to force assignments of the singles and couples.Every acceptable couple pair uses distinct hospitals, so S3 blocks cannot occur in this instance.Source: §B.2 · p. 25
  • In each permitted case, a couple left unmatched forms an S2 block, contradicting the assumed absence of blocking.The proof lists the blocking couple and option for each capacity case.Source: §B.2 · pp. 25–26

B.3. Proof of Theorem 4.5

The proof adapts the Stable Fixtures construction and rounding under sub-completeness, then establishes the resulting matching’s capacity bounds and BIS stability.

B.3. Proof of Theorem 4.5

  • Under sub-completeness, rounding yields a BIS-stable matching with no hospital reductions and at most one added position per hospital.The proof also requires both members of each couple to be assigned or both unmatched.Source: §B.3 · pp. 26–28
  • The construction starts from a stable half-integral matching and assigns each doctor her most-preferred hospital among those with positive edge value.A doctor with no such hospital remains unmatched.Source: §B.3 · pp. 26–27
  • The rounding respects connected couple gadgets: saturation rules out assigning just one member of a couple.Under sub-completeness, an assigned hospital pair is acceptable.Source: §B.3 · p. 27
  • The capacity proof counts doctors incident to one or two hospital half-edges and establishes n1 ≤ 2|C| for the total-expansion bound.Each hospital incident to half-edges has exactly two such edges.Source: §B.3 · p. 27
  • For a preferred alternative, the proof identifies a proposed doctor–hospital edge that is zero in the fractional matching and dominated at the hospital.This rejection argument establishes BIS stability for the rounded matching.Source: §B.3 · p. 28
  • The construction, rounding, and additional verification run in O(L) time without scanning potentially quadratic joint-option lists.Checking whether an explicitly supplied joint ranking satisfies the preference restrictions is outside the construction.Source: §B.3 · p. 28

B.4. Proof of Proposition 4.6

The proposition proves that the |C| upper bound on total additions is tight, using disjoint components that satisfy the stated preference restrictions.

B.4. Proof of Proposition 4.6

  • The universal bound Bmin(I) ≤ |C| is attained, even with a common master list and distinct hospitals in every acceptable couple assignment.The constructed couple preferences are sub-complete and sub-responsive.Source: §B.4 · p. 28
  • Disjoint components force at least one added position each, so m components require at least m additions in any stable solution.There are no acceptable assignments between components.Source: §B.4 · p. 28
  • The union of the component matchings is stable because every doctor gets a most-preferred acceptable assignment and each couple gets its only acceptable pair.This matching attains the lower bound and establishes equality.Source: §B.4 · p. 28

B.5. Proof of Theorem 5.1

The proof establishes a correspondence between integer-program solutions and BIS-stable matchings with admissible capacities, including when the objective is changed.

B.5. Proof of Theorem 5.1

  • An integer solution of ICM defines a matching and capacity vector that are BIS-stable under those capacities.The fixed-capacity equivalence connects the ICM constraints to the original formulation.Source: §B.5 · p. 29
  • Conversely, every BIS-stable matching under an integer capacity vector can be encoded as a feasible ICM solution.Assignment indicators and auxiliary variables extend the matching to satisfy the formulation.Source: §B.5 · p. 29
  • Restricting the capacity vector yields the corresponding equivalence for balanced, unit-expansion, and near-feasible modification.The proof gives the respective signed-change and total-capacity constraints for these regions.Source: §B.5 · p. 29
  • Maximizing the number of matched doctors selects a largest stable matching across admissible capacity vectors without changing the feasibility correspondence.The objective can instead measure capacity.Source: §B.5 · p. 29

B.6. Proof of Theorem 6.1

The proof shows that the cutoff formulation captures precisely the stable matchings and capacity vectors of the original formulation.

B.6. Proof of Theorem 6.1

  • The cutoff constraints exclude S1 blocks by making a hospital full and showing every current assignee outranks the proposed single doctor.The single-doctor prefix recursion supplies the cutoff condition.Source: §B.6 · p. 29
  • For a couple proposing two distinct hospitals, the cutoff constraints prevent an S2 block when at least one hospital cannot accommodate its proposed member.The couple-prefix recursion identifies the proposed option for the constraints.Source: §B.6 · p. 29
  • For a couple proposing the same hospital, constraints (27)–(29) exclude the stated S3 blocking cases.The proof handles cases involving vacancies, priority over incumbents, and couples already assigned to that hospital.Source: §B.6 · p. 29
  • A stable matching can be extended with cutoff variables satisfying the formulation, so both formulations yield the same matchings and capacity vectors.The construction sets hospital cutoffs from fullness and assignee scores, then uses the recursions for the remaining variables.Source: §B.6 · pp. 29–30
Loading 2610.32793v1…