← back to the atlas

d4-conf-ijcai-2017-0348 (d4-conf-ijcai-2017-0348)

Answer: Polynomial-time solvable; the exact output problem belongs to \(\mathrm{FP}\).

The anchor (named result in the paper)

Corollary 10 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateFor finite set Λ ⊂IRn, let λi ∈Λ be the ith element of Λ where i ∈I = {1, . . . , |Λ|}. Consider any u ∈IRn. Then, u is in SI(Λ) if and only if there exist non- negative reals ri for each i ∈I such that u = P i∈I riλi and for all i ∈I, u · λi ≥1.

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

The continuous mirror question, as graded

Given a finite rational catalogue \(A\subseteq\mathbb{Q}^d\) and a rational-mass distribution \(\mu\) over consistent comparison-profile types \(t\), each described by \(\Lambda_t\subseteq\mathbb{Q}^d\), compute for every \(a\in A\) the mass \(M(a)=\sum_{t:\,a\in P_t(A)}\mu_t\), and return a maximizer, where \(P_t(A)=\{a\in A:\exists u\in SI(\Lambda_t),\ u\cdot a\ge u\cdot b\ \forall b\in A\}\) and \(SI(\Lambda_t)=\operatorname{cone}(\Lambda_t)\cap\{u:u\cdot\lambda\ge1\ \forall\lambda\in\Lambda_t\}\).

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

Let \(d\ge1\) and let \(A\subseteq\mathbb Q^d\) be an explicitly listed nonempty catalogue, with \(m=|A|\). Coordinates may have either sign.
A society is given by its support: a list of \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) is the support size, not the number of possible types.
Each type explicitly lists a finite set \(\Lambda_t\subseteq\mathbb Q^d\) of strict comparison differences: \(\lambda=x-y\) represents preferring \(x\) to \(y\). Consistency means that some \(w\in\mathbb R^d\) satisfies \(w\cdot\lambda>0\) for every \(\lambda\in\Lambda_t\). Empty comparison sets are allowed.
Define \(SI(\Lambda_t)=\operatorname{cone}(\Lambda_t)\cap\{u\in\mathbb R^d:u\cdot\lambda\ge1\text{ for all }\lambda\in\Lambda_t\}\), using the usual nonnegative generated cone and \(\operatorname{cone}(\varnothing)=\{0\}\). Utility vectors have no additional sign or normalization restriction.
Define \(P_t(A)=\{a\in A:\exists u\in SI(\Lambda_t),\ u\cdot a\ge u\cdot b\text{ for every }b\in A\}\); utility ties count as optimal.
The problem is to compute exactly every \(M(a)=\sum_{t:a\in P_t(A)}\mu_t\) and return any maximizer. Let \(K=\sum_t|\Lambda_t|\) and let \(L\) be the total binary input length; state running times in \(m,\tau,d,K,L\).

Is this exact mass-aggregation problem solvable in polynomial time, or is it NP-hard?

For a single finite comparison profile, the known characterization is \(u\in SI(\Lambda)\) exactly when \(u=\sum_{\lambda\in\Lambda}r_\lambda\lambda\), \(r_\lambda\ge0\), and \(u\cdot\lambda\ge1\) for every \(\lambda\in\Lambda\). [Montazery and Wilson, 2017](https://www.ijcai.org/proceedings/2017/0168.pdf).
The same characterization and the single-profile possible-optimality notion appear in the [2021 extended treatment](https://cora.ucc.ie/bitstreams/c21e04e3-c9fd-4bdf-bbf3-bb903ed2c572/download); no result settling this exact distribution-over-types aggregation problem was located.

Modeling choices made when packaging the task

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

Result

The exact mass-aggregation problem is deterministically polynomial-time solvable, with both the dimension and support size included in the input. The proof is a reduction to at most \(m\tau\) rational linear feasibility problems, followed by exact rational arithmetic.

1. A linear program for each membership test

Write \(k_t=|\Lambda_t|\), and enumerate \(\Lambda_t=\{\lambda_{t,1},\ldots,\lambda_{t,k_t}\}\).

Fix a type \(t\) and an alternative \(a\in A\). Introduce unrestricted real variables \(u_1,\ldots,u_d\) and nonnegative real variables \(r_1,\ldots,r_{k_t}\). Consider the following feasibility system:

Every coefficient is rational and known from the input. In particular, the last constraints are linear because \(a\) and \(b\) are fixed vectors.

Claim. This system is feasible if and only if \(a\in P_t(A)\).

Proof. Suppose the system is feasible. Constraints 1 and 2 imply \(u\in\operatorname{cone}(\Lambda_t)\). Constraint 3 gives all the inequalities required for \(u\in SI(\Lambda_t)\). Constraint 4 gives \(u\cdot a\ge u\cdot b\) for every other catalogue alternative; the inequality for \(b=a\) holds automatically. Thus \(u\) witnesses \(a\in P_t(A)\).

Conversely, suppose \(a\in P_t(A)\), and choose its witnessing vector \(u\in SI(\Lambda_t)\). Cone membership supplies coefficients \(r_i\ge 0\) satisfying constraint 2. The definition of \(SI(\Lambda_t)\) supplies constraint 3, and the witnessing optimality inequalities supply constraint 4. Hence the system is feasible. \(\square\)

The cone representation used here is also the characterization in Corollary 10 of [Montazery and Wilson (2017)](https://www.ijcai.org/proceedings/2017/0168.pdf). Under the task’s stated definition of \(SI\), however, the equivalence above follows directly from the definition of a finitely generated cone.

2. Boundary cases and hypotheses

If \(\Lambda_t=\varnothing\), constraint 2 becomes \(u_j=0\) for every coordinate. Constraints 1 and 3 disappear, and constraint 4 holds with equality. Consequently, \(P_t(A)=A\), exactly as required by \(\operatorname{cone}(\varnothing)=\{0\}\).

Negative coordinates cause no difficulty: the variables \(u_j\) are unrestricted, and rational linear feasibility allows coefficients of either sign. Weak inequalities in constraint 4 include utility ties exactly.

The algorithm works whether consistency is promised or not. If a type is inconsistent, constraint 3 cannot hold: any vector satisfying it would itself satisfy \(u\cdot\lambda>0\) for every listed comparison. Thus its possible-optimality set is empty under the stated definition.

3. Exact aggregation and correctness

For every pair \((t,a)\), solve the feasibility system and record \(I_{t,a}=1\) if it is feasible and \(I_{t,a}=0\) otherwise. Then compute \(M(a)=\sum_{t=1}^{\tau}I_{t,a}\mu_t\) exactly.

The membership claim proves that each indicator is correct. Therefore every computed mass equals the specified \(M(a)\). Since \(A\) is finite and nonempty, comparing these exact masses and returning any alternative with largest mass produces a maximizer.

Different membership tests may use different witnessing utility vectors. This is precisely what the separate existential quantifier in the definition of each \(P_t(A)\) permits. No joint choice of utility vectors across alternatives is required.

4. Polynomial bit complexity

Use the standard binary encoding of rational numbers by integer numerators and positive integer denominators.

The relevant standard theorem is: feasibility of a finite system of rational linear equalities and weak inequalities over real variables is decidable deterministically in time polynomial in its binary encoding length. This theorem permits unrestricted variables and unbounded feasible regions; neither boundedness nor strict feasibility is required.

For type \(t\), our system has:

Replacing each equality by two inequalities gives \(h_t=2d+2k_t+m-1\) inequalities. All coefficients are input coordinates, their negatives, differences of two input coordinates, or constants. Subtracting two input rationals produces a rational with \(O(L+1)\) bits. Hence a dense encoding of this system has length \(B_t=O(n_t h_t(L+1))\).

Let \(q(n,h,B)\) be a fixed nondecreasing polynomial bounding rational linear feasibility, enlarged to include construction of the system. The total feasibility work is bounded by

\(O\!\left(m\sum_{t=1}^{\tau}q\!\left(d+k_t,\;2d+2k_t+m-1,\;(d+k_t)(2d+2k_t+m-1)(L+1)\right)\right)\).

Since every \(k_t\le K\), this is \(O\!\left(m\tau\,\operatorname{poly}(d+K+m,L)\right)\).

Exact aggregation also has polynomial bit complexity. Write \(\mu_t=p_t/q_t\), with positive integer denominators, and set \(D=\prod_{t=1}^{\tau}q_t\). The binary length of \(D\) is \(O(L)\), because the sum of the input denominator lengths is at most \(L\). For each alternative define the integer

\(N_a=\sum_{t=1}^{\tau}I_{t,a}p_t(D/q_t)\).

Then \(M(a)=N_a/D\). Positivity and \(\sum_t\mu_t=1\) imply \(0\le N_a\le D\), so every output numerator also has \(O(L)\) bits. All these numerators can be computed with elementary integer arithmetic in \(O(m\tau(L+1)^2)\) bit operations. Comparing numerators suffices to find a maximizer, since their denominators are identical.

Thus the complete running time is

\(O\!\left(m\tau\,\operatorname{poly}(d+K+m,L)+m\tau(L+1)^2\right)\),

which is polynomial in the explicitly listed input. The explicit support is essential to this bound: the algorithm processes its \(\tau\) listed types directly.

Conclusion

Computing every exact mass and returning a maximizer belongs to \(\mathrm{FP}\). An NP-hardness result under standard polynomial-time reductions would therefore imply \(\mathrm{P}=\mathrm{NP}\).

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the assigned problem correctly. The reduction preserves the definition of possible optimality, the linear feasibility theorem applies, and the exact aggregation has polynomial bit complexity. No major or minor mathematical issues were found.

Step-by-step verification

1. Membership formulation

For fixed \(t\) and \(a\), all four groups of constraints are linear in the introduced variables. The catalogue vectors and comparison differences are fixed rational input data; no product of decision variables occurs.

Both directions of the claimed equivalence are justified:

Omitting the comparison with \(b=a\) is valid because that inequality is identically satisfied. The same \(u\) must satisfy all catalogue comparisons within a membership test, as required.

The cited Corollary 10 does state the finite-profile characterization attributed to it. [Montazery and Wilson (2017), Corollary 10](https://www.ijcai.org/proceedings/2017/0168.pdf). The argument also correctly observes that, under the task’s explicit definition, this characterization follows directly from cone membership; the proof therefore does not depend on extending the paper’s assumptions.

Finding: Correct.

2. Boundary cases and domain restrictions

The empty-profile treatment is exact: the empty sum in constraint 2 forces \(u=0\), while the remaining optimality inequalities hold with equality. Thus every catalogue alternative is possible-optimal.

Unrestricted utility variables correctly implement the absence of sign or normalization restrictions. Negative input coordinates impose no additional difficulty, and weak optimality inequalities correctly include ties.

The assertion about inconsistent types is also correct. Any vector satisfying all inequalities \(u\cdot\lambda\ge1\) would witness strict consistency. Consequently, an inconsistent profile has no feasible membership system and contributes no mass.

For \(m=1\), the optimality constraints disappear, exactly as the definition requires. The variable and constraint counts remain valid when \(k_t=0\).

Finding: Correct; no missing boundary case affects the argument.

3. Quantifiers and aggregation

The algorithm performs a separate existential feasibility test for every pair \((t,a)\). This matches the definition of \(P_t(A)\), which permits different witnesses for different alternatives.

The proved membership equivalence establishes every indicator \(I_{t,a}\). Summing the corresponding masses therefore computes precisely the requested \(M(a)\). Comparing all computed masses returns a maximizer because the catalogue is finite and nonempty.

Finding: Correct.

4. Applicability of polynomial-time linear feasibility

The prover states the relevant theorem precisely enough: rational linear equalities and weak inequalities over real variables admit deterministic polynomial-time feasibility decisions in binary encoding length.

Its hypotheses are satisfied:

The proof needs exact feasibility decisions, and the stated theorem supplies them. No assumption of numerical tolerance, boundedness, or strict feasibility is introduced.

Finding: Correct application of a standard theorem.

5. System sizes and coefficient lengths

The counts are correct:

\[ n_t=d+k_t,\qquad h_t=2d+2k_t+m-1. \]

There are \(k_t\) nonnegativity inequalities, \(k_t\) profile inequalities, and \(m-1\) catalogue inequalities; replacing the \(d\) equalities adds \(2d\) inequalities.

Differences of two input rationals have \(O(L+1)\) binary length. The stated dense encoding bound

\[ B_t=O\!\left((d+k_t)(2d+2k_t+m-1)(L+1)\right) \]

therefore suffices, including right-hand sides. The polynomial bound accommodates system construction and all \(m\tau\) feasibility calls. Using \(k_t\le K\) gives the claimed aggregate polynomial bound.

Finding: Correct.

6. Exact rational arithmetic

The common denominator \(D=\prod_t q_t\) has \(O(L)\) bits because its logarithm is bounded by the sum of the input denominator lengths.

Every quotient \(D/q_t\) is an integer, and the formula for \(N_a\) exactly represents the mass. Positivity and normalization justify

\[ 0\le N_a\le D. \]

They also bound intermediate partial sums by \(D\). Thus the arithmetic involves integers of \(O(L+1)\) bits. Elementary multiplication and division support the stated \(O(m\tau(L+1)^2)\) bound, including denominator construction and aggregation. Comparing numerators with their shared positive denominator correctly orders the masses.

Finding: Correct.

7. Final complexity conclusion

The algorithm computes all requested outputs with polynomial running time and polynomial output length under the explicitly listed input representation. The conclusion that the function problem belongs to \(\mathrm{FP}\) follows.

The conditional statement about NP-hardness under standard polynomial-time reductions is consistent with this conclusion.

Required clarification or repair: None.

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