← back to the atlas

d4-conf-ijcai-2005-0222 (d4-conf-ijcai-2005-0222)

Answer: \(\Delta_2^p\)-complete; in particular, \(\mathrm{NP}\)-hard even when \(\tau=1\).

The anchor (named result in the paper)

Proposition 17 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximate• MERGE(△dD,GMIN) is Θp 2-complete.

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

The continuous mirror question, as graded

Given propositional variables \(P\), a finite support \(T\) of consistent bases \(K_t\) with positive binary-rational masses \(\mu_t\) summing to \(1\), a consistent integrity formula \(\psi\), and a query \(\alpha\), define \(h_w(j)=\sum_{t:\,d_H(w,K_t)=j}\mu_t\) for each world \(w\models\psi\) and \(j=0,\ldots,|P|\), where \(d_H(w,K_t)\) is the minimum Hamming distance from \(w\) to a model of \(K_t\). Select the worlds whose vectors \((h_w(0),\ldots,h_w(|P|))\) are lexicographically maximal; decide whether every selected world satisfies \(\alpha\).

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

Let \(P\) be a finite set of propositional variables and \(m=|P|\). All formulas are explicitly encoded propositional formulas over \(P\). Each base \(K_t\) is a finite consistent set of formulas, interpreted conjunctively; the integrity formula \(\psi\) is consistent, and the query \(\alpha\) is arbitrary.
A society is given by its support: a nonempty list \(T\) of \(\tau\) types with positive masses \(\mu_t\) encoded as binary rationals, with \(\sum_{t\in T}\mu_t=1\). Here \(\tau=|T|\) is the support size, not the number of possible types. Let \(L\) be the total input bit length; state running times in \(m,\tau,L\).
For each world \(w\models\psi\), define \(d_H(w,K_t)=\min_{v\models K_t}d_H(w,v)\), using Hamming distance, and \(h_w(j)=\sum_{t\in T:\,d_H(w,K_t)=j}\mu_t\) for \(j=0,\ldots,m\).
Select all worlds whose vectors \((h_w(0),\ldots,h_w(m))\) are lexicographically maximal, comparing coordinates from zero upward. Retain every tied maximizer. The decision problem asks whether every selected world satisfies \(\alpha\).

Is this decision problem in \(\mathrm{P}\), or is it \(\mathrm{NP}\)-hard?

For finite multisets of bases, selecting integrity-compatible worlds with lexicographically minimal increasingly sorted Hamming-distance lists yields a \(\Delta_2^p\)-complete inference problem ([source](https://www.cril.univ-artois.fr/~marquis/everaere-konieczny-marquis-ijcai05.pdf)).
Related weighted merging work transforms individual distances by source weights before aggregation ([source](https://www.cril.univ-artois.fr/~konieczny/papers/kr23.pdf)); that definition differs from the mass histogram above. No published complexity classification for this exact rational-mass problem was located.

Modeling choices made when packaging the task

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

Result

The problem is \(\mathrm{NP}\)-hard, even when \(\tau=1\), the sole mass is \(1\), the integrity formula has exactly two models, and the query is a single variable.

Moreover, using the multiset hardness theorem stated in the question, the exact rational-mass problem is \(\Delta_2^p\)-complete, where \(\Delta_2^p=\mathrm{P}^{\mathrm{NP}}\). Thus a polynomial-time algorithm would imply \(\mathrm{P}=\mathrm{NP}\).

1. A direct satisfiability reduction

Let \(F(x_1,\ldots,x_n)\) be an arbitrary propositional formula. Introduce fresh variables \(y_1,\ldots,y_n,s,z\), and define

\(\displaystyle D=\bigwedge_{i=1}^{n}\bigl((x_i\vee y_i)\wedge(\neg x_i\vee\neg y_i)\bigr),\qquad R=\bigwedge_{i=1}^{n}(\neg x_i\wedge y_i).\)

Every model of \(D\) makes exactly one variable in each pair \((x_i,y_i)\) true. Consequently, its Hamming distance on these pairs from the all-zero assignment is exactly \(n\).

Use one type of mass \(1\), whose base consists of the single formula

\(\displaystyle K=(s\wedge\neg z\wedge F\wedge D)\ \vee\ (\neg s\wedge z\wedge R).\)

Set

\(\displaystyle \psi=\neg z\wedge\bigwedge_{i=1}^{n}(\neg x_i\wedge\neg y_i),\qquad \alpha=s.\)

The base is consistent: its second disjunct has a model regardless of whether \(F\) is satisfiable. The integrity formula is also consistent and has precisely two models, denoted \(w_0,w_1\), distinguished by \(w_b(s)=b\).

The second disjunct of \(K\) has one model. Its distances from \(w_0,w_1\) are respectively \(n+1,n+2\): there are \(n\) differences on the variable pairs, one on \(z\), and an additional difference on \(s\) for \(w_1\).

The first disjunct has a model exactly when \(F\) is satisfiable. If it does, every such model has distance \(n+1\) from \(w_0\) and distance \(n\) from \(w_1\). Thus:

| Condition | \(d_H(w_0,K)\) | \(d_H(w_1,K)\) |
|---|---:|---:|
| \(F\) satisfiable | \(n+1\) | \(n\) |
| \(F\) unsatisfiable | \(n+1\) | \(n+2\) |

With one type of mass \(1\), a histogram has its sole nonzero coordinate at the distance to that base. Hence the histogram of a smaller-distance world is lexicographically larger.

Therefore, the unique selected world is \(w_1\) when \(F\) is satisfiable, and \(w_0\) otherwise. Since \(\alpha=s\),

\(\displaystyle F\text{ is satisfiable}\quad\Longleftrightarrow\quad\text{every selected world satisfies }\alpha.\)

This is a polynomial-time many-one reduction from satisfiability. It uses \(m=2n+2\), \(\tau=1\), and output length polynomial in the encoding length of \(F\). In particular, hardness does not depend on large support or complicated rational masses.

2. The multiset theorem transfers exactly

The cited paper defines its Hamming-distance Gmin operator by lexicographically minimizing increasingly sorted distance lists, and Proposition 17 states that its inference problem is \(\Delta_2^p\)-complete. Its bases and integrity constraints satisfy the consistency premises used here. [Everaere–Konieczny–Marquis, Definitions 6–7 and Proposition 17](https://www.cril.univ-artois.fr/~marquis/everaere-konieczny-marquis-ijcai05.pdf).

Here is the required equivalence of objectives.

Consider an explicitly listed multiset of \(N\) bases. For a world \(w\), let \(c_w(j)\) be the number of entries at distance \(j\). Let \(w,u\) have different count vectors, and let \(j\) be their first differing coordinate. Suppose \(c_w(j)>c_u(j)\).

Their increasingly sorted lists agree through all distances below \(j\), and then through \(c_u(j)\) occurrences of \(j\). At the next position, \(w\)'s list still contains \(j\), while \(u\)'s contains a strictly larger distance. That next position exists because both lists have length \(N\). Thus \(w\)'s sorted list is lexicographically smaller. Reversing the inequality reverses the comparison; equal count vectors give identical sorted lists.

It follows that lexicographically minimizing the sorted lists is exactly equivalent to lexicographically maximizing the count vectors, including all ties.

To construct a rational-mass instance, group syntactically identical base entries. Give each resulting type mass \(r_t/N\), where \(r_t\) is its multiplicity. Then, for every world and distance,

\(\displaystyle h_w(j)=\frac{c_w(j)}{N}.\)

The selected worlds are therefore exactly the same. All masses are positive and sum to \(1\); their encodings have polynomial length; and grouping requires only syntactic comparisons. The integrity formula and query remain unchanged.

This proves \(\Delta_2^p\)-hardness for the problem in the question.

3. A polynomial-size integer objective

For membership, write each mass as \(\mu_t=p_t/q_t\), with positive integer denominator. Define

\(\displaystyle Q=\prod_{t\in T}q_t,\qquad a_t=p_t(Q/q_t),\qquad B=Q+1.\)

Then each \(a_t\) is a positive integer and

\(\displaystyle \sum_{t\in T}a_t=Q.\)

The binary length of \(Q\) is \(O(L)\), because the denominator encodings are part of the input.

For a world \(w\), define

\(\displaystyle c_w(j)=Qh_w(j),\qquad S(w)=\sum_{j=0}^{m}c_w(j)B^{m-j}=\sum_{t\in T}a_tB^{m-d_H(w,K_t)}.\)

Each coefficient \(c_w(j)\) is an integer between \(0\) and \(Q=B-1\). Consequently, \(S(w)\) encodes the histogram order exactly.

Explicitly, suppose \(j\) is the first differing coordinate and \(c_w(j)>c_u(j)\). The leading difference contributes at least \(B^{m-j}\), while the absolute value of the remaining contribution is at most

\(\displaystyle Q\sum_{r=0}^{m-j-1}B^r=B^{m-j}-1.\)

Therefore \(S(w)>S(u)\). The reverse comparison follows symmetrically, and equal histograms give equal scores. Hence maximizing \(S\) preserves every selected world and every tie.

Also,

\(\displaystyle 0\leq S(w)\leq QB^m.\)

These scores have \(O((m+1)(L+1))\) bits.

4. An \(\mathrm{NP}\) threshold oracle and universal inference

For an integer threshold \(R\), consider the following certificate:

The verifier computes \(e_t=d_H(w,v_t)\) and accepts when

\(\displaystyle U(w,(v_t))=\sum_{t\in T}a_tB^{m-e_t}\geq R.\)

This is a polynomial-time verification: the certificate has \((\tau+1)m\) assignment bits, formula evaluation is polynomial in \(L\), and all arithmetic uses polynomially many bits.

For every certificate,

\(\displaystyle e_t\geq d_H(w,K_t),\qquad U(w,(v_t))\leq S(w).\)

Conversely, because each base is consistent and the set of worlds is finite, nearest models \(v_t\) exist simultaneously. Choosing them gives \(U(w,(v_t))=S(w)\). Therefore,

\(\displaystyle \text{an accepting certificate exists}\quad\Longleftrightarrow\quad \exists w\models\psi:\ S(w)\geq R.\)

Binary search using this \(\mathrm{NP}\) oracle computes

\(\displaystyle M=\max_{w\models\psi}S(w)\)

with \(O((m+1)(L+1))\) oracle calls.

Finally, make one threshold query with the additional requirement \(w\models\neg\alpha\), using threshold \(M\). An accepting certificate satisfies

\(\displaystyle M\leq U(w,(v_t))\leq S(w)\leq M.\)

Thus its world is a selected counterexample to \(\alpha\). Conversely, every selected counterexample admits nearest-model witnesses that meet threshold \(M\).

The answer to the original universal query is therefore “yes” exactly when this final oracle query answers “no.” This proves membership in \(\mathrm{P}^{\mathrm{NP}}=\Delta_2^p\).

5. Running times and conclusion

The oracle algorithm uses \(O((m+1)(L+1))\) \(\mathrm{NP}\) queries and polynomial additional time in \(m,\tau,L\). This bound uses the input support directly; it never expands rational masses into a multiset.

An elementary deterministic algorithm enumerates worlds and base models, computes all minimum distances, and compares exact integer histograms. A conservative bit-operation bound is

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

Combining Sections 2 and 4 gives \(\Delta_2^p\)-completeness. Independently, Section 1 establishes the requested \(\mathrm{NP}\)-hardness without relying on a published merging classification.

⟨structured verdict parsed — rendered above⟩

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

The prover’s argument is correct and resolves the assigned question. It establishes \(\mathrm{NP}\)-hardness by a direct reduction and, using the cited multiset theorem, establishes \(\Delta_2^p\)-completeness. No major or minor mathematical issues were found.

1. Direct satisfiability reduction

Construction and promises. The intended variable set is precisely the original variables together with the fresh variables introduced in the construction, giving \(m=2n+2\). Both constructed formulas have polynomial encoding length.

The formula \(D\) enforces exactly one true variable in each pair \((x_i,y_i)\). Consequently, every assignment satisfying \(D\) differs from the all-zero assignment on exactly \(n\) pair coordinates.

The second disjunct of \(K\) fixes every variable: \(s=0\), \(z=1\), and each pair to \((0,1)\). It therefore has exactly one model and guarantees consistency of the base independently of \(F\). The integrity formula fixes all variables except \(s\), so it has exactly the two claimed models.

Distance calculations. All four distances in the table are correct:

The first disjunct is satisfiable exactly when \(F\) is satisfiable: the pair constraints permit every assignment of the original variables, with corresponding complementary values of the fresh variables. Taking the minima over the two disjuncts yields exactly the displayed table.

Selection and reduction direction. With one type of mass \(1\), each histogram has one nonzero coordinate. At the smaller of two distinct distances, the smaller-distance world has coordinate \(1\), while the other has coordinate \(0\). Thus smaller distance means lexicographically larger histogram.

The selected world is consequently unique in both cases, and the claimed equivalence between satisfiability of \(F\) and universal satisfaction of \(s\) holds. This is a valid polynomial-time many-one reduction, with no reliance on vacuous universal inference or violated consistency promises.

2. Transfer of the multiset theorem

External theorem. The citation is accurate. The paper’s preliminaries require consistent bases and a consistent integrity formula; Definitions 6–7 use minimum distance to base models and increasingly sorted distance lists; Proposition 17 states \(\Delta_2^p\)-completeness for Hamming-distance Gmin inference. The cited inference question is entailment by the merged result, matching universal satisfaction over selected worlds. [Everaere–Konieczny–Marquis](https://www.cril.univ-artois.fr/~marquis/everaere-konieczny-marquis-ijcai05.pdf).

Equivalence of objectives. The first-differing-coordinate argument is valid. Equal counts below \(j\) give an identical initial segment of the sorted lists. After the common occurrences of \(j\), the list with more occurrences of \(j\) is strictly smaller lexicographically. The next position exists: the greater count means that the common prefix has length strictly less than \(N\).

Equal count vectors give identical lists, so ties are preserved.

Encoding transformation. Grouping syntactically identical entries requires no logical-equivalence test. The masses \(r_t/N\) are positive, sum to \(1\), and have polynomial encoding length. The identity \(h_w(j)=c_w(j)/N\) holds for every world and coordinate. Hence the transformation preserves both selected worlds and the inference answer.

The claimed hardness transfer is justified.

3. Integer objective

Denominator clearing. Since every \(q_t\) divides \(Q\), each \(a_t\) is a positive integer. The normalization of the input masses implies \(\sum_t a_t=Q\). The binary length of the product \(Q\) is bounded by the total denominator encoding length, hence is \(O(L)\).

Order preservation. Every coefficient lies between \(0\) and \(Q=B-1\). At the first differing coordinate, the leading contribution is at least \(B^{m-j}\), whereas the stated bound on the absolute tail is exactly \(B^{m-j}-1\). Therefore the sign of the score difference agrees with the lexicographic comparison. Equality and all ties are also preserved.

The bound \(S(w)\leq QB^m\) is valid because the coefficients sum to \(Q\). The resulting score bit length is \(O((m+1)(L+1))\).

4. Oracle membership and universal inference

Certificate size and verification. The certificate contains \((\tau+1)m\) assignment bits. Checking the formulas, calculating Hamming distances, and evaluating the integer expression all take polynomial time in \(m,\tau,L\).

Threshold equivalence. Every witness distance is at least the corresponding minimum distance. Since \(B>1\) and all weights are positive, this gives \(U\leq S(w)\). Conversely, consistent finite bases have nearest models, and the witnesses can be chosen independently for all types. Those choices attain \(U=S(w)\).

Thus the threshold predicate is indeed in \(\mathrm{NP}\); the verifier need not certify that its witnesses are nearest models.

Optimization and inference. Consistency of \(\psi\) ensures a nonempty optimization domain. Binary search over the stated integer range uses the claimed number of oracle calls. For the final query, imposing \(\neg\alpha\) and threshold \(M\) forces \(U=S(w)=M\). Conversely, each selected counterexample supplies an accepting certificate.

Negating this final oracle answer is permitted in deterministic polynomial time with an \(\mathrm{NP}\) oracle. Membership in \(\Delta_2^p\) follows.

5. Running times and edge cases

The oracle-call count and polynomial additional-time claim are consistent with the certificate and score sizes. The conservative deterministic bound \(O(4^m(m+\tau+L+1)^3)\) accommodates enumeration of world/model pairs, formula evaluation, distance calculations, and exact histogram arithmetic.

The argument also accommodates \(m=0\), empty bases interpreted conjunctively, equal histograms, and queries with no countermodels. No additional mathematical 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.