← back to the atlas

d4-conf-aaai-2015-0062 (d4-conf-aaai-2015-0062)

Answer: Polynomial-time solvable.

The anchor (named result in the paper)

Theorem 1 — class: other

PDF text-layer excerpt — equations and symbol order may be approximateLet π be a MAPF problem for which a solution exists (i.e., non-conflicting paths can be assigned), and let R(π) be the corresponding CA problem created by the re- duction, where val(gi) = maxc × |K|. Any allocation for R(π) that maximizes social welfare corresponds to a solu- tion to π that minimizes the sum of path costs.

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

The continuous mirror question, as graded

Given a finite graph \(G=(V,E)\), an explicit finite horizon \(H\), a finite set of routing types \(T\), a rational distribution \(\mu\) over \(T\), type-specific movement costs, and rational per-capita capacities \(\kappa_{v,q}\), let \(\mathcal P_t(H)\) be the legal whole paths for type \(t\), including goal occupancy through \(H\) after arrival. Choose \(x_{t,P}\ge 0\), the fraction of the whole population of type \(t\) assigned to path \(P\), with \(\sum_{P\in\mathcal P_t(H)}x_{t,P}=\mu_t\) and \(\sum_{t,P:(v,q)\text{ is occupied by }P}x_{t,P}\le\kappa_{v,q}\) for every vertex-time pair. Find a feasible assignment minimizing \(\sum_{t\in T}\sum_{P\in\mathcal P_t(H)}x_{t,P}c_t(P)\).

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

Let \(G=(V,E)\) be a finite undirected graph, with \(m=|V|\), and let \(H\ge 0\) be an explicitly given unary horizon.
A society is given by its support: the list of \(\tau\) types with positive binary-rational masses \(\mu_t\), summing to \(1\); \(\tau\) denotes support size, not the number of possible types. Let \(L\) be the total input bit length.
Each type \(t\) specifies a start \(s_t\), a goal \(g_t\), and nonnegative binary-rational costs for traversing each edge and waiting at each vertex. Starts are pairwise distinct, and goals are pairwise distinct; starts may coincide with goals.
A legal path \(P=(v_0,\ldots,v_H)\in\mathcal P_t(H)\) starts at \(s_t\), moves along an edge or waits each step, and reaches \(g_t\) by \(H\). Upon first reaching its goal it stays there through \(H\); \(c_t(P)\) sums action costs before arrival, with subsequent goal occupancy free.
Given binary-rational capacities \(\kappa_{v,q}\ge 0\) for all \(v\in V\) and \(q\in\{0,\ldots,H\}\), assign population masses \(x_{t,P}\ge 0\) satisfying \(\sum_{P\in\mathcal P_t(H)}x_{t,P}=\mu_t\) and \(\sum_t\sum_{P\in\mathcal P_t(H):v_q=v}x_{t,P}\le\kappa_{v,q}\). These vertex-time inequalities are the only interaction constraints; opposite-direction edge traversals are permitted.
The problem is to find a feasible assignment minimizing \(\sum_t\sum_{P\in\mathcal P_t(H)}x_{t,P}c_t(P)\), or report infeasibility.

Is this minimum-cost mass-routing problem solvable in polynomial time in \(m,\tau,H,L\), or is it \(\mathrm{NP}\)-hard?

For feasible discrete instances, welfare maximization with common goal value \(nC\), where \(n\) is the number of agents and \(C\) bounds the largest individual path cost in a minimum-total-cost solution, yields minimum-total-cost routing when ties favor serving more agents. [Source](https://ojs.aaai.org/index.php/AAAI/article/download/9427/9286)
Fractional path-allocation models have also been studied within discrete routing algorithms, with additional edge-conflict constraints and valid inequalities; this is a neighboring formulation. [Source](https://harabor.net/data/papers/llhs-jcor22-bcpfmapf.pdf)
No result settling the exact mass-routing problem stated here was located.

Modeling choices made when packaging the task

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

Result.

The problem is solvable in polynomial time in \(m,\tau,H,L\). A polynomial-size rational linear program represents the path-allocation problem exactly, and an optimal solution can be converted into a polynomial-size list of weighted legal paths.

The construction retains each type separately, so it preserves type-specific costs and goals.

1. A layered network for each type.

Write \(w_t(v)\) for type \(t\)'s waiting cost at \(v\), and \(e_t(\{u,v\})\) for its traversal cost on an edge.

For each type \(t\), define the permitted transitions
\(A_t=\{(u,v):u\ne g_t,\ \text{and either }u=v\text{ or }\{u,v\}\in E\}\cup\{(g_t,g_t)\}\).

Thus, from its goal, a type can only wait. Define transition costs by
\(a_t(g_t,g_t)=0\),
\(a_t(u,u)=w_t(u)\) for \(u\ne g_t\), and
\(a_t(u,v)=e_t(\{u,v\})\) for \(u\ne v\).

For every time \(q\) with \(0\le q<H\), include an arc from \((u,q)\) to \((v,q+1)\) whenever \((u,v)\in A_t\). Every arc advances time, so this network is acyclic.

A network path from \((s_t,0)\) to \((g_t,H)\) corresponds exactly to a legal path in \(\mathcal P_t(H)\): it uses permitted moves or waits, reaches its goal, and cannot subsequently leave. Its arc-cost sum equals \(c_t(P)\), since the action entering the goal is charged and all subsequent waiting is free. This also handles \(s_t=g_t\): the only possible path stays at the goal and has zero cost.

2. The linear program.

Introduce nonnegative variables:

Here \(\mathbf 1_{\{B\}}\) denotes the indicator of a condition \(B\).

Impose the initial and terminal conditions, for every \(t,v\):
\[ y_{t,v,0}=\mu_t\mathbf 1_{\{v=s_t\}}, \qquad y_{t,v,H}=\mu_t\mathbf 1_{\{v=g_t\}}. \]

Impose conservation, for every \(t,v\) and \(0\le q<H\):
\[ \sum_{z:(v,z)\in A_t}f_{t,v,z,q}=y_{t,v,q}, \qquad \sum_{u:(u,v)\in A_t}f_{t,u,v,q}=y_{t,v,q+1}. \]

Finally, impose the given vertex-time capacities, for every \(v,q\):
\[ \sum_t y_{t,v,q}\le\kappa_{v,q}. \]

Minimize
\[ \sum_t\sum_{q=0}^{H-1}\sum_{(u,v)\in A_t} a_t(u,v)f_{t,u,v,q}. \]

There are no constraints coupling opposite-direction traversals, exactly as required.

3. Exact equivalence with path allocation.

*From path allocations to the linear program.*

Given a feasible assignment \(x\), define
\(y_{t,v,q}=\sum_{P\in\mathcal P_t(H):\,v_q=v}x_{t,P}\) and
\(f_{t,u,v,q}=\sum_{P\in\mathcal P_t(H):\,(v_q,v_{q+1})=(u,v)}x_{t,P}\).

Every legal path uses permitted transitions. Its initial and final vertices give the boundary conditions, and its unique transition at each step gives both conservation equalities. The original capacity inequalities give the linear-program capacities.

Moreover, expanding the finite sums gives
\[ \sum_{t,q,(u,v)\in A_t}a_t(u,v)f_{t,u,v,q} =\sum_t\sum_{P\in\mathcal P_t(H)}x_{t,P}c_t(P). \]

Thus the constructed solution has exactly the original objective value.

*From the linear program to path allocations.*

First suppose \(H\ge1\), and fix a type \(t\). Its arc variables form a nonnegative flow from \((s_t,0)\) to \((g_t,H)\), with value \(\mu_t\).

To decompose this flow explicitly, start at \((s_t,0)\) and follow positive-flow arcs. Such an arc exists whenever positive source flow remains. At every reached intermediate node, positive incoming flow and conservation imply positive outgoing flow. Time increases at each step, so the process reaches layer \(H\). The terminal conditions force its endpoint to be \((g_t,H)\).

Let \(\alpha>0\) be the smallest arc flow on this path. Record the path with weight \(\alpha\), and subtract \(\alpha\) from each of its arcs. Conservation remains valid at intermediate nodes, and the remaining source and terminal flows both decrease by \(\alpha\).

Repeat while positive source flow remains. Each iteration makes at least one previously positive arc zero, and subtraction never makes a zero arc positive. Hence the procedure terminates after at most the number of network arcs.

No flow remains when the source flow is zero: summing conservation over successive layers shows that every layer's total arc flow equals the remaining source flow. Consequently, the recorded weights sum to \(\mu_t\), and their paths reproduce every original arc flow and occupancy.

Applying this procedure to every type gives legal path allocations satisfying the original capacities. The same finite-sum identity proves preservation of cost.

For \(H=0\), the two boundary conditions are compatible precisely when \(s_t=g_t\) for every type. The resulting length-zero paths reproduce the occupancies and have zero cost.

Therefore, feasibility and objective values agree in both directions.

4. Polynomial running time and explicit output.

Each type has \(m(H+1)\) nodes and at most \(H(m+2|E|)\) arcs. The linear program therefore has
\(O(\tau m(H+1)+\tau H(m+|E|))\) variables and
\(O(\tau m(H+1)+m(H+1))\) constraints.

Its coefficients consist of the input rationals and constants in \(\{-1,0,1\}\). Replicating input costs across the explicitly given horizon produces only polynomial encoding length. For a simple graph, \(|E|\le m^2\); if edges are explicitly listed with multiplicity, their number is instead bounded by the input length.

The rational linear-programming theorem supplies an algorithm that detects infeasibility or returns an exact optimal rational solution in time polynomial in the program's binary encoding length. This is the standard polynomial-time solvability result for rational linear programming; see [Khachiyan, *Polynomial algorithms in linear programming*](https://www.mathnet.ru/eng/zvmmf5239).

Its hypotheses hold here. Summing conservation over vertices gives \(\sum_v y_{t,v,q}=\mu_t\) at every layer. Nonnegativity consequently bounds every occupancy and arc variable by \(\mu_t\le1\). The feasible region is thus closed and bounded. Whenever it is nonempty, the linear objective attains a finite minimum.

An exact optimal rational solution has polynomial encoding length. Its decomposition uses at most \(H(m+2|E|)\) paths per type, each containing \(H+1\) vertices. The decomposition also takes polynomial time: each iteration traces a path, finds a minimum, and performs rational subtractions. For bit complexity, take the product of the denominators of the computed arc flows as a common denominator. Its bit length is polynomial, and all residual flows and extracted weights remain multiples of its reciprocal.

Thus the algorithm returns an optimal assignment as a polynomial-size list of positive path weights; every unlisted \(x_{t,P}\) is zero.

Allowing mass to split among paths is essential to this conclusion. The flow decomposition produces precisely such an allowed allocation, completing the proof for the stated problem.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the stated problem correctly: the continuous mass-routing problem is polynomial-time solvable. The LP represents the permitted allocations exactly, and the decomposition gives an explicit optimal path allocation of polynomial size. No major or minor mathematical issues were found.

The transition set correctly permits every edge traversal and wait before arrival, while permitting only a self-loop after reaching the type’s goal. Every arc increases time by one, so the network is acyclic.

A network path from \((s_t,0)\) to \((g_t,H)\) therefore corresponds exactly to a legal path: it reaches the goal by the horizon and remains there afterward. Conversely, every legal path uses the specified transitions.

The cost definition correctly charges the action entering the goal and assigns zero cost to subsequent goal occupancy. If \(s_t=g_t\), the permitted transitions force the path to stay at the goal, with zero cost. No arrival convention is lost.

The boundary conditions impose the full mass \(\mu_t\) at the specified start and goal. The two conservation equations connect occupancies to outgoing and incoming transition masses at every applicable layer.

The capacity constraints include every vertex and every time, including times \(0\) and \(H\). Thus initial and final occupancy are constrained exactly as required.

Variables remain indexed by type, preserving type-specific destinations and costs. There are no edge-conflict constraints or integrality requirements. These choices match the task.

The definitions of \(y\) and \(f\) aggregate the supplied path weights correctly. Each path has exactly one vertex at each time and one transition at each step, which verifies both conservation equations and the boundary conditions.

The capacity inequalities are precisely the original inequalities after aggregation. The objective identity follows by rearranging finite sums and using the already verified equality between path cost and arc-cost sum. There is no interchange-of-infinite-sums issue.

For \(H\ge1\), the boundary conditions and conservation give a nonnegative flow of value \(\mu_t\) from the specified source to the specified terminal.

The positive-flow tracing procedure is valid. Positive residual source flow supplies a positive outgoing arc. At an intermediate node reached by a positive arc, conservation supplies a positive outgoing arc. Time strictly increases, so tracing reaches layer \(H\); the terminal conditions exclude every endpoint other than \((g_t,H)\).

Subtracting the minimum arc flow on the traced path preserves nonnegativity and intermediate conservation. It reduces source and terminal flow equally and eliminates at least one positive arc. Consequently, the stated bound on the number of iterations is valid.

The assertion that no residual flow survives after the source flow vanishes is also justified: conservation makes total residual arc flow equal across successive layers, and nonnegativity rules out positive arcs when that total is zero. The extracted paths therefore reproduce all original arc flows. Conservation then identifies their occupancies with the original \(y\) variables, preserving capacities and cost.

When \(H=0\), the initial and terminal equations concern the same occupancy variables. Since every supported mass is positive, these equations are compatible exactly when each type’s start equals its goal.

This statement concerns compatibility of the boundary conditions; capacity feasibility is still enforced by the LP. Whenever the LP is feasible, the length-zero paths reproduce its occupancies and have zero cost. Thus the edge case is handled correctly.

Unreachable goals, insufficient capacities, and horizons too short for arrival produce LP infeasibility by the established equivalence. No separate reachability assumption is needed.

The node and arc bounds are correct: each layer has \(m\) nodes, and each step has at most \(m+2|E|\) transitions per type. The displayed variable and constraint bounds are therefore polynomial. Nonnegativity bounds, if counted separately, also have polynomial size.

Repeating binary-rational coefficients over an explicitly given unary horizon preserves polynomial encoding length. This use of the horizon representation is essential and matches the task.

The invoked rational linear-programming theorem is stated sufficiently precisely for this application: a rational LP can be solved exactly in polynomial bit complexity, with infeasibility detected. The cited reference is [Khachiyan’s polynomial-time linear-programming result](https://www.mathnet.ru/eng/zvmmf5239).

Its application is valid. Summing conservation propagates total occupancy \(\mu_t\) through every layer. Nonnegativity bounds each occupancy and arc flow by \(\mu_t\le1\). The feasible region is closed and bounded, so every feasible instance has an attained finite optimum.

The LP theorem supplies a polynomial-encoding-length exact optimizer. The decomposition extracts at most the number of arcs per type, and each extracted path contains \(H+1\) vertices. The output-size bound is therefore polynomial.

The common-denominator argument is sound: the bit length of the product of all computed arc-flow denominators is bounded by the sum of their bit lengths. Every subtraction and extracted minimum remains a multiple of the reciprocal of this denominator. Residual flows and weights remain bounded, so their numerators also have polynomial bit length. Together with the polynomial iteration count, this verifies polynomial decomposition time.

The proof establishes the requested classification and an explicit output procedure. No additional lemma, clarification, or repair 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.