← back to the atlas

d4-conf-wine-2023-0022 (d4-conf-wine-2023-0022)

Answer: \(\mathrm{NP}\text{-complete}\)

The anchor (named result in the paper)

Theorem 1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateFor binary preferences, deciding whether an envy-free arrangement on a cycle exists is NP-hard.

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

The continuous mirror question, as graded

Given a finite type set \(T\), binary utilities \(p:T\times T\to\{0,1\}\), and rational masses \(\mu_t\ge 0\) summing to one, decide whether there is a nonnegative mass distribution \(\rho_{abcd}\) over four consecutive types in a large cycle. Require total mass one, stationarity \(\sum_d\rho_{abcd}=\sum_x\rho_{xabc}\), and type marginals \(\mu_t=\sum_{a,c}Q_{atc}\), where \(Q_{abc}=\sum_d\rho_{abcd}\). For every pair of positive-mass triples \((a,t,c)\) and \((d,u,e)\), require \(p(t,a)+p(t,c)\ge p(t,d)+p(t,e)\); for every positive-mass adjacent window \((a,t,u,e)\), require \(p(t,a)\ge p(t,e)\) and \(p(u,e)\ge p(u,a)\). This asks whether a large-cycle mass society can be envy-free except on a set of vanishing population mass.

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

A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive binary-rational masses \(\mu_t\), where \(\sum_{t\in T}\mu_t=1\). Thus \(\tau\) is the support size, not the number of possible types. Here \(m=|T|=\tau\); let \(L\) be the total input bit length.
Preferences are an explicitly given, possibly asymmetric function \(p:T\times T\to\{0,1\}\). The value \(p(t,t)\) concerns distinct individuals of type \(t\) and may be either binary value. Utility is additive over the two neighbors; envy means a strict utility increase after exchanging seats, including adjacent seats.
Define a mass arrangement to be real numbers \(\rho_{abcd}\geq0\), indexed by \(T^4\), representing frequencies of four consecutive types, with \(\sum_{a,b,c,d\in T}\rho_{abcd}=1\) and \(\sum_{d\in T}\rho_{abcd}=\sum_{x\in T}\rho_{xabc}\) for every \((a,b,c)\in T^3\).
Put \(Q_{abc}=\sum_{d\in T}\rho_{abcd}\) and require \(\sum_{a,c\in T}Q_{atc}=\mu_t\) for every \(t\in T\).
Require \(p(t,a)+p(t,c)\geq p(t,d)+p(t,e)\) whenever \(Q_{atc}>0\) and \(Q_{due}>0\), for all \(a,t,c,d,u,e\in T\), allowing repeated types and identical triples.
Also require \(p(t,a)\geq p(t,e)\) and \(p(u,e)\geq p(u,a)\) whenever \(\rho_{atue}>0\). These conditions define envy-freeness for this mass problem; equality permits indifference.

Is deciding whether such an envy-free mass arrangement exists solvable in polynomial time in \(m,\tau,L\), or is it NP-hard?

For finite societies, deciding existence of an envy-free cycle seating is NP-hard with binary preferences; with any fixed number of types it is polynomial-time solvable even for arbitrary preferences. [Source](https://arxiv.org/html/2305.09549v2).
No result settling this exact mass feasibility problem 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 stated mass feasibility problem is \(\mathrm{NP}\)-complete. In particular, it is \(\mathrm{NP}\)-hard even when all masses are dyadic rationals.

The proof below uses the specified mass constraints directly.

1. Consequences of the constraints

For an arrangement \(\rho\), retain the definition \(Q_{abc}=\sum_d\rho_{abcd}\).

Common utility lemma. For each type \(t\), there is a number \(k_t\in\{0,1,2\}\) such that every supported triple centered at \(t\) has utility \(k_t\). Moreover, every supported triple \((d,u,e)\) satisfies
\[ p(t,d)+p(t,e)\leq k_t. \]

Indeed, \(\mu_t>0\) guarantees at least one supported triple centered at \(t\). Applying the nonadjacent comparison in both directions to two such triples shows that their utilities are equal. Comparing one of them with any supported triple proves the asserted upper bound.

We will also use neighbor-incidence quantities. Set
\[ R_{uv}=\sum_c Q_{uvc}. \]
The flow equations give
\[ R_{uv}=\sum_{c,x}\rho_{xuvc}=\sum_x Q_{xuv}. \]
Consequently, both the row and column marginals of \(R\) are \(\mu\). Define
\[ H_{uv}=R_{uv}+R_{vu}. \]
Then
\[ H_{uv}=H_{vu}, \qquad \sum_v H_{uv}=2\mu_u, \qquad \sum_v p(u,v)H_{uv}=k_u\mu_u. \]
Thus \(H_{uv}\) counts the mass of neighbor incidences between the two types, counting both incidences when \(u=v\).

If the preference row of \(t\) contains a \(1\), then \(k_t\geq1\). To see this, choose \(s\) with \(p(t,s)=1\). Since \(\mu_s>0\), some supported triple has \(s\) as a neighbor. The common utility lemma then gives \(k_t\geq1\).

2. Membership in \(\mathrm{NP}\)

Guess the profile \(k\in\{0,1,2\}^{T}\).

Call a triple \((a,b,c)\) admissible if
\[ p(b,a)+p(b,c)=k_b \quad\text{and}\quad p(t,a)+p(t,c)\leq k_t \quad\text{for every }t\in T. \]

Allow \(\rho_{abcd}\) to be positive only when both \((a,b,c)\) and \((b,c,d)\) are admissible and
\[ p(b,a)\geq p(b,d), \qquad p(c,d)\geq p(c,a). \]
Set every other coordinate to zero, and impose the given nonnegativity, normalization, flow, and mass equations.

This is a rational linear feasibility problem of polynomial encoding length: it has at most \(m^4\) variables, and admissibility can be checked in polynomial time. Rational linear feasibility is decidable in time polynomial in its encoding length.

Every envy-free arrangement yields such a profile by the common utility lemma. Conversely, any solution of this linear program satisfies both kinds of envy constraints. Guessing the profile and checking its linear program therefore establishes membership in \(\mathrm{NP}\).

3. Reduction from \(\mathrm{3SAT}\)

Take a formula with variables indexed by \(i\in\{1,\ldots,n\}\) and nonempty clauses indexed by \(j\in\{1,\ldots,r\}\). Each clause has at most three literals and contains each variable at most once.

This restriction preserves \(\mathrm{NP}\)-hardness: starting with ordinary \(\mathrm{3SAT}\), remove tautological clauses and repeated literals. If no clauses remain, output a fixed feasible mass instance. Hence assume \(n,r\geq1\).

Write the literals of clause \(j\) as \(\ell_{j1},\ldots,\ell_{jq_j}\), and put \(q=\sum_j q_j\). Thus \(r\leq q\leq3r\).

For each variable introduce five types
\[ X_i,\ Y_i,\ a_i,\ b_i,\ c_i. \]
The types \(X_i,Y_i\) will monitor its positive and negative literals, respectively.

For each clause introduce types
\[ B_j,\ A_j,\ C_j \]
and one type \(P_{jk}\) for each literal occurrence. Finally introduce two types \(Z,E\).

Define the monitor of a literal by \(M(v_i)=X_i\) and \(M(\neg v_i)=Y_i\).

Masses

Choose positive dyadic numbers \(s,w\) satisfying
\[ s\leq\frac1{64n}, \qquad w\leq\frac{s}{16r}, \]
with denominators of polynomial bit length. For example, take
\[ s=2^{-\lceil\log_2(64n)\rceil}, \qquad w=s\,2^{-\lceil\log_2(16r)\rceil}. \]

Assign masses as follows:

| Types | Mass of each type |
|---|---:|
| \(X_i,Y_i\) | \(2s\) |
| \(a_i,b_i,c_i\) | \(s\) |
| \(B_j,A_j,C_j,P_{jk}\) | \(w\) |
| \(Z\) | \(3/4\) |
| \(E\) | \(1/4-7ns-(3r+q)w\) |

These masses sum to \(1\). Their positivity will also follow from the construction below.

Preferences

All entries not specified here are zero.

The rows of \(E,a_i,b_i,c_i,P_{jk}\) are identically zero.

There are \(5n+3r+q+2\) types. All masses are dyadic with polynomial bit length, and the explicit preference matrix has polynomial size.

4. Soundness: feasibility implies satisfiability

Assume the constructed instance has an envy-free mass arrangement.

The type \(Z\) is isolated and attains utility \(2\)

Since \(Z\) approves itself, \(k_Z\geq1\).

If \(k_Z=1\), then \(H_{ZZ}=\mu_Z\), so its neighbor incidences with other types total
\[ \sum_{u\neq Z}H_{Zu}=2\mu_Z-H_{ZZ}=\mu_Z=\frac34. \]
By symmetry and the degree bounds of the other types, this total is at most
\[ \sum_{u\neq Z}2\mu_u=\frac12, \]
a contradiction.

Therefore \(k_Z=2\). Every supported triple centered at \(Z\) is consequently \(ZZZ\), and
\[ H_{Zu}=0\quad(u\neq Z), \qquad Q_{ZZZ}=\mu_Z>0. \]

Every \(C_j\) approves \(Z\). Comparing its own seat with \(ZZZ\) forces \(k_{C_j}=2\).

Each clause forces a literal monitor to attain utility \(2\)

Fix a clause \(j\). Because the rows of \(B_j,A_j\) are nonzero,
\[ H_{B_jA_j}=k_{B_j}w\geq w, \qquad H_{A_jC_j}=k_{A_j}w\geq w. \]
The total neighbor incidence available at \(A_j\) is \(2w\). Hence both inequalities are equalities:
\[ k_{B_j}=k_{A_j}=1, \qquad H_{A_jB_j}=H_{A_jC_j}=w. \]

Since \(B_j\) approves only \(A_j\) and has utility \(1\), the common utility lemma forbids every supported neighborhood having two neighbors of type \(A_j\).

In particular, every supported triple centered at \(C_j\) has at most one \(A_j\) neighbor. But
\[ H_{C_jA_j}=w=\mu_{C_j}. \]
Averaging therefore forces every such triple to have exactly one \(A_j\) neighbor.

Its other neighbor must be some \(P_{jk}\): \(C_j\) attains utility \(2\), and adjacency to \(Z\) is impossible because \(Z\) is isolated.

The monitor \(M(\ell_{jk})\) approves both \(A_j\) and \(P_{jk}\). Comparing against this supported neighborhood forces
\[ k_{M(\ell_{jk})}=2. \]
Thus every clause has at least one literal whose monitor attains utility \(2\).

The two monitors of a variable cannot both attain utility \(2\)

Fix \(i\). Let \(S_i\) be the union of the types approved by \(X_i\) and \(Y_i\).

It contains \(a_i,b_i,c_i\). Each clause contributes at most one \(A_j\) and one occurrence type \(P_{jk}\), because that clause contains variable \(i\) at most once. Hence
\[ \mu(S_i)\leq3s+2rw. \]

If both monitors attained utility \(2\), all their neighbor incidences would be with \(S_i\), giving
\[ 8s =\sum_{v\in S_i}(H_{X_iv}+H_{Y_iv}) \leq\sum_{v\in S_i}2\mu_v \leq6s+4rw \leq\frac{25s}{4} <8s. \]
This contradiction proves that they cannot both attain utility \(2\).

Set variable \(i\) to true exactly when \(k_{X_i}=2\). A positive literal with monitor utility \(2\) is then true. A negative literal with monitor utility \(2\) has \(k_{Y_i}=2\), which forces \(k_{X_i}\neq2\), so it too is true.

Every clause has such a literal. The formula is satisfiable.

5. Completeness: satisfiability implies feasibility

Assume a satisfying assignment is given.

We construct \(\rho\) by adding frequencies from periodic words. A word \(W\) of length \(h\), with a per-position mass \(\gamma\), contributes \(\gamma\) to the quadruple beginning at each of its \(h\) cyclic positions.

Such contributions automatically satisfy the flow equations: cyclic shifting pairs every outgoing occurrence of a triple with an incoming occurrence.

Words and their masses

For a true variable \(i\), use the words
\[ (X_i,a_i,X_i,b_i), \qquad (Y_i,c_i,Y_i,E,E), \]
each with per-position mass \(s\).

For a false variable, use
\[ (Y_i,c_i,Y_i,b_i), \qquad (X_i,a_i,X_i,E,E), \]
again with per-position mass \(s\).

Thus each variable contributes the required masses of its five types and contributes \(2s\) to \(E\).

In each clause \(j\), select one true literal \(\ell_{jk}\). Use
\[ (B_j,A_j,C_j,P_{jk}) \]
with per-position mass \(w\).

For each unselected occurrence \(P_{jh}\), use
\[ (P_{jh},E,E) \]
with per-position mass \(w\). This supplies every occurrence type with its required mass and contributes \(2(q-r)w\) to \(E\).

Finally use the homogeneous word \(Z\) with mass \(3/4\), and the homogeneous word \(E\) with mass
\[ \eta=\frac14-9ns-(r+3q)w. \]
Since \(q\leq3r\),
\[ 9ns+(r+3q)w \leq\frac9{64}+10rw \leq\frac9{64}+\frac{10}{1024} <\frac14. \]
Thus \(\eta>0\). In particular, the input mass of \(E\) is positive.

The resulting mass of \(E\) is exactly
\[ 2ns+2(q-r)w+\eta =\frac14-7ns-(3r+q)w. \]
All prescribed masses and normalization are therefore satisfied.

Nonadjacent envy constraints

Assign the intended utilities as follows:

Every type attains its intended utility in the words above. It remains to check that no supported neighborhood exceeds that utility when evaluated by the type.

For a utility-\(2\) type, this is automatic because preferences are binary. For a zero-row type, it is also automatic.

For \(B_j\), its sole approved type \(A_j\) occurs only once in the clause word. No supported neighborhood has two \(A_j\) neighbors. The same argument applies to \(A_j\), whose sole approved type is \(C_j\).

Consider a utility-\(1\) monitor of variable \(i\).

Thus every supported neighborhood has score at most the type’s attained utility. This proves all nonadjacent envy inequalities.

Adjacent envy constraints

An endpoint whose utility is \(2\) automatically satisfies its adjacent-swap inequality: its outer neighbor is approved, and the proposed new outer neighbor has preference value at most \(1\). A zero-row endpoint also automatically satisfies its inequality.

Only the utility-\(1\) endpoints need checking.

A utility-\(1\) monitor appears in a word
\[ (M,d,M,E,E), \]
where it approves \(d\) and approves neither \(M\) nor \(E\).

When adjacent to \(d\), the old and new outer neighbors are \(E\) and \(M\), both valued \(0\). When adjacent to \(E\), its old outer neighbor is \(d\), valued \(1\), and its new outer neighbor is \(E\), valued \(0\). Both inequalities hold.

In the clause word \(B_j,A_j,C_j,P_{jk}\), the remaining checks are:

| Endpoint and adjacent type | Old outer neighbor’s value | New outer neighbor’s value |
|---|---:|---:|
| \(B_j\) adjacent to \(A_j\) | \(p(B_j,P_{jk})=0\) | \(p(B_j,C_j)=0\) |
| \(B_j\) adjacent to \(P_{jk}\) | \(p(B_j,A_j)=1\) | \(p(B_j,C_j)=0\) |
| \(A_j\) adjacent to \(B_j\) | \(p(A_j,C_j)=1\) | \(p(A_j,P_{jk})=0\) |
| \(A_j\) adjacent to \(C_j\) | \(p(A_j,B_j)=0\) | \(p(A_j,P_{jk})=0\) |

These exhaust the utility-\(1\) endpoints. Therefore every required adjacent-swap inequality holds.

The constructed \(\rho\) is an envy-free mass arrangement.

6. Conclusion

The reduction is polynomial, uses positive dyadic masses, and proves equivalence between satisfiability and the exact mass feasibility conditions in the question. Together with membership in \(\mathrm{NP}\), this establishes \(\mathrm{NP}\)-completeness.

⟨structured verdict parsed — rendered above⟩

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

The prover’s claim is proved. The argument establishes NP-completeness for the exact mass feasibility problem, including its adjacent-swap constraints. I found no major or minor mathematical gaps.

1. Common utilities and neighbor incidences

The common utility lemma is correct. Positive mass guarantees a supported triple centered at each type. Applying the stipulated comparison in both directions between two triples centered at the same type forces equal utilities. Comparing either with an arbitrary supported triple gives the claimed upper bound. Binary preferences imply that the common utility belongs to \(\{0,1,2\}\).

The identities for \(R\) follow correctly from the flow equations:
\[ R_{uv}=\sum_c Q_{uvc}=\sum_x Q_{xuv}. \]
Its row and column marginals are consequently \(\mu\). Thus the stated symmetry, degree identity, and utility identity for \(H\) are all correct:
\[ \sum_v H_{uv}=2\mu_u, \qquad \sum_v p(u,v)H_{uv}=k_u\mu_u. \]
The definition also correctly counts two incidences for a same-type neighbor pair.

The assertion that a nonzero preference row forces \(k_t\geq1\) is justified. Positive mass of an approved type gives positive neighbor incidence involving that type, hence a supported neighborhood whose evaluation by \(t\) is at least one.

2. Membership in NP

The guessed profile has polynomial length. For each profile, the admissibility tests and the resulting rational linear program have polynomial encoding length: there are at most \(m^4\) variables, and every triple requires only \(m\) preference comparisons.

Both directions of the characterization hold:

The invoked polynomial-time theorem for rational linear feasibility applies to the explicitly described rational system. Guessing the profile and running that algorithm establishes NP membership.

3. Reduction and input validity

The preprocessing of ordinary 3SAT preserves satisfiability. Removing tautological clauses and duplicate literals yields nonempty clauses of size at most three, with each variable appearing at most once per clause. The case in which no clauses remain is correctly treated as satisfiable.

The number of types and the explicit preference matrix have polynomial size. The chosen \(s\) and \(w\) are positive dyadic rationals with polynomial bit length.

The mass accounting is correct:

Positivity of \(E\) is established later by the positive residual mass \(\eta\). This is sufficient because that calculation depends only on \(n,r,q,s,w\), not on satisfiability.

4. Soundness

Isolation of \(Z\). The exclusion of \(k_Z=1\) is valid. It would require cross-type neighbor incidence \(3/4\), while all other types together have degree capacity \(1/2\). Therefore \(k_Z=2\), all its supported central neighborhoods are \(ZZZ\), and it has no cross-type neighbor incidence.

Because every \(C_j\) approves \(Z\), comparison with the supported neighborhood \(ZZZ\) forces \(k_{C_j}=2\).

Clause forcing. The incidence lower bounds involving \(B_j,A_j,C_j\) are correct. The two bounds exhaust the degree capacity \(2w\) of \(A_j\), forcing
\[ k_{B_j}=k_{A_j}=1, \qquad H_{A_jB_j}=H_{A_jC_j}=w. \]

The preference row of \(B_j\), together with \(k_{B_j}=1\), forbids two \(A_j\) neighbors in any supported triple. Since \(C_j\) has total mass \(w\) and incidence \(w\) with \(A_j\), the averaging argument correctly forces exactly one \(A_j\) neighbor in every supported triple centered at \(C_j\).

Its remaining neighbor must be an occurrence type belonging to that clause: both neighbors must be approved by \(C_j\), and \(Z\) is isolated. The monitor of this occurrence approves both neighbors, so its utility is forced to two. Consequently every clause supplies such a monitor.

Variable consistency. The bound
\[ \mu(S_i)\leq3s+2rw \]
correctly uses the restriction that a variable appears at most once in each clause. The monitor types themselves do not belong to \(S_i\).

If both monitors had utility two, their combined required incidence would be \(8s\). Symmetry and the degree capacities of the resource types give the stated upper bound. Its numerical calculation is correct:
\[ 6s+4rw\leq6s+\frac{s}{4}=\frac{25s}{4}<8s. \]

Thus both monitors cannot attain utility two. The proposed truth assignment then makes every clause’s forced literal true. Soundness follows.

5. Completeness

Flow and masses. Contributions from cyclic words satisfy flow, including words with repeated types and the homogeneous words. Counting positions gives precisely the prescribed variable, clause, occurrence, and \(Z\) masses.

The residual calculation for \(E\) is correct:
\[ 2ns+2(q-r)w+\eta =\frac14-7ns-(3r+q)w. \]
The positivity estimate is also valid:
\[ 9ns+(r+3q)w \leq\frac9{64}+\frac{10}{1024}<\frac14. \]
Thus all masses are positive and normalization holds.

Attained utilities. Inspection of the cyclic neighborhoods confirms every listed intended utility. In particular, the four-position variable word gives its monitor utility two, while both monitor positions in the five-position word have utility one. The clause word gives utilities one, one, and two to \(B_j,A_j,C_j\), respectively.

Triple-comparison inequalities. Utility-two and zero-row types are handled correctly. No constructed neighborhood contains two copies of the sole approved type of \(B_j\) or \(A_j\).

The case analysis for a utility-one monitor is exhaustive. In a clause word, the only neighborhood potentially containing two approved types is the pair \(A_j,P_{jk}\). Since the selected occurrence is true, its monitor is the utility-two monitor. The utility-one monitor cannot approve that selected occurrence. The restriction on repeated variables in a clause ensures this conclusion also covers clauses containing other literals.

The occurrence words, variable words, and homogeneous words satisfy the remaining bounds. Therefore every supported neighborhood is evaluated at no more than the evaluating type’s attained utility.

Adjacent-swap inequalities. A utility-two endpoint approves its old outer neighbor, so its inequality follows from binary preferences. Zero-row endpoints satisfy their inequalities directly.

For the utility-one monitor’s five-position word, the stated old and new outer-neighbor values are correct for both monitor positions. The four table entries for \(B_j\) and \(A_j\) also correctly describe their cyclic adjacencies. These cases exhaust all utility-one endpoints.

The construction therefore satisfies every required adjacent-swap inequality.

6. Final assessment

The reduction is polynomial and establishes equivalence with satisfiability using positive dyadic masses. Together with the valid NP-membership argument, it proves the claimed NP-completeness. No repair or additional clarification 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.