Answer: \(\mathrm{NP}\)-hard, already for \(m=2\), \(\tau=1\), and \(k=1\), with linear guards and a globally consistent corpus.
Theorem 1 — class: other
PDF text-layer excerpt — equations and symbol order may be approximateAlgorithm Justify is correct when- ever its subroutine Solve is correct.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given candidates \(C\), ranking types \(T=L(C)\), a rational society \(\mu^\star\in\Delta(T)\), target outcome \(X^\star\subseteq C\), a finite corpus \(\mathcal A\) of scale-free lifted axiom schemas, and a certificate bound \(k\), compute whether there exists an inclusion-minimal explanation \(A_E\) with \(|A_E|\le k\) and normative basis \(A_N\) such that every anonymous rule \(F_\infty:\Delta(T)\to2^C\setminus\{\varnothing\}\) satisfying \(A_E\) yields \(F_\infty(\mu^\star)=X^\star\), \(A_E\) consists of instances from \(A_N\), and \(A_N\) is jointly satisfiable.
Let \(C\) be a nonempty candidate set, \(m=|C|\), and \(T=L(C)\) the strict ranking types. Write \(D=\Delta(T)\cap\mathbb Q^T\). A society is given by its support: the list of its \(\tau\) positive-mass types and their binary rational masses, summing to \(1\); \(\tau\) is the support size, not \(m!\).
An anonymous rule is any function \(F_\infty:D\to 2^C\setminus\{\varnothing\}\); winning sets retain ties, and no continuity or measurability is imposed.
The input corpus \(\mathcal A\) is a finite list of universally quantified schemas \(g\Rightarrow\varphi\). Variables range over societies in \(D\) and auxiliary rational scalars; \(g\) is a Boolean combination of rational polynomial comparisons in their mass coordinates and scalars, and \(\varphi\) is a Boolean combination of atoms \(x\in F_\infty(\mu_i)\), with \(x\in C\). Polynomials are explicitly encoded sparsely, with binary coefficients and exponents and ranking-indexed coordinates. An instance substitutes concrete societies and scalars for every variable. Thus schemas depend on normalized masses, with no electorate-size parameter.
Given \(\mu^\star\in D\), \(\varnothing\ne X^\star\subseteq C\), and a binary integer \(k\ge0\), ask whether there are \(A_N\subseteq\mathcal A\) and a finite set \(A_E\) of instances of schemas in \(A_N\), with \(|A_E|\le k\), satisfying the following conditions.
Some rule satisfies every instance of every schema in \(A_N\). Every rule satisfying \(A_E\) selects exactly \(X^\star\) at \(\mu^\star\), while for each \(B\subsetneq A_E\) some rule satisfying \(B\) selects a different outcome there.
Is this bounded rational-mass justification decision problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard? State running times in \(m\), \(\tau\), total input bit length \(L\), and \(k\).
For finite electorates, incremental instance-graph search is sound and complete assuming a sound and complete solving subroutine ([Nardi–Boixel–Endriss](https://doi.org/10.5281/zenodo.5901351)).
Related discrete justification existence is \(\Sigma_2^{\mathrm P}\)-complete with explicitly supplied instances and \(\mathrm{NEXP}\)-hard with succinct first-order axioms; these results concern different encodings, without the present bound ([Boixel–de Haan](https://ojs.aaai.org/index.php/AAAI/article/download/16656/16463)). No result settling this rational-mass schema formulation was located.
The stated decision problem is \(\mathrm{NP}\)-hard, already when
\(m=2,\qquad \tau=1,\qquad k=1.\)
This holds even when every guard uses only linear polynomial comparisons and the entire corpus is globally consistent.
Consequently, unless \(\mathrm P=\mathrm{NP}\), there is no algorithm with running time polynomial in the total input bit length \(L\), even for these fixed parameter values. More generally, there is no running-time bound \(f(m,\tau,k)L^{O(1)}\) for any computable \(f\), unless \(\mathrm P=\mathrm{NP}\).
I prove this directly for the supplied encoding. I also give a reduction without auxiliary scalars, where hardness comes from choosing a bounded collection of instances.
If \(m=1\), every rule necessarily returns the sole candidate. Taking \(A_N=A_E=\varnothing\) satisfies all requirements, for every \(k\).
If \(m\geq 2\) and \(k=0\), the answer is no: the only possible \(A_E\) is empty, and an unrestricted rule can select a nonempty outcome different from \(X^\star\).
The interesting case therefore has \(m\geq 2\) and \(k\geq 1\).
Minimality lemma. Suppose \(A_N\) is globally consistent and a finite set \(E\) of its instances forces the target outcome. Then some subset \(E'\subseteq E\) forces the target and satisfies the required minimality condition.
Proof. Among the subsets of \(E\) forcing the target, choose an inclusion-minimal one, \(E'\). Every proper subset \(B\subsetneq E'\) fails to force the target. By the definition of “forces,” this means that some rule satisfies \(B\) and returns a different outcome at \(\mu^\star\).
Also, a rule satisfying all schemas in \(A_N\) satisfies \(E'\), so the forcing statement is supported by a consistent collection of instances. Finally, \(|E'|\leq |E|\). ∎
Thus minimality does not obstruct a reduction that first constructs a consistent forcing set within the bound.
Fix \(C=\{a,b\}\). Let \(r\) be the ranking \(a\succ b\), and let \(\mu^\star\) assign mass \(1\) to \(r\). Set \(X^\star=\{a\}\) and \(k=1\).
Let \(H(z_1,\ldots,z_n)\) be any Boolean combination of rational polynomial comparisons. Construct a corpus consisting of the single schema
\(\bigl(\mu_r=1\ \land\ H(z_1,\ldots,z_n)\bigr)\ \Rightarrow\ \bigl(a\in F_\infty(\mu)\ \land\ \neg(b\in F_\infty(\mu))\bigr).\)
All variables are universally quantified as required. The variables \(z_i\) are auxiliary rational scalars.
Because societies have nonnegative masses summing to \(1\), the equality \(\mu_r=1\) uniquely specifies \(\mu=\mu^\star\).
Claim. The constructed justification instance is positive if and only if \(H\) has a satisfying assignment in \(\mathbb Q^n\).
Proof.
First, the entire corpus is always globally consistent: the constant rule \(F_a(\nu)=\{a\}\) satisfies the schema for every substitution.
Suppose \(H(q_1,\ldots,q_n)\) holds for rational \(q_i\). Instantiate the schema with \(\mu=\mu^\star\) and \(z_i=q_i\), and let \(A_E\) contain this single instance. Its antecedent is true, so every rule satisfying it returns exactly \(\{a\}\) at \(\mu^\star\).
Its only proper subset is empty. The constant rule \(F_b(\nu)=\{b\}\) satisfies that subset and returns a different outcome. Hence this is a valid justification with \(A_N\) equal to the corpus.
Conversely, suppose \(H\) has no rational satisfying assignment. Every instance then has a false antecedent and imposes no restriction. In particular, \(F_b\) satisfies every possible \(A_E\). No such collection can force \(\{a\}\) at \(\mu^\star\). ∎
This construction uses normalized masses throughout and introduces no electorate-size parameter.
Let \(\Psi\) be a Boolean satisfiability instance with variables \(p_1,\ldots,p_n\). Introduce rational scalars \(z_1,\ldots,z_n\), and define
\(H_\Psi(z)=\left(\bigwedge_{i=1}^{n}(z_i=0\ \lor\ z_i=1)\right)\land\widehat{\Psi}(z),\)
where \(\widehat{\Psi}\) replaces each occurrence of \(p_i\) by the comparison \(z_i=1\), preserving all Boolean connectives.
Claim. The formula \(\Psi\) is satisfiable if and only if \(H_\Psi\) is satisfiable over \(\mathbb Q\).
Proof. A Boolean assignment defines a rational assignment by assigning \(z_i=1\) when \(p_i\) is true and \(z_i=0\) otherwise. Under this substitution, every atom and Boolean connective has the same truth value.
Conversely, the first conjunction in \(H_\Psi\) forces every \(z_i\) to belong to \(\{0,1\}\). Interpreting \(p_i\) as true exactly when \(z_i=1\) then recovers a satisfying Boolean assignment. ∎
Apply the construction of Section 2 with \(H=H_\Psi\). Its correctness gives
\(\Psi\text{ is satisfiable}\quad\Longleftrightarrow\quad\text{the constructed instance admits a justification}.\)
Every polynomial comparison used here is linear, with constants in \(\{0,1\}\). There is one schema, two candidates, a target society of support size one, and bound one. Moreover, every constructed corpus is globally consistent.
For a source formula of bit length \(N\), variable renaming and construction take polynomial time; for example, \(O(N^2)\) bit operations suffice. The output length is \(O(N\log(N+2))\) under an explicit binary-index encoding.
Since Boolean satisfiability is \(\mathrm{NP}\)-hard, this establishes the claimed hardness for the rational-mass formulation.
The preceding reduction uses scalar assignments as Boolean witnesses. The following reduction shows hardness when guards merely specify one society.
Take a Set Cover instance with nonempty universe \(U=\{1,\ldots,u\}\), sets \(S_1,\ldots,S_s\subseteq U\), and bound \(k\).
Let
\(C=\{a,b_1,\ldots,b_u\},\qquad m=u+1.\)
Choose one ranking \(r\), let \(\mu^\star\) be its unit-mass society, and set \(X^\star=\{a\}\). For each \(j\), introduce the schema
\(\mu_r=1\ \Rightarrow\ \left(a\in F_\infty(\mu)\ \land\ \bigwedge_{i\in S_j}\neg(b_i\in F_\infty(\mu))\right).\)
There are no auxiliary scalars. Every guard consists of one linear equality. Again, the constant rule returning \(\{a\}\) satisfies the entire corpus.
Claim. A bounded justification exists if and only if the Set Cover instance has a cover using at most \(k\) sets.
Proof.
Suppose \(J\subseteq\{1,\ldots,s\}\) is a cover with \(|J|\leq k\). Instantiate its schemas at \(\mu^\star\). Their consequences require \(a\) to win and exclude every \(b_i\), because \(\bigcup_{j\in J}S_j=U\). They therefore force exactly \(\{a\}\). The minimality lemma supplies a valid minimal subset within the same bound.
Conversely, suppose a valid \(A_E\) exists. Discard instances whose antecedents are false. Every remaining instance is at \(\mu^\star\), and its exclusions correspond to one of the sets \(S_j\). Let \(J\) be the collection of their schema indices. Then \(|J|\leq |A_E|\leq k\).
If \(J\) does not cover \(U\), choose an uncovered element \(i\). Define a rule returning \(\{a,b_i\}\) at \(\mu^\star\) and \(\{a\}\) elsewhere. It satisfies every selected instance: \(a\) wins, and none of those instances excludes \(b_i\). Nevertheless, its target outcome differs from \(\{a\}\), contradicting the forcing condition. Hence \(J\) is a cover. ∎
Only one ranking coordinate is referenced. Encoding that ranking takes \(O(m\log(m+2))\) bits, and the target has \(\tau=1\). The reduction has polynomial size and running time; it never enumerates the \(m!\) ranking types.
The principal lower bound fixes \(m=2\), \(\tau=1\), and \(k=1\). Therefore neither small target support nor a small justification bound yields polynomial time for the unrestricted syntax, unless \(\mathrm P=\mathrm{NP}\).
For the specific Boolean-guard fragment in Section 3, exhaustive evaluation of the \(2^n\) Boolean assignments takes \(O(2^n\operatorname{poly}(L))\) time, where \(n\leq L\).
The exclusion-schema fragment in Section 4 is \(\mathrm{NP}\)-complete. Membership follows because a certificate names at most \(\min(k,s)\) schemas, and their union can be checked in polynomial time. A dynamic program over subsets of the universe decides this fragment in
\(O\!\left(L+(s+1)2^{m-1}\bigl(m+\log(s+2)\bigr)\right)\)
bit operations. Each state records the smallest number of selected sets covering that subset. Processing one set updates a state either by omitting the set or by taking its union with the state. Comparing the resulting optimum with the binary input \(k\) adds only a cost already covered by \(L\).
A concrete finite collection of instances admits a finite propositional test. Let \(h\) be the maximum number of society variables in a schema. For at most \(k\) instances, there are at most \(q=1+kh\) distinct societies, including the target.
After evaluating the instantiated guards and identifying equal societies, enumerate the \((2^m-1)^q\) possible nonempty outcomes at those societies. Every such assignment extends to an unrestricted rule by choosing arbitrary nonempty outcomes elsewhere. Hence enumeration checks entailment exactly.
If the concrete instances have total encoding length \(W\), the entailment stage takes
\(O\!\left((2^m-1)^{1+kh}\operatorname{poly}(W+kL+m)\right).\)
Minimality needs only the \(k\) individual deletion checks: a counterexample satisfying \(A_E\setminus\{e\}\) also satisfies every subset of that collection.
This is a finite-instance verification bound. It does not check global schema consistency or bound the bit lengths of instances that must be searched.
The guard-activation construction also applies to
\(H(z_1,\ldots,z_n)\equiv P(z_1,\ldots,z_n)=0\)
for an arbitrary sparsely encoded integer polynomial \(P\). Thus rational zero existence reduces in polynomial time to this problem, still with \(m=2\), \(\tau=1\), \(k=1\), and a globally consistent corpus.
This is Hilbert’s tenth problem over \(\mathbb Q\), whose decidability is a recognized open problem; see [Poonen’s survey](https://math.mit.edu/~poonen/papers/h10_notices.pdf). Consequently, a general terminating decision algorithm would also decide that problem.
The requested \(\mathrm{NP}\)-hardness conclusion is fully proved. No membership in \(\mathrm{NP}\), or general decision-time upper bound, is claimed.
⟨structured verdict parsed — rendered above⟩
The main hardness claim is proved. The reduction satisfies the schema syntax, global consistency requirement, justification bound, and minimality condition. No major or minor mathematical errors were found.
For \(m=1\), the target must be the singleton candidate set. Every rule selects it, so \(A_N=A_E=\varnothing\) is valid; minimality is vacuous.
For \(m\geq2\) and \(k=0\), an unrestricted constant rule can select a nonempty outcome different from \(X^\star\). Thus the empty instance set cannot force the target.
The minimality lemma is correct. A finite forcing set has an inclusion-minimal forcing subset. Failure of entailment for each proper subset means exactly that a rule satisfies that subset and selects a different target outcome. Global consistency also ensures that the selected instances are satisfiable, excluding vacuous forcing through inconsistency.
The construction uses two candidates, one society variable, and rational auxiliary scalars. Its guard is an allowed Boolean combination of rational polynomial comparisons, and its conclusion is an allowed Boolean combination of winner-membership atoms.
Since societies have nonnegative masses totaling \(1\), the equation \(\mu_r=1\) uniquely identifies the specified unit-mass society. No other society can activate the guard.
The constant rule returning \(\{a\}\) satisfies every substitution of the schema. Therefore the entire corpus is globally consistent, independently of the satisfiability of \(H\).
If \(H\) has a rational satisfying assignment, the corresponding concrete instance has a true guard and forces exactly \(\{a\}\) at \(\mu^\star\). The only proper subset of this singleton instance set is empty, which the constant rule returning \(\{b\}\) satisfies. This verifies minimality directly.
If \(H\) has no rational satisfying assignment, every possible instance has a false guard. The constant rule returning \(\{b\}\) consequently satisfies every selectable instance set and defeats target entailment.
This converse covers every choice of \(A_N\), including the empty choice. Universal quantification of the schema variables causes no difficulty: the selected instance substitutes particular rational values, while global consistency is verified separately for all substitutions.
The constraints \(z_i=0\lor z_i=1\) restrict the rational assignments to Boolean values. Replacing each Boolean variable by \(z_i=1\), while preserving connectives, preserves truth under this correspondence in both directions.
All comparisons are linear and have constant-size numerical data. The construction neither expands the Boolean formula into a potentially exponential normal form nor enumerates ranking types.
The stated output-length bound \(O(N\log(N+2))\) and construction-time bound \(O(N^2)\) are valid conservative bounds under the indicated binary-index encoding.
Applying the standard NP-hardness of Boolean formula satisfiability therefore establishes NP-hardness with \(m=2\), \(\tau=1\), and \(k=1\). In these instances, every society variable necessarily takes the unit-mass target value in any activating instance.
A running time polynomial in \(L\) on these fixed parameter values would yield a polynomial-time satisfiability algorithm.
Likewise, a bound \(f(m,\tau,k)L^{O(1)}\) would specialize to the constant factor \(f(2,1,1)\) times a polynomial in \(L\). The claimed exclusion of such a bound, unless \(\mathrm P=\mathrm{NP}\), follows.
No NP-membership conclusion follows from NP-hardness alone, and the output correctly avoids claiming one for the unrestricted problem.
The Set Cover construction is valid and globally consistent.
A cover yields instances that require \(a\) and exclude every competing candidate. Because the universe is nonempty, a cover contains at least one set, so the requirement that \(a\) win is present. The minimality lemma then supplies the required minimal justification within the same bound.
Conversely, every instance with a true guard concerns \(\mu^\star\). False-guard instances impose no restrictions. If the selected schema indices leave an element uncovered, the stated rule returning \(\{a,b_i\}\) at the target satisfies every selected instance and contradicts entailment. This verifies the converse, including empty selections and \(k=0\).
Repeated sets or repeated instances do not invalidate the argument: passing to distinct schema indices cannot increase their number. The construction has polynomial size without enumerating the ranking space.
Exhaustively testing the Boolean assignments gives the stated \(O(2^n\operatorname{poly}(L))\) bound for the specific Boolean-guard fragment.
For the exclusion-schema fragment, a certificate listing at most \(\min(k,s)\) schemas suffices because the established equivalence reduces acceptance to checking their union. This proves membership in NP for that fragment.
The subset dynamic program has \(2^{m-1}\) states and processes \(s\) sets. Subset operations use \(O(m)\) bits, and finite counts require \(O(\log(s+2))\) bits. The stated running-time bound is consistent with these operations and input reading.
At most \(k\) instances introduce at most \(kh\) societies, so including the target gives \(q\leq1+kh\). Each society has exactly \(2^m-1\) possible nonempty outcomes.
Every assignment of outcomes to these finitely many distinct societies extends to a rule on \(D\), because no regularity restrictions are imposed. Thus the enumeration checks entailment exactly.
Individual deletion checks suffice for minimality: every proper subset omits some instance and is contained in that instance’s deletion set.
The displayed bound is explicitly for the entailment stage after guard evaluation. It should not be read as a polynomial bound for evaluating arbitrary sparsely encoded guards with binary exponents, or as an algorithm for global consistency. The output appropriately distinguishes these tasks.
Substituting \(H(z)\equiv P(z)=0\) into the same construction preserves its proved equivalence and polynomial encoding size. Therefore a terminating algorithm for the unrestricted justification problem would decide rational zero existence for integer polynomials.
The identification with Hilbert’s tenth problem over the rationals is correct; the cited [Poonen survey](https://math.mit.edu/~poonen/papers/h10_notices.pdf) discusses precisely this unresolved decidability problem. This observation supports the stated limitation on upper bounds, without weakening the established NP-hardness result.
No repair or additional mathematical clarification is required. The requested classification is established; general decidability and unrestricted upper bounds remain outside the proved claims.
⟨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.