← back to the atlas

d4-conf-ijcai-2018-0115 (d4-conf-ijcai-2018-0115)

Answer: Polynomial-time solvable; a conservative bit-complexity bound is \(O(\tau^2(m+1)L^4)\).

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe computation time of the proposed LpDis algorithm is polynomial, quadratic, in the size of the input, i.e., the size of the two LP-trees.

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

The continuous mirror question, as graded

Given two finite distributions \(\mu\) and \(\nu\) over complete LP-tree types with rational masses, compute the exact value \(\Delta(\mu,\nu)=\sum_{T,U}\mu_T\nu_U d_K(T,U)\), where \(d_K(T,U)\) counts outcome pairs on which the two trees disagree.

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

Let \(m\geq 1\) attributes have explicitly listed, finite nonempty domains \(D_1,\ldots,D_m\), shared by all types; outcomes form \(\mathcal O=\prod_{i=1}^{m}D_i\).
A complete LP-tree is an explicitly represented rooted tree with one attribute at each node and every attribute occurring exactly once on each root-to-leaf path. A nonleaf node labelled \(X_i\) has either one unconditional outgoing edge or one outgoing edge for each value in \(D_i\), labelled by that value.
Each node has an explicit conditional preference table: for every assignment to a specified subset of its ancestor attributes, it lists a strict total order on the node's domain. To compare distinct outcomes, traverse using their common values until the first differing attribute; its applicable local order decides the comparison, inducing \(\succ_T\).
A society is given by its support: a list of types with positive binary rational masses. The input consists of two such societies \(\mu,\nu\), each of total mass \(1\); let \(\tau=|\operatorname{supp}(\mu)\cup\operatorname{supp}(\nu)|\), the joint support size, not the number of possible LP-tree types. Let \(L\) be the total binary input length, including domains, trees, tables, and masses; state running times in \(m,\tau,L\).
Let \(d_K(T,U)\) be the unnormalized number of unordered pairs of distinct outcomes ranked oppositely by \(\succ_T\) and \(\succ_U\), and define \(\Delta(\mu,\nu)=\sum_{T\in\operatorname{supp}(\mu)}\sum_{U\in\operatorname{supp}(\nu)}\mu_T\nu_U d_K(T,U)\).

Is computing the exact rational value \(\Delta(\mu,\nu)\) possible in polynomial time in \(m,\tau,L\), or is it NP-hard?

For two explicitly represented complete LP-trees, exact Kendall distance has an algorithm with a stated quadratic bound in their representation sizes ([Li and Kazimipour](https://www.ijcai.org/proceedings/2018/0262.pdf)).
No result specifically treating the distribution problem defined here was located in the literature search.

Modeling choices made when packaging the task

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

Conclusion

The exact value \(\Delta(\mu,\nu)\) is computable in polynomial time in \(m,\tau,L\). A conservative bound, using ordinary binary arithmetic, is \(O\!\left(\tau^2(m+1)L^4\right)\).

The key is that the supports are explicitly listed: the definition requires at most \(\tau^2\) pairwise distances, followed by an exact weighted sum.

1. Applying the pairwise algorithm

Write \(S_\mu=\operatorname{supp}(\mu)\) and \(S_\nu=\operatorname{supp}(\nu)\). Then \(|S_\mu||S_\nu|\leq\tau^2\).

Li and Kazimipour’s Theorem 1 establishes correctness of their exact Kendall-distance algorithm, and Theorem 2 states a quadratic bound in the explicitly represented tree sizes. Their model permits multi-valued domains, conditional preferences, and different attribute orders and branching structures. Thus it covers the complete LP-trees in this question: every attribute occurs once on each path, and preference tables explicitly list orders conditioned on ancestor attributes. Their distance counts unordered outcome pairs, matching \(d_K\). [Li and Kazimipour, Sections 2–4](https://www.ijcai.org/proceedings/2018/0262.pdf).

Consequently, compute \(k_{T,U}=d_K(T,U)\) for every \(T\in S_\mu\) and \(U\in S_\nu\). No enumeration of other LP-tree types is needed.

2. Bit lengths of the distances

Put \(d_i=|D_i|\) and \(N=|\mathcal O|=\prod_{i=1}^m d_i\). Because the domains are explicitly listed, \(\sum_i d_i=O(L)\). Hence

\(\log_2 N=\sum_{i=1}^m\log_2 d_i\leq\sum_{i=1}^m d_i=O(L).\)

Every distance satisfies

\(0\leq k_{T,U}\leq\binom{N}{2},\)

so its binary representation has \(O(L)\) bits, even when \(N\) is exponential in the input length.

The pairwise algorithm computes counts through local disagreements, products of domain cardinalities, and sums over disjoint classes of outcome pairs. Its counting formulas use domain cardinalities with exponents at most two. These quantities have \(O(L)\) bits: a product with those exponents is at most \(N^2\), and accumulated distances are at most \(\binom{N}{2}\).

Thus the stated quadratic counting bound also yields a polynomial bit-complexity bound. More explicitly, each tree has representation size at most \(L\). Allowing an additional factor \(m+1\) for processing attribute sets and products, and \(O(L^2)\) for schoolbook arithmetic on \(O(L)\)-bit integers, gives the conservative bound

\(O\!\left((m+1)L^4\right)\)

per pair of trees. All cross-support distances therefore take

\(O\!\left(\tau^2(m+1)L^4\right)\)

bit operations.

If \(N=1\), there are no distinct outcome pairs and every distance is zero; this case is immediate.

3. Computing the rational weighted sum exactly

Write the input masses as

\(\mu_T=p_T/q_T,\qquad \nu_U=r_U/s_U,\)

where all numerators and denominators are positive integers encoded in binary. Define

\(Q_\mu=\prod_{T\in S_\mu}q_T,\qquad Q_\nu=\prod_{U\in S_\nu}s_U.\)

Since the total encoding length of the denominators is at most \(L\), both products have \(O(L)\) bits. Define integer weights

\(a_T=p_T(Q_\mu/q_T),\qquad b_U=r_U(Q_\nu/s_U).\)

The divisions are exact because each denominator is a factor of its corresponding product. The total-mass assumptions give

\(\sum_{T\in S_\mu}a_T=Q_\mu,\qquad \sum_{U\in S_\nu}b_U=Q_\nu.\)

Now compute the integer

\(A=\sum_{T\in S_\mu}\sum_{U\in S_\nu}a_Tb_Uk_{T,U}.\)

Substitution into the definition proves

\(\Delta(\mu,\nu)=\dfrac{A}{Q_\mu Q_\nu}.\)

There is no problematic denominator growth. Indeed, nonnegativity and the distance bound imply

\(0\leq A\leq\binom{N}{2}\sum_{T,U}a_Tb_U =\binom{N}{2}Q_\mu Q_\nu.\)

Therefore \(A\), the denominator, and every partial sum have \(O(L)\) bits. Constructing the common denominators and integer weights, evaluating the at most \(\tau^2\) summands, and reducing the final fraction by a greatest common divisor all take polynomial time. With schoolbook arithmetic, a sufficient bound for this stage is \(O(\tau^2L^2+L^3)\).

4. Final complexity classification

Combining the two stages proves the bound

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

This resolves the stated problem as polynomial-time solvable. A separate literature result about distributions is unnecessary: explicit support makes the distribution computation a polynomial number of applications of the pairwise algorithm, followed by polynomial-time exact rational arithmetic.

⟨structured verdict parsed — rendered above⟩

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

Verification result

The polynomial-time conclusion is proved. The argument resolves USER_TASK, including exact rational output and a polynomial bit-operation bound. I found no major or minor issue requiring repair.

1. Scope and number of distance computations

The prover correctly uses the explicitly listed supports rather than the space of all possible types.

Since both supports are subsets of their union,

\[ |S_\mu||S_\nu|\leq \tau^2. \]

Computing one distance for each cross-support pair therefore requires at most \(\tau^2\) applications of the pairwise algorithm. This reasoning does not require identifying or enumerating types outside the input.

The two societies have positive masses and total mass one, so their supports are nonempty. Consequently, \(\tau\geq 1\), as needed when absorbing subsequent overhead into the final bound.

2. Applicability of the cited theorem

The cited paper permits multivalued domains, conditional local preferences, and differing attribute orders and branching structures. Its comparison semantics agree with the task, and its disagreement sets contain unordered outcome pairs. Theorem 1 identifies the algorithm’s output with the exact disagreement count; Theorem 2 states the quadratic representation-size bound. Thus the cited result applies to the stipulated pairwise problem. [Li and Kazimipour, Sections 2–4](https://www.ijcai.org/proceedings/2018/0262.pdf).

The prover’s use of this result is also consistent with the pairwise algorithm explicitly supplied in USER_TASK. No theorem about distributions is necessary: the distribution computation is the finite weighted sum already specified in the task.

Finding: The theorem application is justified; there is no domain, representation, or normalization mismatch.

3. Bit lengths of outcomes and distances

The domains are explicitly listed, so the assertion \(\sum_i d_i=O(L)\) is valid under the stated binary input encoding. The calculation

\[ \log_2 N=\sum_i\log_2 d_i\leq\sum_i d_i=O(L) \]

is correct for every positive integer \(d_i\), including \(d_i=1\).

Every distance counts a subset of the unordered pairs of distinct outcomes. Therefore,

\[ 0\leq k_{T,U}\leq\binom{N}{2}, \]

and its binary encoding has \(O(L)\) bits. Zero is understood to have a constant-length encoding; taking its logarithm is unnecessary.

Finding: Exponentially many outcomes do not cause exponentially long distance outputs.

4. Pairwise bit complexity

The prover does not infer small intermediate values merely from a small final output. It identifies the counting operations used by the algorithm.

The cited counting formulas use local disagreement counts, domain-cardinality products, and additions of disjoint pair counts. Their cardinality factors have exponents at most two, supporting the asserted \(O(L)\) intermediate bit lengths. [Li and Kazimipour, Equations 3–4](https://www.ijcai.org/proceedings/2018/0262.pdf).

Each tree’s explicit representation size is at most \(L\). Applying the quadratic counting bound, allowing the stated factor \(m+1\) for attribute processing, and charging \(O(L^2)\) for arithmetic gives the conservative per-pair bound

\[ O\!\left((m+1)L^4\right). \]

This is an upper bound rather than a claim of optimality.

Finding: The conversion to polynomial bit complexity is justified.

5. Exact rational aggregation

All denominator products are positive. Their binary lengths are bounded by the total lengths of their constituent denominators, hence by \(O(L)\).

The definitions

\[ a_T=p_T(Q_\mu/q_T),\qquad b_U=r_U(Q_\nu/s_U) \]

produce positive integers because the indicated divisions are exact. They also satisfy

\[ \mu_T=\frac{a_T}{Q_\mu},\qquad \nu_U=\frac{b_U}{Q_\nu}. \]

The identities

\[ \sum_T a_T=Q_\mu,\qquad \sum_U b_U=Q_\nu \]

follow directly from the two total-mass assumptions. Substitution into the original definition therefore verifies

\[ \Delta(\mu,\nu)=\frac{A}{Q_\mu Q_\nu}. \]

This remains valid when fractions are initially unreduced, denominators share factors, or a type appears in both societies.

Finding: The integer aggregation computes exactly the requested rational value.

6. Numerator growth and arithmetic cost

The bound

\[ 0\leq A\leq\binom{N}{2}Q_\mu Q_\nu \]

correctly uses nonnegativity and the mass identities. Its right-hand side has \(O(L)\) bits. Every partial sum is between zero and \(A\), so partial sums satisfy the same bit-length bound. Individual summands also satisfy it.

The asserted aggregation cost

\[ O(\tau^2L^2+L^3) \]

is sufficient for the stated products, exact divisions, summands, and final greatest-common-divisor reduction using ordinary binary arithmetic.

Finding: There is no uncontrolled denominator or numerator growth.

7. Edge cases and final bound

The prover explicitly handles \(N=1\): every distance and the requested expectation are zero. Singleton domains mixed with larger domains likewise cause no failure in the counting or arithmetic bounds. Identical trees and zero pairwise distances are also allowed.

Combining the two stages gives

\[ O\!\left(\tau^2(m+1)L^4\right). \]

The aggregation overhead is absorbed because \(m\geq1\), \(\tau\geq1\), and \(L\geq1\).

Actionable feedback: No additional lemma or clarification is required. The output establishes exact polynomial-time computability under the explicit representation required by USER_TASK.

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