← back to the atlas

d4-conf-aaai-2008-0083 (d4-conf-aaai-2008-0083)

Answer: Solvable in deterministic polynomial time in the binary input length.

The anchor (named result in the paper)

Theorem 2 — class: algorithmic

The continuous mirror question, as graded

Given a finite object set \(U\) and a finite support \(T\) with rational masses \(\mu_t>0\) and \(\sum_{t\in T}\mu_t=1\), where each type \(t\) carries an explicitly represented finite strict partial order \(\succ_t\) and a \(k\)-layer contractor \(CON_t\subseteq\succ_t\), compute for every \(t\) an inclusion-minimal \(P^-_t\) satisfying \(CON_t\subseteq P^-_t\subseteq\succ_t\) such that \(\succ_t\setminus P^-_t\) is a strict partial order. Every unit of mass of type \(t\) receives the same contraction.

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

Let \(U\) be a finite object set with \(m=|U|\). A society is given by its support \(T\): the list of its \(\tau=|T|\) types with positive binary rational masses \(\mu_t\), where \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) counts supported types, not all possible types.
Each type supplies a strict partial order \(\succ_t\) and a base contractor \(CON_t\subseteq\succ_t\), both represented explicitly as lists of ordered pairs. An input integer \(k\geq0\) bounds every type's contractor as follows: writing \(D_t=\{y:\exists x\,(x,y)\in CON_t\}\), every directed path in \(\succ_t\cap(D_t\times D_t)\) has at most \(k\) edges.
Compute, for every \(t\in T\), a set \(CON_t\subseteq P^-_t\subseteq\succ_t\) such that \(\succ_t\setminus P^-_t\) is a strict partial order and no proper subset of \(P^-_t\) satisfies these requirements. Every unit of mass of type \(t\) receives this same contraction; any inclusion-minimal choice is allowed. Empty contractors are permitted.
Let \(L\) be the total binary input length; state running times in \(m,\tau,L,k\).

Is this computation solvable in polynomial time in the binary input length, or is it NP-hard?

For an individual explicitly represented relation, a minimal full contractor can be computed in polynomial time; the layered construction terminates within \(k+1\) iterations ([Minimal Contraction of Preference Relations](https://cdn.aaai.org/AAAI/2008/AAAI08-078.pdf)). The extended treatment also gives a polynomial-time algorithm for finite relations ([Contracting preference relations for database applications](https://cse.buffalo.edu/~chomicki/papers-aij10.pdf)). No result explicitly addressing this distribution-over-types formulation was located.

Modeling choices made when packaging the task

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

Resolution

The computation is solvable in deterministic polynomial time in the binary input length. Each explicitly listed supported type can be processed independently. The masses impose no additional constraint on the requested contractions.

Below is a self-contained algorithm and proof. It works for every finite explicitly represented strict partial order, without using the bound \(k\).

1. Reformulation for one type

Fix a type and write \(S=\succ_t\) and \(C=CON_t\). A strict partial order is an irreflexive, transitive relation.

Call a relation \(R\) feasible if

\[ R\subseteq S,\qquad R\cap C=\varnothing,\qquad R\text{ is transitive}. \]

Every feasible \(R\) is irreflexive because \(S\) is irreflexive. Thus \(P=S\setminus R\) is a full contractor exactly when \(R\) is feasible.

Furthermore, complementation within \(S\) reverses inclusion. Consequently, \(P\) is an inclusion-minimal full contractor exactly when \(R\) is an inclusion-maximal feasible relation.

2. Algorithm and correctness

For a relation \(Q\), let \(\operatorname{TC}(Q)\) denote its transitive closure: the pairs connected by directed paths with at least one edge.

Process the edges of \(S\setminus C\) in any fixed order:

Feasibility invariant

Initially, \(R\) is feasible. Suppose it is feasible before processing an edge \(e\).

Because \(R\cup\{e\}\subseteq S\) and \(S\) is transitive, every pair connected by a path in \(R\cup\{e\}\) belongs to \(S\). Hence

\[ H=\operatorname{TC}(R\cup\{e\})\subseteq S. \]

The relation \(H\) is transitive by definition, and therefore irreflexive as a subset of \(S\). If the update is accepted, the test also guarantees \(H\cap C=\varnothing\). A rejected update preserves feasibility trivially.

By induction, the final relation \(R_{\mathrm{fin}}\) is feasible.

Inclusion-maximality

Suppose, for a contradiction, that there is a feasible relation \(R'\) with

\[ R_{\mathrm{fin}}\subsetneq R'\subseteq S. \]

Choose \(e\in R'\setminus R_{\mathrm{fin}}\). Since \(R'\cap C=\varnothing\), this edge belongs to \(S\setminus C\) and was processed.

Let \(R_e\) be the maintained relation just before processing \(e\). The maintained relation only grows, so

\[ R_e\subseteq R_{\mathrm{fin}}\subseteq R'. \]

Because \(e\) is absent from the final relation, its update was rejected. Thus

\[ \operatorname{TC}(R_e\cup\{e\})\cap C\ne\varnothing. \]

But \(R'\) is transitive and contains \(R_e\cup\{e\}\), so it contains that entire transitive closure. This contradicts \(R'\cap C=\varnothing\).

Therefore \(R_{\mathrm{fin}}\) is inclusion-maximal feasible, and \(P=S\setminus R_{\mathrm{fin}}\) is an inclusion-minimal full contractor.

3. Efficient computation of each closure

The transitive closure in each iteration has a particularly simple form. For the edge \(e=(x,y)\), define

\[ A=\{x\}\cup\{a:(a,x)\in R\}, \qquad B=\{y\}\cup\{b:(y,b)\in R\}. \]

Then

\[ \operatorname{TC}(R\cup\{(x,y)\}) = R\cup(A\times B). \]

To prove this identity, first observe that \(S\) contains no directed cycle: transitivity along a cycle would imply a reflexive pair, contradicting irreflexivity.

Every path in \(R\cup\{(x,y)\}\subseteq S\) therefore uses the added edge at most once. A path not using it has its endpoints related by \(R\), because \(R\) is transitive. A path using it consists of an \(R\)-path to \(x\), the edge \((x,y)\), and an \(R\)-path from \(y\), with either surrounding path possibly empty. Its endpoints consequently belong to \(A\) and \(B\).

Conversely, each pair in \(A\times B\) is connected by precisely such a path. This proves the identity.

Using Boolean matrices for \(R\) and \(C\), an iteration therefore:

The check finishes before any insertion, so rejected updates leave \(R\) unchanged.

4. Running time and binary input length

For each supported type, define

\[ r_t=|\succ_t|, \qquad v_t=\bigl|\{u:u\text{ occurs in a pair of }\succ_t\}\bigr|. \]

Objects outside this endpoint set participate in no relation pair and require no computation. In particular,

\[ v_t\le \min\{m,2r_t\}. \]

After assigning integer indices to the listed endpoints, each iteration takes \(O(v_t^2)\) matrix operations. There are at most \(r_t\) iterations, so the total number of operations across types is

\[ O\!\left(L^2+\sum_{t\in T}r_t v_t^2\right). \]

Here \(O(L^2)\) conservatively covers parsing, endpoint indexing, and constructing the matrices. Empty relations are handled directly.

Since \(r_t\le m^2\) and \(v_t\le m\), this gives

\[ O(L^2+\tau m^4) \]

operations, independently of \(k\).

For polynomiality in the binary input length, the stronger bound is useful. Explicit pair lists imply \(\sum_t r_t\le L\), and hence

\[ \sum_t r_t v_t^2 \le L\min\{m,2L\}^2. \]

On a bit-cost random-access model, charging \(O(\log(L+2))\) for operations on compressed indices gives

\[ O\!\left( \left[L^2+L\min\{m,2L\}^2\right]\log(L+2) \right) = O(L^3\log(L+2)). \]

Thus the algorithm is polynomial in \(L\), even if the input describes a large number of isolated objects succinctly. Its output contains only subsets of the input pair lists, so output length is also polynomial.

A bound using the given layer parameter

The cited layered construction gives another bound. Its layer condition is exactly the stated path bound on \(\succ_t\cap(D_t\times D_t)\), and its correctness theorem supplies an inclusion-minimal full contractor. For a nonempty contractor, at most \(\min\{k+1,m\}\) layers need processing. [Mindolin and Chomicki, Theorem 2 and Algorithm 1](https://cdn.aaai.org/AAAI/2008/AAAI08-078.pdf).

A direct Boolean-matrix implementation finds each layer by scanning pairs and computes its added edges by scanning triples. This costs \(O(m^3)\) operations per layer, giving the alternative bit-cost bound

\[ O\!\left( \left[L^2+\tau\min\{k+1,m\}m^3\right]\log(L+2) \right). \]

Empty contractors return \(P^-_t=\varnothing\) immediately. Endpoint compression applies to this implementation as well. In particular, a large binary-encoded \(k\) does not force that many iterations.

5. Applying the algorithm to the society

Run the algorithm once for each of the \(\tau\) listed types and output the resulting \(P^-_t\). Assign that same result to every unit of mass of type \(t\).

Every type’s contractor satisfies all its requirements by the proof above. Since the task contains no constraint relating different types’ choices, their collection is a valid society output. Neither enumerating unsupported types nor performing arithmetic on the masses is necessary.

⟨structured verdict parsed — rendered above⟩

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

The output resolves the assigned task. The algorithm, correctness proof, and polynomial running-time bound are sound. No major or minor mathematical issues were found.

For a fixed type, the definition of feasibility correctly captures the requirements on the retained relation \(R=S\setminus P\). In particular, \(R\subseteq S\) guarantees irreflexivity because \(S\) is irreflexive, and \(R\cap C=\varnothing\) is equivalent to \(C\subseteq P\).

Complementation within the fixed relation \(S\) reverses inclusion. Therefore inclusion-maximality of feasible \(R\) is exactly equivalent to inclusion-minimality of the corresponding full contractor \(P\). The output correctly addresses inclusion-minimality, which is the requirement in the task.

The algorithm processes every edge in \(S\setminus C\), so it considers every edge that could belong to a feasible retained relation.

The assertion \(\operatorname{TC}(R\cup\{e\})\subseteq S\) is justified: all edges of the closure-generating relation belong to \(S\), and transitivity of \(S\) places the endpoints of every positive-length path in \(S\). Consequently, taking the closure cannot introduce reflexive pairs or pairs outside the original preference relation.

An accepted update is transitive and avoids \(C\) by the explicit test. A rejected update preserves the previous feasible relation. The induction proving final feasibility is valid.

The contradiction argument handles arbitrary feasible strict supersets, which is necessary for inclusion-maximality.

If \(e\in R'\setminus R_{\mathrm{fin}}\), then feasibility of \(R'\) ensures \(e\notin C\), so \(e\) was processed. Every accepted closure contains the previous maintained relation; hence the maintained relation grows monotonically.

Since an accepted update would insert \(e\) permanently, its absence from \(R_{\mathrm{fin}}\) proves that its update was rejected. Rejection supplies a forbidden pair in \(\operatorname{TC}(R_e\cup\{e\})\). Transitivity of \(R'\), together with \(R_e\cup\{e\}\subseteq R'\), forces that forbidden pair into \(R'\), contradicting feasibility.

This establishes the claimed maximality and therefore the required minimality of the returned contractor.

The identity
\(\operatorname{TC}(R\cup\{(x,y)\})=R\cup(A\times B)\)
is correct under the maintained hypotheses.

Irreflexivity and transitivity of \(S\) exclude directed cycles. Therefore a path in \(R\cup\{(x,y)\}\subseteq S\) cannot traverse the added edge more than once. Transitivity of \(R\) compresses any nonempty preceding or following segment into the corresponding relation pair. The definitions of \(A\) and \(B\) also include the empty-segment cases.

The converse inclusion follows from the paths described in the output. The formula remains valid when the processed edge already belongs to \(R\).

Because the invariant already gives \(R\cap C=\varnothing\), checking only \((A\times B)\cap C\) is sufficient. Completing that check before insertion correctly preserves the state on rejection.

The endpoint bound \(v_t\leq\min\{m,2r_t\}\) is correct. Scanning predecessor and successor matrix entries, checking the Cartesian product, and inserting accepted pairs cost \(O(v_t^2)\) operations per iteration. There are at most \(r_t\) iterations.

The preprocessing allowance \(O(L^2)\) is sufficient for parsing and indexing explicit endpoint identifiers and initializing the compressed matrices. In particular, \(\sum_t v_t^2\leq4(\sum_t r_t)^2\), so matrix initialization fits within that allowance.

Both subsequent bounds follow correctly:
\(\sum_t r_t v_t^2\leq\tau m^4\) and
\(\sum_t r_t v_t^2\leq L\min\{m,2L\}^2\).
Explicit pair representation justifies \(\sum_t r_t\leq L\).

Compressed matrix addresses and indices have \(O(\log(L+2))\) bits. The stated bit-cost random-access bound \(O(L^3\log(L+2))\) therefore follows. The polynomial conclusion does not require the supplied bound \(k\).

Returning subsets of the input pair lists also gives polynomial output length.

The supplementary citation is accurate. Definition 5 identifies layers using maximum path lengths through contractor destination nodes, and Theorem 2 supplies minimality and termination for a contractor satisfying the layer bound. These hypotheses match the task’s strict partial order and destination-path restriction. [Mindolin and Chomicki, Definition 5, Theorem 2, and Algorithm 1](https://cdn.aaai.org/AAAI/2008/AAAI08-078.pdf).

For a nonempty contractor on a finite universe, the number of layers is bounded by both \(k+1\) and \(m\). The cited algorithm’s layer selection and edge construction permit the claimed pair and triple scans, giving \(O(m^3)\) operations per layer. Endpoint compression supports the stated index-cost accounting when isolated objects are represented succinctly.

This supplementary argument is consistent with the independently proved algorithm.

The task imposes no condition coupling different types’ choices. Processing each listed supported type independently therefore satisfies the entire society requirement. The positive rational masses impose no additional computational constraint, and assigning one result to every unit of the corresponding type meets the assignment requirement.

Empty relations yield the empty contractor. For an empty base contractor, the algorithm retains the entire original relation and returns the empty contractor; the supplementary implementation explicitly handles this case directly. Isolated objects, \(k=0\), and a large binary-encoded \(k\) cause no failure.

No repair or additional clarification is needed.

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