Answer: Polynomial-time solvable, with a topological ordering returned on every yes-instance.
Proposition 2 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateGiven a set of locally consistent preferences P, checking for the cc-acyclic sufficient conditions can be done in polynomial time.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given \(m\) attributes, \(\tau\) types with positive rational masses \(\mu_t\) summing to \(1\), and a complete CP-theory \(P_t\) for each type, form \(P_\mu=\bigcup_{t:\mu_t>0}P_t\). Under the promise that \(P_\mu\) is locally consistent, decide whether \(H(P_\mu)\) is acyclic and, if so, return a topological ordering.
Let \(V\) be a set of \(m\) attributes, each with an explicitly listed finite nonempty domain \(D_X\).
A society is given by its support: a list of \(\tau\) types with positive binary rational masses \(\mu_t\) summing to \(1\). Here \(\tau\) is the support size, not the number of possible types; \(L\) is the total input bit length.
Each type supplies its entire CP-theory \(P_t\) as an explicit finite list of statements \(\rho:X=x\succ X=x'[\Omega]\), where \(x,x'\in D_X\) are distinct, \(\rho\) is a partial assignment, and \(\operatorname{var}(\rho),\{X\},\Omega\subseteq V\) are pairwise disjoint. The statement prefers \(x\) to \(x'\) in context \(\rho\), allowing attributes in \(\Omega\) to vary while all remaining attributes stay equal.
Set \(P_\mu=\bigcup_{t:\mu_t>0}P_t\). Promise local consistency: for each attribute \(X\) and each full assignment to \(V\setminus\{X\}\), the directed graph on \(D_X\) containing \(x\to x'\) for every statement about \(X\) whose context is satisfied is acyclic.
For any statement set \(P\), define \(E_C(P)=\{(Y,X):\exists(\rho:X=x\succ X=x'[\Omega])\in P,\ Y\in\operatorname{var}(\rho)\}\) and \(E_R(P)=\{(X,Z):\exists(\rho:X=x\succ X=x'[\Omega])\in P,\ Z\in\Omega\}\).
For \((Y,X)\in E_C(P)\), let \(c_P(Y,X)=|\{\rho(Y): (\rho:X=x\succ X=x'[\Omega])\in P,\ Y\in\operatorname{var}(\rho)\}|\). Define \(H(P)=(V,E_R(P)\cup\{(Y,X)\in E_C(P):c_P(Y,X)\geq2\})\).
Decide whether \(H(P_\mu)\) is acyclic and, if so, return a topological ordering of its attributes; any topological ordering is acceptable.
Is this promised decision problem solvable in time polynomial in \(m,\tau,L\), with a topological ordering returned on yes-instances, or is it NP-hard?
Known for discrete inputs: checking acyclicity of \(H(P)\) for an explicitly listed, locally consistent CP-theory is polynomial-time, with the stated bound \(O(m|P|+m)\). The supplied result does not separately formulate a society with rational masses.
The promised problem is solvable in polynomial time, with a topological ordering returned on every yes-instance. The rational masses cause no additional difficulty: every listed type has positive mass, so \(P_\mu=\bigcup_{t=1}^{\tau}P_t\).
In fact, the algorithm below works without the local-consistency promise.
For each ordered pair of attributes \((Y,X)\), maintain a register \(a(Y,X)\), initially empty, and a Boolean flag \(b(Y,X)\), initially false. Also maintain an initially empty directed graph \(G\) on \(V\).
Scan every statement \(\rho:X=x\succ X=x'[\Omega]\) in every listed type:
After the scan, insert \((Y,X)\) into \(G\) for every pair whose flag \(b(Y,X)\) is true.
Duplicates need not be removed: repeated occurrences of the same context value do not set a flag.
The edges inserted in step 1 are exactly \(E_R(P_\mu)\), by its definition.
For an ordered pair \((Y,X)\), define
\(S_{Y,X}=\{\rho(Y):(\rho:X=x\succ X=x'[\Omega])\in P_\mu,\ Y\in\operatorname{var}(\rho)\}\).
Thus, whenever \((Y,X)\in E_C(P_\mu)\), its cardinality is \(c_{P_\mu}(Y,X)\).
If \(S_{Y,X}\) is empty, the register remains empty and the flag remains false. Otherwise, the register stores the first encountered member of \(S_{Y,X}\). The flag becomes true exactly when some encountered member differs from that first member. Consequently,
\(b(Y,X)=\mathrm{true}\) if and only if \(|S_{Y,X}|\geq 2\).
The edges inserted after the scan are therefore exactly the context edges satisfying the required threshold. Hence \(G=H(P_\mu)\).
Repeatedly remove a vertex of indegree zero from the current graph, appending it to an output list and updating the remaining indegrees.
If all vertices are removed, return yes and the output list. For any edge \((U,W)\), the vertex \(W\) cannot be removed while \(U\) remains, because that edge would give \(W\) positive indegree. Thus every edge points forward in the returned list, proving that it is a topological ordering.
If the procedure stops with vertices remaining, return no. Every remaining vertex then has an incoming edge from another remaining vertex. Starting at any such vertex and repeatedly choosing an incoming predecessor produces a repeated vertex, since the remaining graph is finite. The segment between repetitions gives a directed cycle. Thus the rejection is correct.
All statements and all context and importance-set entries are explicitly present in the input. Their total number is bounded by a constant multiple of \(L\). Attribute and domain-value identifiers can be normalized against the explicitly listed attributes and domains using polynomial-time string comparisons; each encoded identifier has length at most \(L\).
After normalization, the construction uses at most \(m^2\) registers, \(m^2\) flags, and an \(m^2\)-entry adjacency matrix. Each listed context or importance-set entry requires only a constant number of register comparisons or graph updates. Register comparisons have polynomial bit cost because their stored values come from the input.
With the adjacency matrix, computing indegrees and performing all removals takes \(O(m^2)\) graph operations. Indegrees have \(O(\log(m+1))\) bits. These bounds, together with polynomial-time input normalization, establish a running time polynomial in \(m,\tau,L\).
No rational arithmetic is needed: under the promise that all listed masses are positive, the graph depends only on the listed statements. This directly settles the society formulation without requiring a separate extension of the supplied theorem.
⟨structured verdict parsed — rendered above⟩
The prover’s claim is correct. The algorithm constructs exactly \(H(P_\mu)\), correctly decides acyclicity, and returns a topological ordering on yes-instances. Its running time is polynomial in the stated input parameters. No mathematical or complexity gaps require repair.
Every listed mass is positive, so the equality \(P_\mu=\bigcup_{t=1}^{\tau}P_t\) follows directly from the definition. The numerical magnitudes of the masses do not affect the requested graph. Omitting rational arithmetic is justified under the input promises.
Step 1 inserts \((X,Z)\) precisely when a listed statement about \(X\) contains \(Z\in\Omega\). These are exactly the edges of \(E_R(P_\mu)\). Repeated statements or repeated edge insertions do not change the adjacency matrix.
For each pair \((Y,X)\), the register stores the first encountered context value for \(Y\) in a statement about \(X\). The flag becomes true precisely when a different value is encountered. Thus its final value is true exactly when \(\lvert S_{Y,X}\rvert\geq 2\).
This handles all relevant cases: no occurrences, occurrences with only one distinct value, and occurrences with at least two distinct values. Repeated occurrences cannot incorrectly trigger the flag.
Whenever \(\lvert S_{Y,X}\rvert\geq 2\), the pair necessarily belongs to \(E_C(P_\mu)\), and its count is \(c_{P_\mu}(Y,X)=\lvert S_{Y,X}\rvert\). Therefore the edges inserted after scanning are exactly the context edges required by the definition of \(H(P_\mu)\). Together with the importance edges, this establishes \(G=H(P_\mu)\).
The removal procedure maintains indegrees in the remaining graph. A vertex cannot be removed while an incoming predecessor remains. Consequently, if all vertices are removed, every edge points forward in the output list. The returned list is a valid topological ordering.
If removal stops before exhausting the graph, every remaining vertex has an incoming predecessor among the remaining vertices. The finite predecessor sequence must repeat a vertex, giving a directed cycle as claimed. Thus rejection is correct. Isolated vertices and an empty attribute set, if permitted, are also handled by the procedure.
Explicit listing bounds the number of scanned entries by the input length. Normalization through polynomial-time string comparisons is sufficient; no constant-time assumption about arbitrary encoded identifiers is needed.
The registers, flags, and adjacency matrix require polynomial space. Processing entries has polynomial bit cost. Computing indegrees and removing vertices with an adjacency matrix takes \(O(m^2)\) graph operations, and the indegrees have the stated logarithmic bit size. These bounds establish polynomial running time in \(m,\tau,L\).
The algorithm does not test or rely on local consistency. Its correctness follows from the graph definitions alone, so the stronger claim that it works without that promise is supported. The supplied discrete theorem is not invoked, and no unverified theorem application remains.
Repair feedback: None required.
⟨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.