← back to the atlas

d4-conf-ecai-2016-0327 (d4-conf-ecai-2016-0327)

Answer: Computing an optimal consensus is \(\mathrm{NP}\)-hard, even for \(\tau=2\), equal masses, and clauses of length at most two. The threshold decision problem is \(\mathrm{NP}\)-complete.

The anchor (named result in the paper)

Proposition 2 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateLet m be the number of clauses in S = [Φ1, . . . , Φn]. The Transformational Approach computes one max# consensus for S. It requires one call to a Partial Max-SAT solver on a set of hard constraints made of mn clauses and a set of soft constraints made of m clauses.

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 consistent clause sets \(\Phi_t\), each with positive binary-rational mass \(\mu_t\) and \(\sum_t \mu_t=1\), compute a set of clauses \(\Gamma\subseteq\bigcup_t\Phi_t\) maximizing \(\sum_{\delta\in\Gamma}\sum_{t:\delta\in\Phi_t}\mu_t\), subject to \(\Gamma\cup\Phi_t\) being satisfiable for every type \(t\).

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

A society is given by its support: a list of \(\tau\geq 1\) distinct types, each an explicitly listed finite satisfiable set \(\Phi_t\) of Boolean clauses, with positive binary-rational mass \(\mu_t\) and \(\sum_{t=1}^{\tau}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types.
Logically equivalent clauses are identified; clause sets have no multiplicities. Put \(U=\bigcup_{t=1}^{\tau}\Phi_t\), \(m=|U|\), and let \(L\) be the total input bit length, including clauses and masses.
A consensus is a set \(\Gamma\subseteq U\) such that \(\Gamma\cup\Phi_t\) is satisfiable for every \(t\); the satisfying assignment may differ between types. Empty clause sets and the empty consensus are allowed.
Compute any consensus maximizing \(W(\Gamma)=\sum_{\delta\in\Gamma}\sum_{t:\delta\in\Phi_t}\mu_t\). State running times in \(m\), \(\tau\), and \(L\).

Is computing an optimal consensus for this mass-weighted problem possible in polynomial time, or is it \(\mathrm{NP}\)-hard?

For finite agent profiles, a maximum-cardinality consensus can be computed using one call to Partial Max-SAT on a polynomial-size instance ([source](https://doi.org/10.3233/978-1-61499-672-9-795)).
Discrete consensus extraction also has Weighted Partial Max-SAT formulations for several preference criteria ([source](https://www.ijcai.org/Proceedings/16/Papers/159.pdf)); these are not a complexity classification of the stated mass-weighted problem. No classification of this exact continuous formulation was located.

Modeling choices made when packaging the task

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

Classification

Computing an optimal consensus is \(\mathrm{NP}\)-hard, even when \(\tau=2\), both masses equal \(\frac12\), and every clause has at most two literals. The associated threshold decision problem is \(\mathrm{NP}\)-complete. Thus a polynomial-time algorithm exists only if \(\mathrm{P}=\mathrm{NP}\).

For \(\tau=1\), the unique optimum is \(U=\Phi_1\), which can be returned in \(O(L)\) time. The hardness begins already at support size two.

1. A reduction from Independent Set

We use the classical \(\mathrm{NP}\)-completeness of Independent Set. This also follows from the \(\mathrm{NP}\)-completeness of Vertex Cover: a vertex set \(I\) is independent exactly when its complement is a vertex cover. See [Karp’s original NP-completeness results](https://www2.seas.gwu.edu/~simhaweb/champalg/tsp/papers/KarpOriginal.pdf).

Let \(G=(V,E)\) be an explicitly represented finite simple graph with \(n=|V|\geq1\). Introduce one Boolean variable \(x_v\) for each vertex \(v\). Construct two types:

\(\displaystyle \Phi_1=\{x_v:v\in V\},\qquad \Phi_2=\{\neg x_u\lor\neg x_v:\{u,v\}\in E\},\qquad \mu_1=\mu_2=\frac12.\)

This is a valid society:

Consequently, \(m=n+|E|\). Using vertex labels of \(O(\log(n+1))\) bits, the construction has output length \(O((n+|E|)\log(n+1))\) and takes polynomial time.

Feasible consensuses correspond exactly to independent sets

First, no consensus can contain an edge clause \(\neg x_u\lor\neg x_v\). Indeed, \(\Phi_1\) forces both \(x_u\) and \(x_v\) true, so adding that clause makes the union unsatisfiable.

Every consensus therefore has the form

\(\displaystyle \Gamma_I=\{x_v:v\in I\}\)

for some \(I\subseteq V\).

If \(I\) contains both endpoints of an edge \(\{u,v\}\), then \(\Gamma_I\cup\Phi_2\) contains \(x_u\), \(x_v\), and \(\neg x_u\lor\neg x_v\). Hence it is unsatisfiable.

Conversely, suppose \(I\) is independent. Assign \(x_v\) true exactly for vertices in \(I\). Every unit in \(\Gamma_I\) is satisfied, and every edge clause in \(\Phi_2\) is satisfied because no edge has both endpoints in \(I\). Thus \(\Gamma_I\cup\Phi_2\) is satisfiable. Also, the all-true assignment satisfies \(\Gamma_I\cup\Phi_1\).

We have proved

\(\displaystyle \Gamma_I\text{ is a consensus}\quad\Longleftrightarrow\quad I\text{ is independent in }G.\)

The objective preserves the optimization problem

Each positive unit clause belongs only to \(\Phi_1\), so its weight is \(\frac12\). Therefore

\(\displaystyle W(\Gamma_I)=\frac{|I|}{2},\qquad \max_{\Gamma\text{ consensus}}W(\Gamma)=\frac{\alpha(G)}2,\)

where \(\alpha(G)\) is the maximum independent-set size.

Any optimal consensus consequently gives a maximum independent set by reading its selected unit clauses. Likewise, \(G\) has an independent set of size at least \(k\) exactly when the constructed society has a consensus of weight at least \(\frac{k}{2}\).

This proves the claimed hardness. In particular, bounding \(\tau\) alone cannot yield a polynomial-time algorithm unless \(\mathrm{P}=\mathrm{NP}\).

2. The threshold decision problem is in NP

Consider the decision problem asking whether some consensus has weight at least a supplied binary-rational threshold \(B\).

Let \(n\) denote the number of variables occurring in the input; then \(n\leq L\). A certificate consists of a subset \(\Gamma\subseteq U\) and, for each type \(t\), an assignment satisfying \(\Gamma\cup\Phi_t\). Its length is \(O(m+\tau n)\), polynomial in the input length. Evaluating all these clause sets takes polynomial time.

Exact weight comparisons also take polynomial time. Write the input masses as \(\mu_t=p_t/q_t\), and define

\(\displaystyle Q=\prod_{t=1}^{\tau}q_t,\qquad a_t=p_t\frac{Q}{q_t},\qquad b_\delta=\sum_{t:\delta\in\Phi_t}a_t.\)

The bit length of \(Q\) is \(O(L)\), because the denominator encodings are included in \(L\). Since the masses sum to one,

\(\displaystyle \sum_t a_t=Q,\qquad 1\leq b_\delta\leq Q,\qquad W(\Gamma)=\frac{\sum_{\delta\in\Gamma}b_\delta}{Q}.\)

The score numerator has \(O(L+\log(m+1))\) bits. Comparing it with \(B\) by cross multiplication therefore takes polynomial time in \(L\) and the encoding length of \(B\).

Together with the reduction above, this establishes \(\mathrm{NP}\)-completeness of the threshold problem, already on the stated two-type restriction.

3. One polynomial-size Weighted Partial Max-SAT instance

The binary masses permit a direct formulation without expanding a type into agents.

Introduce a selector \(s_\delta\) for each \(\delta\in U\). For every type \(t\), make a separate copy of the original variables. Write \(\delta^{(t)}\) for the corresponding renamed clause.

Use the following hard clauses:

\(\displaystyle \{\delta^{(t)}:\delta\in\Phi_t,\ 1\leq t\leq\tau\} \;\cup\; \{\neg s_\delta\lor\delta^{(t)}:\delta\in U,\ 1\leq t\leq\tau\}. \)

For each \(\delta\in U\), add the soft unit clause \(s_\delta\) with integer weight \(b_\delta\) defined above.

For a chosen selector set \(\Gamma=\{\delta:s_\delta\text{ is true}\}\), the hard clauses require the variables in copy \(t\) to satisfy precisely \(\Phi_t\) together with every selected clause. Because the variable copies are disjoint, the hard clauses admit such assignments exactly when \(\Gamma\) is a consensus. Their soft score is \(QW(\Gamma)\). Hence an optimal Max-SAT assignment yields an optimal consensus.

There are at most \(2\tau m\) hard clauses, \(m\) soft clauses, and \(m+\tau n\) variables. The hard-clause literal count is \(O(\tau L)\); the soft weights use \(O(mL)\) bits. With binary variable identifiers, the complete encoding has size

\(\displaystyle N=O\!\left(\tau L\log(2+\tau L)+mL\right).\)

Construction takes \(\operatorname{poly}(m,\tau,L)\) time, followed by one Weighted Partial Max-SAT call and \(O(m)\) extraction time. This polynomial-size formulation is consistent with the hardness result; it does not make the optimization polynomial-time solvable.

4. An exact algorithm exponential in the number of clauses

An unconditional running-time bound is

\(\displaystyle O\!\left(2^m(\tau+1)L^3\right).\)

Here is a construction establishing that bound, including when clauses contain many variables.

Represent subsets of \(U\) by \(m\)-bit masks. Enumerate the variables as \(x_1,\ldots,x_n\). Let \(P_i\) be the clauses containing \(x_i\), and \(N_i\) the clauses containing \(\neg x_i\). Define

\(\displaystyle R_0=\{\varnothing\},\qquad R_i=\{M\cup P_i:M\in R_{i-1}\}\cup \{M\cup N_i:M\in R_{i-1}\}. \)

By induction, \(R_i\) consists exactly of the sets of clauses having a true literal among the first \(i\) assigned variables. Thus \(R_n\) consists exactly of the clause-satisfaction masks attainable by full assignments. Each table has at most \(2^m\) entries.

For each type \(t\), initialize a Boolean table

\(\displaystyle f_t(M)=1\quad\Longleftrightarrow\quad M\in R_n\text{ and }\Phi_t\subseteq M.\)

Compute its downward closure,

\(\displaystyle F_t(S)=\bigvee_{M\supseteq S}f_t(M).\)

This takes \(O(m2^m)\) table updates: for each clause position \(j\), and every mask \(S\) omitting \(j\), replace the entry at \(S\) by its disjunction with the entry at \(S\cup\{j\}\). Induction over the processed positions proves the displayed closure formula.

Now \(F_t(S)=1\) exactly when some assignment satisfies both \(S\) and \(\Phi_t\). Therefore \(S\) is a consensus exactly when every \(F_t(S)\) equals one. Scan these masks and return one maximizing \(\sum_{\delta\in S}b_\delta\).

The mask construction, closures, and exact score comparisons obey the stated conservative bit-operation bound, using \(m,n\leq L\). Thus the problem is tractable for bounded \(m\), while remaining \(\mathrm{NP}\)-hard for fixed \(\tau=2\).

⟨structured verdict parsed — rendered above⟩

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

Verdict

The output resolves the task correctly. The reduction establishes \(\mathrm{NP}\)-hardness for exactly the stated mass-weighted problem, already with two distinct satisfiable types, equal masses, and clauses of length at most two. The threshold problem’s membership in \(\mathrm{NP}\), the Weighted Partial Max-SAT formulation, and the exponential running-time bound are also justified.

I found no major or minor mathematical issues requiring repair.

Step-by-step verification

1. Source problem and validity of the constructed society

The reduction uses the standard decision problem Independent Set: given an explicitly represented finite simple graph and an integer \(k\), decide whether there is an independent vertex set of size at least \(k\). Its \(\mathrm{NP}\)-completeness is the cited standard result; it is also stated in [CMU’s complexity lecture notes](https://www.cs.cmu.edu/~15451-s16/lectures/lec18.pdf).

All hypotheses needed for the construction are satisfied:

The edge-free case is valid: \(\Phi_2\) is then empty, which the task expressly permits.

The equality \(m=n+|E|\) and the construction-size bound \(O((n+|E|)\log(n+1))\) are correct. The requirement \(n\geq1\) introduces no substantive restriction on the source problem.

2. Characterization of feasible consensuses

The exclusion of every edge clause is correct. A consensus must be compatible with \(\Phi_1\), which forces both endpoints of every edge true. Adding the corresponding negative edge clause therefore makes that union unsatisfiable.

Consequently, every feasible consensus consists solely of selected positive unit clauses.

Both directions of the claimed correspondence are established:

The argument correctly allows the witnessing assignments to differ between types. It does not impose a common assignment, which would change the problem.

3. Preservation of the objective and hardness

Every selectable positive unit belongs only to \(\Phi_1\), so its weight is exactly \(\frac12\). Thus the displayed identities
\[ W(\Gamma_I)=\frac{|I|}{2}, \qquad \max_{\Gamma\text{ consensus}}W(\Gamma)=\frac{\alpha(G)}2 \]
are correct.

An optimal consensus directly identifies a maximum independent set. The threshold mapping \(k\mapsto\frac{k}{2}\) also preserves yes-instances and no-instances and has polynomial encoding length.

This proves both optimization hardness and threshold-decision hardness under all the advertised restrictions. In particular, a bound on support size alone cannot make the general problem polynomial-time solvable unless \(\mathrm{P}=\mathrm{NP}\).

4. Membership of the threshold problem in \(\mathrm{NP}\)

The proposed certificate is sufficient: it specifies the selected clauses and one satisfying assignment for each type. Its length \(O(m+\tau n)\) is polynomial because the explicit input implies \(m,n,\tau=O(L)\).

Verification checks exactly the required feasibility condition by evaluating \(\Gamma\cup\Phi_t\) separately for every type.

The rational-arithmetic argument is correct:

Cross multiplication verifies the threshold exactly in polynomial time. The output explicitly includes the encoding length of \(B\), which is necessary because \(B\) is additional decision input.

Therefore the claimed \(\mathrm{NP}\)-completeness follows.

5. Weighted Partial Max-SAT formulation

The formulation correctly represents the task:

Although selectors are shared, the assignment variables for different types are disjoint. Thus the construction preserves the task’s permission to use different assignments for different types.

The soft objective is exactly \(QW(\Gamma)\), so optimizing it preserves the desired optimum.

The stated bounds on clauses, variables, literal occurrences, and binary weight encodings are consistent with the construction. In particular, multiplying denominators increases their bit length only polynomially. The resulting instance is polynomial in \(m,\tau,L\).

The output correctly distinguishes a polynomial-size formulation from a polynomial-time solution of that formulation.

6. Exact algorithm and running time

The recurrence for \(R_i\) correctly records attainable clause-satisfaction masks after assigning the first \(i\) variables. For either value of the next variable, its newly satisfied clauses are precisely the corresponding set \(P_i\) or \(N_i\).

At completion, \(R_n\) therefore records exactly the attainable full-assignment satisfaction masks.

The initialization of \(f_t\) correctly retains only masks satisfying every clause of \(\Phi_t\). The stated downward-closure updates compute
\[ F_t(S)=\bigvee_{M\supseteq S}f_t(M). \]
Consequently, the interpretation of \(F_t(S)\) as feasibility of \(S\cup\Phi_t\) is correct.

Scanning masks accepted for every type and maximizing their integer scores therefore returns an optimal consensus.

The table sizes and update counts, together with \(m,n,\tau=O(L)\) and polynomial-length integer arithmetic, support the conservative bound
\[ O\!\left(2^m(\tau+1)L^3\right). \]
No hidden dependence exponential in the number of variables is introduced.

7. Boundary cases and scope

The claimed unique optimum for \(\tau=1\) is correct: \(U=\Phi_1\) is feasible, and every clause has positive weight.

The exponential algorithm also covers \(m=0\): its sole mask represents the empty consensus. Empty types, unused variables, and tautological clauses do not invalidate the stated mask interpretation.

All conclusions concern the explicit support and binary-rational masses specified in the task. The proof does not depend on expanding masses into a finite agent population.

Feedback

No additional lemma, clarification, or mathematical repair is needed. The prover’s claimed classification is established.

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