Answer: \(\mathrm{EXPTIME}\)-complete, hence \(\mathrm{NP}\)-hard; no algorithm polynomial in \(m,\tau,L\) exists.
Corollary 8 — class: hardness
PDF text-layer excerpt — equations and symbol order may be approximateOptimal repair problem is EXPTIME-complete in ALC and PSPACE-complete in ALC w.r.t. acyclic TBoxes.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite ALC agenda \(\Phi\) of \(m\) axioms, a finite support of \(\tau\) complete rankings \(\pi\) with binary-rational masses \(\mu_\pi\geq 0\) summing to \(1\), and a rational threshold vector \(\theta\in\mathbb{Q}^m\), decide whether there is a consistent subset \(S\subseteq\Phi\) such that \(q_r(S)=\sum_\pi\mu_\pi\mathbf{1}\{\text{the axiom ranked }r\text{ by }\pi\text{ belongs to }S\}\) is lexicographically greater than \(\theta\); the optimization version finds a lexicographically maximal consistent subset.
An agenda \(\Phi\) consists of \(m\) explicitly encoded \(\mathcal{ALC}\) axioms: general concept inclusions, concept assertions, and role assertions; arbitrary TBoxes and ABoxes are allowed. A subset is consistent if it has an \(\mathcal{ALC}\) model.
A society is given by its support: a list of \(\tau\) distinct strict complete rankings \(\pi\) of \(\Phi\), each with positive binary-rational mass \(\mu_\pi\), with \(\sum_\pi\mu_\pi=1\). Here \(\tau\) is the support size, not the number of possible rankings.
Write \(\pi(r)\) for the axiom ranked \(r\), with rank \(1\) most preferred. For \(S\subseteq\Phi\), define \(q_r(S)=\sum_\pi\mu_\pi\mathbf{1}\{\pi(r)\in S\}\) and \(q(S)=(q_1(S),\ldots,q_m(S))\).
The input also contains \(\theta\in\mathbb{Q}^m\), encoded in binary, with no restriction on its coordinates. Decide whether some consistent \(S\subseteq\Phi\) satisfies \(q(S)>_{\mathrm{lex}}\theta\), meaning that its first differing coordinate is larger. The associated optimization problem finds a consistent subset maximizing \(q(S)\); any maximizer is acceptable.
Let \(L\) be the total input bit length, including axiom encodings, rankings, masses, and threshold coordinates. State running times in \(m,\tau,L\).
Is this decision problem solvable in polynomial time in \(m,\tau,L\), or is it \(\mathrm{NP}\)-hard?
Discrete optimal repair with explicitly listed voters and rank-count vectors is \(\mathrm{EXPTIME}\)-complete for \(\mathcal{ALC}\), and \(\mathrm{PSPACE}\)-complete with acyclic TBoxes ([source](https://www.ijcai.org/proceedings/2018/0268.pdf)).
No result settling this exact rational-mass formulation was located in the literature search.
The decision problem is \(\mathrm{EXPTIME}\)-complete, and therefore \(\mathrm{NP}\)-hard. In fact, hardness holds with \(\tau=1\), mass \(1\), and even \(m=1\). Consequently, there is no algorithm polynomial in \(m,\tau,L\), since \(\mathrm{P}\subsetneq\mathrm{EXPTIME}\).
Both decision and optimization admit a deterministic running-time bound of
\(O\!\left(2^m\left[2^{p(L)}+(m+1)(\tau+1)L^2\right]\right)\),
for a fixed polynomial \(p\).
We use the following standard theorem: given an explicitly encoded \(\mathcal{ALC}\) concept \(C\) and a general TBox \(T\), deciding whether some model \(\mathcal I\) of \(T\) satisfies \(C^{\mathcal I}\ne\varnothing\) is \(\mathrm{EXPTIME}\)-complete. Both arbitrary concepts and general concept inclusions are allowed in the present task, so this theorem applies. See [Meier and Schneider, *Generalized Satisfiability for the Description Logic ALC*](https://arxiv.org/abs/1103.0853).
Let an instance of this problem be
\(T=\{C_i\sqsubseteq D_i:1\le i\le k\}\), together with \(C\).
Define
\(E_T=\bigsqcap_{i=1}^{k}(\neg C_i\sqcup D_i)\),
where the empty conjunction denotes \(\top\). Choose a fresh role name \(s\), absent from \(T\) and \(C\), and form the single GCI
\(\alpha=\bigl(\top\sqsubseteq E_T\sqcap\exists s.C\bigr)\).
Claim. The ontology \(\{\alpha\}\) is consistent if and only if \(C\) is satisfiable with respect to \(T\).
*Forward direction.* Suppose \(\mathcal I\models\alpha\). Every domain element belongs to \(E_T^{\mathcal I}\). For every \(i\), this implies
\(C_i^{\mathcal I}\subseteq D_i^{\mathcal I}\),
so \(\mathcal I\models T\). The domain is nonempty. Choose a domain element \(x\). Since \(x\in(\exists s.C)^{\mathcal I}\), some \(s\)-successor of \(x\) belongs to \(C^{\mathcal I}\). Thus \(C^{\mathcal I}\ne\varnothing\).
*Reverse direction.* Suppose \(\mathcal I\models T\) and choose \(d\in C^{\mathcal I}\). Extend \(\mathcal I\) by interpreting the fresh role as
\(s^{\mathcal I}=\Delta^{\mathcal I}\times\{d\}\).
Because \(\mathcal I\models T\), every domain element belongs to \(E_T^{\mathcal I}\). Every domain element also has an \(s\)-successor in \(C^{\mathcal I}\), namely \(d\). Hence the extension satisfies \(\alpha\). Freshness of \(s\) ensures that this extension preserves the interpretations of \(T\) and \(C\). This proves the claim.
Now construct the target instance:
This is a valid society with \(m=\tau=1\). Its only subsets are \(\varnothing\) and \(\{\alpha\}\), with scores
\(q(\varnothing)=(0)\), and \(q(\{\alpha\})=(1)\).
Therefore,
\(\exists\,S\subseteq\Phi\text{ consistent with }q(S)>_{\mathrm{lex}}\theta \quad\Longleftrightarrow\quad \{\alpha\}\text{ is consistent} \quad\Longleftrightarrow\quad C\text{ is satisfiable with respect to }T\).
The encoding of \(\alpha\) contains each source concept once, together with conjunctions, negations, and one existential restriction. Its size is polynomial in the source input length, and the ranking, mass, and threshold have constant size. This is a polynomial-time many-one reduction, proving \(\mathrm{EXPTIME}\)-hardness.
Write each mass as \(\mu_\pi=a_\pi/b_\pi\), with positive integers \(a_\pi,b_\pi\). The argument covers arbitrary binary-encoded rational masses, including dyadic ones.
Set
\(D=\prod_{\pi}b_\pi\), and \(u_\pi=a_\pi(D/b_\pi)\).
The total bit length of the denominators is at most \(L\), so \(D\) has \(O(L)\) bits. Since the masses sum to \(1\),
\(\sum_\pi u_\pi=D\).
For any subset \(S\), define the integer rank scores
\(t_r(S)=\sum_\pi u_\pi\mathbf 1\{\pi(r)\in S\}\).
Then
\(q_r(S)=t_r(S)/D\), with \(0\le t_r(S)\le D\).
Thus every score numerator has \(O(L)\) bits.
Write a threshold coordinate as \(\theta_r=c_r/d_r\), where \(c_r\) may be signed and \(d_r>0\). Exact comparison of \(q_r(S)\) with \(\theta_r\) reduces to comparing the signed integers
\(d_r t_r(S)\quad\text{and}\quad c_rD\).
Their bit lengths are \(O(L)\). Schoolbook multiplication takes \(O(L^2)\) bit operations. Computing the scores requires \(m\tau\) contributions, and lexicographic comparison examines at most \(m\) coordinates.
Including common-denominator preprocessing, a sufficient bound for these arithmetic operations is
\(O\!\left((m+1)(\tau+1)L^2\right)\).
This bound handles arbitrary threshold coordinates and requires no expansion of masses into explicitly listed voters.
Consistency of an explicitly encoded \(\mathcal{ALC}\) knowledge base with arbitrary TBoxes and ABoxes is decidable in deterministic exponential time. In particular, there is a fixed polynomial \(p\) giving a bound \(2^{p(L)}\) for every subset of the input agenda. See [Baader, Horrocks, and Sattler, *Description Logics*, Section 3.4.1](https://www.cs.ox.ac.uk/ian.horrocks/Publications/download/2007/BaHS07a.pdf).
Enumerate all \(2^m\) subsets \(S\subseteq\Phi\). For each subset, test consistency and compute its exact score. Accept if a consistent subset exceeds the threshold.
Enumeration examines every possible witness, and both tests are exact. Hence the algorithm decides the problem correctly in time
\(O\!\left(2^m\left[2^{p(L)}+(m+1)(\tau+1)L^2\right]\right)\).
Because the agenda and support are explicitly listed, \(m,\tau\le L\). This bound is \(2^{\operatorname{poly}(L)}\), proving membership in \(\mathrm{EXPTIME}\).
For optimization, retain a consistent subset with the greatest score encountered. The empty ontology is consistent, and the search space is finite, so a maximizer exists. Two score vectors have the same denominator \(D\), making their lexicographic comparison an exact comparison of their integer numerator vectors. The same running-time bound applies.
Optimization is also \(\mathrm{EXPTIME}\)-hard under polynomial-time oracle reductions: in the one-axiom construction above, the unique maximizer is \(\{\alpha\}\) when that singleton is consistent, and \(\varnothing\) otherwise. Thus any optimizer decides the source satisfiability problem.
The exact rational-mass formulation is therefore settled without needing to transfer the discrete-voter hardness theorem.
⟨structured verdict parsed — rendered above⟩
The prover’s argument resolves the task. The decision problem is \(\mathrm{EXPTIME}\)-complete, including the restriction \(m=\tau=1\). The stated decision and optimization running times are valid. I found no mathematical gaps or false steps.
The cited source problem is correctly stated: given an explicitly encoded \(\mathcal{ALC}\) concept \(C\) and an unrestricted general TBox \(T\), determine whether \(T\) has a model in which \(C\) has nonempty extension. This problem is \(\mathrm{EXPTIME}\)-complete. The source’s definitions match the prover’s formulation. [Meier and Schneider](https://arxiv.org/pdf/1103.0853)
The reduction uses unrestricted \(\mathcal{ALC}\) concepts and general concept inclusions, all permitted by USER_TASK. There is no mismatch involving acyclic TBoxes or restricted concept syntax.
The expression \(E_T=\bigsqcap_{i=1}^{k}(\neg C_i\sqcup D_i)\) is a valid \(\mathcal{ALC}\) concept. Requiring every domain element to satisfy \(E_T\) is exactly equivalent to satisfying every inclusion \(C_i\sqsubseteq D_i\).
The constructed \(\alpha=(\top\sqsubseteq E_T\sqcap\exists s.C)\) is one permitted GCI. Choosing \(s\) fresh is essential and is explicitly required.
The construction has polynomial encoding size: it copies the source concept expressions without expanding definitions or introducing exponential duplication. Keeping the agenda size equal to one does not keep its total bit length constant; the source instance is encoded inside \(\alpha\).
From \(\mathcal I\models\alpha\), every domain element satisfies \(E_T\), so every source GCI holds.
Standard \(\mathcal{ALC}\) interpretations have nonempty domains. Consequently, the selected element \(x\) exists. Its membership in \((\exists s.C)^{\mathcal I}\) supplies an element of \(C^{\mathcal I}\). Thus both required source conditions follow.
No assumption about finite models is used.
The source hypothesis explicitly supplies a model of \(T\) and an element \(d\in C^{\mathcal I}\).
Interpreting \(s\) as \(\Delta^{\mathcal I}\times\{d\}\) gives every domain element an \(s\)-successor satisfying \(C\). Since \(s\) occurs in neither \(T\) nor \(C\), this interpretation change preserves both source conditions.
Every domain element therefore satisfies both conjuncts on the right of \(\alpha\). The reverse implication is correct, including when \(T\) is empty.
The constructed society is valid: its one ranking is strict and complete, its mass is positive and equals one, and its support contains no duplicates.
With threshold \(\theta=(0)\), the empty subset has score equal to the threshold and fails the strict comparison. The singleton has score \((1)\) and passes exactly when it is consistent.
Hence the displayed equivalence preserves both yes-instances and no-instances. Together with the polynomial construction size, it proves polynomial-time many-one \(\mathrm{EXPTIME}\)-hardness.
The common-denominator construction is valid without requiring reduced fractions or dyadic denominators. Each \(D/b_\pi\) is an integer, and normalization gives \(\sum_\pi u_\pi=D\).
The bit length of \(D\) is bounded by the sum of the denominator bit lengths, up to a constant. Thus it is \(O(L)\). Positivity and normalization imply \(0\le t_r(S)\le D\), so the score numerators also have \(O(L)\) bits.
For a signed threshold numerator and positive denominator, comparison by \(d_rt_r(S)\) and \(c_rD\) preserves the comparison direction and handles equality exactly. Arbitrary negative or out-of-range threshold coordinates cause no difficulty.
Schoolbook multiplication and integer division on these operands take \(O(L^2)\) bit operations. The preprocessing, score additions, and coordinate comparisons fit within the claimed \(O((m+1)(\tau+1)L^2)\) bound.
The invoked theorem applies to arbitrary \(\mathcal{ALC}\) TBoxes and ABoxes, including both concept assertions and role assertions. Each subset is a knowledge base of encoding size at most the input size, so a uniform bound \(2^{p(L)}\) is legitimate.
The cited section deserves careful reading: its basic tableau procedure has a larger bound, but footnote 3 explicitly identifies an exponential-time implementation using reused search results. The same chapter also states the complexity of reasoning with arbitrary knowledge bases. The prover invokes the complexity theorem rather than asserting that the basic tableau procedure itself attains its bound. [Baader, Horrocks, and Sattler, Sections 3.4.1–3.4.2](https://www.cs.ox.ac.uk/ian.horrocks/Publications/download/2007/BaHS07a.pdf)
Enumeration covers every possible witness, and both consistency and score comparisons are exact. Its stated total bound is therefore valid. Explicit encoding gives \(m,\tau\le L\), making the bound deterministic exponential time in \(L\).
The empty subset is consistent, and the finite search space guarantees a maximizer. Maintaining the greatest exact score during enumeration returns an acceptable maximizer even when there are ties.
In the hardness construction, the optimizer’s output is uniquely determined: the singleton when consistent, and the empty subset otherwise. Thus an optimizer decides the source problem, establishing the claimed oracle-reduction hardness.
Finally, \(\mathrm{EXPTIME}\)-completeness implies \(\mathrm{NP}\)-hardness. The unconditional exclusion of polynomial time follows from the deterministic time hierarchy separation \(\mathrm P\subsetneq\mathrm{EXPTIME}\); it does not require assuming \(\mathrm P\ne\mathrm{NP}\).
No repair or additional clarification is necessary.
⟨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.