← back to the atlas

d4-conf-ecai-2012-0134 (d4-conf-ecai-2012-0134)

Answer: Yes; deterministic polynomial-time solvable.

The anchor (named result in the paper)

Theorem 3 — class: algorithmic

PDF text-layer excerpt — equations and symbol order may be approximateLet k be a positive integer taken as the input, 3-PHASES is ( k−1 k , 1 k)-approximate in the uniform case.

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

The continuous mirror question, as graded

Given a matroid activity instance \(M=(X,\mathcal F)\), nonnegative revenue weights \(w\), \(p\) visitor types of equal mass \(1/p\) identified with activity labels, and a positive integer \(k\), compute an integral base \(B\) whose revenue is at least \((k-1)/k\) of the maximum base revenue and whose served population mass is at least \(1/k\) of the maximum mass any base can serve. A type is served when \(B\) contains an activity with its label.

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

Let \(M=(X,\mathcal F)\) be a matroid on \(m\geq1\) activities, supplied by an independence oracle with polynomial evaluation time \(T_{\mathrm{ind}}\). Each activity has one label \(\lambda(x)\) and a nonnegative binary rational revenue \(w(x)\); labels partition \(X\). No simplicity restriction is imposed.
A society is given by its support: the list of the \(\tau=p\geq1\) types with positive mass, each with its mass as a binary rational. Types are exactly the activity labels and each has mass \(1/p\), so total mass is one. The support size \(\tau\) is not the number of possible types.
A feasible outcome is an integral base \(B\). Define \(R(B)=\sum_{x\in B}w(x)\) and \(S(B)=\sum_{\ell\in\lambda(B)}1/p\). Let \(R^*=\max_{B\text{ base}}R(B)\) and \(S^*=\max_{B\text{ base}}S(B)\), with separate maxima.
The input also contains a positive integer \(k\), encoded in binary; \(L\) denotes the total explicit input bit length. Guarantees use inequalities, including when an optimum is zero.

Does a deterministic algorithm, polynomial in \(m,\tau,L,\log k,T_{\mathrm{ind}}\), always return a base \(B\) satisfying \(R(B)\geq\frac{k-1}{k}R^*\) and \(S(B)\geq\frac1kS^*\)?

Known results: a deterministic polynomial-time algorithm achieves these ratios for nonnegative revenue and the number of distinct labels on arbitrary matroids ([source](https://doi.org/10.3233/978-1-61499-098-7-360)). The specified equal-mass formulation is exactly that problem after normalizing label count by \(p\); consequently this target is already settled.

Modeling choices made when packaging the task

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

Conclusion

Yes. The known label-count theorem applies to this equal-mass formulation. The binary encoding of \(k\) also causes no difficulty, as shown below.

Applicable known theorem

Theorem 3 of Gourvès, Monnot, and Tlilane, *Approximate Tradeoffs on Matroids*, gives the following result:

For an arbitrary matroid with nonnegative element weights and one label per element, a deterministic polynomial-time algorithm returns a base \(B\) satisfying
\[ W(B)\geq \frac{k-1}{k}\max_{A\text{ base}}W(A), \qquad |\lambda(B)|\geq \frac1k\max_{A\text{ base}}|\lambda(A)|. \]
The parameter \(k\) is an input positive integer. No simplicity assumption is required in this case. The paper’s “uniform” assumption means that every label has unit gain; it does not require a uniform matroid. Its algorithm uses greedy selection and cardinality matroid intersection. [Theorem 3 and Section 8](https://pdfs.semanticscholar.org/d933/f0c91c297eefa247ed9367932330fdb08726.pdf).

We use this established theorem rather than reprove it.

Normalization and exact arithmetic

Define
\[ C(B)=|\lambda(B)|, \qquad C^*=\max_{B\text{ base}}C(B). \]
Because every supported type is an activity label and has mass \(1/p\),
\[ S(B)=\frac{C(B)}p, \qquad S^*=\frac{C^*}p. \]
The second identity follows because multiplication by the fixed positive constant \(1/p\) preserves maximizers. Consequently,
\[ C(B)\geq \frac{C^*}{k} \quad\Longleftrightarrow\quad S(B)\geq \frac{S^*}{k}. \]

If integer weights are desired, write each revenue as \(w(x)=a_x/b_x\), where \(a_x\geq0\) and \(b_x\geq1\) are integers. Set
\[ D=\prod_{x\in X}b_x, \qquad u(x)=a_x(D/b_x). \]
Then \(u(x)\) is a nonnegative integer and
\[ U(B):=\sum_{x\in B}u(x)=D R(B), \qquad U^*=D R^*. \]
Thus the revenue guarantee for \(U\) is exactly the requested guarantee for \(R\). The bit length of \(D\) is at most the sum of the denominator bit lengths, and every \(u(x)\) has bit length \(O(L)\). This transformation takes polynomial time.

Algorithm and correctness

First compute a maximum-revenue base \(B_R\) by the matroid greedy algorithm, processing elements in nonincreasing revenue order and accepting an element whenever independence is preserved. Fix an input order to break ties deterministically. Let \(r=|B_R|\).

Rank zero

If \(r=0\), the only base is empty. Hence \(R^*=S^*=0\), and returning it satisfies both inequalities.

Assume henceforth that \(r\geq1\).

Large binary parameter

If \(k>m\), return \(B_R\). Its revenue is \(R^*\), so the revenue inequality holds.

Every nonempty base has at least one label, while \(C^*\leq m\). Therefore,
\[ C(B_R)\geq1>\frac{m}{k}\geq\frac{C^*}{k}. \]
Dividing by \(p>0\) proves the satisfaction inequality.

Zero revenue optimum

Suppose \(k\leq m\) and \(R^*=0\). Compute a maximum-cardinality common independent set \(I\) of:

Extend \(I\) to a base \(B\) of \(M\).

To verify optimal satisfaction, every base \(A\) contains a subset with exactly one representative of each label. That subset is independent in both matroids and has size \(C(A)\). Hence \(|I|\geq C^*\). Conversely, any common independent set extends to a base, whose label count is at least its cardinality. Hence \(|I|\leq C^*\). Thus
\[ C(B)\geq |I|=C^*, \]
and therefore \(S(B)=S^*\). Nonnegativity gives \(R(B)\geq0=\frac{k-1}{k}R^*\).

Remaining case

Suppose \(k\leq m\) and \(R^*>0\). Apply the stated theorem to \(M\), the original labels, and the integer weights \(u\). All hypotheses hold: \(M\) is an arbitrary oracle matroid, labels partition its ground set, and weights are nonnegative.

Its returned base satisfies
\[ D R(B)\geq \frac{k-1}{k}D R^*, \qquad C(B)\geq\frac{C^*}{k}. \]
Division by \(D>0\) and \(p>0\), respectively, gives both requested inequalities.

Running time

Greedy optimization and base extension require polynomially many independence queries. The partition-matroid oracle checks label multiplicities in polynomial time, so deterministic cardinality matroid intersection is polynomial in \(m,\tau,L,T_{\mathrm{ind}}\).

The known tradeoff algorithm is invoked only when \(k\leq m\); thus even polynomial dependence on the numerical value of \(k\) is polynomial in \(m\). Larger values require only a binary comparison and the greedy branch. All arithmetic uses polynomial bit length.

The complete algorithm is therefore deterministic and polynomial in \(m,\tau,L,\log k,T_{\mathrm{ind}}\).

⟨structured verdict parsed — rendered above⟩

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

Verdict

The prover resolves the assigned task correctly. The cited theorem applies to the specified equal-mass problem, and the additional branches correctly handle zero optima and binary encoding of the parameter. No major or minor mathematical issues were found.

Step-by-step verification

1. Applicability of the cited theorem

The citation is accurate. Theorem 3 states the claimed tradeoff for every positive integer \(k\) supplied as input. Section 8 defines the uniform case by unit label gains and explicitly removes the labeled-simplicity restriction. The source assumes polynomial-time independence oracles, and its algorithm uses greedy phases and cardinality matroid intersection. Its final greedy phase returns a base. Thus the cited result matches the required representation and feasible outcomes. [Theorem 3 and Sections 3 and 8](https://pdfs.semanticscholar.org/d933/f0c91c297eefa247ed9367932330fdb08726.pdf).

The prover is entitled to invoke this established theorem without reproducing its proof. The task itself also explicitly supplies the corresponding known result.

2. Normalization of satisfaction

Under the task’s explicit identification of supported types with activity labels, every represented label contributes exactly \(1/p\). Therefore both identities
\(S(B)=C(B)/p\) and \(S^*=C^*/p\) are correct.

Since \(p\geq1\), division by \(p\) preserves inequalities. The claimed equivalence between the label-count guarantee and the satisfaction guarantee is exact. The argument does not confuse support size with the number of possible types.

3. Rational-to-integer revenue conversion

Every denominator is positive, so \(D\) is a positive integer and \(D/b_x\) is integral. Consequently the identities \(u(x)=Dw(x)\), \(U(B)=DR(B)\), and \(U^*=DR^*\) are valid.

The bit-length estimates are correct: the product’s bit length is bounded by the sum of denominator bit lengths, and multiplying by a numerator leaves each transformed weight with bit length \(O(L)\). Exact products and divisions of these integers take polynomial time.

Scaling by \(D>0\) preserves the requested revenue guarantee, including zero revenues.

4. Greedy optimization and rank zero

The described greedy procedure is the standard maximum-weight-base algorithm for a finite matroid. Its hypotheses hold: the revenues are additive, comparisons are exact, and independence is available through the given oracle. Processing every element produces a maximal independent set, hence a base. The stated tie-breaking makes this procedure deterministic.

Thus \(R(B_R)=R^*\), and \(r=|B_R|\) is the matroid rank.

If \(r=0\), the empty set is the unique base. Both optima are zero, so the prover’s return value satisfies both inequalities. Loops cause no difficulty.

5. Branch for a large binary parameter

When \(r\geq1\), the returned base is nonempty and has at least one label. Also \(C^*\leq m\).

For \(k>m\), the complete chain
\(C(B_R)\geq1>m/k\geq C^*/k\)
is valid. The revenue guarantee follows from revenue optimality and \((k-1)/k\leq1\).

This branch correctly avoids a running time proportional to an arbitrarily large numerical value of \(k\).

6. Branch for zero revenue optimum

The two matroids used in the intersection step have the same ground set. The second is indeed a partition matroid because labels partition the activities.

Both directions establishing \(|I|=C^*\) are justified:

Extending the maximum common independent set therefore produces a base with exactly the optimal satisfaction. Nonnegative revenue gives the required revenue inequality when \(R^*=0\).

7. Remaining case and running time

In the remaining branch, the matroid, labels, nonnegative integer weights, and positive integer parameter satisfy the stated theorem’s hypotheses. Dividing its guarantees by \(D\) and \(p\) yields precisely the two requested inequalities.

The branches exhaust all valid inputs. In particular, \(k=1\) is included in the cited theorem.

Greedy optimization, base extension, and deterministic cardinality matroid intersection require polynomially many oracle calls and polynomial additional work. The exact arithmetic has polynomial bit length. The theorem is invoked only for \(k\leq m\), so polynomial dependence on its numerical value is sufficient here.

The claimed deterministic polynomial running time follows.

Required feedback

None. No missing clarification, false step, or blocking issue was identified.

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