Answer: \(\mathrm{NP}\)-hard
Theorem 4 — class: hardness
Given an agenda \(\Phi\), integrity constraint \(\Gamma\), finite support \(S\subseteq\mathcal{J}(\Phi,\Gamma)\) with positive binary-rational masses \(\mu_t\) summing to \(1\), and constraint sets \(L,L_1,\ldots,L_u\), define \(D_\mu(K)=\sum_{t\in S}\mu_t d_g(K,t)\). Is there a complete, \(\Gamma\)-consistent judgment set \(K\) minimizing \(D_\mu\) over all such judgment sets, with \(L\subseteq K\) and \(L_i\not\subseteq K\) for every \(i\)?
Let \(\Phi\) be a finite, nonempty propositional agenda, closed under complementation and containing no doubly negated formulas; write \(m=|\Phi|/2\). Let \(\Gamma\) be a propositional integrity constraint. Variables occurring in these formulas need not themselves be agenda issues.
Let \(\mathcal J(\Phi,\Gamma)\) consist of judgment sets choosing exactly one formula from each complementary pair whose conjunction with \(\Gamma\) is satisfiable.
Define an undirected graph on \(\mathcal J(\Phi,\Gamma)\): distinct \(J,J'\) are adjacent exactly when no third feasible judgment set \(H\) satisfies \(J\cap J'\subseteq H\subseteq J\cup J'\). Let \(d_g\) be its shortest-path distance, with every edge of length \(1\).
A society is given by its support: a nonempty list \(S\subseteq\mathcal J(\Phi,\Gamma)\) of \(\tau\) distinct types with positive binary-rational masses \(\mu_t\) summing to \(1\). Here \(\tau\) is the support size, not the number of possible types.
The input also contains \(L,L_1,\ldots,L_u\subseteq\Phi\), with \(u\geq0\); these sets may be empty. Define \(D_\mu(K)=\sum_{t\in S}\mu_t d_g(K,t)\).
Decide whether some global minimizer \(K\in\operatorname{argmin}_{H\in\mathcal J(\Phi,\Gamma)}D_\mu(H)\) satisfies \(L\subseteq K\) and \(L_i\not\subseteq K\) for every \(i\). All tied minimizers are eligible; the containment conditions do not restrict the minimization domain.
Is this decision problem solvable in polynomial time, or is it NP-hard? State running times in \(m\), \(\tau\), \(u\), and the total input bit length \(L_{\mathrm{bit}}\), including all formulas and rational masses.
For finite, explicitly listed profiles with an unweighted sum of geodesic distances, the corresponding decision problem is \(\Theta_3^p\)-complete.
The problem is \(\mathrm{NP}\)-hard, even when \(m=2\), \(\tau=2\), \(u=0\), and both masses equal \(1/2\). Thus it has no polynomial-time algorithm unless \(\mathrm{P}=\mathrm{NP}\).
The ability to use variables outside the agenda is essential to this fixed-parameter hardness construction.
Let \(F\) be an arbitrary propositional formula. Choose fresh variables \(p,q\) that do not occur in \(F\), and construct
\(\Phi=\{p,\neg p,q,\neg q\}\),
\(\Gamma=(\neg p\land\neg q)\lor(p\land q)\lor(p\land\neg q\land F)\).
Use the two support types
\(A=\{\neg p,\neg q\},\qquad B=\{p,q\}\),
with \(\mu_A=\mu_B=1/2\). Set \(L=\{p,\neg q\}\) and \(u=0\).
This construction has size \(O(|F|+1)\). The agenda satisfies the required syntactic conditions. Both support types are feasible regardless of whether \(F\) is satisfiable: their respective first and second disjuncts make \(\Gamma\) true.
There are only four possible complete judgment sets. Besides \(A,B\), they are
\(C=\{p,\neg q\},\qquad E=\{\neg p,q\}\).
The set \(E\) is infeasible because its choices falsify every disjunct of \(\Gamma\). For \(C\), substituting \(p=\mathrm{true}\) and \(q=\mathrm{false}\) into \(\Gamma\) leaves precisely \(F\). Therefore
\(C\in\mathcal J(\Phi,\Gamma)\quad\Longleftrightarrow\quad F\text{ is satisfiable}.\)
The graph contains exactly \(A,B\). They are adjacent because there is no third feasible judgment set. Hence
\(D_\mu(A)=D_\mu(B)=1/2.\)
Neither contains \(L\), so the constructed instance is a no-instance.
The feasible vertices are exactly \(A,B,C\). Since \(A\cap B=\varnothing\) and \(A\cup B=\Phi\), the feasible set \(C\) witnesses that \(A,B\) are not adjacent.
The vertices \(A,C\) differ on only the issue \(p\). Any complete judgment set between them must therefore be one of these two endpoints, so they are adjacent. The same argument applies to \(C,B\), which differ only on \(q\). Thus the graph is the path
\(A-C-B.\)
Its distances give
\(D_\mu(A)=\tfrac12(0+2)=1,\qquad D_\mu(C)=\tfrac12(1+1)=1,\qquad D_\mu(B)=\tfrac12(2+0)=1.\)
These are all feasible vertices, so all three are global minimizers. In particular, \(C\) is an eligible minimizer containing \(L\).
Consequently, the constructed instance is a yes-instance exactly when \(F\) is satisfiable. This proves the claimed polynomial-time reduction and \(\mathrm{NP}\)-hardness.
It also rules out a running time of the form \(f(m,\tau,u)L_{\mathrm{bit}}^{O(1)}\), for any function \(f\), unless \(\mathrm{P}=\mathrm{NP}\): all three parameters are constant in the reduction.
To give an exact algorithm, first establish that the graph is connected.
Choose one representative from each complementary pair, and encode every complete judgment set by a vector in \(\{0,1\}^m\). Let \(h(x,y)\) denote Hamming distance. A complete judgment set \(z\) lies between \(x,y\) in the definition of adjacency exactly when it agrees with their common coordinates.
Lemma. For every two feasible vertices \(x,y\),
\(d_g(x,y)\leq h(x,y)\leq m.\)
Proof. Induct on \(h(x,y)\). The assertion is immediate when \(x=y\). For distinct adjacent vertices, the edge itself has length \(1\leq h(x,y)\).
Otherwise, nonadjacency supplies a third feasible vertex \(z\) between \(x,y\). Coordinate by coordinate,
\(h(x,z)+h(z,y)=h(x,y).\)
Because \(z\) differs from both endpoints, both distances on the left are positive and strictly smaller than \(h(x,y)\). Applying the induction hypothesis and concatenating the resulting paths gives a walk of length at most \(h(x,y)\). Hence the shortest-path distance is at most that value. This completes the induction. \(\square\)
The promised nonempty support ensures that the feasible domain is nonempty. The lemma therefore establishes connectivity and finiteness of every distance used in the objective.
Let \(v\) be the number of distinct propositional variables occurring anywhere in the agenda or integrity constraint. In particular, \(v\leq L_{\mathrm{bit}}\), but \(v\) need not be bounded by \(m\).
An exact deterministic algorithm proceeds as follows.
Enumerate all \(2^v\) truth assignments. For every assignment satisfying \(\Gamma\), evaluate the agenda representatives and mark its resulting vector as feasible.
This produces exactly \(\mathcal J(\Phi,\Gamma)\): every marked vector has a satisfying witness, and every feasible judgment set has such a witness by definition. Write \(N=|\mathcal J(\Phi,\Gamma)|\); then \(N\leq2^m\).
Identify coordinate subsets with masks. For each feasible vector \(x\), define
\(f_x(R)=1\)
when \(R\neq\varnothing\) and flipping precisely the coordinates in \(R\) gives a feasible vertex; otherwise define \(f_x(R)=0\).
Compute every subset sum
\(c_x(T)=\sum_{R\subseteq T}f_x(R).\)
For a feasible vertex \(y\neq x\), let \(T\) be the coordinates on which \(x,y\) differ. The complete judgment sets between them are precisely the vectors obtained from \(x\) by flipping subsets of \(T\). Thus \(c_x(T)\) counts the feasible vertices in that interval other than \(x\), including \(y\). Consequently,
\(x,y\text{ are adjacent}\quad\Longleftrightarrow\quad c_x(T)=1.\)
All subset sums for a fixed \(x\) can be computed using \(O(m2^m)\) additions: initialize an array with \(f_x\), then, for each coordinate, add the entry indexed by the mask with that coordinate removed to each entry containing it. After processing any collection of coordinates, the array sums over exactly the removals of those coordinates; after all coordinates, it equals \(c_x\).
There are at most \(2^m\) feasible choices of \(x\), so graph construction uses \(O(m4^m)\) additions of integers with \(O(m)\) bits.
Run breadth-first search from each of the \(\tau\) support vertices. This takes \(O(\tau4^m)\) graph operations and supplies every required distance.
For exact rational arithmetic, write \(\mu_t=a_t/b_t\), and set
\(B=\prod_{t\in S}b_t,\qquad w_t=a_t(B/b_t).\)
Then \(w_t\) is a positive integer, \(\sum_t w_t=B\), and minimizing \(D_\mu(K)\) is equivalent to minimizing
\(C(K)=\sum_{t\in S}w_t d_g(K,t).\)
The product \(B\) has \(O(L_{\mathrm{bit}})\) bits. By the distance lemma,
\(0\leq C(K)\leq mB,\)
so all scores have \(O(L_{\mathrm{bit}}+\log(m+1))\) bits.
Compute the global minimum over all feasible vertices. Then test whether any vertex attaining that value satisfies all the containment conditions. This order preserves the required unrestricted minimization domain.
An empty exclusion set is handled correctly: it is contained in every vertex, so it makes the final eligibility test fail everywhere.
Using elementary integer arithmetic, a conservative deterministic bit-time bound is
\(O\!\left(\left[2^v+(m+\tau)4^m+\bigl(\tau+(u+1)m\bigr)2^m\right](L_{\mathrm{bit}}+1)^2\right).\)
The terms cover truth-assignment enumeration, graph construction and breadth-first searches, and objective evaluation and containment checks, respectively. Since \(v,m\leq L_{\mathrm{bit}}\), this also gives a bound of \(2^{O(L_{\mathrm{bit}})}\).
Thus the decision problem is exactly decidable, but its dependence on formula complexity cannot be replaced by polynomial dependence on \(L_{\mathrm{bit}}\), even with fixed \(m,\tau,u\), unless \(\mathrm{P}=\mathrm{NP}\).
⟨structured verdict parsed — rendered above⟩
The argument establishes the claimed NP-hardness and gives a valid exact algorithm with a conservative running-time bound. I find no mathematical error or substantive gap. There is one minor omission: the standard complexity theorem used as the source of the reduction should be stated explicitly.
The reduction starts from satisfiability of an arbitrary propositional formula \(F\). Freshness of \(p,q\) is essential: it ensures that fixing the agenda choices does not constrain variables in \(F\).
The constructed agenda has exactly two complementary pairs, is nonempty, and contains no doubly negated formulas. Thus \(m=2\).
Both support types are feasible independently of \(F\):
They are distinct, and their positive rational masses sum to \(1\). Thus \(\tau=2\), and the construction satisfies the promised input conditions even when \(F\) is unsatisfiable. The choice \(u=0\) is permitted.
The construction copies \(F\) once and adds only a fixed number of formulas and support entries. Its stated linear size and polynomial construction time are justified.
The four listed judgment sets exhaust all complete choices for this agenda.
For \(E\), all three disjuncts of \(\Gamma\) are false, so infeasibility is correctly established.
For \(C\), substituting its agenda choices reduces \(\Gamma\) exactly to \(F\). Since \(p,q\) are fresh, the claimed equivalence
\(C\in\mathcal J(\Phi,\Gamma)\iff F\text{ is satisfiable}\)
is valid.
No additional feasible judgment sets have been omitted.
When \(F\) is unsatisfiable, the feasible domain consists exactly of \(A,B\).
There is no third feasible vertex, so the adjacency condition makes \(A,B\) adjacent. Their distances to themselves and each other are respectively \(0\) and \(1\), giving
\(D_\mu(A)=D_\mu(B)=1/2\).
Neither vertex contains \(L=\{p,\neg q\}\). The constructed instance is therefore correctly classified as a no-instance.
When \(F\) is satisfiable, the feasible domain consists exactly of \(A,B,C\).
The nonadjacency of \(A,B\) follows directly from
\(A\cap B=\varnothing\), \(A\cup B=\Phi\), and the third feasible vertex \(C\).
For each of the pairs \(A,C\) and \(C,B\), the vertices differ on exactly one complementary pair. Agreement on the other pair leaves only the two endpoints as possible complete judgment sets in the relevant interval. Their adjacency is therefore justified.
The graph is exactly the stated three-vertex path. All three objective calculations are correct, and they exhaust the feasible minimization domain. Consequently, \(C\) is a global minimizer containing \(L\).
The reduction preserves both yes- and no-instances. It proves the claimed hardness once the standard source problem’s NP-hardness is invoked.
Minor issue: The write-up does not explicitly state that unrestricted propositional satisfiability is NP-complete under polynomial-time many-one reductions. This is the standard theorem supporting the final hardness inference, and its hypotheses match the source problem here.
Minimum clarification: State that source theorem explicitly. No modification of the reduction is needed.
The exclusion of a running time \(f(m,\tau,u)L_{\mathrm{bit}}^{O(1)}\), unless \(\mathrm P=\mathrm{NP}\), is also correct: the reduction fixes all three parameters.
The Boolean-vector encoding correctly translates the interval condition into agreement on coordinates common to the endpoints.
The induction is valid:
This establishes connectivity and \(d_g(x,y)\leq m\). The promised support supplies a nonempty feasible domain. There is no circular reliance on connectivity: the induction itself supplies paths.
Enumerating assignments to all variables in the agenda and integrity constraint produces exactly the feasible vectors. This correctly includes variables outside the agenda.
The definition of \(f_x\) excludes \(x\). For a differing-coordinate mask \(T\), \(c_x(T)\) counts every other feasible vertex in the interval, including \(y\). Hence adjacency is equivalent to \(c_x(T)=1\), with no off-by-one error.
The described subset-sum procedure is valid and uses \(O(m2^m)\) additions per feasible \(x\). Since there are at most \(2^m\) such vertices, the stated \(O(m4^m)\) bound follows. Counts have \(O(m)\) bits.
Breadth-first search correctly computes distances in the unweighted graph. The bound \(O(\tau4^m)\) graph operations is conservative.
The common-denominator transformation is exact:
\(w_t=a_t(B/b_t)\) is a positive integer, and
\(C(K)=B D_\mu(K)\).
The normalization of the masses gives \(\sum_t w_t=B\).
The bit-length bounds for \(B\) and \(C(K)\) follow from the input encoding and the verified distance bound.
The algorithm first computes the minimum over the entire feasible domain and only then checks eligibility. It therefore respects the task’s unrestricted minimization requirement and permits every tied minimizer.
Its handling of an empty exclusion set is correct. Empty \(L\), inconsistent containment requirements, and \(u=0\) are also handled by the same containment test without needing a separate algorithmic branch.
The displayed deterministic bit-time bound conservatively covers assignment evaluation, graph construction, breadth-first searches, rational preprocessing, objective comparisons, and containment checks.
The inequalities \(v,m\leq L_{\mathrm{bit}}\) justify the resulting \(2^{O(L_{\mathrm{bit}})}\) upper bound. The algorithm makes no polynomial-time claim contradicted by the reduction.
The target is resolved in substance: the problem is NP-hard even with the stated constant parameters. The only requested repair is an explicit statement of the standard source complexity theorem.
⟨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.