← back to the atlas

Proportional Fairness in Obnoxious Facility Location (aamas24-00124)

Answer: \(\mathrm{P}\): polynomial-time solvable, with an exact rational maximizer computable in \(O(m\tau L^2)\) bit operations for \(m=2\).

The anchor (named result in the paper)

Lemma 5.10 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximate2-UFS Randomized mechanism is optimal for utilitarian welfare amongst all randomized mechanisms satisfying 2-UFS in expectation. Surprisingly, imposing the stronger fairness axiom of 2-UFS as opposed to 2-IFS has a minimal effect on the welfare-optimal mechanism’s approximation ratio. Again, the approximation ratio is computed algebraically.

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

The continuous mirror question, as graded

Given rational locations \(x_t\in[0,1]\) and masses \(\mu_t\ge0\) with \(\sum_{t=1}^{\tau}\mu_t=1\), compute an exact endpoint lottery \(\pi^\star=p^\star\delta_0+(1-p^\star)\delta_1\) maximizing \(\sum_t\mu_t\bigl(p x_t+(1-p)(1-x_t)\bigr)\) subject to \(p x_t+(1-p)(1-x_t)\ge\mu_t/2\) for every \(t\) and \(0\le p\le1\).

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

A society is given by its support: \(\tau\ge1\) distinct rational locations \(x_t\in[0,1]\), each with a positive binary-rational mass \(\mu_t\), where \(\sum_{t=1}^{\tau}\mu_t=1\). Types are locations; repeated locations are merged by adding their masses. Thus \(\tau\) is the support size, not the number of possible types.
An obnoxious facility gives utility \(|y-x_t|\) to type \(t\) when placed at \(y\). An endpoint lottery is \(\pi_p=p\delta_0+(1-p)\delta_1\), where \(\delta_y\) is point mass at \(y\) and \(p\in[0,1]\).
Its expected utility is \(u_t(p)=p x_t+(1-p)(1-x_t)\). It satisfies \(2\)-Unanimous Fair Share in expectation precisely when \(u_t(p)\ge\mu_t/2\) for every support type.
Compute an exact rational maximizer \(p^\star\) of \(\sum_{t=1}^{\tau}\mu_t u_t(p)\) subject to these inequalities and \(0\le p\le1\); any maximizer is acceptable.
Let \(L\) be the total binary input length and \(m=2\) the number of allowed facility locations. State running times in \(m,\tau,L\).

Can this exact optimization problem be solved in time polynomial in \(m,\tau,L\), or is it NP-hard?

For a finite list of agents, an explicit polynomial-time endpoint-lottery mechanism maximizes utilitarian welfare subject to expected \(2\)-Unanimous Fair Share, with each co-located group guaranteed its size divided by twice the total population. [Discrete welfare optimality](https://arxiv.org/html/2301.04340v2#S5.SS4)
No result addressing exactly the binary-rational mass formulation 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. For the specified \(m=2\), the algorithm below uses \(O(\tau)=O(m\tau)\) rational arithmetic operations and \(O(\tau L^2)=O(m\tau L^2)\) bit operations with schoolbook integer arithmetic. Its output has \(O(L)\) bits.

Here \(m\) counts allowed facility locations, while \(\tau\) counts support types.

1. Feasibility

Since the positive masses sum to \(1\), each satisfies \(\mu_t\leq 1\). At \(p=1/2\), every type receives

\(u_t(1/2)=\frac{x_t}{2}+\frac{1-x_t}{2}=\frac12\geq\frac{\mu_t}{2}.\)

Thus the feasible set is always nonempty.

2. Compute the exact feasible interval

For each support type, rewrite its constraint as

\((1-x_t)+(2x_t-1)p\geq\mu_t/2.\)

There are three cases:

\(p\geq\ell_t:=\frac{\mu_t/2-(1-x_t)}{2x_t-1}\).

\(p\leq r_t:=\frac{1-x_t-\mu_t/2}{1-2x_t}\).

Define

\(p_{\min}:=\max\bigl(\{0\}\cup\{\ell_t:x_t>1/2\}\bigr),\)

\(p_{\max}:=\min\bigl(\{1\}\cup\{r_t:x_t<1/2\}\bigr).\)

The case analysis proves both directions: a probability satisfies every constraint and belongs to \([0,1]\) if and only if it belongs to \([p_{\min},p_{\max}]\). Feasibility of \(1/2\) additionally gives

\(0\leq p_{\min}\leq 1/2\leq p_{\max}\leq 1.\)

Both interval endpoints are rational and can be computed by scanning the support once.

3. Maximize welfare

Let \(M:=\sum_{t=1}^{\tau}\mu_t x_t\). Using \(\sum_t\mu_t=1\), welfare is

\(W(p):=\sum_t\mu_t u_t(p)=1-M+(2M-1)p.\)

Consequently, return:

For the first case, \(W\) is strictly increasing, so its maximum on the feasible interval is its right endpoint. For the second, it is strictly decreasing, so its maximum is its left endpoint. For the third, it is constant, and the selected probability is feasible.

This proves that the algorithm returns an exact rational maximizer in every case, including \(\tau=1\).

4. Bit complexity

Use the explicit binary encoding of rational numerators and denominators. Write \(x_t=a_t/b_t\) and \(\mu_t=c_t/d_t\), with positive denominators.

The bounds can be computed directly as

\(\ell_t=\frac{b_tc_t-2d_t(b_t-a_t)}{2d_t(2a_t-b_t)}\quad\text{when }2a_t>b_t,\)

\(r_t=\frac{2d_t(b_t-a_t)-b_tc_t}{2d_t(b_t-2a_t)}\quad\text{when }2a_t<b_t.\)

Each numerator and denominator has \(O(L)\) bits. Bounds are compared exactly by cross multiplication with positive denominators. Maintaining their maximum or minimum only selects an existing bound, so it does not accumulate denominators.

For the mean,

\(M=\sum_t\frac{a_tc_t}{b_td_t}.\)

Its partial sums can be represented without reduction, using the product of the processed denominators. The binary length of this product is at most

\(1+\sum_t\bigl(\log_2 b_t+\log_2 d_t\bigr)=O(L).\)

Every partial sum belongs to \([0,1]\), because its terms are nonnegative and \(\mu_tx_t\leq\mu_t\). Hence its numerator is at most its denominator and also has \(O(L)\) bits. The comparison with \(1/2\) is therefore an exact integer comparison involving \(O(L)\)-bit integers.

There are \(O(\tau)\) arithmetic operations and comparisons. Each takes at most \(O(L^2)\) bit operations using schoolbook arithmetic, establishing the claimed \(O(\tau L^2)\) bound. Reduction of fractions is unnecessary: the selected numerator and denominator already specify an exact rational output of \(O(L)\) bits.

5. Relation to the discrete formulation

The cited paper gives a welfare-optimal endpoint mechanism for finite agent lists satisfying expected unanimous fair share ([Section 5.4, Lemma 3](https://arxiv.org/html/2301.04340v2#S5.SS4)). The proof above establishes the binary-rational mass formulation directly. In particular, it avoids expanding masses into an agent list, whose length could be exponential in the input length.

Thus binary encoding of the masses does not obstruct polynomial-time exact optimization. An NP-hardness result under standard polynomial-time reductions would imply \(\mathrm{P}=\mathrm{NP}\).

⟨structured verdict parsed — rendered above⟩

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

Verification report

The prover resolves the assigned problem correctly. The algorithm returns an exact rational welfare maximizer, and its arithmetic, bit-complexity, and output-size bounds are justified for the specified \(m=2\). No major or minor issues were found.

1. Scope and input assumptions

The proof uses the support types and their masses directly. It does not confuse support size \(\tau\) with a population size or expand the masses into individual agents.

The stated rational encoding uses explicitly represented binary numerators and denominators, consistent with the task’s binary-rational input formulation. The runtime expressions involving \(m\) are explicitly restricted to \(m=2\); they do not claim an algorithm for an unspecified variable number of facility locations.

2. Feasibility

Positivity and normalization imply \(0<\mu_t\leq1\) for every support type. The calculation
\[ u_t(1/2)=1/2\geq\mu_t/2 \]
is correct. Thus \(p=1/2\) is a feasible probability for every valid input.

This includes \(\tau=1\), where normalization forces the single mass to equal \(1\).

3. Exact feasible interval

The rewritten inequality
\[ (1-x_t)+(2x_t-1)p\geq\mu_t/2 \]
is algebraically correct.

Each branch handles the coefficient’s sign correctly:

The definitions of \(p_{\min}\) and \(p_{\max}\) correctly intersect these bounds with \([0,1]\). Including \(0\) and \(1\) also handles empty collections of lower or upper bounds.

The claimed equivalence between feasibility and membership in \([p_{\min},p_{\max}]\) follows from the individual constraint equivalences. Since \(1/2\) satisfies all constraints, the endpoint ordering is valid. Locations \(0\) and \(1\) introduce no exceptional denominator cases.

4. Welfare maximization

The expression
\[ W(p)=1-M+(2M-1)p \]
follows correctly from \(M=\sum_t\mu_t x_t\) and mass normalization.

The selection rule uses the correct slope:

The rule also handles a singleton feasible interval. Every returned value is rational and feasible, and the proof establishes optimality for every valid input.

5. Exact arithmetic and bit complexity

Both displayed integer formulas for \(\ell_t\) and \(r_t\) are correct. Their denominators are strictly positive in their respective branches, so cross multiplication preserves comparison directions.

The numerator and denominator of each candidate bound have \(O(L)\) bits. Maintaining an extremum selects an existing rational rather than accumulating denominators, which justifies the endpoint-size bound.

For \(M\), the proposed unreduced representation using the product of processed denominators is valid. The logarithms of those denominators sum to \(O(L)\), so every partial denominator has \(O(L)\) bits. Every partial sum lies in \([0,1]\), making its nonnegative numerator no larger than its denominator. Intermediate products and sums therefore also have \(O(L)\) bits.

The algorithm performs \(O(\tau)\) arithmetic operations and comparisons. Schoolbook arithmetic gives the claimed \(O(\tau L^2)\) bit-operation bound. The output has \(O(L)\) bits without requiring fraction reduction.

Consequently, the stated \(O(m\tau)\) arithmetic and \(O(m\tau L^2)\) bit bounds are valid for \(m=2\).

6. Literature statement and complexity conclusion

The citation is accurate: Section 5.4 describes the discrete endpoint mechanism, and Lemma 3 states its utilitarian optimality under expected \(2\)-UFS. [Section 5.4 and Lemma 3](https://arxiv.org/html/2301.04340v2#S5.SS4)

The submitted proof establishes the rational-mass result independently, so it requires no transfer of the discrete theorem to weighted inputs.

The polynomial-time conclusion follows from the explicit algorithm and its bit bound. The conditional statement about NP-hardness implying \(\mathrm{P}=\mathrm{NP}\) is appropriately qualified.

Actionable feedback

No additional clarification or repair is required.

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