← back to the atlas

d4-conf-aaai-2015-0787 (d4-conf-aaai-2015-0787)

Answer: Polynomial-time solvable in \(m,\tau,L\), with bit running time \(O((m+1)(m+\tau)L^2)\).

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateGiven an instance of ASIP, Algorithm 1 terminates in polynomial time. If a stable invitation exists the algorithm produces a maximum one, otherwise it determines that no stable invitation exists.

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 types \(T\), rational masses \(\mu_t \ge 0\) summing to \(1\), and for each type a set \(A_t \subseteq [0,1]\) of attendance fractions at which attending is preferred to the outside option, encoded as a finite union of rational intervals with specified endpoint inclusion, choose invited masses \(y_t \in [0,\mu_t]\) maximizing \(a=\sum_t y_t\). Require \(y_t>0\) to imply \(a\in A_t\), and require that whenever \(y_t<\mu_t\), no right-neighborhood of \(a\) lies in \(A_t\). Find a maximum stable invitation or certify that none exists.

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

A society is given by its support: a list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\), with \(\sum_{t\in T}\mu_t=1\); \(\tau\) counts supported types, not possible types.
Preferences are truthful and depend only on attendance fraction. Each \(A_t\subseteq[0,1]\) is an explicitly listed finite union of rational intervals with specified endpoint inclusion; empty sets and singleton intervals are allowed. At every positive fraction, membership means strictly preferring attendance to the outside option, and nonmembership means strictly preferring the outside option; there is no indifference.
An invitation consists of real masses \(0\le y_t\le\mu_t\), with attendance \(a=\sum_{t\in T}y_t\). It is stable if, for every \(t\), \(y_t>0\Rightarrow a\in A_t\), and \(y_t<\mu_t\Rightarrow\nexists\varepsilon\in(0,1-a]\; (a,a+\varepsilon)\subseteq A_t\).
The empty invitation is allowed. Membership of \(0\) in \(A_t\) has no effect; at \(a=1\) there is no right-neighborhood within the attendance domain.
The computational problem is to find a stable invitation maximizing \(a\), or determine that none exists. Let \(m\) be the total number of listed intervals and \(L\) the total input bit length; state running times in \(m,\tau,L\).

Is this continuous maximum stable invitation problem solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

For finitely many agents with arbitrary anonymous preferences and no indifference to the outside option, finding a maximum stable invitation or determining nonexistence is polynomial-time solvable. [Lee and Shoham](https://arxiv.org/pdf/1405.7751)
No result settling the exact continuous problem above 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 problem is polynomial-time solvable in \(m,\tau,L\). In fact, the set of feasible attendance fractions has at most \(4m+3\) elements. Consequently, whenever a stable invitation exists, a maximum is attained.

1. Feasibility at a fixed attendance fraction

For \(a\in[0,1]\), define
\[ \]
\(P(a)=\{t\in T:a\in A_t\}\),

\(R(a)=\{t\in T:\exists\varepsilon\in(0,1-a]\text{ with }(a,a+\varepsilon)\subseteq A_t\}\).

For \(S\subseteq T\), write \(M(S)=\sum_{t\in S}\mu_t\).

Lemma. A stable invitation with attendance \(a\) exists if and only if

\(R(a)\subseteq P(a)\quad\text{and}\quad M(R(a))\le a\le M(P(a)).\)

Proof. Suppose \(y\) is stable with attendance \(a\). If \(t\in R(a)\), the second stability condition rules out \(y_t<\mu_t\); hence \(y_t=\mu_t>0\). The first stability condition then gives \(t\in P(a)\). If \(t\notin P(a)\), the first condition forces \(y_t=0\). Summing these restrictions gives the stated inequalities.

Conversely, suppose the conditions hold. Set \(y_t=\mu_t\) for \(t\in R(a)\), and \(y_t=0\) for \(t\notin P(a)\). Distribute the remaining attendance

\(d=a-M(R(a))\)

among the types in \(P(a)\setminus R(a)\). Their total capacity is

\(M(P(a)\setminus R(a))=M(P(a))-M(R(a))\ge d\ge0\).

Thus this distribution exists: successively assign each such type the smaller of its mass and the remaining amount. Every type receiving positive mass lies in \(P(a)\). Every type receiving less than its full mass lies outside \(R(a)\). These are precisely the two stability conditions. \(\square\)

The lemma also handles the boundary fractions correctly. At \(a=0\), positivity of the masses makes feasibility equivalent to \(R(0)=\varnothing\), independently of membership of \(0\). At \(a=1\), we have \(R(1)=\varnothing\), and feasibility is equivalent to \(P(1)=T\).

2. Computing the right-neighborhood condition

Consider a listed interval with endpoints \(\ell\le r\). It contains a right-neighborhood of \(a\) exactly when

\(\ell\le a<r\),

regardless of either endpoint’s inclusion.

If this inequality holds, choose a positive \(\varepsilon<r-a\); every point in \((a,a+\varepsilon)\) is strictly between the interval’s endpoints.

Conversely, suppose no interval listed for a type satisfies this inequality. Each interval whose left endpoint is at most \(a\) ends at or before \(a\). Every other interval starts strictly after \(a\). Because the list is finite, a sufficiently small right-neighborhood of \(a\) misses all these intervals. Therefore, for \(a<1\),

\(t\in R(a)\iff\text{some interval listed for }t\text{ has }\ell\le a<r.\)

At \(a=1\), both sides are false because every right endpoint is at most \(1\). Singleton and empty intervals contribute nothing to \(R(a)\). Membership in \(P(a)\) is computed separately using the specified endpoint inclusion.

3. A finite set containing every feasible attendance

Sort the distinct listed interval endpoints together with \(0\) and \(1\), obtaining

\(0=e_0<e_1<\cdots<e_k=1,\qquad k\le2m+1.\)

Fix an open gap \(I_i=(e_i,e_{i+1})\). Each listed interval has constant membership throughout \(I_i\), since neither endpoint lies inside the gap. Hence every \(A_t\) has constant membership there. Write

\(P_i=\{t\in T:I_i\subseteq A_t\}\).

For every \(a\in I_i\), we have \(P(a)=R(a)=P_i\). Indeed, membership gives an accepted right-neighborhood contained in the gap, while nonmembership excludes any such neighborhood.

The fixed-fraction lemma therefore gives

\(a\text{ is feasible in }I_i\iff a=M(P_i).\)

Thus each gap contains at most one feasible attendance fraction. It contains one exactly when

\(e_i<M(P_i)<e_{i+1}.\)

When this condition holds, a witnessing invitation is simply

\(y_t=\mu_t\text{ for }t\in P_i,\qquad y_t=0\text{ otherwise}.\)

Every remaining feasible fraction must be one of the endpoints. There are at most \(k+1\) endpoints and at most \(k\) feasible fractions inside gaps, so the feasible attendance set has cardinality at most

\(2k+1\le4m+3.\)

This proves that a maximum exists whenever the feasible set is nonempty, despite the real-valued invitation variables and potentially open preference intervals.

4. Algorithm and running time

The algorithm is:

The preceding results prove that this algorithm examines every possible feasible attendance fraction and returns a maximum stable invitation.

Each endpoint or gap requires one scan of the intervals and types, costing \(O(m+\tau)\) exact arithmetic operations. The total is

\(O\bigl(m\log(m+1)+(m+1)(m+\tau)\bigr)\)

exact arithmetic operations.

For an explicit bit bound, let \(D\) be the product of the denominators of all input masses and interval endpoints. Its bit length is \(O(L)\), because the input explicitly contains those denominators. Scale the input rationals by \(D\). All endpoints, masses, and mass sums then have integer representations of \(O(L)\) bits. Midpoint membership can be tested by doubling coordinates, also using \(O(L)\)-bit integers.

Computing \(D\), scaling the input, comparing values, and constructing the final invitation can all be performed using ordinary integer arithmetic in total time bounded by

\(O\bigl((m+1)(m+\tau)L^2\bigr).\)

The returned invitation has rational coordinates of \(O(L)\) bits each. Thus both the computation and its output size are polynomial in the stated input parameters.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the stated problem correctly: the continuous maximum stable invitation problem is polynomial-time solvable in \(m,\tau,L\). The proof establishes an exact feasibility criterion, shows that only finitely many attendance fractions can be feasible, and gives an exhaustive algorithm with a valid polynomial bit-complexity bound.

No major or minor mathematical issues were found.

Step-by-step verification

1. Fixed-fraction feasibility criterion

The definitions of \(P(a)\) and \(R(a)\) accurately represent the two stability conditions.

For necessity:

For sufficiency, the proposed construction is valid. The inclusion \(R(a)\subseteq P(a)\) makes the mandatory and prohibited assignments consistent. The remaining amount satisfies
\(0\le d\le M(P(a)\setminus R(a))\), so the described greedy allocation fills it exactly without exceeding any capacity.

Every type receiving positive mass belongs to \(P(a)\), and every type receiving less than its full mass lies outside \(R(a)\). Thus both stability conditions hold.

The lemma is fully proved.

2. Boundary fractions

The boundary conclusions are correct.

At \(a=0\), the lower feasibility bound and positivity of all masses force \(R(0)=\varnothing\). Conversely, when \(R(0)=\varnothing\), the empty invitation is stable. Membership of \(0\) plays no role.

At \(a=1\), \(R(1)=\varnothing\) because the permitted range for \(\varepsilon\) is empty. The upper feasibility bound requires \(M(P(1))\ge1\). Since total mass is \(1\) and every supported mass is positive, this is equivalent to \(P(1)=T\).

3. Right-neighborhood computation

For a listed interval with endpoints \(\ell\le r\), the condition \(\ell\le a<r\) is exactly the condition that it contains a right-neighborhood of \(a\). Endpoint inclusion does not matter because the neighborhood excludes \(a\), and its upper endpoint can be chosen strictly below \(r\).

The converse for a finite union is also justified. If no listed interval satisfies the condition, each interval either ends at or before \(a\), or starts strictly after \(a\). Finiteness allows a sufficiently small neighborhood to avoid every interval of the second kind; intervals of the first kind contain no point greater than \(a\).

The treatment of \(a=1\), singleton intervals, and empty intervals is correct. Computing membership separately preserves all endpoint-inclusion information.

4. Finite feasible attendance set

Within any open gap between consecutive distinct endpoints, membership in each listed interval, and hence in each \(A_t\), is constant.

The identity \(P(a)=R(a)=P_i\) throughout the gap is justified:

The feasibility lemma consequently reduces to \(a=M(P_i)\). Thus a gap contains precisely one feasible fraction when \(e_i<M(P_i)<e_{i+1}\), and none otherwise. The stated full-or-zero invitation witnesses feasibility in that case.

Every other feasible fraction is an endpoint. There are at most \(2m+2\) distinct endpoints after adding \(0\) and \(1\), giving \(k\le2m+1\). Therefore the cardinality bound \(2k+1\le4m+3\) is valid.

A nonempty finite set has a maximum, so maximum attainment is established even with open preference intervals.

5. Algorithm correctness

The endpoint tests use the exact feasibility criterion. The gap tests identify every possible feasible fraction in each gap. Together, these tests exhaust \([0,1]\).

Choosing the largest retained fraction and applying the lemma therefore returns a maximum stable invitation. If nothing is retained, no stable invitation exists.

6. Running time and output representation

There are \(O(m+1)\) endpoints and gaps. Each requires a scan costing \(O(m+\tau)\) arithmetic operations, so the stated arithmetic-operation bound is valid.

Under the explicit rational encoding in the task, the product \(D\) of input denominators has \(O(L)\) bits. Scaling by \(D\) gives integer coordinates of \(O(L)\) bits. Mass sums remain bounded by \(D\), and doubled coordinates suffice for midpoint comparisons.

Ordinary integer arithmetic therefore supports the claimed conservative bound
\(O((m+1)(m+\tau)L^2)\), including preprocessing, sorting, feasibility tests, and construction. The greedy construction uses differences and minima of scaled integers, so its output coordinates also have \(O(L)\) bits each.

No cited external theorem or unproved mathematical lemma is needed.

Repair feedback

None required. The argument is complete and internally consistent.

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