← back to the atlas

d4-conf-aaai-2008-0190 (d4-conf-aaai-2008-0190)

Answer: The decision problem is \(\mathrm{NP}\)-hard, even for \(\tau=1\). The stated stopping condition always certifies global optimality.

The anchor (named result in the paper)

Proposition 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateLet x1, ..., xk be the ordered sequence of k- best solutions generated during Step 2 with function uw, if uw(xk) ≤U −fw(x∗) with x∗= Argmini=1,...,kfw(xi) then x∗is optimal for fw, i.e. fw(x∗) = minx∈X fw(x).

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

The continuous mirror question, as graded

Given a finite product domain \(X\) and a finite-support distribution \(\mu\) over complete GAI utility types \(\theta\), with rational masses \(\mu_\theta\), utilities \(u_\theta\), positive weights \(w_\theta\), and benchmarks \(r_\theta>\max_{x\in X}u_\theta(x)\), find an alternative minimizing \(F_\mu(x)=\operatorname*{ess\,sup}_{\theta\sim\mu} w_\theta(r_\theta-u_\theta(x))\). Let \(A_\mu(x)=\int w_\theta u_\theta(x)\,d\mu(\theta)\) and \(B_\mu=\int w_\theta r_\theta\,d\mu(\theta)\). If \(x_1,\ldots,x_k\) are ranked by decreasing \(A_\mu\) and \(x^*\) minimizes \(F_\mu\) among them, does \(A_\mu(x_k)\le B_\mu-F_\mu(x^*)\) certify that \(x^*\) globally minimizes \(F_\mu\)?

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

Let \(X=\prod_{j=1}^{m}X_j\), with each attribute domain explicitly listed, finite, and nonempty. Each complete GAI utility type specifies rational factor tables \(u_\theta(x)=\sum_{a=1}^{s_\theta}u_{\theta,a}(x_{Z_{\theta,a}})\), whose scopes cover all attributes; table entries may have either sign, and different types may have different scopes.
A society is given by its support: the list of the \(\tau\) types with positive binary-rational masses \(\mu_\theta\), summing to \(1\). Here \(\tau\) is the support size, not the number of possible types. Each type also specifies rational \(w_\theta>0\) and \(r_\theta>\max_{x\in X}u_\theta(x)\).
Define \(F_\mu(x)=\operatorname*{ess\,sup}_{\theta\sim\mu}w_\theta(r_\theta-u_\theta(x))\), \(A_\mu(x)=\sum_\theta\mu_\theta w_\theta u_\theta(x)\), and \(B_\mu=\sum_\theta\mu_\theta w_\theta r_\theta\). Alternatives are deterministic elements of \(X\).
For the associated decision problem, a rational threshold \(q\) is supplied. For the stopping question, \(x_1,\ldots,x_k\) are the first \(k\) distinct alternatives in a ranking of all of \(X\) by nonincreasing \(A_\mu\), with arbitrary tie-breaking, and \(x^*\in\operatorname*{arg\,min}_{1\le i\le k}F_\mu(x_i)\).
State running times in \(m\), \(\tau\), the total input bit length \(L\), and, when relevant, \(k\).

Is deciding whether \(\min_{x\in X}F_\mu(x)\le q\) in \(\mathrm{P}\), or is it NP-hard?
Does \(A_\mu(x_k)\le B_\mu-F_\mu(x^*)\) always certify global optimality of \(x^*\), or is there an admissible counterexample?

For finite agent lists, the analogous stopping implication is established; it is a correctness certificate, without a polynomial bound on the number of alternatives enumerated. General GAI weighted Tchebycheff optimization is also shown NP-hard, using benchmarks equal to utility upper bounds. [Source](https://cdn.aaai.org/AAAI/2008/AAAI08-164.pdf)
No result explicitly treating this finite-support distribution formulation was located in the search.

Modeling choices made when packaging the task

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

1. Conclusions and finite-support identity

The decision problem is \(\mathrm{NP}\)-hard, even when \(\tau=1\), every attribute is Boolean, and every factor involves at most three attributes. On the promised admissible inputs, yes-instances have polynomially verifiable certificates.

The stopping condition always certifies global optimality. There is no admissible counterexample.

Since every listed type has positive mass and the support is finite, define \(d_\theta(x)=w_\theta(r_\theta-u_\theta(x))\). Then
\[ F_\mu(x)=\max_{1\leq\theta\leq\tau}d_\theta(x). \]
The strict benchmark assumption ensures \(d_\theta(x)>0\), although the stopping proof below does not require this positivity.

2. Hardness with a strict benchmark

We give a polynomial-time reduction from \(\mathrm{3SAT}\), the \(\mathrm{NP}\)-complete satisfiability problem for conjunctions of clauses containing at most three literals.

Let the formula have variables \(z_1,\ldots,z_m\) and clauses \(C_1,\ldots,C_h\). Set \(X_j=\{0,1\}\), interpreting alternatives as truth assignments.

Use one supported type, with \(\mu_1=w_1=1\). For each clause \(C_a\), let \(Z_a\) contain its variables and explicitly list the factor table
\[ u_{1,a}(x_{Z_a})= \begin{cases} 0,&\text{if }C_a\text{ is satisfied},\\ -1,&\text{if }C_a\text{ is violated}. \end{cases} \]
Each table has at most eight entries. Add a zero unary factor for every attribute, ensuring that the scopes cover all attributes.

Write \(v(x)\) for the number of violated clauses. The resulting utility is \(u_1(x)=-v(x)\). Choose \(r_1=1\) and \(q=1\). These choices are admissible because
\[ \max_{x\in X}u_1(x)\leq 0<1=r_1. \]
Furthermore,
\[ F_\mu(x)=r_1-u_1(x)=1+v(x). \]
Consequently, \(\min_xF_\mu(x)\leq1\) holds exactly when some assignment violates no clauses, which is exactly satisfiability of the original formula.

The construction has \(h+m\) factors and bit length \(O((h+m)\log(m+1))\) under ordinary indexed encodings. Thus it is a polynomial-time reduction whose outputs satisfy every premise, including the strict benchmark inequality.

Therefore the decision problem is \(\mathrm{NP}\)-hard. A polynomial-time algorithm in \(m,\tau,L\) would imply \(\mathrm{P}=\mathrm{NP}\).

For verification, an alternative can be specified by its coordinate indices. Evaluating its selected table entries and comparing the resulting rational \(F_\mu(x)\) with \(q\) takes polynomial time, as quantified below. Thus feasibility has polynomially verifiable certificates. This verification uses the stated admissibility promise; it does not attempt to verify \(r_\theta>\max_xu_\theta(x)\) for arbitrary malformed inputs.

3. Proof of the stopping certificate

Let \(1\leq k\leq|X|\), and assume the supplied alternatives are indeed the first \(k\) distinct alternatives in a ranking by nonincreasing \(A_\mu\).

For every alternative \(y\), the definitions give
\[ B_\mu-A_\mu(y) =\sum_{\theta=1}^{\tau}\mu_\theta w_\theta(r_\theta-u_\theta(y)) =\sum_{\theta=1}^{\tau}\mu_\theta d_\theta(y). \]
Each \(d_\theta(y)\leq F_\mu(y)\). Multiplying these inequalities by the positive masses and summing, using \(\sum_\theta\mu_\theta=1\), yields
\[ B_\mu-A_\mu(y)\leq F_\mu(y). \]

Now assume the stopping condition
\[ A_\mu(x_k)\leq B_\mu-F_\mu(x^*) \]
holds. For every unenumerated alternative \(y\), the ranking property gives \(A_\mu(y)\leq A_\mu(x_k)\). Hence
\[ F_\mu(y) \geq B_\mu-A_\mu(y) \geq B_\mu-A_\mu(x_k) \geq F_\mu(x^*). \]
For every enumerated alternative \(x_i\), the choice of \(x^*\) gives \(F_\mu(x_i)\geq F_\mu(x^*)\). These two cases cover all of \(X\), proving global optimality.

Equality throughout is harmless, so arbitrary tie-breaking does not invalidate the certificate. This proves the finite-support formulation directly, extending the average-versus-maximum argument in the cited [Gonzales–Perny–Queiroz paper](https://cdn.aaai.org/AAAI/2008/AAAI08-164.pdf).

4. Running times

Let \(N=|X|=\prod_{j=1}^{m}|X_j|\). The following conservative bounds count bit operations.

Exact arithmetic remains polynomial in \(L\). To see this explicitly, let \(D\) be the product of all positive denominators appearing in the input. Its bit length is \(O(L)\). Every input rational can be represented as an integer divided by \(D\). Utilities then have denominator \(D\), weighted losses denominator \(D^2\), and \(A_\mu,B_\mu\) denominator \(D^3\). All corresponding integers have \(O(L)\) bits: their numerators arise from sums and products of input numbers, with at most polynomially many summands.

Using schoolbook integer arithmetic, preprocessing costs \(O(L^3)\). A conservative per-alternative evaluation bound is
\[ T=O((m+\tau+L)L^2). \]
It includes factor lookup, utility evaluation, aggregation, and rational comparison. Therefore:

Because domains are explicitly listed, \(N\leq(L+1)^m\), giving corresponding bounds purely in \(m,\tau,L\). The prefix-checking bound assumes the ranking property; evaluating the prefix alone does not verify that no omitted alternative has larger \(A_\mu\).

5. The certificate can require exponentially many alternatives

An explicit admissible example shows why the certificate supplies no polynomial bound on \(k\).

Take even \(m=2t\geq2\), Boolean attributes, and two types with \(\mu_1=\mu_2=1/2\) and \(w_1=w_2=1\). Define unary-factor utilities
\[ u_1(x)=\sum_{j=1}^{m}x_j,\qquad u_2(x)=-\sum_{j=1}^{m}x_j, \]
and benchmarks \(r_1=m+1,\ r_2=1\). They are strictly above the respective maxima \(m\) and \(0\).

Writing \(H(x)=\sum_jx_j\), direct calculation gives
\[ A_\mu(x)=0,\qquad B_\mu=t+1,\qquad F_\mu(x)=\max\{2t+1-H(x),\,1+H(x)\} =t+1+|H(x)-t|. \]
Thus precisely the alternatives with \(H(x)=t\) are optimal. Since all alternatives tie under \(A_\mu\), an allowed ranking places every nonoptimal alternative first. Before the first optimum appears, \(F_\mu(x^*)>B_\mu\), so the stopping inequality fails. It first holds at
\[ k=2^m-\binom{m}{t}+1. \]
Moreover, \(\binom{m}{t}\leq2^{m-1}\): Pascal’s identity expresses it as the sum of the two equal middle coefficients in row \(m-1\), whose entire sum is \(2^{m-1}\). Hence \(k\geq2^{m-1}+1\).

This family has input length \(O(m\log(m+1))\). Consequently, an admissible tie-breaking order can require exponentially many alternatives before the valid certificate fires.

⟨structured verdict parsed — rendered above⟩

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

Verdict: proved. The output resolves both questions: the decision problem is NP-hard on admissible inputs, and the stated stopping condition always certifies global optimality. No major or minor mathematical issues were found.

1. Finite-support identity

The replacement of the essential supremum by a maximum is justified. Every listed type has positive mass, so none can be excluded as a measure-zero event. The support is finite and nonempty because its masses sum to \(1\).

The strict benchmark condition and positive weights imply \(d_\theta(x)>0\) for every type and alternative. The observation that this positivity is unnecessary for the stopping argument is also correct.

2. Hardness reduction

The reduction correctly uses the standard NP-completeness of satisfiability for conjunctions of clauses containing at most three literals.

Every constructed attribute domain is explicitly listed, finite, and nonempty. Each clause factor depends on at most three distinct attributes, so its table has at most eight entries. Repeated literals or tautological clauses do not invalidate the construction: their truth values still determine the specified table entries. The added zero unary factors ensure complete scope coverage, including variables absent from every clause.

The single supported type satisfies all distribution and weight requirements: \(\tau=1\), \(\mu_1=1\), and \(w_1=1\). All numerical entries are rational.

The utility identity \(u_1(x)=-v(x)\) follows directly from the clause tables. Consequently, every utility value is nonpositive, and \(r_1=1\) satisfies the strict benchmark promise even when the formula is unsatisfiable.

The computation \(F_\mu(x)=1+v(x)\) is correct. With threshold \(q=1\), the decision condition holds exactly when an assignment violates zero clauses. Both directions of the satisfiability equivalence are established.

The factor count and stated output-length bound are valid under the specified ordinary indexed encoding. The reduction is polynomial and produces admissible instances. Thus the NP-hardness conclusion follows.

The certificate claim is appropriately restricted to promised admissible inputs. Coordinate indices specify an alternative with polynomial length, and exact evaluation verifies the threshold comparison in polynomial time. The output does not incorrectly claim that this verifier also checks the benchmark promise.

3. Stopping implication

The identity
\(B_\mu-A_\mu(y)=\sum_\theta\mu_\theta d_\theta(y)\)
is correct.

Each summand satisfies \(d_\theta(y)\leq F_\mu(y)\). Positive masses preserve these inequalities, and their normalization gives
\(B_\mu-A_\mu(y)\leq F_\mu(y)\).
This argument permits negative factor entries and different scopes across types.

For an unenumerated alternative, the supplied ranking hypothesis implies \(A_\mu(y)\leq A_\mu(x_k)\). Every inequality in the subsequent chain has the correct direction. The stopping hypothesis therefore excludes any strict improvement among unenumerated alternatives.

For enumerated alternatives, incumbent minimality supplies the required comparison. These cases exhaust the product domain. When \(k=|X|\), the unenumerated case is vacuous and incumbent minimality already establishes global optimality.

Equality and arbitrary tie-breaking cause no problem because the proof uses only weak inequalities. The argument establishes exactly the requested implication, without assuming that the stopping condition is necessary.

The attribution to the cited paper is accurate: its Proposition 1 uses the corresponding average-versus-maximum bound and ranking argument. The submitted proof independently handles the distribution masses, so no unverified extension of that proposition is needed. [Gonzales–Perny–Queiroz, Proposition 1](https://cdn.aaai.org/AAAI/2008/AAAI08-164.pdf).

4. Arithmetic and running times

The common-denominator argument is valid. The product \(D\) of input denominators has bit length \(O(L)\), and each input denominator divides it. The stated denominators \(D\), \(D^2\), and \(D^3\) accommodate utilities, weighted losses, and mass-weighted aggregates, respectively.

The corresponding integer numerators have \(O(L)\) bits: products involve a bounded number of input quantities, and summing polynomially many terms adds only logarithmic bit-length overhead. Signed entries do not change this bound.

The preprocessing and per-alternative bounds are conservative and sufficient for explicit tables and schoolbook arithmetic. Factor lookup can be included within the claimed bound without assuming a special indexing structure.

The witness, prefix, exhaustive-search, and sorting bounds follow from the stated evaluation bound. Sorting uses polynomial-size exact comparison keys. Explicit domain listing justifies \(N\leq(L+1)^m\).

The prefix bound correctly assumes the ranking hypothesis. The output explicitly distinguishes checking the stopping inequality from verifying that the supplied prefix is globally ranked.

5. Enumeration example

Both utilities have unary factors covering all attributes. Their maxima are \(m\) and \(0\), so the chosen benchmarks satisfy the strict inequalities.

The calculations of \(A_\mu(x)\), \(B_\mu\), and \(F_\mu(x)\) are correct. For even \(m=2t\), the minimum loss is \(t+1\), attained exactly at Hamming weight \(t\).

All alternatives tie under \(A_\mu\), making the proposed ordering admissible. Before an optimum appears, the incumbent loss exceeds \(B_\mu\), so the stopping inequality fails. At the first optimum it holds with equality. The stated first stopping index is therefore correct.

The central-binomial-coefficient bound is valid for every specified even \(m\geq2\), including the smallest case. The resulting lower bound is exponential in \(m\) and, given the stated input length, rules out a polynomial bound in input length for all admissible tie-breaking orders.

Repair feedback: None required. The claims, proofs, promise handling, and runtime qualifications are mutually 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.