← back to the atlas

d4-conf-ijcai-2017-0319 (d4-conf-ijcai-2017-0319)

Answer: \(\Delta_2^{\mathrm P}\)-complete for every fixed positive \(k\); in particular, \(\mathrm{NP}\)-hard.

The anchor (named result in the paper)

Theorem 5 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximateLet A = (θ1, . . . , θk) be a tuple of answers for a CQ q(x) to a ranked ontology K. If Cd contains P, then de- ciding whether A is a top-k answer is in Cd, Ck, and (∆P 2 )Cc in the data, KB, and combined complexity, respectively, and ∆P 2 -complete in the ranking complexity. If Cc is contained in NP, then it is ∆P 2 -complete in the combined complexity. In particular, for ranked ontologies in EL, top-k query an- swering is in P in the data and KB complexity, and ∆P 2 - complete in the ranking and combined complexity.

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

The continuous mirror question, as graded

Given a shared ontology \(O\), a conjunctive query \(q(x)\), fixed \(k\), a proposed answer tuple \(A\), and a distribution \(\mu\) over a finite support \(\mathcal{T}\) of complete user preference rankings \(P_t\), decide whether \(\sum_{t \in \mathcal{T}: A\text{ is a top-}k\text{ answer under }(P_t,O)} \mu_t \ge \eta\), for a rational target share \(\eta\). Use the paper's top-\(k\) definition, including its treatment of ties; each ranking is given in a permitted polynomial-time-computable representation.

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

Let \(V\) be a nonempty set of \(m\) Boolean context variables. The shared ontology \(O\) consists of annotated \(\mathcal{EL}\) axioms \(\langle\lambda:\varphi\rangle\), where \(\varphi\) is a propositional formula over \(V\); for a valuation \(W\), put \(O_W=\{\lambda:\langle\lambda:\varphi\rangle\in O,\ W\models\varphi\}\).
A society is given by its support: the list of the \(\tau\) types with positive mass, each with its mass as a binary rational. Here \(\tau\) is the support size, not the number of possible types; require \(\sum_t\mu_t=1\).
Each type supplies a total numerical ranking \(r_t:\{0,1\}^{m}\to[0,1]\cap\mathbb Q\), represented by a Boolean circuit outputting a binary numerator and positive denominator. Rankings may have ties and need not attain \(1\).
Given a CQ \(q(x)\), let \(N\) be the individual names occurring in \(O\) or \(q\), and let \(B\) contain all substitutions \(\theta:x\to N\), including substitutions of rank zero. Define \(s_t(\theta)=\max\{r_t(W):O_W\models q(x\theta)\}\), with the empty maximum equal to \(0\).
Fix a positive integer \(k\). The proposed answer is an ordered tuple \(A=(\theta_1,\ldots,\theta_\ell)\) of distinct members of \(B\), with \(0\le\ell\le k\). It is top-\(k\) for type \(t\) if either its entries exhaust \(B\), or \(\ell=k\), \(s_t(\theta_1)\ge\cdots\ge s_t(\theta_k)\), and \(s_t(\theta)\le s_t(\theta_k)\) for every \(\theta\in B\setminus\{\theta_1,\ldots,\theta_k\}\). Ties require no further tie-breaking.
Given a binary rational \(\eta\in[0,1]\), the decision problem asks whether \(\sum_{t:A\text{ is top-}k\text{ for }t}\mu_t\ge\eta\).
Is this decision problem in \(\mathrm P\), or is it \(\mathrm{NP}\)-hard, in combined complexity? State running times in \(m\), \(\tau\), the total input bit length \(L\), \(|O|\), \(|q|\), and \(|N|\), with \(k\) fixed.
For one ranking, top-\(k\) verification over \(\mathcal{EL}\) is \(\Delta_2^{\mathrm P}\)-complete in ranking and combined complexity, and polynomial in data and KB complexity when the ranking and query are fixed ([source](https://www.ijcai.org/proceedings/2017/0131.pdf)).
No result settling this exact support-distribution threshold problem was identified in the literature search.

Modeling choices made when packaging the task

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

Result and interpretation

For every fixed positive \(k\), the problem is \(\Delta_2^{\mathrm P}\)-complete under polynomial-time many-one reductions, where \(\Delta_2^{\mathrm P}=\mathrm P^{\mathrm{NP}}\). In particular, it is \(\mathrm{NP}\)-hard and therefore has no polynomial-time algorithm unless \(\mathrm P=\mathrm{NP}\).

Here the proposed tuple \(A\) is part of the input: the question asks whether this particular tuple receives sufficient support.

The hardness holds even with \(\tau=1\), mass \(1\), threshold \(\eta=1\), a fixed atomic query, and a fixed ontology containing just \(k+1\) annotated assertions. Thus the explicit support representation does not remove the difficulty.

1. Preliminary cases

Let \(d\) be the number of answer variables and \(n=|N|\). Then \(|B|=n^d\), with the usual convention that there is exactly one substitution when \(d=0\).

Assume the input satisfies the stated validity requirements, including distinct entries of \(A\) belonging to \(B\).

If \(A\) exhausts \(B\), it is top-\(k\) for every type under the definition in the question, so the answer is yes. This includes \(B=\varnothing\) and \(A=()\).

If \(A\) does not exhaust \(B\) and \(\ell<k\), it is top-\(k\) for no type. The answer is then yes exactly when \(\eta=0\).

It remains to consider \(\ell=k<|B|\).

2. Membership in \(\Delta_2^{\mathrm P}\)

We use the standard fact that Boolean CQ entailment over \(\mathcal{EL}\) is in \(\mathrm{NP}\) in combined complexity. This is recalled in Section 6 of the [cited paper](https://www.ijcai.org/proceedings/2017/0131.pdf). It applies here because, after choosing \(W\) and a substitution, \(O_W\) is an ordinary \(\mathcal{EL}\) ontology and the instantiated query is a Boolean CQ.

Fix a type \(t\). Let \(b\ge1\) bound the number of output bits of its denominator circuit. Every denominator is consequently smaller than \(2^b\).

If two attainable rational scores \(a/u\) and \(c/v\) differ, then

\(\left|a/u-c/v\right|=|av-cu|/(uv)\ge1/(uv)>2^{-2b}\).

This also applies when one score is \(0\), represented as \(0/1\). Every answer score is either \(0\) or an attained ranking value, since there are finitely many valuations.

Put \(D=2^{2b+1}\). It follows that the map \(s\mapsto\lfloor Ds\rfloor\) preserves both equality and strict ordering among all answer scores: distinct scores become numbers differing by more than \(2\) before rounding.

For each proposed entry define

\(h_{t,i}=\lfloor D s_t(\theta_i)\rfloor\).

Also define the largest outsider score, including a zero baseline:

\(u_t=\max\bigl(\{0\}\cup\{s_t(\theta):\theta\in B\setminus A\}\bigr)\),

and put \(h_{t,\mathrm{out}}=\lfloor Du_t\rfloor\).

For an integer \(j>0\), the predicate \(s_t(\theta_i)\ge j/D\) is in \(\mathrm{NP}\). A certificate consists of:

Evaluating annotations and the ranking circuit, and comparing the resulting rational with \(j/D\), all take polynomial time. The existential characterization is correct because \(j/D>0\), so the empty-maximum convention cannot create a false witness.

Similarly, \(u_t\ge j/D\) is in \(\mathrm{NP}\): additionally guess a substitution \(\theta\in B\setminus A\). Its representation requires \(O(d\log(n+1))\) bits.

For \(j=0\), both predicates are automatically true. Binary search over \(j\in\{0,\ldots,D\}\) therefore computes each integer \(h_{t,i}\) and \(h_{t,\mathrm{out}}\) using \(O(b+1)\) NP-oracle calls.

By the order-preservation property, \(A\) is top-\(k\) for this type exactly when

\(h_{t,1}\ge\cdots\ge h_{t,k}\quad\text{and}\quad h_{t,\mathrm{out}}\le h_{t,k}\).

Thus ties, zero scores, and rankings that never attain \(1\) are all handled correctly.

Repeat this computation for every listed type. Finally, add exactly the masses of the accepting types and compare the sum with \(\eta\). Binary rational arithmetic is polynomial-time here: a common denominator obtained by multiplying the input denominators has bit length at most their total input bit length, hence \(O(L)\).

Taking \(b\) to be the largest denominator-output width across all circuits, the algorithm uses

\(O\bigl(\tau(k+1)(b+1)\bigr)\)

NP-oracle calls and polynomial work per call. Since \(b\le L\) and \(k\) is fixed, this proves membership in \(\Delta_2^{\mathrm P}\).

3. Hardness: encoding an oracle computation

We prove \(\Delta_2^{\mathrm P}\)-hardness directly, without assuming that the cited single-ranking hardness reduction transfers to the present definitions.

Let \(H\) be any language in \(\mathrm P^{\mathrm{NP}}\). By the NP-completeness of SAT, there is a deterministic polynomial-time SAT-oracle machine \(M\) deciding \(H\).

Fix an input \(u\). Choose a polynomial bound \(T=T(|u|)\ge1\) on the machine’s running time, query lengths, and number of queries, for every sequence of oracle answers. Set \(t=T\).

A purported oracle transcript is a bit string \(y=(y_1,\ldots,y_t)\). Simulate \(M\) on \(u\), answering its successive queries with these bits. Any positions after the final query are padding positions and must contain \(0\).

For every position, supply a certificate block of \(T\) bits. A SAT query of length at most \(T\) needs at most \(T\) assignment bits. Call a transcript together with its certificate blocks *valid* when:

Queries answered \(0\) require no certificate.

Let \(C(y,c)\) be this validity predicate, and let \(\alpha(y)\in\{0,1\}\) indicate whether the simulated machine accepts.

Both functions have polynomial-size Boolean circuits constructible in polynomial time from \(u\). Indeed, the bounded machine simulation and all certificate checks run in polynomial time; unrolling those bounded computations produces polynomial-size circuits.

Let \(e\) be the genuine SAT-oracle transcript, padded with zeros.

Lemma. The transcript \(e\) is the lexicographically greatest transcript admitting certificates \(c\) with \(C(e,c)=1\).

Proof. It admits certificates because every genuine yes-answer has a satisfying assignment.

Suppose a valid transcript \(y\) were lexicographically larger. At the first differing position \(i\), we would have \(e_i=0\) and \(y_i=1\). All earlier answers agree, so the deterministic simulations reach the same next query, or both have already finished making queries.

In the first case, the genuine answer \(e_i=0\) means that query is unsatisfiable, contradicting the certificate required by \(y_i=1\). In the second case, validity requires the padding bit to be \(0\), again a contradiction. \(\square\)

Define

\(\operatorname{val}(y)=\sum_{i=1}^{t}y_i2^{t-i}\), and \(R(y)=(\operatorname{val}(y)+1)/2^t\).

The function \(R\) strictly increases with lexicographic order, and \(0<R(y)\le1\). Consequently, \(R(e)\) is strictly greater than \(R(y)\) for every other valid transcript.

4. Turning the transcript into a top-\(k\) instance

Use individuals \(a_1,\ldots,a_k,b\), a concept name \(P\), and the fixed query \(q(x)=P(x)\).

The context variables comprise a selector bit \(z\), the transcript bits, and all certificate bits. In particular, \(m=1+T+T^2\), so \(V\) is nonempty.

The shared ontology is

\(O=\{\langle P(a_i):z\rangle:1\le i\le k\}\cup\{\langle P(b):\neg z\rangle\}\).

Use one type, of mass \(1\), with ranking

\(r(z,y,c)=R(y)\) when \(C(y,c)=1\) and \(z=\alpha(y)\), and \(r(z,y,c)=0\) otherwise.

This has the required circuit representation: output denominator \(2^t\), and numerator \(\operatorname{val}(y)+1\) when the condition holds, or \(0\) otherwise. Both outputs have polynomial bit length. The ranking is total and takes values in \([0,1]\cap\mathbb Q\).

Set \(A=(x\mapsto a_1,\ldots,x\mapsto a_k)\) and \(\eta=1\).

There are exactly \(k+1\) substitutions in \(B\), so \(A\) does not exhaust \(B\). Moreover,

For the reverse implications, when an assertion is absent, interpret all names as distinct elements and interpret \(P\) as containing exactly the asserted elements. This is a countermodel to the absent assertion.

Thus every proposed entry has the same score: the maximum rank of a valid accepting transcript, or \(0\) if none exists. The outsider’s score is the maximum rank of a valid rejecting transcript, or \(0\).

If \(M\) genuinely accepts \(u\), then \(\alpha(e)=1\). Every proposed entry has score \(R(e)\), while the outsider has strictly smaller score. Hence \(A\) is top-\(k\).

If \(M\) genuinely rejects \(u\), the outsider has score \(R(e)\), strictly greater than every proposed entry’s score. Hence \(A\) is not top-\(k\).

Because the sole type has mass \(1\) and \(\eta=1\), the threshold instance accepts exactly when \(u\in H\).

The construction has polynomial size and is computable in polynomial time. Since \(H\) was arbitrary, this proves \(\Delta_2^{\mathrm P}\)-hardness for every fixed positive \(k\), completing the classification.

5. Explicit running-time bounds

Here \(|O|\) and \(|q|\) denote encoding lengths; annotation and circuit lengths are included in \(L\).

The oracle algorithm above has polynomial running time with an NP oracle, using \(O(\tau(k+1)(L+1))\) calls. It avoids enumerating either the \(2^m\) valuations or the \(n^d\) substitutions.

For an ordinary deterministic bound, let \(E(o,h,n)\) bound the time for one Boolean CQ-entailment test over an \(\mathcal{EL}\) ontology of length at most \(o\), with query-pattern length at most \(h\) and \(n\) available names.

Enumerate all valuations and all substitutions. For each valuation:

The entailment result is shared across all types. Exact comparisons and the final mass calculation take polynomial time in \(L\). This gives

\(O\!\left(2^m\left[\operatorname{poly}(L)+n^d\left(E(|O|,|q|,n)+\tau\operatorname{poly}(L)\right)\right]+\operatorname{poly}(L)\right)\).

NP membership of \(\mathcal{EL}\) CQ entailment supplies a fixed polynomial \(p\) such that one may take

\(E(|O|,|q|,n)\le2^{p(|O|+|q|(1+\lceil\log_2(n+1)\rceil)+n+1)}\),

after consistently relabeling individual names. This yields an explicit unconditional exponential upper bound in the requested parameters.

When the query is fixed, ordinary \(\mathcal{EL}\) CQ entailment is polynomial in ontology size, as recalled in the [source](https://www.ijcai.org/proceedings/2017/0131.pdf). Since \(d\) is then fixed, the enumeration bound simplifies, for nonempty \(B\), to

\(O\!\left(\tau\,2^m\,|N|^d\,\operatorname{poly}(L)\right)\).

In particular, fixing both \(m\) and the query gives polynomial time. Fixing the query and ontology alone does not: the hardness construction varies only the context variables and ranking circuit.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover’s claim is proved. The argument establishes \(\Delta_2^{\mathrm P}\)-completeness under polynomial-time many-one reductions for every fixed positive \(k\), and therefore answers the requested combined-complexity question with \(\mathrm{NP}\)-hardness.

I found no major or minor mathematical issues. The membership argument, direct hardness reduction, and stated running-time bounds are valid under the input requirements in USER_TASK.

1. Interpretation and preliminary cases

The prover correctly treats \(A\) as the proposed tuple supplied in the input. It verifies support for that tuple rather than searching for a tuple.

Writing \(d\) for the number of answer variables and \(n=|N|\), the count \(|B|=n^d\) is correct, with the stated convention that there is one substitution when \(d=0\). In particular, when \(n=0\) and \(d>0\), \(B\) is empty.

The preliminary cases follow exactly from the task’s definition:

Assuming the stated input-validity requirements is legitimate. The task supplies valid rankings and valid tuples; it does not ask the algorithm to recognize whether an arbitrary circuit satisfies the ranking promises.

2. Membership in \(\Delta_2^{\mathrm P}\)

Entailment theorem and hypotheses

The invoked fact is that Boolean conjunctive-query entailment for ordinary \(\mathcal{EL}\) ontologies belongs to \(\mathrm{NP}\) in combined complexity. Section 6 of the [cited paper](https://www.ijcai.org/proceedings/2017/0131.pdf) explicitly recalls this result and polynomial KB complexity.

Its hypotheses are satisfied: selecting \(W\) yields an ordinary \(\mathcal{EL}\) ontology \(O_W\), and substituting all answer variables yields a Boolean CQ. Constructing these objects has polynomial cost in the supplied encodings.

The prover uses this entailment result directly; it does not rely on transferring the paper’s top-\(k\) theorem to the task’s modified definitions.

Rational separation

If denominators have at most \(b\ge1\) output bits, each positive denominator is strictly less than \(2^b\). For distinct rational values, the calculation
\[ \left|\frac{a}{u}-\frac{c}{v}\right| =\frac{|av-cu|}{uv} \ge\frac1{uv} >2^{-2b} \]
is correct. Reduced fractions are unnecessary: the nonzero integer \(|av-cu|\) is at least \(1\).

The calculation also covers the zero baseline represented by \(0/1\). Every answer score is either zero or an attained ranking value because the valuation domain is finite.

With \(D=2^{2b+1}\), distinct scores differ by more than \(2\) after multiplication by \(D\). Consequently, taking floors preserves strict order and equality. The bit length of \(D\), rather than its numerical magnitude, is linear in \(b\).

Oracle predicates and binary search

For \(j>0\), the proposed predicate
\[ s_t(\theta_i)\ge j/D \]
has exactly the stated existential characterization. A successful witness must supply a valuation at which entailment holds and the ranking reaches the threshold. Conversely, any such witness proves the predicate.

The restriction \(j>0\) correctly handles the empty-maximum convention. At \(j=0\), the predicate is automatically true.

For outsiders, guessing a substitution in \(B\setminus A\) is polynomially bounded. Checking membership, exclusion from the supplied tuple, annotations, circuit outputs, rational comparisons, and the entailment certificate all have polynomial verification cost. The zero baseline is handled by the same special treatment of \(j=0\).

For any score \(s\in[0,1]\), the largest integer \(j\in\{0,\ldots,D\}\) satisfying \(s\ge j/D\) is exactly \(\lfloor Ds\rfloor\). Thus binary search computes the claimed integers using \(O(b+1)\) oracle calls. The endpoint \(s=1\) is included.

Top-\(k\) test and mass arithmetic

Order preservation justifies the equivalence between the original score comparisons and
\[ h_{t,1}\ge\cdots\ge h_{t,k}, \qquad h_{t,\mathrm{out}}\le h_{t,k}. \]
The outsider maximum represents precisely the universal outsider condition. Its extra zero baseline cannot change that condition because all scores are nonnegative.

The procedure therefore handles ties, zero scores, and rankings whose maximum is below \(1\).

Summing the accepted types’ rational masses is polynomial-time. The product of their input denominators has bit length bounded by the total denominator encoding length, and the numerators and comparison with \(\eta\) also have polynomial bit length.

There are \(k+1\) score quantities per type, giving
\[ O\bigl(\tau(k+1)(b+1)\bigr) \]
NP-oracle calls with polynomial work per call. Under the supplied explicit circuit representation, \(b\le L\). This establishes membership in \(\mathrm P^{\mathrm{NP}}\).

3. Oracle-transcript hardness argument

Bounded simulation and certificates

For an arbitrary language \(H\in\mathrm P^{\mathrm{NP}}\), the use of a deterministic polynomial-time SAT-oracle machine is justified by SAT’s NP-completeness. The chosen polynomial bound covers simulations under every oracle-answer sequence, which is necessary for the subsequent circuit construction.

There are at most \(T\) query positions, and a SAT formula of encoding length at most \(T\) needs at most \(T\) assignment bits. Thus the certificate blocks are sufficient and have total polynomial length.

The validity predicate deliberately certifies only answers equal to \(1\). It makes no claim that an answer equal to \(0\) is correct. Padding positions are explicitly forced to zero.

The bounded simulation, satisfaction checks, and acceptance indicator are polynomial-time computations. Their uniform conversion to polynomial-size Boolean circuits is applicable as stated.

Lexicographic maximum lemma

The genuine transcript \(e\) admits certificates because every actual SAT yes-answer has a satisfying assignment.

The first-difference argument is valid. If a valid transcript \(y\) were larger than \(e\), their first differing position would have \(e_i=0\) and \(y_i=1\). Agreement on earlier answers forces the deterministic simulations to have the same query at that position, or to be in padding positions.

This proves the stated lemma without requiring certificates for negative answers.

Numerical encoding

The encoding
\[ R(y)=\frac{\operatorname{val}(y)+1}{2^t} \]
strictly respects lexicographic order on equal-length binary transcripts. Its range is
\[ 2^{-t}\le R(y)\le1. \]
In particular, the genuine transcript has positive rank, and its rank strictly exceeds that of every other valid transcript. Both facts are used correctly in the reduction.

4. Reduction to the specified ontology problem

The constructed instance meets all input requirements:

The numerator \(\operatorname{val}(y)+1\) can equal \(2^t\); the claim of polynomial output bit length accommodates this endpoint. There is no overflow assumption in the stated construction.

The set \(N\) contains exactly the \(k+1\) displayed individual names, so \(B\) contains exactly \(k+1\) substitutions.

The entailment equivalences are also correct. A present assertion entails the corresponding atomic query. When it is absent, the supplied interpretation with distinct named elements and exactly the asserted elements in \(P\) is a countermodel. This argument does not assume that all models obey a unique-name requirement.

The resulting proposed-entry scores are the maximum ranks of valid accepting transcripts, with zero when there are none. The outsider score is the corresponding maximum for rejecting transcripts.

If the genuine computation accepts, every proposed entry has score \(R(e)\), and the outsider has a strictly smaller score. If the genuine computation rejects, the outsider has score \(R(e)\), strictly exceeding every proposed-entry score. These statements also hold when one transcript class is empty because \(R(e)>0\).

Thus the constructed threshold instance accepts exactly when \(u\in H\). Its size and construction time are polynomial. Since \(H\) was arbitrary, the reduction establishes the claimed \(\Delta_2^{\mathrm P}\)-hardness under polynomial-time many-one reductions.

The stronger restriction to a fixed query and fixed annotated ontology is justified: the additional context variables occur in the ranking circuit, while the ontology annotations continue to use only the selector \(z\).

5. Running-time bounds

The oracle-call bound follows from the membership construction.

The deterministic enumeration bound correctly accounts for:

The displayed bound
\[ O\!\left( 2^m\left[ \operatorname{poly}(L)+ n^d\left(E(|O|,|q|,n)+\tau\operatorname{poly}(L)\right) \right] +\operatorname{poly}(L) \right) \]
is therefore valid. Scores can remain represented by attained ranking outputs or zero, so enumeration does not force their representations to grow with the number of valuations.

NP membership supplies a deterministic exponential bound of the stated form for \(E\). The expression includes the encoding cost of substituted names, and consistent relabeling is legitimate.

For a fixed query, polynomial KB complexity applies uniformly to its instantiated query pattern. Since \(d\) is fixed, the simplified bound
\[ O\!\left(\tau\,2^m\,|N|^d\,\operatorname{poly}(L)\right) \]
is valid for nonempty \(B\), as explicitly stipulated. Empty \(B\) was already handled separately.

The concluding statements about fixing \(m\) and the query, and about hardness when only the query and ontology are fixed, follow from the established bounds and reduction.

Repair feedback

No repair or additional mathematical clarification is needed. The write-up establishes its claimed classification and supplies valid running-time bounds.

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