← back to the atlas

d4-conf-aaai-2017-0024 (d4-conf-aaai-2017-0024)

Answer: \(\mathrm P\); also fixed-parameter tractable parameterized by \(k\).

The anchor (named result in the paper)

Theorem 1 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateThe TOURNAMENT FIXING PROBLEM can be solved in time 2O(k2 log k)nO(1) on tournaments of size n with a feedback arc set of size k. This theorem implies that when the given tournament has a feedback arc set of size k, where k2 log k = O(log n) then it can be decided in polynomial time whether the tournament can be fixed to make a given player win.

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

The continuous mirror question, as graded

Given finitely many competitor types \(T\), rational masses \(\mu_t\) summing to \(1\), a deterministic type-level winner for each match, a target type \(t^\star\), and bracket depth \(R\), can the masses be paired over \(R\) rounds so that the final mass \(2^{-R}\) is entirely of type \(t^\star\)? At round \(r\), choose match masses \(q^r_{\{a,b\}}\geq 0\) satisfying \(2q^r_{\{a,a\}}+\sum_{b\ne a}q^r_{\{a,b\}}=p_a^r\); the next-round mass of each type is the sum of match masses whose winner has that type. The question is whether such a schedule exists.

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

A society is given by its support: a nonempty list \(T\) of \(\tau\) competitor types with positive binary rational masses \(\mu_t\), where \(\sum_{t\in T}\mu_t=1\). Here \(\tau\) is the support size, not the number of possible types; set \(m=|T|=\tau\).
The input also specifies a symmetric deterministic winner table \(w(a,b)\in\{a,b\}\), with \(w(a,a)=a\), a target \(t^\star\in T\), and a nonnegative integer depth \(R\) encoded in unary. Let \(L\) be the total input bit length and \(k\) the minimum feedback arc set size of the tournament on distinct types, oriented from winner to loser.
Let \(\mathcal U\) be the unordered pairs of types, allowing repetitions. A schedule has nonnegative real match masses \(q^r_{\{a,b\}}\) for \(\{a,b\}\in\mathcal U\) and \(0\le r<R\), starts with \(p_a^0=\mu_a\), and satisfies \(2q^r_{\{a,a\}}+\sum_{b\ne a}q^r_{\{a,b\}}=p_a^r\) and \(p_c^{r+1}=\sum_{\{a,b\}\in\mathcal U:\,w(a,b)=c}q^r_{\{a,b\}}\). Thus every round pairs all surviving mass, including matches within a type, with no byes.
Feasibility means that such a schedule exists with \(p_{t^\star}^R=2^{-R}\) and \(p_a^R=0\) for every \(a\ne t^\star\).

Is this feasibility problem in \(\mathrm P\) or \(\mathrm{NP}\)-hard, with running times measured in \(m,\tau,R,L\)? If it is \(\mathrm{NP}\)-hard, is it nevertheless fixed-parameter tractable parameterized by \(k\)?

For finite players in a balanced knockout bracket, feasibility is [\(\mathrm{NP}\)-complete](https://ojs.aaai.org/index.php/AAAI/article/download/8805/8664), and admits time [\(2^{O(k^2\log k)}n^{O(1)}\)](https://ojs.aaai.org/index.php/AAAI/article/view/11132), where \(n\) counts players and \(k\) is their tournament's minimum feedback arc set size.
No result settling this precise divisible-mass problem was located.

Modeling choices made when packaging the task

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

Result

The divisible-mass feasibility problem is in \(\mathrm P\). It can be decided in time \((m+R+L)^{O(1)}\), with \(m=\tau\). Consequently, it is also fixed-parameter tractable parameterized by \(k\), without computing a feedback arc set.

The reason is that the defining schedule constraints form a rational linear program of polynomial encoding length.

1. Exact linear programming formulation

Introduce nonnegative real variables:

Impose the following linear equalities.

Initial masses: for every \(a\in T\),
\(p_a^0=\mu_a\).

Pairing constraints: for every \(a\in T\) and \(0\le r<R\),
\(2q_{\{a,a\}}^r+\sum_{b\ne a}q_{\{a,b\}}^r-p_a^r=0\).

Winner constraints: for every \(c\in T\) and \(0\le r<R\),
\(p_c^{r+1}-\sum_{\{a,b\}\in\mathcal U:\,w(a,b)=c}q_{\{a,b\}}^r=0\).

Terminal masses:
\(p_{t^\star}^R=2^{-R}\), and \(p_a^R=0\) for every \(a\ne t^\star\).

These constraints are linear because the winner table is fixed input: it determines which variables occur in each winner equation.

Equivalence proof. Every feasible schedule supplies values satisfying all these constraints, by the schedule definition. Conversely, every feasible assignment supplies nonnegative match masses satisfying precisely the required initial, pairing, winner, and terminal conditions. Thus its match masses constitute a feasible schedule. This proves equivalence in both directions; no additional realizability condition is needed under the stated definition.

For consistency, summing the pairing equations gives
\(2\sum_{\{a,b\}\in\mathcal U}q_{\{a,b\}}^r=\sum_{a\in T}p_a^r\).
Every unordered pair has exactly one winner, so summing the winner equations gives
\(\sum_{c\in T}p_c^{r+1}=\sum_{\{a,b\}\in\mathcal U}q_{\{a,b\}}^r\).
Induction from the initial total mass therefore yields
\(\sum_{a\in T}p_a^r=2^{-r}\).

The formulation also handles \(R=0\): there are no match variables, and feasibility requires the initial distribution itself to be concentrated on the target.

2. Polynomial encoding length and exact decision

There are \(m(m+1)/2\) unordered pairs allowing repetitions. Hence the number of variables is
\(N=(R+1)m+Rm(m+1)/2\),
and the number of equality constraints is
\(E=2(R+1)m\).
There are additionally \(N\) nonnegativity constraints.

All matrix coefficients belong to \(\{-2,-1,0,1,2\}\). The right-hand sides are input masses, zeros, and \(2^{-R}\). The input masses have total encoding length at most \(L\). Moreover, \(2^{-R}=1/2^R\) has binary rational encoding length \(O(R+1)\): the denominator has \(R+1\) binary digits.

The constraint matrix has \(O((R+1)m^2)\) nonzero entries. Recording their row and column indices therefore gives total sparse encoding length
\(O\!\left(L+R+1+(R+1)m^2\log((R+1)m+2)\right)\).
A dense encoding also has polynomial length.

We now apply the standard rational linear programming theorem: feasibility of a finite system of non-strict linear inequalities with rational coefficients over real variables is decidable in time polynomial in its binary encoding length. This is the polynomial-time feasibility result underlying [Khachiyan’s linear programming algorithm](https://www.mathnet.ru/eng/dan42319).

Its hypotheses hold here: every coefficient is rational, every constraint is linear and non-strict, and each equality can be replaced by two inequalities. Consequently, the decision runs in time \((m+R+L)^{O(1)}\).

Because \(R\) is encoded in unary and the support is explicitly listed, both \(R\) and \(m\) are bounded by the input length up to encoding constants. The running time is therefore polynomial in \(L\). This uses exact rational feasibility, so it does not depend on numerical tolerances.

3. Parameterization and the finite-player comparison

A parameterized problem is fixed-parameter tractable if it admits running time \(f(k)L^C\), where \(C\) is independent of \(k\). The algorithm above has this form with \(f(k)=1\). Thus the problem is fixed-parameter tractable parameterized by \(k\), and no structural restriction on the tournament is necessary.

The cited [finite-player hardness result](https://ojs.aaai.org/index.php/AAAI/article/download/8805/8664) concerns a draw assigning indivisible players to a balanced bracket. The present problem instead permits arbitrary nonnegative real match masses. Its constraints impose no integrality or individual-player assignment requirements. The linear program is therefore exact for the stated divisible-mass problem; finite-player hardness does not establish hardness for it.

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the stated problem correctly: divisible-mass feasibility is in \(\mathrm P\), and hence is fixed-parameter tractable parameterized by \(k\). The formulation matches the schedule definition exactly, and its encoding length is polynomial. No major or minor mathematical issues were found.

Step-by-step verification

1. Variables and constraints

The variables cover every required mass: \(p_a^r\) for all types and stages, and \(q_{\{a,b\}}^r\) for all unordered pairs, including repeated types, in every round. Their nonnegativity agrees with the task.

The initial, pairing, winner, and terminal equations reproduce the task’s conditions exactly. In particular:

The fixed winner table determines coefficients and variable incidence; it introduces no nonlinear dependence.

2. Equivalence with schedule feasibility

Both implications are justified.

A feasible schedule supplies values satisfying the displayed constraints. Conversely, a feasible LP assignment supplies precisely the nonnegative match masses and stage masses required by the schedule definition.

The statement that no additional realizability condition is needed is correct for the definition in USER_TASK. That definition does not require an assignment of individual players to a bracket, integrality, or any additional compatibility across rounds.

Thus the LP is an exact formulation.

3. Conservation calculation

The summation identities are correct. In the summed pairing equations, each cross-type variable occurs twice, while each within-type variable already has coefficient two. Consequently,
\[ 2\sum_{\{a,b\}\in\mathcal U}q_{\{a,b\}}^r =\sum_{a\in T}p_a^r. \]

Every unordered pair has one deterministic winner, so summing the winner equations counts every match variable once. Together with the initial total mass of one, these identities justify the claimed total mass \(2^{-r}\) at every stage.

There is no inconsistency between the conservation identities and the terminal constraints.

4. Boundary cases

The formulation handles \(R=0\) correctly: there are no match variables, and the initial and terminal equations constrain the same stage masses. Given the task’s strictly positive support masses, the stated concentration condition holds exactly when the support consists solely of the target.

For \(m=1\), the repeated-type pair remains present, so the formulation also covers the singleton support without an exception.

5. Size and encoding bounds

The variable count
\[ N=(R+1)m+\frac{Rm(m+1)}2 \]
is correct.

The equality count
\[ E=2(R+1)m \]
correctly includes \(m\) initial equations, \(Rm\) pairing equations, \(Rm\) winner equations, and \(m\) terminal equations. Redundancy among equations does not invalidate this count or the LP algorithm.

The coefficient bound is valid. Encoding \(2^{-R}\) as a rational with denominator \(2^R\) requires \(O(R+1)\) bits.

The claimed \(O((R+1)m^2)\) nonzero count is valid, including endpoint equations and nonnegativity constraints if those are explicitly represented. Although column indices range up to \(N=O((R+1)m^2)\), their bit length is still \(O(\log((R+1)m+2))\), so the stated sparse encoding bound is sound. A dense encoding likewise has polynomial length.

6. Polynomial-time feasibility theorem

The prover states the required theorem precisely enough: rational, non-strict linear feasibility over real variables is decidable in polynomial time in binary encoding length. This is the standard polynomial-time LP result associated with [Khachiyan’s cited paper](https://www.mathnet.ru/eng/dan42319).

All hypotheses are explicitly verified. Replacing each equality by two inequalities preserves feasibility and increases encoding length only polynomially. Exact feasibility applies even when the feasible set has lower dimension; no strict feasibility assumption is needed.

Since the support is explicitly listed and \(R\) is unary, the resulting running time is polynomial in \(L\).

7. Parameterization and scope

The polynomial-time bound implies the stated FPT bound with \(f(k)=1\), independently of the tournament’s feedback arc set.

The finite-player comparison introduces no unsupported inference into the argument. The polynomial conclusion follows entirely from the exact LP formulation; it does not rely on either cited finite-player result.

No additional clarification or repair is 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.