← back to the atlas

Winner Robustness via Swap- and Shift-Bribery: Parameterized Counting Complexity and Experiments (d4-conf-ijcai-2021-0592)

Answer: Deterministic polynomial time in \(m,\tau,L,\log(1/\varepsilon)\), including exact identification of \(-\infty\).

The anchor (named result in the paper)

Theorem 1 — class: hardness

PDF text-layer excerpt — equations and symbol order may be approximatePLURALITY #SWAP-BRIBERY is #P-hard and #W[1]-hard when parameterized by the swap radius, even for unit prices.

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

The continuous mirror question, as graded

Given \(m\) candidates, a rational distribution \(\mu\) over ranking types \(\sigma\in S_m\), target \(p\), and rational normalized radius \(\rho\), take \(N\)-voter realizations with \(N\mu_\sigma\in\mathbb{Z}\) and uniformly count labelled final profiles at exact swap distance \(N\rho\). Compute or approximate \(\Lambda_p(\mu,\rho)=\lim_{N\to\infty}N^{-1}\log P_{p,N}(N\rho)\), equivalently the maximum entropy of feasible mass transfers making \(p\) a Plurality winner minus the unconstrained maximum.

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

Let \(C\) contain \(m\ge 2\) candidates, with designated candidate \(p\). Rankings are strict total orders, identified with \(S_m\).
A society is given by its support \(T\): the list of the \(\tau\) types with positive mass, each mass \(\mu_\sigma\) a binary rational, with \(\sum_{\sigma\in T}\mu_\sigma=1\). Thus \(\tau=|T|\), not \(m!\). Let \(L\) be the input bit length.
Write \(d(\sigma,\pi)\) for Kendall swap distance and \(M=\binom m2\). The normalized radius is a binary rational \(\rho\in[0,1]\); an \(N\)-voter realization has exact total distance \(NM\rho\). Count labelled final profiles uniformly, rather than swap sequences.
A mass transfer is an array \(x_{\sigma\pi}\ge0\), indexed by \(\sigma\in T\) and \(\pi\in S_m\). Let \(U\) consist of arrays satisfying \(\sum_\pi x_{\sigma\pi}=\mu_\sigma\) and \(\sum_{\sigma,\pi}d(\sigma,\pi)x_{\sigma\pi}=M\rho\).
For \(c\in C\), put \(s_c(x)=\sum_{\sigma,\pi:\pi(1)=c}x_{\sigma\pi}\), where \(\pi(1)\) is the top candidate. Let \(W=\{x\in U:s_p(x)\ge s_c(x)\text{ for all }c\in C\}\); tied Plurality winners count as winners.
Define \(H(x)=-\sum_{\sigma,\pi}x_{\sigma\pi}\log(x_{\sigma\pi}/\mu_\sigma)\), using natural logarithms and \(0\log0=0\), and \(\Lambda_p(\mu,\rho)=\max_{x\in W}H(x)-\max_{x\in U}H(x)\), with \(\Lambda_p=-\infty\) when \(W=\varnothing\).
The labelled-profile rate is interpreted along \(N=kD\), where \(D\) is a common denominator of the input masses, \(M\rho\), and every coordinate of every vertex of \(U\) and \(W\), omitting \(W\) if empty.
Given binary rational \(0<\varepsilon<1\), is computing \(\Lambda_p\) to additive error \(\varepsilon\), including identifying \(-\infty\), possible in time polynomial in \(m,\tau,L,\log(1/\varepsilon)\), or is this problem NP-hard?
Discrete unit-price Plurality swap-bribery counting is \(\#\mathrm P\)-hard and \(\#\mathrm W[1]\)-hard parameterized by the exact swap radius. [Source](https://arxiv.org/pdf/2010.09678).
No result settling this continuous entropy-rate problem was identified in the literature search.

Modeling choices made when packaging the task

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

1. Result

The problem is polynomial-time solvable. There is a deterministic algorithm that identifies whether \(\Lambda_p=-\infty\), and otherwise outputs a rational \(\widehat\Lambda_p\) satisfying \(\lvert\widehat\Lambda_p-\Lambda_p\rvert\le\varepsilon\), in time polynomial in \(m,\tau,L,\log(1/\varepsilon)\).

The proof has two parts: an exact aggregation into polynomially many variables, followed by entropy optimization with polynomial dependence on the requested number of precision bits.

2. Counting rankings with a prescribed top candidate and distance

For \(\sigma\in T\) and \(c\in C\), let \(r_\sigma(c)\) be the position of \(c\) in \(\sigma\), numbered from \(1\).

Let \(A_{h,j}\) denote the number of permutations of \(h\) elements having exactly \(j\) inversions. Set \(A_{0,0}=1\), and set \(A_{h,j}=0\) outside the possible inversion range. Inserting the largest element into a permutation of \(h-1\) elements creates any number of additional inversions from \(0\) through \(h-1\), exactly once for each insertion position. Consequently,

\(A_{h,j}=\displaystyle\sum_{\ell=0}^{h-1}A_{h-1,j-\ell}.\)

This recurrence computes all required values for \(h\le m-1\) using polynomially many integer operations. Every entry is at most \((m-1)!\), so its binary encoding has length \(O(m\log m)\).

Define

\(a_{\sigma c k}=\bigl|\{\pi\in S_m:\pi(1)=c,\ d(\sigma,\pi)=k\}\bigr|.\)

Lemma. For every \(\sigma,c,k\),

\(a_{\sigma c k}=A_{m-1,k-r_\sigma(c)+1}.\)

Proof. Kendall distance equals the number of candidate pairs whose relative order differs between the two rankings. If \(\pi(1)=c\), the pairs involving \(c\) contribute exactly \(r_\sigma(c)-1\): precisely the candidates preceding \(c\) in \(\sigma\) change their relative order with \(c\).

The remaining contribution is the inversion count of the suffix of \(\pi\), relative to the order obtained by deleting \(c\) from \(\sigma\). Relabelling these remaining candidates by their positions in that order gives a bijection with permutations of \(m-1\) elements. Hence the suffix must have exactly \(k-r_\sigma(c)+1\) inversions. This proves the formula. \(\square\)

Thus all cell multiplicities \(a_{\sigma c k}\), for \(0\le k\le M\), are computable exactly in polynomial time.

3. An exact polynomial-size feasible formulation

Retain only indices in

\(I=\{(\sigma,c,k):\sigma\in T,\ c\in C,\ 0\le k\le M,\ a_{\sigma c k}>0\}.\)

Write \(n=|I|\). Then \(n\le\tau m(M+1)=O(\tau m^3)\).

For each retained index introduce the aggregate mass

\(z_{\sigma c k}=\displaystyle\sum_{\pi:\,\pi(1)=c,\ d(\sigma,\pi)=k}x_{\sigma\pi}.\)

Define the rational polytope \(P_U\) by the constraints

\(z_{\sigma c k}\ge0,\)

\(\displaystyle\sum_{c,k:\,(\sigma,c,k)\in I}z_{\sigma c k}=\mu_\sigma\qquad(\sigma\in T),\)

\(\displaystyle\sum_{(\sigma,c,k)\in I}kz_{\sigma c k}=M\rho.\)

Define \(P_W\) by adding, for every \(c\ne p\),

\(\displaystyle\sum_{\sigma,k:\,(\sigma,p,k)\in I}z_{\sigma p k}\ge\sum_{\sigma,k:\,(\sigma,c,k)\in I}z_{\sigma c k}.\)

These systems have polynomially many variables and constraints, and polynomial total encoding length. Their distance coefficients are integers at most \(M\).

Every \(x\in U\) aggregates to a point of \(P_U\), and every \(x\in W\) aggregates to a point of \(P_W\). Conversely, a point \(z\) in either reduced polytope has the lift

\(x_{\sigma\pi}=\dfrac{z_{\sigma c k}}{a_{\sigma c k}},\qquad c=\pi(1),\quad k=d(\sigma,\pi).\)

This lift preserves every row sum, total distance, and Plurality score. Therefore,

\(W=\varnothing\quad\Longleftrightarrow\quad P_W=\varnothing.\)

Exact rational linear programming decides this condition in polynomial time.

Also, \(U\) is always nonempty. For each \(\sigma\), place mass \((1-\rho)\mu_\sigma\) on \(\sigma\) and mass \(\rho\mu_\sigma\) on its reversal. Their distances from \(\sigma\) are \(0\) and \(M\), respectively, giving the required total distance \(M\rho\).

Hence identifying \(-\infty\) requires only this polynomial-size feasibility test.

4. The aggregation preserves the entropy optimum

Consider one cell containing \(a=a_{\sigma c k}\) rankings, with total mass \(z=z_{\sigma c k}\).

The function \(t\mapsto-t\log(t/\mu_\sigma)\), continuously extended at zero, is concave. Jensen’s inequality therefore gives

\(-\displaystyle\sum_{\pi\text{ in the cell}}x_{\sigma\pi}\log(x_{\sigma\pi}/\mu_\sigma)\le-z\log\!\left(\dfrac{z}{\mu_\sigma a}\right).\)

Equality holds when every ranking in the cell receives mass \(z/a\), including when \(z=0\). Since this uniform allocation preserves all constraints, define

\(\overline H(z)=-\displaystyle\sum_{(\sigma,c,k)\in I}z_{\sigma c k}\log\!\left(\dfrac{z_{\sigma c k}}{\mu_\sigma a_{\sigma c k}}\right).\)

We obtain the exact identities

\(\displaystyle\max_{x\in U}H(x)=\max_{z\in P_U}\overline H(z),\qquad \max_{x\in W}H(x)=\max_{z\in P_W}\overline H(z).\)

Both maxima exist whenever their feasible sets are nonempty, because those sets are compact and entropy is continuous.

For simpler optimization notation, index the cells by \(i\in I\), write their multiplicities as \(a_i\), and define

\(F(z)=-\displaystyle\sum_{i\in I}z_i\log z_i+\sum_{i\in I}z_i\log a_i.\)

The row-sum constraints imply

\(\overline H(z)=F(z)+\displaystyle\sum_{\sigma\in T}\mu_\sigma\log\mu_\sigma.\)

The final term is constant and cancels in the difference. Thus, when \(P_W\ne\varnothing\),

\(\Lambda_p=\displaystyle\max_{z\in P_W}F(z)-\max_{z\in P_U}F(z).\)

It remains to approximate these two maxima with polynomial dependence on \(\log(1/\varepsilon)\).

5. Handling lower-dimensional feasible sets exactly

We first explain how to prepare either nonempty polytope \(P\in\{P_U,P_W\}\) for convex optimization.

We use the standard exact rational linear-programming theorem: feasibility, bounded linear optimization, and rational optimizing witnesses are computable in time polynomial in the explicit rational input length. Such witnesses can be chosen with polynomial encoding length.

Write the inequalities defining \(P\) as \(\alpha_j^\mathsf{T}z\le b_j\), together with its stated equalities. For each inequality, maximize its slack \(b_j-\alpha_j^\mathsf{T}z\) over \(P\).

If this maximum is zero, the inequality is an equality throughout \(P\). If it is positive, obtain a rational feasible witness where the slack is positive. Average these witnesses, also including one feasible point. The resulting rational point \(z^\circ\) satisfies every inequality that is not universally tight strictly.

Let \(E\) be the affine subspace defined by the original equalities and all universally tight inequalities. Since all other inequalities have positive slack at \(z^\circ\), a sufficiently small neighborhood of \(z^\circ\) within \(E\) lies in \(P\). Therefore \(E=\operatorname{aff}(P)\).

All these computations have polynomial bit complexity.

If \(\dim E=0\), then \(P\) is a singleton and its objective can be evaluated directly. Otherwise, Gaussian elimination gives a rational parametrization

\(z=v+By,\qquad y\in\mathbb R^d,\quad d=\dim E,\)

where \(y\) consists of selected free coordinates of \(z\). Because every point of \(P\) has coordinates in \([0,1]\), the transformed feasible set

\(K=\{y:v+By\in P\}\)

is contained in \([0,1]^d\).

Let \(y^\circ\) correspond to \(z^\circ\). Write its remaining inequalities as \(\beta_j^\mathsf{T}y\le\gamma_j\), with positive slacks \(s_j=\gamma_j-\beta_j^\mathsf{T}y^\circ\). The rational number

\(r=\min\!\left(1,\min_j\dfrac{s_j}{1+\|\beta_j\|_1}\right)>0\)

satisfies \(B_2(y^\circ,r)\subseteq K\). Indeed, for \(\|u\|_2\le r\),

\(\lvert\beta_j^\mathsf{T}u\rvert\le\|\beta_j\|_1\|u\|_2<s_j.\)

An outer radius \(R=d+1\) suffices because \(K\subseteq[0,1]^d\). Thus

\(B_2(y^\circ,r)\subseteq K\subseteq B_2(y^\circ,R).\)

The parameters \(y^\circ,r,R,v,B\) have polynomial encoding length. Exact membership and separation for \(K\) are available by checking its explicit rational inequalities.

This handles forced zero coordinates and forced winner ties without any assumption of interior feasibility in the original ambient space.

6. Entropy optimization with polynomial precision complexity

Fix an accuracy parameter \(0<\eta<1\).

Uniform smoothing

For a positive dyadic rational \(\delta\le1\), put

\(F_\delta(z)=-\displaystyle\sum_i(z_i+\delta)\log(z_i+\delta)+\sum_i z_i\log a_i.\)

We claim that, throughout \([0,1]^n\),

\(\lvert F_\delta(z)-F(z)\rvert\le n\delta\bigl(\log(1/\delta)+2\bigr).\)

To verify this, let \(h(t)=-t\log t\), with \(h(0)=0\). For \(t>0\),

\(\dfrac{d}{dt}\bigl(h(t+\delta)-h(t)\bigr)=\log\!\left(\dfrac{t}{t+\delta}\right)<0.\)

Hence this difference decreases on \([0,1]\). Its endpoint values are \(\delta\log(1/\delta)\) and \(-(1+\delta)\log(1+\delta)\). Since \(\log(1+\delta)\le\delta\) and \(\delta\le1\), the latter has absolute value at most \(2\delta\). Summing the resulting coordinatewise bound proves the claim.

Choose \(\delta=2^{-q}\), where \(q\) is large enough that

\(n2^{-q}(q+2)\le\eta.\)

This suffices because \(\log(1/\delta)=q\log2\le q\). Such a \(q\) can be found in polynomial time and satisfies

\(q=O\bigl(\log(n+1)+\log(1/\eta)\bigr).\)

Consequently,

\(\left|\max_P F_\delta-\max_P F\right|\le\eta.\)

A globally convex, Lipschitz objective

To apply a standard convex-optimization theorem, define \(\phi_\delta(t)=(t+\delta)\log(t+\delta)\) on \([0,1]\), and extend it linearly outside that interval using its endpoint tangents. Explicitly:

The derivative is constant on each exterior interval and increases on the middle interval, where \(\phi_\delta''(t)=1/(t+\delta)>0\). The derivatives agree at the endpoints. Thus this extension is globally convex and continuously differentiable.

Define, in the affine coordinates from Section 5,

\(f(y)=\displaystyle\sum_i\phi_\delta((v+By)_i)-\sum_i(v+By)_i\log a_i.\)

On \(K\), this equals \(-F_\delta(v+By)\).

Since \(1\le a_i\le(m-1)!\), we have \(\log a_i\le m^2\). The absolute derivative of each scalar summand is bounded by \(q+3+m^2\). Therefore

\(\|\nabla f(y)\|_2\le\|B\|_2\sqrt n\,(q+3+m^2).\)

For example, the rational quantity

\(K_f=nd\left(1+\max_{i,j}|B_{ij}|\right)(q+3+m^2)\)

is a valid global Lipschitz bound. Its encoding length is polynomial.

Polynomial-time evaluation

The function \(f\) can be evaluated to arbitrary rational additive accuracy in polynomial time.

For completeness, a positive rational \(u\) can be written as \(u=2^e w\), with \(1\le w<2\). Then \(\log u=e\log2+\log w\), and

\(\log w=2\displaystyle\sum_{\ell=0}^{\infty}\frac{t^{2\ell+1}}{2\ell+1},\qquad t=\frac{w-1}{w+1},\quad 0\le t<\frac13.\)

The tail decreases geometrically. The same series with \(t=1/3\) computes \(\log2\). Truncation therefore computes \(\log u\) to error \(\zeta\) in time polynomial in the encoding length of \(u\) and \(\log(1/\zeta)\).

Applying this to the finitely many logarithms in \(f\), with accuracies adjusted for their rational multipliers, gives the required evaluation oracle. Its running time is polynomial in the query encoding length, the problem encoding length, and the requested precision.

Applying the ellipsoid theorem

We use the standard oracle convex-optimization theorem: a globally convex Lipschitz function with an arbitrary-precision rational evaluation oracle can be minimized over a convex body with known rational inner and outer balls and a polynomial-time membership oracle, in time polynomial in the encoded parameters and \(\log(1/\eta)\). A precise formulation is [Dadush’s thesis, Theorem 2.5.9](https://homepages.cwi.nl/~dadush/papers/dadush-thesis.pdf).

All its hypotheses have now been verified:

The theorem therefore approximates \(\max_P F_\delta\) to additive error \(\eta\) in polynomial time. Combined with smoothing, this approximates \(\max_P F\) to additive error \(2\eta\).

The zero-dimensional case follows by direct evaluation with the same error bound.

7. The final algorithm and error bound

The algorithm is:

For each of the two maxima, the error is at most \(2\eta=\varepsilon/2\). Hence

\(\lvert\widehat\Lambda_p-\Lambda_p\rvert \le\left|\widehat V_W-\max_{P_W}F\right| +\left|\widehat V_U-\max_{P_U}F\right| \le\varepsilon.\)

Every stage takes time polynomial in \(m,\tau,L,\log(1/\varepsilon)\).

The denominator \(D\) governs the specified sequence of finite realizations; it is not needed to compute the continuous entropy maxima. The multiplicity term \(z_i\log a_i\) accounts for the distinct final rankings within each cell, as required by labelled-profile counting. Thus the cited hardness of [finite Plurality swap-bribery counting](https://arxiv.org/pdf/2010.09678) does not obstruct this algorithm for the entropy-rate quantity.

⟨structured verdict parsed — rendered above⟩

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

The prover resolves the assigned continuous problem. The aggregation is exact, the feasibility test is polynomial in the explicit input size, and the entropy optimization argument supports polynomial dependence on the requested precision bits. I found no major or minor mathematical issue requiring repair.

The claimed output is a rational additive approximation to \(\Lambda_p\), with exact identification of \(-\infty\). This matches USER_TASK.

The proof optimizes the continuous quantity defined in the task. It does not need to compute the denominator \(D\) or enumerate finite voter realizations. Its discussion of \(D\) therefore leaves no missing algorithmic requirement.

The recurrence for \(A_{h,j}\) is correct: insertion of the largest element produces each possible additional inversion count from \(0\) through \(h-1\) exactly once. The initialization \(A_{0,0}=1\), together with zero values outside the inversion range, covers the base and boundary cases.

The multiplicity formula
\[ a_{\sigma c k}=A_{m-1,k-r_\sigma(c)+1} \]
is correct. Fixing \(c\) at the top changes exactly the \(r_\sigma(c)-1\) pairs consisting of \(c\) and candidates originally above it. The remaining pair disagreements are precisely inversions of the suffix relative to the ranking obtained by deleting \(c\).

This also handles unattainable distances, since the corresponding table entries are zero. The number of table entries and recurrence operations is polynomial in \(m\), and the stated factorial bound gives polynomial bit length for every entry.

The bound \(n\le\tau m(M+1)\) is valid. Row sums, exact distance, and all Plurality comparisons depend only on the aggregate cell masses.

Conversely, every retained cell has positive multiplicity, so the proposed uniform lift is well-defined. It preserves nonnegativity, row sums, total distance, and candidate scores. Consequently, the equivalence between emptiness of \(W\) and emptiness of \(P_W\) is exact.

The invoked rational linear-programming theorem applies to these explicit rational systems. Their numbers of variables and constraints, coefficient lengths, and total encoding lengths are polynomial in the task parameters.

The construction proving \(U\ne\varnothing\) is also correct. Reversal has Kendall distance \(M\), and the two assigned masses give total distance \(M\rho\). The cases \(\rho=0\) and \(\rho=1\) remain valid. Since \(m\ge2\), a ranking and its reversal are distinct.

Jensen’s inequality applies because each support mass \(\mu_\sigma\) is positive and the cell entropy summand is concave, including its continuous extension at zero.

The cell bound is attained by the uniform lift. Uniformization preserves every constraint, so the two asserted identities between original and aggregated entropy maxima follow exactly.

The constant term has the correct sign:
\[ \overline H(z)=F(z)+\sum_{\sigma\in T}\mu_\sigma\log\mu_\sigma. \]
It cancels between the two maxima. Thus the reduction retains the multiplicity contribution needed for labelled final profiles.

Compactness and continuity justify attainment whenever the relevant feasible set is nonempty.

Maximizing each inequality’s slack correctly identifies the inequalities that hold as equalities throughout the polytope.

The averaged witness has positive slack for every inequality that is not universally tight: all component witnesses have nonnegative slack, and at least one has positive slack for each such inequality. This establishes the claimed relative interior point and the identification of the affine hull.

The number of LP calls is polynomial. Polynomial-length rational witnesses, their average, and rational Gaussian elimination give polynomial-length affine-coordinate data.

Selecting free coordinates from \(z\) correctly ensures \(K\subseteq[0,1]^d\). The proposed inner radius is positive and satisfies the stated ball inclusion; the denominator \(1+\|\beta_j\|_1\) supplies the strict margin. The outer radius \(R=d+1\) is sufficient.

The singleton case is explicitly separated. Forced zero coordinates and forced winner ties therefore do not invalidate the optimization argument.

The derivative
\[ \frac{d}{dt}\bigl(h(t+\delta)-h(t)\bigr) =\log\!\left(\frac{t}{t+\delta}\right) \]
is correct for \(t>0\). Together with continuity at zero, it establishes the endpoint bounds used in the proof.

Both endpoint estimates are valid for \(0<\delta\le1\), so
\[ |F_\delta(z)-F(z)| \le n\delta\bigl(\log(1/\delta)+2\bigr) \]
holds throughout the stated cube.

Choosing \(\delta=2^{-q}\) with \(n2^{-q}(q+2)\le\eta\) suffices. Such a choice needs only
\[ q=O\bigl(\log(n+1)+\log(1/\eta)\bigr) \]
bits. The resulting uniform bound transfers to the maxima, including when their optimizers lie on the boundary.

The exterior formulas are the endpoint tangents of the middle expression. Their derivatives match at both endpoints, and the derivative is nondecreasing globally. Hence the extension is convex and continuously differentiable on the entire real line.

Composition with the affine parametrization and addition of the linear multiplicity term preserve convexity. On \(K\), the objective is exactly \(-F_\delta\).

The scalar derivative bound is valid, including the exterior intervals. The stated \(K_f\) safely bounds the gradient norm for positive dimension. Its numerical value may be large, but its binary encoding length is polynomial, as required by the subsequent theorem.

The logarithm series and range reduction are correct. After normalization, the series parameter is less than \(1/3\); the series for \(\log2\) uses \(1/3\) itself. Both converge geometrically. Adjusting logarithm accuracies for the rational coefficients gives the claimed polynomial-time rational evaluation oracle, including queries outside \(K\).

I checked the cited [Dadush thesis, Theorem 2.5.9](https://homepages.cwi.nl/~dadush/papers/dadush-thesis.pdf). It has the stated hypotheses: a centered convex body with weak membership access and a globally convex Lipschitz function with arbitrary-accuracy rational evaluations. It returns an additive enclosure of the minimum in polynomial oracle time; the surrounding computational conventions measure complexity in encoded parameter lengths.

All these hypotheses are verified in the write-up. Exact membership supplies weak membership, and the evaluation oracle has the necessary bit complexity. The cited ellipsoid theorem therefore supports the asserted deterministic polynomial-time approximation.

Smoothing contributes at most \(\eta\), and optimization contributes at most \(\eta\), giving error at most \(2\eta\) for each maximum.

With \(\eta=\varepsilon/4\), subtraction gives total error at most \(\varepsilon\). All constructed systems, rational parameters, and oracle computations have polynomial encoding or running-time bounds in the specified parameters.

Exact infeasibility detection occurs before entropy optimization, so identifying \(-\infty\) requires no numerical threshold decision.

No additional clarification is needed to verify the argument. The cited discrete counting hardness does not contradict the established algorithm for this continuous objective.

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