Complexity Theory

Completed

Combinatorics·Captain: yousofy

Block Sensitivity vs. Sensitivity: Eight-layer exponent $2.085$ Open Problem

Motivation

A rule that assigns an output bit to every input string can react very differently to changing one bit and changing several bits together. Quantifying that difference is a basic question about Boolean functions in theoretical computer science. Sensitivity measures how many individual bit changes can affect one output; block sensitivity allows disjoint groups of bits to change separately. The question here is how far apart these two measures can grow.

Hao Huang's 2019 theorem established a polynomial relation between sensitivity and polynomial degree, resolving the Sensitivity Conjecture. The sharper question about the exponent remained. OpenAI's 2026 superquadratic separation ruled out a universal quadratic bound. The subsequent accepted exponent-2.075 contribution by Robin Kothari and Codex provides the established comparison point for this mission. The target is the stronger quantitative bound 2.085.

Setting

A total Boolean function is a map

f:\{0,1\}^n\longrightarrow\{0,1\}

that assigns an output to every length- $n$ bit string. For an input $x$ and a set $B$ of coordinate positions, write $x^B$ for the string obtained by reversing exactly the bits in $B$ .

A coordinate $i$ is sensitive at $x$ when $f(x^{\{i\}})\ne f(x)$ . Write $s(f,x)$ for the number of such coordinates and define

s(f)=\max_x s(f,x).

A sensitive block at $x$ is a nonempty coordinate set $B$ with $f(x^B)\ne f(x)$ . Define $bs(f,x)$ as the largest size of a family of pairwise disjoint sensitive blocks at that same input, and set

bs(f)=\max_x bs(f,x).

Each block is flipped separately from the original input. All functions and coordinate sets in these definitions are finite.

Formalization target

The main theorem is the campaign statement

\operatorname{AchievesExponent}(2.085),\qquad 2.085=\frac{417}{200}.

Its full meaning is

\forall\varepsilon>0\;\forall S\in\mathbb N,\ S\ge2\;\Longrightarrow\; \exists n\in\mathbb N\;\exists f:\{0,1\}^n\to\{0,1\},

s(f)\ge S\quad\text{and}\quad bs(f)\ge s(f)^{2.085-\varepsilon}.

The exact formal target and its proof status are recorded here. Both the dimension and the function may depend on $\varepsilon$ and $S$ . The decimal denotes an exact rational number. The statement permits arbitrarily small positive exponent loss and explicitly requires arbitrarily large sensitivity. For example, choosing $\varepsilon=0.001$ gives exponent 2.084 at every requested sensitivity threshold. This is a concrete checkpoint within the broader problem of determining the optimal separation exponent.

Significance and current status

The target raises the established exponent bound from 2.075 to 2.085, with the quantifiers stated above. In particular, it supplies a fixed exponent strictly above 2.075 for a family whose sensitivities are unbounded. This distinction matters: a favorable comparison for one finite Boolean function, without an appropriate asymptotic conclusion, would not establish the target.

The new contribution is an eight-layer numerical certificate within the existing nine-predicate framework. Its foundation comes from Kothari and Codex's accepted 2.075 proof, which retains credit to abhishekdpseok's accepted 2.0635 development and the earlier OpenAI and community proofs.

The complete self-contained proof has compiled successfully in Lean 4.33.1. The certificate and its assembly have also passed independent checks. Prove2Me has accepted the complete proof, submission c6096517-61e7-4f51-bc68-c1521d61eb65, on 20 October 2026. The target record is the reference for subsequent verification status. The separate proof explanation supplies the construction details and exact arithmetic.

Difficulty

The sensitivity estimate must hold at every input. Checking only the input that supports many sensitive blocks leaves that requirement unresolved. Likewise, a collection of output-changing sets is insufficient unless its members are nonempty and pairwise disjoint.

The asymptotic quantifiers impose a further requirement: witnesses must exist beyond every sensitivity threshold. Merely increasing the dimension does not establish this, since a function can ignore added coordinates. Finally, the exact rational exponent requires rigorous arithmetic bounds; a numerical logarithm estimate alone does not prove the formal statement.

Formalization scope

The shared Lean representation uses f : (Fin n → Bool) → Bool and the definitions in SensitivityCampaign and OAI.Paper320. Sensitivity is the finite supremum over all inputs. Block sensitivity takes the finite supremum over all block families at each input, assigning zero to a family that fails the disjointness, nonemptiness, or output-change conditions. The empty family is allowed.

The target imposes no normalization on $f$ or on a distinguished input. Dimensions zero and constant functions are permitted by the underlying types, but cannot satisfy the required sensitivity threshold $S\ge2$ . Real exponentiation is applied after casting the natural-number complexity measures to real numbers.

The development uses Mathlib and the unchanged campaign definitions. Reusable infrastructure includes the complexity-measure definitions and the finite-certificate interface. Independent verification, clearer reusable statements, and stronger rigorously certified bounds are welcome contributions. Any stronger target should preserve totality, global sensitivity, and the unbounded-sensitivity requirement.

Selected references

Hao Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture, Annals of Mathematics 190(3), 949–955, 2019. DOI.
OpenAI, A superquadratic separation between sensitivity and block sensitivity, OpenAI Math Release preprint, September 2026. Manuscript; formalization scope.
Robin Kothari and Codex, Separation exponent at least 2.075, Prove2Me accepted proof, 2026, submission 819ad4c6-aa25-48ca-82e9-c8df39c182c0. Theorem and proof record.
abhishekdpseok, Separation exponent at least 2.0635, Prove2Me accepted proof, 2026, submission f80a3f37-72fa-4d56-a094-3e4d351764f3. Theorem and proof record.

5 thms3 active usersReviewed

Operations Research Optimization·Captain: mikedeng1

Multi-purchase Behavior: Modeling, Estimation, and Optimization: Revenue Maximization under the BundleMVL-2 Multi-Purchase Choice Model Is NP-CompleteResearch Paper

Motivation

Recommendation platforms and online retailers choose which products to show a customer, and customers often buy more than one of them in a single visit. Classical choice models such as the multinomial logit (MNL) assume a customer buys at most one product, and under MNL the revenue-maximizing set of products to display is easy to find: it is one of the $n$ revenue-ordered sets, so it can be found in linear time. Tulabandhula, Sinha, Karra and Patidar (arXiv:2006.08055, Manufacturing & Service Operations Management, 2023) introduce the BundleMVL-K model, a multivariate logit model in which a customer buys a bundle of up to $K$ products, with pairwise interaction terms that capture complementarity and substitution. They estimate it on retail data and design algorithms for choosing the recommendation set.

The first question for any such model is whether the revenue problem stays tractable once purchases of two products are allowed. Theorem 1 of the paper answers it negatively: already for $K=2$ the unconstrained revenue problem is NP-complete. This mission formalizes that theorem and its proof, a reduction from Max-Cut.

Setting

The products are $W=\{1,\dots,n\}$ . Product $i$ has a revenue $r_i>0$ . A BundleMVL-2 instance assigns a nonnegative weight $V_{\{i\}}$ to every product and $V_{\{i,j\}}$ to every unordered pair of products, together with a no-purchase weight $v_0>0$ . (In the paper $V_S=\exp(\sum_{i\in S}\alpha_i+\sum_{i<j\in S}\beta_{ij})$ , and $\beta_{ij}=-\infty$ , so $V_{\{i,j\}}=0$ , is allowed.) A customer shown the recommendation set $C\subseteq W$ buys the nonempty bundle $S\subseteq C$ , $|S|\le 2$ , with probability $V_S/(v_0+\sum_{S'}V_{S'})$ , and buys nothing with probability $v_0/(v_0+\sum_{S'}V_{S'})$ . The expected revenue of $C$ is eq. (4),

R_2(C)=\frac{\sum_{i\in C} r_iV_{\{i\}}+\sum_{i\in C}\sum_{j\in C,\,j>i}(r_i+r_j)V_{\{i,j\}}}{v_0+\sum_{i\in C}V_{\{i\}}+\sum_{i\in C}\sum_{j\in C,\,j>i}V_{\{i,j\}}}.

With the indicator $x^C_i$ of $C$ , the weights $\theta_{ii}=V_{\{i\}}$ , $\theta_{ij}=V_{\{i,j\}}/2$ ( $i\ne j$ ) and the revenues $\hat r_{ii}=r_i$ , $\hat r_{ij}=r_i+r_j$ ( $i\ne j$ ), both numerator and denominator are quadratic forms in $x^C$ .

The revenue problem (5) is $\max_{C\subseteq W}R_2(C)$ ; its decision version asks, for a threshold $\kappa$ , whether some $C$ has $R_2(C)\ge\kappa$ . SIMPLE MAX CUT asks, for a simple graph $G$ and an integer $M$ , whether the nodes of $G$ split into two parts with at least $M$ edges between them.

Formalization targets

Goal: Theorem 1

\text{SIMPLE MAX CUT is NP-complete}\ \Longrightarrow\ \text{BundleMVL-2-DEC is NP-complete}.

NP-completeness is in the sense of Cook's Definition 4: membership in NP and a polynomial-time many-one reduction from every NP language.

Milestones

Eq. (4), second form: $R_2(C)=\dfrac{\sum_{i,j}\hat r_{ij}\theta_{ij}x^C_ix^C_j}{v_0+\sum_{i,j}\theta_{ij}x^C_ix^C_j}$ .
Compare-Step: $\max_C R_2(C)\ge\kappa\iff\max_C\sum_{i,j}\theta_{ij}x^C_ix^C_j(\hat r_{ij}-\kappa)\ge\kappa v_0$ .
Problem (7) is Max-Cut: for $Q=\begin{pmatrix}0&\mathbf d^\top/2\\ \mathbf d/2&-A'\end{pmatrix}$ , the objective $\sum_{i,j}q_{ij}x^C_ix^C_j$ never decreases when the hub $0$ is added to $C$ , and equals the size of the cut $(C\setminus\{0\},\ \text{rest})$ when $0\in C$ .
The $\theta$ transformation: with $r_0>\kappa$ and $\kappa/2>r_1>\dots>r_m>0$ , $\theta_{ij}=q_{ij}/(r_i+r_j-\kappa)$ is nonnegative and $\theta_{ij}(r_i+r_j-\kappa)=q_{ij}$ .
Reduction correctness: $G$ has a cut of size $\ge M$ iff the constructed instance ( $\kappa=1$ , $v_0=M$ ) has some $C$ with $R_2(C)\ge 1$ .
Hardness half: $\text{SIMPLE MAX CUT}\le_p\text{BundleMVL-2-DEC}$ .
Membership half: $\text{BundleMVL-2-DEC}\in\mathrm{NP}$ .

Significance

The result. Theorem 1 separates the multi-purchase model from its single-purchase counterpart: the revenue-ordered structure that makes MNL assortment optimization linear-time fails once pairs can be bought, and no polynomial-time exact algorithm exists unless P = NP. This is what justifies the paper's design of exact algorithms without running-time guarantees (a noisy binary search over the Compare-Step) and of polynomial-time heuristics, and it places BundleMVL-2 next to other hard assortment problems such as the mixture of two multinomial logits (Rusmevichientong et al. 2010, as cited by the paper) and the MMC model of Benson, Kumar and Tomkins (2018), whose hardness is the paper's Theorem 2.

Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. The paper's argument constructs the instance and asserts the equivalence; it does not argue NP membership or the polynomial running time of the reduction, and it leaves the revenues and threshold free subject to inequalities. A formal proof must fix concrete rational parameters, show that the instance code has polynomial size, and handle malformed inputs. The Compare-Step identity (milestone 2) is also the correctness lemma for the paper's binary-search algorithm.

Difficulty

The mathematics of the reduction is short; the obstacles are the two halves that the paper treats as evident. First, the reduction must be a polynomial-time computable map on strings, in Cook's one-tape Turing-machine model, that sends codes of Max-Cut instances to codes of BundleMVL-2 instances and every other string to a non-member; the rational entries $\theta_{ij}=2q_{ij}/(r_i+r_j-\kappa)$ must be computed and written in reduced form. Second, NP membership needs a polynomial-time verifier that evaluates $R_2(C)$ exactly in rational arithmetic, with a bound on the bit size of the sums. An approach that states the reduction as "for every graph there is an instance with the same answer" proves nothing: a fixed yes- or no-instance does that.

Formalization scope

The development is in MultiPurchase.Hardness. Conventions committed to:

Products are Fin n, 0-based; in the reduction the hub is 0 : Fin (m+1) and graph node i : Fin m is product i.succ.
All parameters are rational (ℚ). Weights may be zero ( $V\ge 0$ ), as the paper's own reduction requires ( $V_{\{i\}}=\theta_{ii}=0$ ); revenues are positive and $v_0>0$ . These well-formedness conditions are part of the yes-predicate.
Only pair weights $V_{\{i,j\}}$ with $i<j$ are read, so the code of an instance determines its answer. The empty bundle is the no-purchase option; $R_2(\emptyset)=0$ .
The decision version is "some $C\subseteq W$ has $R_2(C)\ge\kappa$ " (ties count). Instances are coded over the published four-letter alphabet BSym, rationals as reduced numerator and denominator.
The reduction uses $\kappa=1$ , $r_0=2$ , $r_i=1/4-i/(8(m+1))$ for the nodes, $V_{\{i,j\}}=2\theta_{ij}$ , $v_0=M$ ; Max-Cut instances with $M=0$ are outside the construction (they need $v_0=0$ ).
The NP-completeness of SIMPLE MAX CUT (Karp 1972) is a hypothesis of the goal; the platform has no proof of it.

The complexity layer is the published CookPvsNP_defs (Cook's $P$ , $NP$ , $\le_p$ , NP-completeness) and ProjSchedTW_Complexity_Encoding (binary codes, cutSize, maxCutLang), with the proved CookPvsNP.polyReducible_trans. Contributions welcome: Turing-machine programs for rational arithmetic and list manipulation (reusable for every NP-membership proof over rational data), the polynomial-time reduction, and a proof of Karp's theorem for SIMPLE MAX CUT, which would discharge the hypothesis.

Selected references

T. Tulabandhula, D. Sinha, S. R. Karra, P. Patidar, Multi-Purchase Behavior: Modeling, Estimation and Optimization, Manufacturing & Service Operations Management, 2023; arXiv:2006.08055v2. https://arxiv.org/abs/2006.08055
R. M. Karp, Reducibility among Combinatorial Problems, in Complexity of Computer Computations, Plenum, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
A. R. Benson, R. Kumar, A. Tomkins, A Discrete Choice Model for Subset Selection, WSDM 2018. https://doi.org/10.1145/3159652.3159702
S. Cook, The P versus NP Problem, Clay Mathematics Institute problem description. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

12 thms3 active usersReviewed

Completed

Combinatorics·Captain: Robin Kothari

Block Sensitivity vs. Sensitivity: Reach 2.075Open Problem

The quantitative sensitivity question

Sensitivity and block sensitivity measure how a Boolean function responds to changes in its input. They are central examples of query complexity measures: an algorithm learns an unknown input by querying its individual coordinates, while these measures describe how many changes the function can detect at a single input. Understanding their relationship helps distinguish the complexity caused by individual coordinate changes from the complexity caused by changes to groups of coordinates.

The Block Sensitivity vs. Sensitivity campaign tracks the largest certified separation exponent. Its classical benchmark is a quadratic separation. OpenAI problem 132 supplied a superquadratic construction and a Lean formalization in 2026. Subsequent campaign entries reached 2.0391, 2.05, and 2.0635. This entry establishes the exact exponent $2.075=83/40$ using the same definitions and quantifiers.

Boolean functions and sensitive changes

A total Boolean function assigns an output bit to every input of $n$ bits:

f:\{0,1\}^n\longrightarrow\{0,1\}.

For an input $x$ and a coordinate set $D$ , let $x^D$ denote the input obtained by flipping precisely the coordinates in $D$ . The sensitivity at an input counts the individual coordinates whose flips change the output:

s(f,x)=\bigl|\{i:f(x^{\{i\}})\ne f(x)\}\bigr|.

The block sensitivity at an input, denoted $bs(f,x)$ , is the largest number of pairwise disjoint nonempty coordinate sets $D_1,\ldots,D_k$ such that flipping any one of them changes the output at $x$ . The sets are tested separately, always starting from the same input. The corresponding global measures are

s(f)=\max_x s(f,x),\qquad bs(f)=\max_x bs(f,x).

The maxima range over all inputs, including inputs on which the output is zero and inputs on which it is one. No monotonicity, symmetry, or restriction on the number of variables is imposed.

Target: exponent at least 2.075

For every real $\varepsilon>0$ and every integer $S\ge2$ , establish the existence of a dimension $n$ and a total Boolean function $f$ with

s(f)\ge S,\qquad bs(f)\ge s(f)^{83/40-\varepsilon}.

The campaign predicate SensitivityCampaign.AchievesExponent (2.075 : ℝ) states this exact proposition. The decimal is interpreted exactly, as $83/40$ , rather than as an approximate floating-point value. The function and dimension may depend on both the exponent loss $\varepsilon$ and the requested threshold $S$ .

The threshold quantifier is essential: the target concerns arbitrarily large sensitivity. A small isolated function, or a collection of functions whose sensitivity stays bounded, does not by itself establish the campaign statement. The use of an arbitrary positive exponent loss agrees with the campaign's other entries and allows their values to be compared directly.

What this entry establishes

This result increases the certified exponent beyond the campaign's 2.0635 entry. It provides an intermediate achieved bound toward the separate 2.10 research target. It does not assert that 2.10 has been reached or identify the optimal exponent.

The complete Lean proof has compiled successfully, passed local kernel replay, and been accepted by Prove2Me. The verified theorem and full proof establish the stated target. Its supporting development includes nine-predicate sensitivity estimates, bounds on joint changes of nested predicates, finite labeling existence, disjoint sensitive-block witnesses, and an exact integer certificate. The accompanying proof explanation describes how these ingredients establish the stated target. The finite-certificate and logarithmic-score theorems from the campaign foundation remain referenced as reusable milestones.

The difficulty in improving the bound

A construction must have many disjoint sensitive blocks at one input while keeping sensitivity small at every input. A large block family supplies only the lower-bound half of this requirement. An input that makes many individual coordinates sensitive can invalidate the global upper bound even if the intended block-witness input behaves well.

Joint boundary behavior is another constraint: analyzing several related predicates independently can lose information about which changes can occur together. The formal proof therefore needs correct sensitivity estimates for the actual input-coordinate flips throughout the construction. Numerical growth estimates must also account for every fixed overhead before they can certify a finite exponent inequality.

Formalization scope and reusable foundations

The function type is (Fin n → Bool) → Bool. Sensitivity and block sensitivity use the existing OAI.Paper320 definitions, imported through Definitions.Def_SensitivityCampaign. Both measures are natural numbers defined using maxima over finite collections. The exponent comparison casts them to real numbers and uses real exponentiation. Since every requested witness has sensitivity at least two, the base of that power is positive.

The mission retains the shared campaign definitions without modifications. The two foundation milestones are SensitivityCampaign.finite_certificate, which turns suitable finite sensitivity and block-sensitivity bounds into the asymptotic target, and SensitivityCampaign.finite_certificate_log, which expresses the same interface using a logarithmic score. Their normalization and unbounded-sensitivity conclusions are part of their proved statements.

The supplied proof targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The supporting assertions are proved in the submitted source; no conjectural lemma or numerical approximation is used as an assumption. The general transfer estimates and exact certificate provide material for subsequent improvements, while this mission's goal remains the fixed campaign value 2.075.

Selected references and credits

OpenAI, A superquadratic separation between sensitivity and block sensitivity, problem 132, 2026. Formalization and source links.
Prove2Me contributors, Separation exponent at least 2.0391, 2026. Accepted theorem and proof.
Robin Kothari, Separation exponent at least 2.05, 2026. Accepted theorem and proof.
abhishekdpseok, Separation exponent at least 2.0635, 2026. Accepted theorem and proof, submission f80a3f37-72fa-4d56-a094-3e4d351764f3. The present development reuses its foundation, including its earlier source credits.
Robin Kothari and Codex, Seven-level nine-state sensitivity certificate: exponent 2.075, 19 October 2026. Full Lean proof and mathematical explanation supplied with this entry.

5 thms3 active usersReviewed

Numerical Analysis Optimization Quantum Information·Captain: mikedeng1

Optimizing Quantum Optimization Algorithms via Faster Quantum Gradient Computation: an ε-Accurate Gradient of a Smooth Analytic Function from Õ(c√d/ε · log(d/δ)) Phase-Oracle QueriesResearch Paper

Motivation

Many proposed quantum optimization and machine-learning methods (variational quantum eigensolvers, QAOA, quantum classifiers) tune the real parameters of a circuit by gradient descent on an objective $f:\mathbb R^d\to\mathbb R$ that is only accessible as a black box. Classically, a finite-difference estimate of $\nabla f$ costs on the order of $d$ evaluations of $f$ . Quantum algorithms can access $f$ coherently through a phase oracle $O_f:|x\rangle\mapsto e^{if(x)}|x\rangle$ , and the question is how many such queries are needed to learn $\nabla f(x)$ to accuracy $\varepsilon$ in the sup norm.

Timeline.

2005: Jordan (Phys. Rev. Lett. 95, 050501) gave an algorithm that reads off the gradient of a nearly affine function from a single oracle call on a uniform superposition over a grid, followed by an inverse quantum Fourier transform. The guarantee requires $f$ to be very close to affine on the grid.
2017–2019: Gilyén, Arunachalam and Wiebe (arXiv:1711.00465v3; SODA 2019) ran Jordan's algorithm on a high-degree central difference of $f$ rather than on $f$ . For functions whose derivatives satisfy a Gevrey-type bound, they obtained $\widetilde O(c\sqrt d/\varepsilon)$ phase queries (Theorem 25), and proved a matching $\Omega(\sqrt d/\varepsilon)$ lower bound for a class of smooth functions.
2024: Nannicini's lecture notes (arXiv:2408.07086) present Jordan's algorithm in this form. Their Lean formalization on the platform contains the grid, its Fourier transform and the algorithm's state, which this mission reuses.

Setting

A point of $\mathbb R^d$ is $x=(x_1,\dots,x_d)$ , with $\|x\|_\infty=\max_i|x_i|$ . The paper's $\mathbb N$ is $\{1,2,\dots\}$ .

Grid and Jordan's algorithm. For $n$ qubits put $N=2^n$ . A bit string $b$ encoding the integer $j$ labels the grid point $x^{(b)}=j/N-1/2+1/(2N)$ , and $G_n$ is the set of these points (Definition 17). Algorithm 2 prepares $d$ registers of $n$ qubits in uniform superposition over $G_n^d$ . It applies the phase oracle $|x\rangle\mapsto e^{2\pi i N f(x)}|x\rangle$ once, applies the inverse grid Fourier transform to each register, and measures the outcome $(k_1,\dots,k_d)\in G_n^d$ .

Index sequences and analyticity. For $\alpha\in[d]^k$ , $\partial_\alpha f$ is the $k$ -th partial derivative along the coordinates $\alpha_1,\dots,\alpha_k$ , and $y^\alpha=\prod_j y_{\alpha_j}$ (Definition 4). The function $f$ is analytic around $x$ if

f(x+y)=\sum_{k=0}^\infty\sum_{\alpha\in[d]^k}\frac{y^\alpha\,\partial_\alpha f(x)}{k!}\quad\text{for all }y\in\mathbb R^d

(Definition 5, there at $x=0$ ).

Central differences. The central difference coefficients are

a_\ell^{(2m)}=\frac{(-1)^{\ell-1}}{\ell}\frac{\binom m{|\ell|}}{\binom{m+|\ell|}{|\ell|}}\quad(0<|\ell|\le m),\qquad a_0^{(2m)}=0.

The degree- $2m$ central difference of $f$ is $f_{(2m)}(y)=\sum_{\ell=-m}^m a_\ell^{(2m)}f(\ell y)$ , an approximation of $\nabla f(0)\cdot y$ (Definition 7).

Queries. A fractional query $O_f^s:|x\rangle\mapsto e^{isf(x)}|x\rangle$ with $|s|\le1$ counts as one query (Definitions 10–11). The algorithm of Theorem 25 has parameters $m,n_\varepsilon,n_M,T$ and $r>0$ . It runs Algorithm 2 with $n=n_\varepsilon+n_M$ qubits per register on the phase $2\pi\,2^{n_\varepsilon} g_{(2m)}(rz)$ , where $g(y)=f(x+y)$ . It reads each outcome $k$ as $(2^{n_M}/r)\,k$ , repeats $T$ times and outputs the coordinate-wise median. One run costs $\sum_\ell\lceil 2\pi 2^{n_\varepsilon}|a^{(2m)}_\ell|\rceil$ queries to $O_f$ .

Formalization targets

Goal: Theorem 25

There is an absolute constant $C$ such that for every $d\ge1$ , $0<\varepsilon\le c$ and $\delta>0$ some parameter choice, made before $x$ and $f$ , uses at most

C\,\frac{c\sqrt d}{\varepsilon}\,\log\Big(2+\frac{c\sqrt d}{\varepsilon}\Big)\log\Big(2+\log\Big(2+\frac{c\sqrt d}{\varepsilon}\Big)\Big)\log\Big(2+\frac d\delta\Big)

queries. For every $x$ and every smooth $f$ that is analytic around $x$ with $|\partial_\alpha f(x)|\le c^k k^{k/2}$ ( $k\ge1$ ), it outputs $\tilde\nabla f(x)$ with $\|\nabla f(x)-\tilde\nabla f(x)\|_\infty\le\varepsilon$ with probability at least $1-\delta$ .

Milestones

Lemma 34, $\sum_\ell|a^{(2m)}_\ell\ell^{k+1}|\le6e^{-7m/6}m^{k+3/2}$ for $k\ge2m$ .
Lemma 22: (23), $|f'(0)\delta-f_{(2m)}(\delta)|\le e^{-m/2}\|f^{(2m+1)}\|_\infty|\delta|^{2m+1}$ ; and (24), $\sum_{\ell=0}^m|a_\ell^{(2m)}|<\sum_{\ell=1}^m 1/\ell\le\ln m+1$ .
The moment identity (proof of Theorem 24): $\sum_{\ell=-m}^m a_\ell^{(2m)}\ell^k$ is $1$ for $k=1$ and $0$ for the other $k\le2m$ .
Lemma 36, a tail bound $\mathbb P[|\sum_\alpha H_\alpha x^\alpha|\ge\sqrt2(r\sqrt{dk/2})^k]\le r^{-2k}$ for i.i.d. symmetric $x_i\in[-1/2,1/2]$ .
Theorem 24: $|\nabla f(0)y-f_{(2m)}(y)|\le\sum_{k\ge2m+1}(8Rcm\sqrt d)^k$ for all but a $1/1000$ fraction of $y\in R\cdot G_n^d$ .
The choice of $r$ (proof of Theorem 25): with $r^{-1}=9cm\sqrt d\,(81\cdot8\cdot42\pi cm\sqrt d/\varepsilon)^{1/(2m)}$ ,

\sum_{k=2m+1}^\infty(8rcm\sqrt d)^k\le\frac{\varepsilon r}{8\cdot42\pi}.

Lemma 20: if $|f(x)-g\cdot x-c|\le1/(42\pi N)$ off a $1/1000$ fraction of $G_n^d$ and $\|g\|_\infty\le1/3$ , then $\Pr[|k_i-g_i|>4/N]\le1/3$ .
Theorem 21 (query part): $O(\log(d/\rho))$ runs and a median give $\Pr[\|\tilde g-g\|_\infty>\varepsilon]\le\rho$ .
Display (25): $\sum_\ell\lceil|a^{(2m)}_\ell|S\rceil\le2m+S(2\log m+2)$ . The page prints the middle term $S\sum_\ell a^{(2m)}_\ell$ without absolute values; the formal statement uses $|a^{(2m)}_\ell|$ .

Significance

The result. Theorem 25 gives a quantum gradient algorithm whose query count grows like $\sqrt d$ in the dimension and nearly linearly in $1/\varepsilon$ . Jordan's original analysis gives $\sqrt d/\varepsilon^2$ , and classical finite differences need on the order of $d$ evaluations. Section 6 of the paper shows that $\sqrt d/\varepsilon$ cannot be beaten for a class of smooth functions, so Theorem 25 is optimal up to logarithmic factors. Section 5.5 shows that probability oracles built from parametrized circuits satisfy the derivative bound, so the theorem applies to gradient-based training of variational circuits.

Formalizing it. The theorems are proved in the paper; this mission is not aware of a machine-checked proof of any of them. A formal proof would check the explicit constants (1/1000, $42\pi$ , $8Rcm\sqrt d$ , $6e^{-7m/6}$ ) and the accounting of fractional queries, which are spread across the main text and Appendix A. It would also produce reusable libraries: exactness and coefficient bounds for central differences, concentration of random multilinear forms, and a phase-estimation-style analysis of Jordan's algorithm on the published Lean model.

Difficulty

Jordan's algorithm reads off a gradient only if the phase is almost exactly affine on the whole grid. A truncated Taylor expansion of $f$ makes the error of order- $k$ terms grow like $d^{k}$ on the cube, which destroys the $\sqrt d$ scaling. The approximation is only good on most of the grid, not all of it. The guarantee therefore has to tolerate a small fraction of bad grid points inside the quantum algorithm (Lemma 20) and has to control random multilinear forms (Lemma 36). The analysis also has to keep explicit, $m$ -uniform control of the central difference coefficients, whose sizes enter both the approximation error and the query count.

Formalization scope

Representation. $\mathbb R^d$ is Fin d → ℝ, whose norm is $\|\cdot\|_\infty$ . $\partial_\alpha f$ is iteratedFDeriv along coordinate vectors, and functions are assumed $C^\infty$ (ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞)). "Analytic" is the Taylor representation (5) at the relevant point (IsTaylorRep), not Mathlib's local AnalyticAt.
Fractions and probabilities. "All but a $1/1000$ fraction of $G_n^d$ " means the number of bad grid labels is at most $N^d/1000$ . Probabilities are those of the published Algorithm 2 state QAlgorithms.gradientAlgState. Independent runs multiply.
Indices and constants. $\mathbb N$ starts at $1$ : derivative bounds are for $k\ge1$ , and $m\ge1$ . $O(\cdot)$ and $\widetilde O(\cdot)$ are absolute constants quantified before every parameter, with the polylog factor of display (26) written out.
Added hypotheses.
- Theorem 24 assumes $8Rcm\sqrt d<1$ , the condition under which its printed series is finite.
- Lemma 22 uses a bound $B$ on $|f^{(2m+1)}|$ in place of the supremum.
- Theorem 21 requires its register size $n=n_\varepsilon+n_M$ to be a natural number.
Query count. The count is a definition: $T\sum_\ell\lceil2\pi2^{n_\varepsilon}|a_\ell^{(2m)}|\rceil$ .
Not formalized. Gate complexity (no circuit model), the probability-to-phase oracle conversions, the lower bounds and Theorem 23.
Ruled out. None of the following counts as Theorem 25: a goal with an existential over arbitrary functions of $f$ (which could output $\nabla f(x)$ with no queries), a query count not tied to the algorithm that is run, or a statement for one fixed $d$ .

Contributions are welcome at every level. Most useful are general facts about central difference coefficients (moment identities, $\sum|a_\ell|$ , the binomial ratio bounds), concentration of multilinear forms in independent symmetric variables, and the single-run analysis of gradientAlgState. These are reusable beyond this mission.

Selected references

A. Gilyén, S. Arunachalam, N. Wiebe, Optimizing quantum optimization algorithms via faster quantum gradient computation, arXiv:1711.00465v3 (2018); Proceedings of SODA 2019. https://arxiv.org/abs/1711.00465
S. P. Jordan, Fast quantum algorithm for numerical gradient estimation, Physical Review Letters 95(5):050501, 2005. https://arxiv.org/abs/quant-ph/0405146
J. Li, General explicit difference formulas for numerical differentiation, Journal of Computational and Applied Mathematics 183(1):29–52, 2005.
G. Nannicini, Quantum algorithms for optimizers, arXiv:2408.07086, 2024. https://arxiv.org/abs/2408.07086
M. A. Nielsen, I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2002 (phase estimation, §5.2).

14 thms3 active usersReviewed

Completed

Combinatorics·Captain: Abhishek Anand

Block Sensitivity vs. Sensitivity: Reach 2.0635Open Problem

Establish a separation exponent of at least $2.0635$ between block sensitivity and sensitivity of total Boolean functions.

For every $\varepsilon>0$ and integer $S\ge2$ , construct $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.0635-\varepsilon}$ .

5 thms3 active usersReviewed

Completed

Combinatorics·Captain: @bwdaugherty

Block Sensitivity vs. Sensitivity: α ≥ 2.0391Open Problem

Improve the separation exponent between block sensitivity and sensitivity of total Boolean functions. This mission targets $\alpha\ge2.0391$ ; higher is better.

For every $\varepsilon>0$ and every integer $S\ge2$ , the goal asks for a function $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.0391-\varepsilon}$ . The shared definition SensitivityCampaign.AchievesExponent expresses exactly this requirement.

Using a finite certificate. Choose a total Boolean function $f$ , an input $x$ , and integers $A,B>1$ . Prove $s(f)\le A$ , $B\le bs(f,x)$ , and $A^{2.0391}\le B$ , then apply SensitivityCampaign.finite_certificate. Here $bs(f,x)$ means block sensitivity at the chosen input. The shared theorem handles normalization and passage to arbitrarily large sensitivity. Its proof is a foundation milestone; a proof depending on an open milestone remains conditional until that milestone is proved.

Direct proofs of the asymptotic goal are equally welcome. Keep the shared definitions, replace the target value, and give your theorem a unique name. Use exact certified bounds; numerical estimates alone do not establish a record.

Background: the campaign proposal.

5 thms3 active usersReviewed

Completed

Combinatorics·Captain: Leo Shaposhnik

Block Sensitivity vs. Sensitivity: Reach 2.0205Open Problem

For every $\varepsilon>0$ and every integer $S\ge2$ , there exists a total Boolean function $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.0205-\varepsilon}$ .

The construction refines the tournament recursion of OpenAI/math. It keeps all four sensitivity profiles, sharpens the target-row count to fifteen, and bounds the gate contribution by separating the cases with and without a sink.

At depth $d=17$ , use tournament parameter $M=1475863$ , label alphabet $r=88$ , and $K=1439236$ disjoint OR copies. The proof obtains a finite seed and integers $A,B>1$ satisfying global sensitivity $s(f)\le A$ , block sensitivity at zero $bs(f,0)\ge B$ , and the exact integer comparison $A^{4041}<B^{2000}$ . This implies $A^{2.0205}<B$ ; the shared finite-certificate theorem supplies arbitrarily large sensitivity and the campaign conclusion.

The shared campaign definitions are retained. The local proof was checked in Lean 4.33.1 with Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. This draft targets a certified campaign improvement; no global optimality claim is made

15 thms3 active usersReviewed

Completed

Combinatorics·Captain: marwahaha

Block Sensitivity vs. Sensitivity: OpenAI BaselineResearch Paper

Certify the separation exponent $\alpha\ge2.000252407$ using OpenAI's construction. Sensitivity $s(f)$ counts individual bit flips that change the output; block sensitivity $bs(f)$ counts disjoint sensitive blocks. Both are maximized over inputs. The notation $bs(f,x)$ fixes one input, and $0$ denotes the all-zero input.

The goal requires arbitrarily large sensitivity and $bs(f)\ge s(f)^{2.000252407-\varepsilon}$ for every $\varepsilon>0$ . OpenAI's depth-nine seed, with $M=9^{10}$ , supplies a slightly larger exponent; the displayed decimal must be certified exactly.

This mission is the campaign's foundation. Its central reusable milestone turns a finite certificate $s(f)\le A$ , $bs(f,x)\ge B$ , $A,B>1$ , and $A^a\le B$ into the asymptotic claim at exponent $a\ge0$ . Normalization and sensitivity growth are proof obligations. Later missions import this theorem and the shared definitions.

OpenAI's quantitative separation is already proved on Prove2Me. This mission certifies the numerical exponent and the reusable bridge; its goal remains Open until all required proofs are accepted.

40 thms3 active usersReviewed

Number Theory·Captain: mikedeng1

Integer Factorization: Why Two-Item Joint Replenishment Is Hard 4: For Primes p_i Near 2^(λa_i), ∏p_i Has a Divisor in [⌈L⌉, ⌊U⌋] iff the a_i Split into Two Equal-Sum PartsResearch Paper

Motivation

The RangeDivisor problem asks whether an integer has a divisor in a specified short interval. It is the decision problem connecting number theory to the two item periodic joint replenishment model studied by Schulz and Telha. Their Appendix starts with Partition, the problem of splitting a list of positive integers into two groups of equal sum, and constructs a RangeDivisor instance from primes chosen near carefully scaled powers of two. The equivalence between the two yes instances is the mathematical target here. Schulz and Telha, Appendix, pp. 16–17

The route has a history. Karp included Partition among classical combinatorial decision problems in 1972. Shor discussed an NP complete variant of factoring in 2011, and Schulz and Telha adapted that connection to their joint replenishment setting. The paper cites a 2016 conditional short interval result of Dudek, Grenié, and Molteni to obtain primes that can be sampled near the requested powers. That prime existence claim motivates the reduction, while this mission starts with primes satisfying the specified windows. Karp, 1972 Shor, 2011 Schulz and Telha, p. 16

Setting

A Partition input is an indexed list $a_1,\ldots,a_n$ of natural numbers. It is a yes instance if some index set $S$ has $2\sum_{i\in S}a_i=\sum_i a_i$ . Indices matter: equal entries may occur more than once and can be assigned separately. For this reduction, $n\ge1$ , $B\ge1$ , and each entry lies in $[2^B,2^{B+1})$ . The total is assumed even. Write $A=\frac12\sum_i a_i$ , so $A$ is then an integer even though its Lean definition is real valued. Schulz and Telha, Appendix, p. 16

Set $\lambda=3B/2^B$ and $b_i=\lambda a_i$ . The input also includes a real constant $c$ and a prime $p_i$ for each index. Every prime lies in the open interval

2^{b_i}-cb_i2^{b_i/2}<p_i<2^{b_i}+cb_i2^{b_i/2},

and the paper's quantitative small window condition $cb_i<\lambda2^{b_i/2}/(4n)$ holds for every $i$ . Define $M=\prod_i p_i$ , $L=2^{\lambda(A-1/2)}$ , and $U=2^{\lambda(A+1/2)}$ . The RangeDivisor instance uses the integer endpoints $\lceil L\rceil$ and $\lfloor U\rfloor$ . A valid instance $(M,L',U')$ has $0<L'\le U'\le M$ and $L'+U'<2\sqrt{2L'U'}$ ; it is a yes instance if some divisor of $M$ belongs to $[L',U']$ . These conditions are part of the target, not conventions left to the reader. Schulz and Telha, pp. 12, 15–17

Formalization targets

Appendix reduction

The goal states the full correctness of the rounded numerical construction. Under the prime windows above and the paper's condition $2^{\lambda/2}+2^{-\lambda/2}<2\sqrt2$ , the triple $(M,\lceil L\rceil,\lfloor U\rfloor)$ is a valid RangeDivisor instance and

M\text{ has a divisor in }[\lceil L\rceil,\lfloor U\rfloor] \quad\Longleftrightarrow\quad (a_i)_{i=1}^n\text{ admits an equal sum partition}.

The milestones follow the Appendix's stated intermediate claims: the elementary power estimate, the chain of prime windows, the equivalence for a subset sum and its subproduct, the unrounded divisor equivalence, the numerical interval condition, and the paper's rounding assertion. The unrounded equivalence is a separate milestone because it isolates the number theoretic claim from the integer endpoint convention. Schulz and Telha, pp. 15–17

Significance

The result turns equal sum partitions into divisors in a controlled interval of a product of primes. This is the first mathematical half of the paper's route from Partition to the periodic joint replenishment decision problem; Lemma 3 supplies the second half. The present theorem identifies exactly which numerical statements that route needs, including validity of the rounded interval. Without the equivalence, the constructed integer might have a divisor in the interval for reasons unrelated to the original Partition input. Schulz and Telha, §3 and Appendix

The paper proves its reduction on paper. This mission asks for machine checked proofs of the reduction's arithmetic assertions, not a new complexity result. The reusable pieces are finite product bounds for real powers, the description of divisors of a finite prime product as subproducts, and a rounding result for the RangeDivisor side condition. Such pieces can support other reductions that encode additive choices by products of nearby primes.

Difficulty

The prime bounds are stated one index at a time, while a divisor of $M$ may combine any number of factors. Controlling the product through a strict interval must account for every subset size, including the empty subset and repeated primes. The converse has an additional discrete issue: a product close to the target power should correspond to the exact integer half sum, not merely to a nearby real value. After that, changing real endpoints to integer endpoints must preserve both the divisor question and the numerical promise required by RangeDivisor. A statement only about divisors in the unrounded interval leaves the eventual decision instance incomplete.

Formalization scope

Lean represents inputs as functions Fin n → ℕ, index subsets as finite sets, primes with Nat.Prime, and exponents and interval endpoints in the real numbers. The real powers use real exponentiation; $A$ uses real division, not truncated natural division. The general Partition and RangeDivisor predicates are separate definitions. The Appendix's $\lambda$ , $b_i$ , $L$ , and $U$ are derived definitions of the particular input, so a theorem cannot choose convenient values for them. Strict window inequalities remain strict, and the goal retains the printed sampling window rather than assuming only the later multiplicative bound. It explicitly asserts the rounded instance condition as well as the yes instance equivalence.

The printed converse needs an even total: if the total is odd, $A$ is half integral and a subset one half unit away can produce a product inside $(L,U)$ without being a Partition solution. A computational reduction can send an odd total to a fixed no instance; this theorem covers the nontrivial even branch. The prose condition that $B$ is sufficiently large is replaced by the paper's displayed inequality $cb_i<\lambda2^{b_i/2}/(4n)$ , and the printed endpoint condition is stated directly. The proof must not gain a vacuous equivalence by allowing zero indices, by selecting the primes existentially to fit the answer, or by dropping the sampled prime windows.

This mission formalizes the correctness of the reduction behind Theorem 2; polynomial running time, randomized prime sampling, the conditional prime count, the padding of arbitrary Partition inputs to a fixed bit range, and the NP hardness assertion are outside its Lean statement. The Riemann hypothesis is needed by the paper to justify finding suitable primes efficiently, not as an assumption of the arithmetic equivalence once those primes are given. Contributions that establish the product, divisor, or rounding milestones are welcome. Schulz and Telha, pp. 15–17

Selected references

A. S. Schulz and C. Telha, Integer Factorization: Why Two-Item Joint Replenishment Is Hard, Operations Research, 2024; the formalization uses arXiv:2007.09045v1 (2020), Appendix, pp. 16–17.
R. M. Karp, Reducibility Among Combinatorial Problems, in Complexity of Computer Computations, 1972. DOI.
P. W. Shor, An NP-complete variant of factoring, 2011. Original post cited by the paper.
A. W. Dudek, L. Grenié, and G. Molteni, Primes in explicit short intervals on RH, International Journal of Number Theory 12(5), 2016, 1391–1407; cited in Schulz and Telha, p. 16.

10 thms3 active usersReviewed

Completed

Theoretical Computer Science·Captain: avi

Fast Integer Multiplication on Multitape Turing Machines: Schönhage–Strassen and the ToolkitResearch Paper

Motivation

Every fast integer-multiplication algorithm in the literature is stated for the multitape Turing machine. The algorithms are built from a small set of standard subroutines whose costs are usually quoted as "well known":

linear-time addition;
sorting by merging on tapes;
fast matrix transposition;
a crude $O(n^{1+\delta})$ multiplier, used for the small multiplications inside fixed-point arithmetic.

Harvey–van der Hoeven (2021) use all of these in §2.1, §2.3 and §4–§5 of their $O(n\log n)$ paper. They cite Brent–Zimmermann for the arithmetic, Knuth vol. 3 for merge sort, and Bostan–Gaudry–Schost for transposition.

This mission formalizes that toolkit in the shared machine model IntMul_MultitapeModel. Its goal is the classical Schönhage–Strassen bound $\mathsf M(n)=O(n\log n\log\log n)$ . The toolkit is exactly what is missing before the recursive step of the companion mission, Harvey–van der Hoeven Proposition 5.4, can be decomposed. Proposition 5.4 is the last open link on that mission's main line.

Timeline (multitape Turing model).

Folklore: schoolbook multiplication in $O(n^2)$ ; addition in $O(n)$ .
1962: Karatsuba–Ofman, $O(n^{\log_2 3})$ .
1963–1966: Toom and Cook, $O(n^{1+\epsilon})$ for every $\epsilon>0$ .
1971: Schönhage–Strassen, $O(n\log n\log\log n)$ .
1973 (2nd ed. 1998): Knuth, TAOCP vol. 3 §5.4, merge sorting on tapes.
2007: Bostan–Gaudry–Schost, Appendix: transposing an $m\times k$ matrix with $N$ bits in total in $O(N\log\min(m,k))$ on a multitape machine.
2019/2021: Harvey–van der Hoeven, $O(n\log n)$ , using all of the above.

Setting

The machine model, input and output conventions, and the time-bound predicate $\mathrm{MulTimeBound}$ are those of IntMul_MultitapeModel. That model follows Montanaro's lecture notes:

$k\ge2$ one-way tapes, with a read-only input tape and a separate output tape;
$\triangleright$ appears only in cell $0$ of each tape;
$\mathrm{START}\ne\mathrm{HALT}$ , and the halting state freezes the configuration.

For subroutines whose input is not of the form $x\#y$ , the new definitions file IntMul_MultitapeWords starts the machine on an arbitrary word over $\{0,1,\#\}$ . It also provides the encodings

$\mathrm{bits}(x)$ , a bit string written as a word;
$u_1\#u_2\#\cdots\#u_m$ , a list of words joined by separators.

Formalization targets

Goal: Schönhage–Strassen

$\mathrm{MulTimeBound}(n\mapsto n\ln n\ln\ln n)$ : a single multitape machine multiplies $n$ -bit integers for every $n\ge1$ in worst-case time $O(n\log n\log\log n)$ .

Milestones

Schoolbook multiplication: $\mathrm{MulTimeBound}(n^2)$ .
Karatsuba–Ofman: $\mathrm{MulTimeBound}(n^{\log_2 3})$ .
Linear-time addition: on input $x\#y$ with $|x|=|y|=n$ , output $\operatorname{bin}_{n+1}(\operatorname{val}x+\operatorname{val}y)$ within $c(n+1)$ steps.
Merge sort on tapes:
- Input: $m$ records, each a key of $\ell$ bits and a payload of $q$ bits, written as $k_1\#p_1\#k_2\#p_2\#\cdots$ .
- Output: the records stably sorted by key value, in the same format.
- Time: $c\,(N+1)(\lceil\log_2 m\rceil+1)$ , where $N$ is the input length.
Matrix transposition:
- Input: an $m\times k$ matrix ( $m,k\ge1$ ) with entries of $\ell\ge1$ bits, in row-major order. Entries are separated by $\#$ and rows by $\#\#$ .
- Output: the transpose, in the same format.
- Time: $c\,(N+1)(\lceil\log_2\min(m,k)\rceil+1)$ .

Formalization scope

Constants may depend only on the machine. All time bounds count exact steps of one fixed machine in the shared model. Building machines by composing smaller ones (subroutine calls, scratch tapes, recursion) is the solvers' business; any reusable infrastructure for it is welcome as published lemmas.

Selected references

A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7 (1971), 281–292.
A. Karatsuba, Yu. Ofman, Multiplication of multidigit numbers on automata, Soviet Physics Doklady 7 (1963), 595–596.
D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, 2nd ed., Addison-Wesley, 1998, §5.4.
A. Bostan, P. Gaudry, É. Schost, Linear recurrences with polynomial coefficients and application to integer factorization and Cartier–Manin operator, SIAM J. Comput. 36 (2007), 1777–1806, Appendix.
R. P. Brent, P. Zimmermann, Modern Computer Arithmetic, Cambridge University Press, 2011, Ch. 1.
D. Harvey, J. van der Hoeven, Integer multiplication in time $O(n\log n)$ , Ann. of Math. 193 (2021), §2.1.
A. Montanaro, Computational Complexity, lecture notes, §3–§4.

15 thms3 active usersReviewed

Completed

Algorithmic Game Theory·Captain: mikedeng1

Settling the Complexity of Computing Approximate Two-Player Nash Equilibria: An (ε, δ)-WeakNash of a Bipartite Polymatrix Game Yields a (√ε(√ε + 5), δ)-Well-Supported WeakNashResearch Paper

Motivation

Computing an approximate Nash equilibrium of a two-player game is one of the central questions of algorithmic game theory. For a constant approximation $\epsilon$ , the algorithm of Lipton, Markakis and Mehta runs in quasi-polynomial time $n^{O(\log n/\epsilon^2)}$ , and for a long time it was unknown whether polynomial time is possible. A. Rubinstein, Settling the Complexity of Computing Approximate Two-Player Nash Equilibria (FOCS 2016, arXiv:1606.04550), proved that, assuming an exponential-time hypothesis for PPAD, quasi-polynomial time is also necessary.

The proof is a chain of reductions. Its middle links produce multiplayer games in which only most players are approximately best-responding (the WeakNash notions of Babichenko, Papadimitriou and Rubinstein, Can Almost Everybody be Almost Happy?, ITCS 2016). Its last link turns a bipartite multiplayer game into a two-player game. Section 8.1 of the paper sits between the two: it shows that the weaker mixed-response notion of WeakNash can be converted into the stronger support-based notion, with a loss of only a square root in the approximation. This mission formalizes that step, Lemma 8.1, together with the intermediate claims of its proof.

Timeline. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 2009, doi:10.1137/070699652) introduced the trimming argument (their Lemma 4.28 and Claim 6) for exact-all-players $\epsilon$ -approximate equilibria of general games. Babichenko–Papadimitriou–Rubinstein (2016) introduced $(\epsilon,\delta)$ -WeakNash. Rubinstein (2016) adapted the trimming argument to WeakNash of bipartite polymatrix games, where the constant no longer grows with the number of players.

Setting

A finite game has a finite set of players $\mathcal I$ , a finite action set $S^v$ for each player $v$ , and utilities $u_v$ on action profiles. A mixed strategy $x^v$ is a probability vector on $S^v$ ; a mixed profile $x=(x^v)_v$ is one mixed strategy per player, drawn independently. For an action $s\in S^v$ , $U^v_s(x^{-v})$ is the expected utility of $v$ when $v$ plays $s$ and the others play $x^{-v}$ , and $U^v_{\max}(x^{-v})=\max_{s}U^v_s(x^{-v})$ .

$x^v$ is an $\epsilon$ -best mixed response if $\mathbb E_{a\sim x}[u_v(a)]\ge\max_{y\in\Delta S^v}\mathbb E_{a\sim(y;x^{-v})}[u_v(a)]-\epsilon$ .
$x$ is an $(\epsilon,\delta)$ -WeakNash if at least a $(1-\delta)$ -fraction of all players play an $\epsilon$ -best mixed response.
$x$ is an $(\epsilon,\delta)$ -Well-Supported WeakNash if, for at least a $(1-\delta)$ -fraction of all players $v$ , every action in the support of $x^v$ satisfies $U^v_s(x^{-v})\ge U^v_{\max}(x^{-v})-\epsilon$ .

A polymatrix game is one in which each pair of players plays a two-player subgame, each player uses one action in all of its subgames, and its utility is the sum of its subgame payoffs. In a complete bipartite polymatrix game the players form two sides $V_A$ , $V_B$ with $n_A=|V_A|$ , $n_B=|V_B|$ ; every $v\in V_A$ plays a bimatrix subgame $U^{v,w}$ against every $w\in V_B$ , and same-side pairs play nothing. Lemma 8.1 assumes the payoffs of $V_A$ -vertices lie in $[0,1/n_B]$ and those of $V_B$ -vertices in $[0,1/n_A]$ , so every utility lies in $[0,1]$ .

The trimmed profile $\hat x$ with parameter $k$ : every player $v$ that plays $\epsilon$ -optimally in $x$ drops the actions with $U^v_s(x^{-v})<U^v_{\max}(x^{-v})-\epsilon k$ , whose total mass is $z^v$ , and renormalises, $\hat x^v_s=x^v_s/(1-z^v)$ on the kept actions; every other player keeps $x^v$ .

Formalization targets

Goal: Lemma 8.1

For a complete bipartite polymatrix game with the payoff ranges above, $\epsilon>0$ , and an $(\epsilon,\delta)$ -WeakNash $x$ , the trimmed profile with $k=1+1/\sqrt\epsilon$ satisfies

\hat x\ \text{is a}\ \bigl(\sqrt\epsilon\,(\sqrt\epsilon+5),\ \delta\bigr)\text{-Well-Supported WeakNash}.

Milestones (proof of Lemma 8.1)

For $k>1$ and an $\epsilon$ -optimal player $v$ : $z^v\le 1/k<1$ .
Claim 8.2: $\sum_{s}|\hat x^v_s-x^v_s|\le 2/(k-1)$ for every player $v$ .
For every vertex $v$ and action $s$ : $|U^v_s(x^{-v})-U^v_s(\hat x^{-v})|\le 2/(k-1)$ .
For every $k>1$ : $\hat x$ is a $\bigl(k\epsilon+\tfrac{2}{k-1},\delta\bigr)$ -Well-Supported WeakNash.

Significance

The result. Lemma 8.1 is the link that allows the hardness of WeakNash, the notion the PPAD-hardness argument naturally produces, to be transferred to the support-based notion used by the two-player reduction of Section 8.2 (Lemma 8.3, via Althöfer's games). The polynomial loss $\epsilon\mapsto O(\sqrt\epsilon)$ and the unchanged $\delta$ are what keep the final constant approximation constant. The same trimming technique, with constants that do not depend on the number of players, applies to any polymatrix game with normalised payoffs.

Formalizing it. The result is proved on paper; it is not formalized anywhere. The published platform items DGPNash.WellSupported.* formalize the Daskalakis–Goldberg–Papadimitriou version, which assumes every player is $\epsilon$ -optimal and has a constant growing with the number of players; this mission produces the WeakNash and polymatrix version and a reusable vocabulary of WeakNash notions (Definitions 2.5–2.9) for the rest of the paper.

Difficulty

The obvious argument applies the trimming of Daskalakis–Goldberg–Papadimitriou to every player, and it fails in two places. First, only a $(1-\delta)$ -fraction of players are $\epsilon$ -optimal; for the others the trimmed mass $z^v$ can equal $1$ , so the renormalisation is undefined and those players cannot be trimmed, while their neighbours' payoffs still depend on them. Second, the general bound on how much a payoff moves when the other players' strategies move grows with the number of players, which would make the final constant depend on $n_A$ and $n_B$ ; Lemma 8.1 has no such dependence, and the payoff normalisation $[0,1/n_B]$ , $[0,1/n_A]$ is what must absorb it. The constant $2/(k-1)$ of milestone 4 is tight enough that the page's own displayed chain, which ends at $4/(k-1)$ , does not reach it directly.

Formalization scope

Players are the disjoint union VA ⊕ VB; action sets are finite types S i; subgame payoffs are PA v w (for $v\in V_A$ against $w\in V_B$ ) and PB w v. The general polymatrix payoff (Definition 2.9) sums over $j\ne i$ ; the bipartite instance sets same-side subgames to zero.
Mixed profiles, lotteries and expected payoffs are those of the published agt_games bundle. $U^v_s$ is DGPNash.NashMap.purePayoff; $U^v_{\max}$ , $z^v$ and the trim formula are maxPurePayoff, trimMass, trim of DGPNash_WellSupported_Equilibria.
The " $(1-\delta)$ -fraction of $i$ 's" is $(1-\delta)\,|\mathcal I|\le\#\{i:\ldots\}$ , over all players of both sides. The support of $x^v$ is $\{s: x^v_s>0\}$ . Maxima over strategies are written as "for every lottery / every action".
Added hypotheses: $\epsilon>0$ (needed for $k=1+1/\sqrt\epsilon$ ); $k>1$ in every general- $k$ milestone (the page's "for $k>1$ ").
Conventions: players that are not $\epsilon$ -optimal keep $x^v$ in $\hat x$ , since the page defines $\hat x^v$ only for the $\epsilon$ -optimal ones. "Bounded away from 1" is stated as $z^v\le 1/k$ . "In polynomial time" is not formalized.
Milestones 1 and 2 use no polymatrix structure and are stated for arbitrary finite games.

The bare existence of some $(\sqrt\epsilon(\sqrt\epsilon+5),\delta)$ -Well-Supported WeakNash is a consequence of Nash's theorem and does not use $x$ ; the goal therefore names the specific trimmed profile $\hat x$ computed from $x$ .

Contributions welcome: proofs of the milestones; general lemmas expressing $U^v_s$ of a polymatrix game as a bilinear sum and the multilinearity of expected payoffs, which are reusable for the rest of the paper.

Selected references

A. Rubinstein, Settling the Complexity of Computing Approximate Two-Player Nash Equilibria, FOCS 2016; arXiv:1606.04550 (version dated August 26, 2016). https://arxiv.org/abs/1606.04550
C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, The Complexity of Computing a Nash Equilibrium, SIAM J. Comput. 39(1):195–259, 2009. https://doi.org/10.1137/070699652
Y. Babichenko, C. H. Papadimitriou, A. Rubinstein, Can Almost Everybody be Almost Happy?, Proc. ITCS 2016, pp. 1–9.
R. J. Lipton, E. Markakis, A. Mehta, Playing Large Games Using Simple Strategies, EC 2003. https://doi.org/10.1145/779928.779933

10 thms3 active usersReviewed

Completed

Operations Research Optimization Theoretical Computer Science·Captain: mikedeng1

Convex Quadratic and Semidefinite Programming Relaxations in Scheduling V: 3-Occurrence Max3Sat L-Reduces to R | rⱼ | Σ Cⱼ with Constants 32 and 1Research Paper

Motivation

The scheduling problem $R\,|\,r_j\,|\sum C_j$ asks for a nonpreemptive schedule of jobs on unrelated parallel machines, each job with a machine-dependent processing time and a release date, so that the total completion time is minimal. It is NP-hard, and the question that remains is how well it can be approximated in polynomial time. Positive results include the 2-approximation of Skutella (J. ACM 2001), based on a convex quadratic relaxation. This mission covers the negative side, from §7 of the same paper: the problem has no polynomial-time approximation scheme unless P = NP.

The standard route to such a statement is an L-reduction (Papadimitriou and Yannakakis 1991) from a problem already known to be MaxSNP-hard. MaxSNP-hard problems have no approximation scheme unless P = NP, by the PCP theorem (Arora et al. 1998).

Timeline.

1991: Papadimitriou and Yannakakis define MaxSNP and L-reductions, and show that MAX3SAT with a bounded number of occurrences per variable is MaxSNP-complete.
1998: Hoogeveen, Schuurman and Woeginger prove that $R\,|\,|\sum w_jC_j$ and $R\,|\,r_j\,|\sum C_j$ are MaxSNP-hard, by a reduction from a MaxSNP-hard variant of 3-dimensional matching.
2001: Skutella (§7, pp. 32–33) gives a shorter reduction from 3-OCCURRENCE MAX3SAT, the variant of MAX3SAT in which every variable occurs at most three times (MaxSNP-hard, see Ausiello et al. 1999, Corollary 8.15).

Setting

An instance $I$ of 3-OCCURRENCE MAX3SAT has $n$ variables and $m$ clauses. Each clause is a set of one to three literals (a variable $x$ or its negation $\neg x$ ), and each variable occurs at most three times in total. A truth assignment $t$ gives each variable the value true or false and satisfies a clause when one of the clause's literals is true. $\#(t)$ denotes the number of satisfied clauses, and $\mathrm{OPT}_{\mathrm{SAT}}(I)=\max_t \#(t)$ .

The scheduling instance $R(I)$ has $n+m$ jobs and $2n$ machines.

Every variable $x$ has a true machine and a false machine, and one v-job. The v-job is released at time $0$ , has processing time $4$ on the two machines of $x$ , and cannot run anywhere else.
Every clause $c$ has one c-job, released at time $3$ , with processing time $0$ . It may run on the false machine of $x$ when $x$ occurs in $c$ , on the true machine of $x$ when $\neg x$ occurs in $c$ , and nowhere else.

A schedule $S$ gives every job $j$ a machine and a start time $S_j\ge r_j$ , with no two jobs on one machine overlapping. Its value is the total completion time $\mathrm{VAL}(S)=\sum_j (S_j+p_j)$ . The truth assignment $\mathrm{SAT}(S)$ sets $x$ true exactly when the v-job of $x$ runs on the true machine. $\mathrm{OPT}_{\mathrm{SCH}}(R(I))$ is the minimum of $\mathrm{VAL}$ over feasible schedules.

Formalization targets

Goal: the L-reduction inequalities (Lemma 7.1 b) and the proof of Theorem 7.2, p. 33)

$R(I)$ has an optimal schedule $S_0$ , and

\mathrm{VAL}(S_0)=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I),\qquad \mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{VAL}(S_0)

for every feasible schedule $S$ . These are the two conditions of an L-reduction, with constants $\alpha=32$ and $\beta=1$ .

Milestones

Lemma 7.1 a) (p. 32): $\#(\mathrm{SAT}(S))\ge 4n+4m-\mathrm{VAL}(S)$ for every feasible $S$ .
Lemma 7.1 b) (p. 33): $\mathrm{OPT}_{\mathrm{SCH}}(R(I))=4n+4m-\mathrm{OPT}_{\mathrm{SAT}}(I)$ .
The two counting facts of the proof of Theorem 7.2: $\mathrm{OPT}_{\mathrm{SAT}}(I)\ge m/2$ and $n\le 3m$ .
The first L-reduction condition: $\mathrm{OPT}_{\mathrm{SCH}}(R(I))\le 12m+4m\le 32\,\mathrm{OPT}_{\mathrm{SAT}}(I)$ .
The second L-reduction condition: $\mathrm{OPT}_{\mathrm{SAT}}(I)-\#(\mathrm{SAT}(S))\le\mathrm{VAL}(S)-\mathrm{OPT}_{\mathrm{SCH}}(R(I))$ .

Significance

The result. The two inequalities are what an L-reduction requires. Combined with the MaxSNP-hardness of 3-OCCURRENCE MAX3SAT, they show that $R\,|\,r_j\,|\sum C_j$ is MaxSNP-hard (Theorem 7.2, due to Hoogeveen, Schuurman and Woeginger), and therefore has no polynomial-time approximation scheme unless P = NP. Together with the constant-factor algorithms of the earlier sections of the paper, this places the problem in APX but outside PTAS. The identity of Lemma 7.1 b) is exact, so the reduction transfers solutions in both directions with no loss beyond the affine shift $k\mapsto 4n+4m-k$ .

Formalizing it. The result is proved, on paper, by both the 1998 and the 2001 reductions. As far as the platform's corpus shows, neither is machine-checked. This mission produces a checked version of the combinatorial core of Skutella's reduction: the exact relation between optimal schedules of $R(I)$ and optimal truth assignments of $I$ , and the two L-reduction constants. A Lean model of 3-OCCURRENCE MAX3SAT and of nonpreemptive schedules with release dates and machine eligibility is a by-product.

Difficulty

The obvious argument is the paper's intuition: given a truth assignment, a c-job can start at time $3$ without conflicting with a v-job exactly when its clause is satisfied. That is not enough for Lemma 7.1 a), which concerns every feasible schedule. In an arbitrary schedule a v-job may be delayed so that c-jobs of unsatisfied clauses run before it on its machine, and v-jobs and c-jobs may start at arbitrary real times. To compare such a schedule with a normalized one, its total completion time has to be bounded from below by $4n+4m-\#(\mathrm{SAT}(S))$ . The bound depends on the occurrence limit of three, which caps how many c-jobs can share a machine with a given v-job; without that limit Lemma 7.1 a) is false. Lemma 7.1 b) also needs the existence of an optimal schedule, which the paper takes for granted.

Formalization scope

Variables and clauses are Fin n and Fin m; here $n$ and $m$ count variables and clauses, not jobs and machines as in the rest of the paper. A literal is a pair (x, b) with b = true for $x$ and b = false for $\neg x$ , and a clause is a Finset of literals. Jobs are Fin n ⊕ Fin m and machines Fin n × Bool. Infinite processing times are encoded by an eligibility relation. Start times are real numbers, and $\mathrm{VAL}$ is a real number; $\#$ and $\mathrm{OPT}_{\mathrm{SAT}}$ are natural numbers cast to the reals, so no natural-number subtraction occurs. $\mathrm{OPT}_{\mathrm{SCH}}$ is never a primitive: statements assert, or assume, a feasible schedule that is no worse than every feasible schedule.

Two conventions are fixed that the page leaves implicit:

Every clause has between one and three literals. An empty clause would leave its c-job with no machine, so $R(I)$ would have no schedule, and "at least $m/2$ " would fail.
Every variable occurs at least once. The bound $n\le 3m$ , and with it the constant $32$ , needs this: a variable that occurs nowhere adds $4$ to $\mathrm{OPT}_{\mathrm{SCH}}$ and nothing to $\mathrm{OPT}_{\mathrm{SAT}}$ .

Zero-length jobs need a precise non-overlap rule. Two distinct jobs on one machine must satisfy $S_j+p_j\le S_k$ or $S_k+p_k\le S_j$ . Under this rule a c-job at time $3$ conflicts with a v-job running over $[0,4)$ , but several c-jobs may share a start time. Reading jobs as half-open intervals $[S_j,S_j+p_j)$ would let a zero-length c-job sit inside a v-job, so every clause would count as satisfied: that formalization is ruled out.

Not formalized: MaxSNP, MaxSNP-hardness and Theorem 7.2's statement itself; the definition of an L-reduction as a pair of polynomial-time maps; the polynomial running time of $R$ and $\mathrm{SAT}$ ; the weighted variant for $R\,|\,|\sum w_jC_j$ in the last paragraph of §7, which the paper does not prove. Contributions are welcome on the counting facts, on a normal form for schedules of $R(I)$ (v-jobs at time $0$ , c-jobs at time $3$ or $4$ ), and on the existence of optimal schedules.

Selected references

M. Skutella, Convex quadratic and semidefinite programming relaxations in scheduling, J. ACM 48(2), 206–242, 2001. https://doi.org/10.1145/375827.375840
J. A. Hoogeveen, P. Schuurman, G. J. Woeginger, Non-approximability results for scheduling problems with minsum criteria, IPCO 1998, LNCS 1412, 353–366. https://doi.org/10.1007/3-540-69346-7_27
C. H. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
G. Ausiello, P. Crescenzi, G. Gambosi, V. Kann, A. Marchetti-Spaccamela, M. Protasi, Complexity and Approximation, Springer, 1999. https://doi.org/10.1007/978-3-642-58412-1
S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306

7 thms3 active usersReviewed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 1: In O(√nL) Predictor-Corrector Iterations It Finds LP and Dual Optima or Detects InfeasibilityResearch Paper

Motivation

Interior-point methods solve linear programs in polynomially many iterations, but the classical analyses assume something about the instance before the algorithm starts: a known strictly feasible primal–dual pair, a nonempty interior, or a big- $M$ bound on the feasible region of order $2^L$ , where $L$ is the bit length of the data. In practice none of this is known in advance, and an infeasible or unbounded instance should be reported rather than assumed away.

Ye, Todd and Mizuno (1994) removed these assumptions. They embed a standard-form linear program and its dual into a single homogeneous and self-dual artificial program (HLP), which always has a known interior starting point, and apply the Mizuno–Todd–Ye predictor–corrector method to it. The resulting algorithm needs no regularity assumption, no big- $M$ parameter, and an $O(\sqrt n L)$ iteration bound, the best known for interior-point methods. Self-dual embeddings of this kind are now the standard initialization in interior-point solvers for linear and conic programs.

Timeline. Karmarkar (1984) gave the first polynomial interior-point method on a homogeneous canonical form. Mizuno, Todd and Ye (1990) introduced the predictor–corrector method with $O(\sqrt nL)$ iterations under a known interior start. Kojima, Mizuno and Yoshise (1993) built a self-dual big- $M$ artificial problem. Ye, Todd and Mizuno (1994) combined homogeneity and self-duality without big $M$ , obtaining the result formalized here.

Setting

Given $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , the primal problem is (LP) $\min\{c^Tx : Ax=b,\ x\ge0\}$ and its dual is (LD) $\max\{b^Ty : A^Ty\le c\}$ , with dual slacks $s=c-A^Ty$ .

Fix $x^0>0$ , $s^0>0$ , $y^0$ and put $\bar b=b-Ax^0$ , $\bar c=c-A^Ty^0-s^0$ , $\bar z=c^Tx^0+1-b^Ty^0$ . The homogeneous self-dual program (HLP) in the variables $(y,x,\tau,\theta,s,\kappa)$ is

\begin{aligned} \min\ & ((x^0)^Ts^0+1)\,\theta\\ \text{s.t. } & Ax-b\tau+\bar b\theta=0,\qquad s=-A^Ty+c\tau-\bar c\theta\ge0,\qquad \kappa=b^Ty-c^Tx+\bar z\theta\ge0,\\ & -\bar b^Ty+\bar c^Tx-\bar z\tau=-(x^0)^Ts^0-1,\qquad x\ge0,\ \tau\ge0 . \end{aligned}

Its feasible set is $\mathcal F_h$ , and $\mathcal F_h^0$ is the subset with $(x,\tau,s,\kappa)>0$ . A strictly self-complementary solution is an optimal solution with $\theta=0$ and $(x+s;\tau+\kappa)>0$ . The paper then fixes $y^0=0$ , $x^0=s^0=e$ , so the objective is $(n+1)\theta$ and $(0,e,1,1,e,1)\in\mathcal F_h^0$ .

With $\mu=(x^Ts+\tau\kappa)/(n+1)$ , the neighborhood of the central path is $\mathcal N(\beta)=\{z\in\mathcal F_h^0 : \|(Xs;\tau\kappa)-\mu e\|\le\beta\mu\}$ (Euclidean norm). The predictor–corrector algorithm starts at $(0,e,1,1,e,1)$ . At even steps it solves a Newton system with centering parameter $\gamma=0$ and moves by the largest step keeping the iterate in $\mathcal N(1/2)$ . At odd steps it takes a full Newton step with $\gamma=1$ . A termination projection then solves a least-squares problem on the columns where $x_j^k\ge s_j^k$ and produces a candidate exact solution.

Formalization targets

Goal: Corollary 7

For integer data with bit length $L$ and $n\ge1$ , there is an absolute constant $C$ and a finite predictor–corrector run that reaches, within

k\le C\sqrt n\,L

iterations, an iterate whose termination output $u=(y^*,x^*,\tau^*,\theta^*,s^*,\kappa^*)$ either has $\tau^*>0$ with $x^*/\tau^*$ optimal for (LP) and $(y^*/\tau^*,s^*/\tau^*)$ optimal for (LD), or has $\tau^*=0$ with $c^Tx^*<0$ and (LD) infeasible, or $-b^Ty^*<0$ and (LP) infeasible.

Theorem 6

The same bound, with the conclusion that the termination output, rescaled to the normalization $e^Tx+e^Ts+\tau+\kappa-(n+1)\theta=n+1$ , is a strictly self-complementary solution of (HLP).

Milestones

Proposition 1 (self-duality of skew-symmetric programs), Theorem 2 (ii), (iv), (v), Theorem 5 (ii), the two Mizuno–Todd–Ye estimates in the proof of Theorem 6, the predictor-step and corrector-step claims, the termination claim, the integrality and $O(L)$ size of the (HLP) data, and Theorem 3 (i), (ii).

Significance

The result. Corollary 7 gives a single polynomial algorithm that decides the status of an arbitrary linear program. It returns optimal primal and dual solutions when they exist and an infeasibility certificate otherwise. It needs no Phase I, no big- $M$ constant and no interior assumption, and its $O(\sqrt nL)$ iteration count matches the best bound known under those assumptions. Theorem 3 is the bridge: an exact strictly self-complementary solution of (HLP) determines the status of (LP) and (LD).

Formalizing it. The paper's result is proved; no machine-checked proof of it is known. The mission produces a formal account of the self-dual embedding, the central-path neighborhood analysis for (HLP), an exact finite-termination step from an approximate iterate, and the reading of a bit-length complexity bound with explicit quantifier order. The neighborhood estimates and the bit-length machinery are reusable for other interior-point and complexity results.

Difficulty

The per-step estimates are short calculations once the orthogonality $d_x^Td_s+d_\tau d_\kappa=0$ is available. The step that resists is termination. Geometric decrease of the gap reaches $2^{-O(L)}$ in $O(\sqrt nL)$ iterations, but turning such an iterate into an exact strictly self-complementary solution requires a quantitative separation: on $\mathcal N(1/2)$ , once the gap is below $2^{-O(L)}$ , the comparison $x_j\ge s_j$ must identify the optimal partition and the least-squares projection must land in the positive orthant. That separation bound rests on determinant estimates for integer matrices (Hadamard-type bounds in terms of $L$ ) and on the strict complementarity of (HLP), neither of which comes from the iteration analysis itself. A second subtlety is that the algorithm is not a function: without a rank assumption the Newton system leaves $d_y$ undetermined.

Formalization scope

Data for the complexity statements are integer matrices and vectors, cast to $\mathbb R$ ; all optimization objects are real. $L$ is Schrijver's encoding size, $\sum(1+\lceil\log_2(|v|+1)\rceil)$ over the entries plus the dimensions, so $L\ge1$ whenever $n\ge1$ .
Every $O(\cdot)$ is pinned with an absolute constant chosen before $m$ , $n$ and the data: $O(\sqrt nL)$ as $C\sqrt n\,L$ , $2^{-O(L)}$ as $2^{-C'L}$ , and $O(L)$ as $C\cdot L$ . The hypothesis $n\ge1$ , implicit in the paper, is explicit.
The algorithm is a relation on finite runs: any solution of the Newton system may be used, and each predictor step taken before termination must attain the maximum in (13). The conclusion asserts a successful run and its output. Stopping at the successful iterate avoids requiring a later step whose maximum may not exist.
The termination projection is defined relationally (an output is built from a minimizer) and its existence is part of the conclusion. Theorem 6 is stated for the output rescaled to the normalization (9): the projection imposes only homogeneous constraints, so the unscaled output need not be feasible for (HLP).
"(LP) has a solution (feasible and bounded)" is read as "(LP) has an optimal solution". "An indication that (LP) or (LD) is infeasible" is the negative sign of $c^Tx^*$ or $-b^Ty^*$ together with the infeasibility it certifies, not the bare disjunction "one of them is infeasible".
"Optimal for (HLP)" means minimizing the objective over $\mathcal F_h$ . It is not defined as $\theta=0$ , which would make Theorem 2 (iv) definitional.
Norms are Euclidean and written out explicitly, since Lean's default norm on $\mathbb R^n$ is the sup norm.
(LP) and (LD) are built on the published general-form LP definitions (LinearOptimization_DualLP). The self-dual objects of the Vanderbei and Matoušek series are different embeddings and are not reused.

A complete development needs: skew-symmetric LP duality and strict complementarity (Goldman–Tucker) for (HLP), the Mizuno–Todd–Ye neighborhood calculus, and Hadamard-type bounds on integer determinants. Contributions to any milestone, or to these supporting libraries, are welcome.

Selected references

Y. Ye, M. J. Todd, S. Mizuno, An $O(\sqrt nL)$ -iteration homogeneous and self-dual linear programming algorithm, Mathematics of Operations Research 19(1), 53–67, 1994. https://doi.org/10.1287/moor.19.1.53
S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Mathematics of Operations Research 18(4), 964–981, 1993. https://doi.org/10.1287/moor.18.4.964
S. Mehrotra, Y. Ye, Finding an interior point in the optimal face of linear programs, Mathematical Programming 62, 497–515, 1993. https://doi.org/10.1007/BF01585180
M. Kojima, S. Mizuno, A. Yoshise, A little theorem of the big M in interior point algorithms, Mathematical Programming 59, 361–375, 1993. https://doi.org/10.1007/BF01581253
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4, 373–395, 1984. https://doi.org/10.1007/BF02579150
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

22 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 2: The Adaptive-Step Algorithm in N∞(β) or N∞⁻(β) with γ ≤ 2(1 − β) Attains Precision t in O(nt) IterationsResearch Paper

Why wide neighbourhoods

Primal-dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal-dual pairs whose complementarity products $x_js_j$ are all equal. Every such method confines its iterates to a neighbourhood of that path, and the neighbourhood governs both the theory and the practice. The first primal-dual path-following algorithm, by Kojima, Mizuno and Yoshise (1989), used the one-sided neighbourhood $\{x_js_j \ge \tfrac12\,x^Ts/n\}$ and attained precision $t$ in $O(nt)$ iterations. Kojima–Mizuno–Yoshise and Monteiro–Adler then switched to the narrow Euclidean neighbourhood $\mathcal N_2(\beta)$ and improved the bound to $O(\sqrt n\,t)$ . Practical codes nevertheless favour wide neighbourhoods, which allow long steps.

Mizuno, Todd and Ye (Cornell ORIE Technical Report 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993) analyse adaptive-step algorithms, which at every iteration take the longest step that keeps the iterate in the neighbourhood. This mission formalizes their §4: the adaptive-step algorithm in the wide neighbourhoods $\mathcal N_\infty(\beta)$ and $\mathcal N_\infty^-(\beta)$ attains precision $t$ in $O(nt)$ iterations. With $\beta$ close to $1$ , $\mathcal N_\infty^-(\beta)$ contains almost all of the strictly feasible set.

Setting

Fix $n\ge1$ , $m\ge0$ , $A\in\mathbb R^{m\times n}$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ , and consider

\text{(P)}\ \min\ c^Tx\ \text{ s.t. } Ax=b,\ x\ge0,\qquad \text{(D)}\ \max\ b^Ty\ \text{ s.t. } A^Ty+s=c,\ s\ge0 .

The strictly feasible pairs $\mathcal F^0$ are the $(x,s)$ with $x>0$ , $s>0$ , $Ax=b$ , and $A^Ty+s=c$ for some $y$ . For such a pair the duality gap is $x^Ts$ , and the duality measure is $\mu=x^Ts/n$ . Write $X=\operatorname{diag}(x)$ , $S=\operatorname{diag}(s)$ and $e=(1,\dots,1)^T$ .

Norms: $\|\cdot\|$ is the Euclidean norm, $\|\cdot\|_\infty$ the maximum norm, and $\|z\|^-_\infty:=\|z^-\|_\infty$ , $\|z\|^+_\infty:=\|z^+\|_\infty$ with $(z^-)_j=\min\{z_j,0\}$ and $(z^+)_j=\max\{z_j,0\}$ . For $\beta\in(0,1)$ the wide neighbourhoods are

\mathcal N_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|_\infty\le\beta\mu\},\qquad \mathcal N^-_\infty(\beta)=\{(x,s)\in\mathcal F^0:\ \|Xs-\mu e\|^-_\infty\le\beta\mu\}.

The second says only that $x_js_j\ge(1-\beta)\mu$ for every $j$ .

The search direction $d=(d_x,d_s)$ with centering parameter $\gamma$ solves, for some $d_y$ ,

Sd_x+Xd_s=\gamma\mu e-Xs,\qquad Ad_x=0,\qquad A^Td_y+d_s=0, \tag{2}

and the step is $x(\theta)=x+\theta d_x$ , $s(\theta)=s+\theta d_s$ . The scaled quantities $p=X^{-1/2}S^{1/2}d_x$ , $q=X^{1/2}S^{-1/2}d_s$ , $r=(XS)^{-1/2}(\gamma\mu e-Xs)$ satisfy $p+q=r$ and $p^Tq=0$ . The componentwise product $Pq=(p_jq_j)_j$ is the second-order term $D_xd_s$ .

Algorithm 2 with neighbourhood $\mathcal N$ and $\gamma\in(0,1)$ starts at $(x^0,s^0)\in\mathcal N$ with $(x^0)^Ts^0\le2^t$ . While $(x^k)^Ts^k>2^{-t}$ , it computes $d$ from (2), takes the largest $\bar\theta$ such that $(x(\theta),s(\theta))\in\mathcal N$ for all $\theta\in[0,\bar\theta]$ , and sets $(x^{k+1},s^{k+1})=(x(\bar\theta),s(\bar\theta))$ .

Formalization targets

Goal: Theorem 2 with an explicit iteration count

Let $\beta,\gamma\in(0,1)$ with $\gamma\le2(1-\beta)$ , and let $\mathcal N$ be $\mathcal N_\infty(\beta)$ or $\mathcal N_\infty^-(\beta)$ . Every run of Algorithm 2 reaches $(x^k)^Ts^k\le 2^{-t}$ for some

k\ \le\ \Big\lceil\frac{\ln2\cdot n\,t}{2\beta\gamma(1-\gamma)}\Big\rceil .

The paper states " $O(nt)$ iterations"; the count above is the one its inequality (15) yields.

Milestones, in the order the proof uses them

Lemma 1(b): $-\|r\|^2/4\le p_jq_j\le r_j^2/4$ for each $j$ .
Lemma 1(c): $\|Pq\|^-_\infty\le\|r\|^2/4\le n\|r\|^2_\infty/4$ , $\|Pq\|^+_\infty\le\|r\|^2_\infty/4$ , $\|Pq\|_\infty\le\|r\|^2/4$ .
Lemma 2(c): if $\gamma\le2(1-\beta)$ and $(x,s)\in\mathcal N_\infty^-(\beta)$ then $\|r\|^2\le n\mu$ ; in $\mathcal N_\infty(\beta)$ , $\|r\|_\infty^2\le(1+\beta)\mu$ .
Lemma 5: $\bar\theta\ge\theta_2=\min\{1,\beta\gamma\mu/\|Pq\|_\infty\}$ in $\mathcal N_\infty(\beta)$ , and $\bar\theta\ge\theta_2^-=\min\{1,\beta\gamma\mu/\|Pq\|^-_\infty\}$ in $\mathcal N_\infty^-(\beta)$ .
Proof of Theorem 2: $\theta_2^-\ge\theta_2\ge4\beta\gamma/n$ (for $n\ge2$ ).
(15): $\mu^{k+1}\le\big(1-4\beta\gamma(1-\gamma)/n\big)\mu^k$ .

Significance

Theorem 2 shows that the adaptive long-step method in a neighbourhood covering almost all of $\mathcal F^0$ keeps the worst-case complexity of the original Kojima–Mizuno–Yoshise algorithm. Its per-iteration analysis (Lemma 5, Lemma 1(c)) is also what the paper reuses for its potential-reduction variant (§5, Theorem 3) and for its probabilistic explanation of why such methods take far fewer iterations in practice (§6). Lemma 1(b)–(c) are the standard bounds on the second-order Newton term, and they recur throughout the interior-point literature.

The results are proved in the paper. As far as the platform's corpus shows, none of them has a machine-checked proof: there is no formalization of the wide neighbourhoods $\mathcal N_\infty$ , $\mathcal N_\infty^-$ , of the Newton system (2), or of an adaptive-step iteration. A complete development yields a reusable layer for primal-dual interior-point analysis in standard form (the neighbourhoods, the scaled direction, the second-order bounds) and the first formally verified iteration bound for a long-step primal-dual method.

Difficulty

Most of the steps are finite-dimensional inequalities. The sticking points are the following.

The bound $p_jq_j\ge-\|r\|^2/4$ uses the orthogonality $p^Tq=0$ , which comes from $Ad_x=0$ and $d_s=-A^Td_y$ . Those relations hold only for a solution of the full system (2), not for the first equation alone.
Lemma 5 needs every point of the segment $[0,\theta_2]$ to lie in the neighbourhood, including strict positivity of $x(\theta)$ and $s(\theta)$ and dual feasibility. Positivity of the products alone does not give positivity of the factors without a continuity argument along the segment.
"The largest $\bar\theta$ " is a maximum over a set defined by infinitely many conditions. The theorem needs only that $\bar\theta$ dominates $\theta_2$ , but the formal run must say what $\bar\theta$ is.
Converting the per-iteration contraction (15) into the explicit count needs $(1-\delta)^k\le e^{-k\delta}$ , real powers of $2$ , and a ceiling.

Formalization scope

Vectors are Fin n → ℝ, with coordinates indexed $0,\dots,n-1$ , and A : Matrix (Fin m) (Fin n) ℝ. Mathlib's default norm on Fin n → ℝ is the sup norm, so the Euclidean norm norm2 and the norms normInf, normInfNeg, normInfPos are defined explicitly. $\mu$ divides by $n$ as a real number. Here $\log$ is the natural logarithm and $2^t$ is a real power with $t\in\mathbb R$ .

Committed conventions and repairs:

The direction is "any $(d_x,d_y,d_s)$ solving (2)". No rank assumption on $A$ is made.
"The largest $\bar\theta$ " is IsGreatest of the set of admissible step lengths, and $\bar\theta$ is not capped at $1$ . When no maximum exists (always the case for $n=1$ , where $Pq=0$ ), no iteration exists. A run is then possible only if it has already stopped, and the theorem holds trivially. A sorry-free check confirms that an iteration exists for $n=2$ .
A run is a pair of sequences that starts as required and makes one iteration from every iterate with $(x^k)^Ts^k>2^{-t}$ . Its behaviour after the stopping test is unconstrained.
In $\theta_2$ and $\theta_2^-$ , a zero norm makes the quotient $+\infty$ and the minimum $1$ . Since Lean's real division by zero is $0$ , this case is defined explicitly.
The bound $\theta_2\ge4\beta\gamma/n$ is stated for $n\ge2$ . At $n=1$ it can fail (e.g. $\beta=1/2$ , $\gamma=0.9$ ), and Algorithm 2 makes no iterations there.
The goal covers both neighbourhoods. A goal for $\mathcal N^-_\infty$ alone would be weaker than the paper.
Lemma 1 assumes only $x,s>0$ and $\gamma\in[0,1]$ of the pair, which is all its statement uses.

The goal is not to be read with a hidden constant. A statement of the form "there is $C$ with at most $Cnt$ iterations", with $C$ allowed to depend on the instance, would be trivially true and is ruled out by the explicit count. Lemma 1(a) and Lemma 2(a), 2(b) belong to the paper's predictor–corrector analysis, which is a separate mission.

Contributions are welcome at every level: proofs of the milestones, helper lemmas about the norms on Fin n → ℝ, and the run-to-count argument.

Selected references

S. Mizuno, M. J. Todd, Y. Ye, On adaptive-step primal-dual interior-point algorithms for linear programming, Cornell ORIE Technical Report No. 944 (1990, rev. 1991); Mathematics of Operations Research 18(4):964–981, 1993. https://doi.org/10.1287/moor.18.4.964
M. Kojima, S. Mizuno, A. Yoshise, A primal-dual interior point algorithm for linear programming, in N. Megiddo (ed.), Progress in Mathematical Programming, Springer, 1989, pp. 29–47. https://doi.org/10.1007/978-1-4613-9617-8_2
R. D. C. Monteiro, I. Adler, Interior path following primal-dual algorithms. Part I: Linear programming, Mathematical Programming 44:27–41, 1989. https://doi.org/10.1007/BF01587075
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453

11 thms3 active usersReviewed

Probability Quantum Information Theoretical Computer Science·Captain: mikedeng1

Strengths and Weaknesses of Quantum Computing I: Relative to a Random Oracle, a Quantum Algorithm Needs Ω(2^{n/2}) Queries to Decide Whether 1ⁿ Has a PreimageResearch Paper

Motivation

Grover's algorithm (Grover 1996) finds a marked item among $N$ with $O(\sqrt N)$ queries, a quadratic speed-up over any classical algorithm. Whether quantum computers can do substantially better on search, and so solve NP-type problems by brute force in polynomial time, was settled in the negative by Bennett, Bernstein, Brassard and Vazirani (arXiv:quant-ph/9701001, SIAM J. Comput. 26(5), 1997): relative to a random oracle, a quantum algorithm needs $\Omega(2^{n/2})$ queries to decide whether a string has a preimage. The bound matches Grover's algorithm up to a constant factor, and its hybrid argument is one of the two standard lower-bound methods of the field, together with the polynomial method (Beals et al. 1998) and the adversary method (Ambainis 2000).

Timeline:

1996: Grover's algorithm searches $N$ items with $O(\sqrt N)$ queries.
1997: the paper proves $\mathbf{BQTime}(o(2^{n/2})) \not\supseteq \mathbf{NP}$ relative to a random oracle with probability 1 (Theorem 3.5), and the $\Omega(2^{n/3})$ bound for random permutations (Theorem 3.6).
1998: Boyer, Brassard, Høyer and Tapp give tight bounds for quantum searching.
1999: Zalka shows Grover's algorithm is exactly optimal.

Setting

A $T$ -query algorithm acts on vectors $\varphi \in \mathbb{C}^{(X \cup \{\bot\}) \times R \times W}$ , where $X$ is the set of query strings, $R$ the set of answers (an additive group) and $W$ a finite workspace. A basis configuration $(x, z, w)$ with $x \in X$ is querying $x$ ; $(\bot, z, w)$ is not querying. For an oracle $f : X \to R$ the oracle operator is

O_f\,|x, z, w\rangle = |x, z + f(x), w\rangle, \qquad O_f\,|\bot, z, w\rangle = |\bot, z, w\rangle .

The algorithm consists of a unit vector $\varphi_0$ , unitaries $U_0, \dots, U_{T-1}$ that do not depend on the oracle, and a set of accepting configurations. With oracle $A$ its states are $\varphi_{i+1} = U_i O_A \varphi_i$ ; the acceptance probability is the squared norm of the accepting part of $\varphi_T$ . The query magnitude of $y$ in $\varphi$ is $q_y(\varphi) = \sum_{z, w} |\varphi(y, z, w)|^2$ (Definition 3.2). The algorithm decides a property if it accepts with probability at least $2/3$ when the property holds and at most $1/3$ when it fails.

In the main theorem $X = R = \{0,1\}^n$ with bitwise addition, and the oracle is a uniformly random function $A : \{0,1\}^n \to \{0,1\}^n$ . The question is whether $1^n$ belongs to $\mathcal{L}_A = \{y : \exists x\ A(x) = y\}$ .

Formalization targets

Goal: Theorem 3.5 (finite form)

\exists\, c > 0\ \exists N\ \forall n \ge N\ \forall M \text{ with } T \le c\, 2^{n/2} \text{ queries}: \quad \Pr_A\bigl[M^A \text{ fails to decide } \exists x\ A(x) = 1^n\bigr] \ge \tfrac18 .

The constant is existential, matching the theorem's hypothesis $T(n) = o(2^{n/2})$ ; $c$ and $N$ do not depend on the workspace or the algorithm.

Milestones

Theorem 3.1: unit vectors at distance $\varepsilon$ have measurement distributions within total variation $4\varepsilon$ .
Theorem 3.3 (corrected): changing oracle answers on time–string pairs of total query magnitude $\le \varepsilon^2/T$ moves the final state by at most $2\varepsilon$ .
Corollary 3.4 (corrected): outside a set of at most $4T^2/\varepsilon^2$ strings, changing the oracle at one string moves the final state by at most $\varepsilon$ .
$\Pr[1^n \text{ has no preimage}] = ((2^n-1)/2^n)^{2^n} \ge 1/4$ .
$\Pr[1^n \text{ has a unique preimage}] = ((2^n-1)/2^n)^{2^n-1} \ge 1/e$ .
Final states within $1/13$ for $A$ and $A_y$ force failure on one of them.
The double counting: failing oracles with a unique preimage are at least half the successful oracles with none.

Significance

The theorem shows that the quadratic speed-up of Grover's algorithm cannot be improved for unstructured search, and that relative to a random oracle $\mathbf{NP} \not\subseteq \mathbf{BQP}$ ; any quantum algorithm for NP-complete problems must use the structure of the problem. Theorem 3.3 and Corollary 3.4 isolate the constraint unitary evolution places on "quantum parallelism" and are reused across quantum lower bounds, including the permutation bound of the companion mission (Theorem 3.6).

The results are proved on paper and, to our knowledge, have no machine-checked proof. The mission produces a formal query model with an XOR oracle, a formal hybrid argument, and the lower bound with its constants checked. Two printed bounds are wrong by constant factors (below); the formal statements carry the corrected constants, and a formal proof settles them. Grover's matching upper bound is on the platform as Grover.search_succeeds_bounded, for a phase oracle and one fixed algorithm.

Difficulty

The obvious argument — each query reveals one bit about where the preimage is, so $\Omega(2^n)$ queries are needed — fails for quantum algorithms, which query all strings in superposition at once. The difficulty is to bound how much a superposition of queries can learn, which requires controlling the accumulated effect of small changes across $T$ unitary steps, and then converting a bound on states into a statement about the probability of failure over random oracles, where the set of sensitive strings depends on the oracle.

Formalization scope

The paper's oracle quantum Turing machines are replaced by the query model above, the model its proofs use. Every oracle QTM running $T$ steps is a $T$ -query algorithm: oracle answers on lengths other than $n$ are fixed and absorbed into the unitaries, as the proof fixes them, and the input $1^n$ is absorbed into $\varphi_0$ . Queries return the full value $A(x) \in \{0,1\}^n$ ; one Boolean query is two full-value queries, so the goal implies the Boolean-oracle bound with $c$ halved. Strings are Fin n → ZMod 2; states are EuclideanSpace ℂ (Option X × R × W); probabilities over oracles are counting fractions over all $(2^n)^{2^n}$ functions; total variation distance is the paper's $\sum_x |\mathcal D(x) - \mathcal D'(x)|$ without the factor $1/2$ .

Corrections: Theorem 3.3 is printed with conclusion $\le \varepsilon$ , which fails (one query string, $T = 1$ , distance $2$ at $\varepsilon = 1$ ; machine-checked); the true bound is $2\varepsilon$ . Corollary 3.4 is printed with $|S| \le 2T^2/\varepsilon^2$ , which fails (16 strings, $T = 1$ , $\varepsilon = 0.45$ ); the true bound is $4T^2/\varepsilon^2$ . The printed constant $T(n) \le 2^{n/2}/20$ in the proof of Theorem 3.5 does not support the step $2^n - \mathrm{card}(S) \ge 2^{n-1}$ even with the paper's own count; the goal states an existential constant, and $c = 1/37$ works with the corrected Corollary 3.4. The closing probability- $1$ argument over countably many machines and the class statement about $\mathbf{BQTime}$ are not formalized.

A formalization in which algorithms query at every step on every branch (no $\bot$ sector), only one side of the bounded-error condition is tested, or the probability is taken over a set of oracles that excludes the hard instances, proves a weaker theorem and is ruled out by these definitions.

Needed infrastructure: norms of finite-dimensional complex vectors, unitaries as linear isometry equivalences, finite counting of functions. The query model and the hybrid argument are reusable for any quantum query lower bound.

Selected references

C. H. Bennett, E. Bernstein, G. Brassard, U. Vazirani, Strengths and weaknesses of quantum computing, SIAM J. Comput. 26(5):1510–1523, 1997. arXiv:quant-ph/9701001
L. K. Grover, A fast quantum mechanical algorithm for database search, STOC 1996. arXiv:quant-ph/9605043
M. Boyer, G. Brassard, P. Høyer, A. Tapp, Tight bounds on quantum searching, Fortschr. Phys. 46, 1998. arXiv:quant-ph/9605034
C. Zalka, Grover's quantum searching algorithm is optimal, Phys. Rev. A 60, 1999. arXiv:quant-ph/9711070
R. Beals, H. Buhrman, R. Cleve, M. Mosca, R. de Wolf, Quantum lower bounds by polynomials, J. ACM 48, 2001. arXiv:quant-ph/9802049
A. Ambainis, Quantum lower bounds by quantum arguments, J. Comput. Syst. Sci. 64, 2002. arXiv:quant-ph/0002066

9 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming 1: The Predictor–Corrector Algorithm Between N₂(1/4) and N₂(1/2) Attains Precision t in O(√n·t) IterationsResearch Paper

Motivation

Linear programming asks for the best value of a linear objective subject to linear equations and inequalities. Primal-dual interior-point methods seek feasible primal and dual solutions while keeping every constrained coordinate positive. The resulting pair has a measurable gap between its objective values, so an algorithm can stop when the gap is below a chosen precision. Mizuno, Todd, and Ye studied methods that adjust the length of each step according to the current point. Their technical report gives a predictor–corrector algorithm whose worst-case iteration count grows on the scale of the square root of the number of variables times the requested precision parameter Mizuno, Todd, and Ye, Cornell ORIE Technical Report No. 944, pp. 6–9.

The result matters to readers who need a mathematical guarantee for an adaptive step rule. The algorithm takes one predictor step that reduces the gap and then one corrector step that recenters the pair. Its step length is defined by remaining inside a specified neighborhood, rather than by a fixed schedule. The theorem connects that local rule to a global termination bound.

Setting

Fix an integer $n\ge1$ of variables, an arbitrary number $m$ of equality constraints, a real matrix $A\in\mathbb R^{m\times n}$ , and vectors $b\in\mathbb R^m$ and $c\in\mathbb R^n$ . The primal problem minimizes $c^Tx$ over $Ax=b$ , $x\ge0$ . Its dual problem maximizes $b^Ty$ over $A^Ty+s=c$ , $s\ge0$ . The dual slack is $s$ . The development reuses a published general-form LP model and specializes it to this pair.

The strictly feasible pairs $F^0$ are the pairs $(x,s)$ satisfying the two feasibility systems for some dual multiplier $y$ , with every coordinate of $x$ and $s$ strictly positive. The multiplier is allowed to vary with the pair. Write $X=\operatorname{diag}(x)$ , $S=\operatorname{diag}(s)$ , and $e$ for the vector of ones. The duality measure is $\mu=x^Ts/n$ . For $0<\beta<1$ , the Euclidean central-path neighborhood is

N_2(\beta)=\{(x,s)\in F^0:\|Xs-\mu e\|_2\le\beta\mu\}.

The search direction $(d_x,d_y,d_s)$ at $(x,s)$ with parameter $\gamma$ solves the three equations $Sd_x+Xd_s=\gamma\mu e-Xs$ , $Ad_x=0$ , and $A^Td_y+d_s=0$ . A step of length $\theta$ yields $(x+\theta d_x,s+\theta d_s)$ . Algorithm 1 begins in $N_2(1/4)$ . It takes a predictor direction with $\gamma=0$ to the greatest step whose entire path remains in $N_2(1/2)$ , then takes one full corrector direction with $\gamma=1$ . The resulting pair starts the next iteration. The algorithm stops when $x^Ts\le2^{-t}$ ; its starting gap is at most $2^t$ report, pp. 4 and 6–7.

Formalization targets

Theorem 1: termination

For every real precision parameter $t$ , every run following Algorithm 1 from an allowed starting pair reaches the stopping threshold at some iteration $k$ with

k\le\left\lceil2(\log2)8^{1/4}\sqrt n\,t\right\rceil, \qquad (x^k)^Ts^k\le2^{-t}.

The paper states the iteration order as $O(\sqrt n\,t)$ . The explicit ceiling records the count given by its proof without allowing an unspecified constant to depend on the LP instance report, Theorem 1, pp. 8–9.

Source milestones

The supporting targets are equations (4)–(5), Lemma 1(a), Lemma 2(a)–(b), Lemma 3, Lemma 4, and the contraction displayed in the proof of Theorem 1. They cover the duality measure along a step, bounds on the scaled second-order term, preservation of the inner neighborhood, the predictor step length, and the per-iteration reduction. The milestone list follows the order in which these facts enter the report's analysis report, pp. 4–9.

Significance

Theorem 1 gives a stopping guarantee for a fully specified adaptive predictor–corrector method on a feasible primal-dual LP pair. In particular, the requested precision can grow while the iteration bound scales with $\sqrt n$ , rather than with $n$ , in this neighborhood model. It also gives a quantitative reason to track two neighborhoods: the predictor may leave the inner one, while the corrector brings the iterate back for the next round.

The report proves this mathematical claim, but this mission does not assert that its proof has already been machine checked. A completed formalization would supply reusable Lean definitions for strictly feasible LP pairs, Euclidean centrality, search directions, and algorithmic step relations. Solvers may formalize the report's argument or another proof of the same statements; the audited goal and milestones fix the mathematical contract.

Difficulty

The predictor direction is aimed at reducing the duality measure, but a long step can move the componentwise products $x_js_j$ away from their common average or make a coordinate nonpositive. The corrector recenters the pair, yet its effect must be controlled in the same Euclidean neighborhood. A gap decrease alone therefore does not imply that another iteration can be taken. The central difficulty is to establish both a nonzero admissible predictor length and preservation of strict feasibility and centrality under the full corrector step.

Formalization scope

Vectors are functions on Fin n, and $A$ is a finite matrix. The report's indices $1,\ldots,n$ correspond to Lean indices $0,\ldots,n-1$ . The norm in $N_2$ and in Lemmas 1–2 is explicitly $\ell_2$ : Lean's default norm on functions is a supremum norm. All powers of two use real exponents, and $\log$ is natural logarithm. The hypothesis $n\ge1$ gives meaning to $\mu=x^Ts/n$ ; no sign condition on $t$ is imposed, since for $t\le0$ the starting pair already meets the stopping test.

The source's “largest” predictor step is represented as an attained greatest element of the admissible set, with admissibility required throughout the step interval. Some interior points have admissible intervals without a greatest member. In particular, at $n=1$ there may be no continuing run under this literal algorithm rule; the goal retains $n\ge1$ and makes this limitation explicit. The denominator $\|Pq\|_2$ in Lemma 4 can vanish. The formal lower bound uses its limiting value $1/2$ in that case, avoiding a zero returned by Lean's total division. The separate contraction milestone assumes $n\ge2$ , because its printed lower bound on the predictor length fails at $n=1$ .

The definitions keep primal feasibility, an existential dual multiplier, coordinatewise strict positivity, and the three direction equations visible. A sequence is constrained by the transition relation whenever its gap exceeds $2^{-t}$ ; values after stopping play no role. These conditions exclude trivial encodings in which the gap threshold is built into the run or centrality is measured with the wrong norm. The remaining work includes Euclidean finite-sum estimates, positivity along steps, and the iteration-count argument. The LP specialization and norm infrastructure can be reused in further interior-point developments.

Selected references

Shinji Mizuno, Michael J. Todd, and Yinyu Ye, On Adaptive-Step Primal-Dual Interior-Point Algorithms for Linear Programming, Cornell ORIE Technical Report No. 944, 1990, revised 1991; published in Mathematics of Operations Research 18(4), 1993. Technical-report PDF. The PDF used here is the technical report, so all page and result indices refer to that version.

12 thms3 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 5: KNAPSACK Reduces to Two-Machine Flow Shop Makespan with a Release Date or Tree Precedence and to Two- and Three-Machine Job Shop MakespanResearch Paper

Motivation

In 1975 P. Brucker, J. K. Lenstra and A. H. G. Rinnooy Kan classified a large part of deterministic machine scheduling by computational complexity, using the then new theory of NP-completeness of Cook and Karp. Their report, Complexity of Machine Scheduling Problems (Mathematisch Centrum, Amsterdam, 1975; published in Annals of Discrete Mathematics 1, 1977), gives for many problems either a polynomial algorithm or a polynomial reduction from a known NP-complete problem. It drew the boundary between easy and hard scheduling problems that later surveys and the standard three-field classification build on.

This mission covers four reductions of the report's Theorem 4 that concern shops with several machines. A flow shop processes every job on machines $M_1, \dots, M_m$ in this order; a job shop lets each job follow its own route. For two machines and no further constraints, the flow shop is solved by Johnson's rule (Johnson, 1954) and the job shop with at most two operations per job by Jackson's extension of it (1956). The four reductions show that these positive results stop exactly where one more feature is added: one job with a nonzero release date, tree-shaped precedence constraints, a third operation per job, or a third machine.

Setting

A general shop instance has jobs $J_1,\dots,J_n$ and machines $M_1,\dots,M_m$ . Job $J_j$ consists of $m_j$ operations; its $r$ -th operation runs on machine $\mu_{jr}$ for $p_{jr}\in\mathbb N$ time units, and the tuple $\mu_j$ is the job's machine order (a machine may occur more than once). Each job has a release date $r_j$ , and some pairs of jobs carry a precedence constraint $J_j<J_k$ .

A schedule gives every operation a start time. It is feasible if no operation of $J_j$ starts before $r_j$ ; the operations of each job run in the order $\mu_j$ , each after the previous one completes; two operations on the same machine never overlap; and $J_j<J_k$ implies $C_j\le B_k$ , where $C_j$ is the completion time of $J_j$ and $B_k$ the starting time of $J_k$ . The makespan is $C_{\max}=\max_j C_j$ .

In the report's notation $n|m|\ell,\lambda|C_{\max}$ , $\ell=F$ means a flow shop and $\ell=G$ a job shop; $\lambda$ may contain $r_n\ge 0$ (only the last job has a release date), tree (the precedence graph is a branching: no directed cycle, and either every indegree or every outdegree is at most one) and $m_j\le m_*$ (at most $m_*$ operations per job). The recognition version of a problem asks, for an instance and a number $y$ , whether a feasible schedule with $C_{\max}\le y$ exists.

KNAPSACK asks, for positive integers $a_1,\dots,a_t$ and $b$ , whether some $S\subseteq T=\{1,\dots,t\}$ has $\sum_{j\in S}a_j=b$ . A problem $P'$ is reducible to $P$ ( $P'\propto P$ ) if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer.

Formalization targets

Goal: Theorem 4(g)–(j)

\mathrm{KNAPSACK}\ \propto\ n|2|F,r_n{\ge}0|C_{\max},\quad n|2|F,\mathit{tree}|C_{\max},\quad n|2|G,m_j{\le}3|C_{\max},\quad n|3|G,m_j{\le}2|C_{\max}.

Each part is a polynomial-time many-one reduction between languages of binary strings. The other six parts of Theorem 4 (single-machine problems) belong to other missions of this series.

Milestones: the four equivalences

For positive $a_1,\dots,a_t,b$ with $0<b<A=\sum_{j\in T}a_j$ , and for each of the paper's four constructions with its threshold $y$ ,

\exists\,S\subseteq T:\ \sum_{j\in S}a_j=b\iff\text{the constructed instance has a feasible schedule with } C_{\max}\le y,

with $y=A+1$ for (i), $y=2A$ for (j), $y=t(A+1)$ for (g) and $y=t(A+1)+1$ for (h). The milestones are stated directly about the printed constructions, in the order (i), (j), (g), (h) of the report.

Significance

With the NP-completeness of KNAPSACK (Karp, 1972), the goal makes the four problems NP-complete. As the report notes, (i) and (j) together with the elementary reductions of its Theorem 1 make the general job shop $n|m|G|C_{\max}$ NP-complete for every fixed $m\ge 2$ . Parts (g) and (h) show that Johnson's two-machine algorithm admits neither release dates nor precedence constraints in general. Because KNAPSACK can be solved in pseudo-polynomial time, these results establish NP-hardness in the ordinary sense only; strong NP-hardness of some of these problems came later (Garey, Johnson and Sethi, 1976, for the three-machine flow shop).

The results are proved in the report; no machine-checked proof of any of them is known to exist. A formalization adds explicit constructions and complete equivalence proofs where the report is brief: in (h) it proves one inequality and states that the rest "is analogous to that of reduction (g)", and the forward directions are given by figures. It also produces a reusable formal model of general shops with integral start times, release dates, precedence and repeated machines.

Difficulty

Polynomial-time computability of the constructions is routine in principle but laborious in Cook's Turing-machine model, which is the setting of the goal: binary arithmetic for $A$ , $t a_j$ and $t(A-b)$ , and parsing of the KNAPSACK code.

The mathematical difficulty is the reverse direction of each equivalence. The report's arguments are phrased in terms of "a processing order on $M_1$ " and treat the jobs before and after an extra job as two blocks. A formal proof must derive such an order from arbitrary start times and must handle every interleaving, including idle time and the case where the extra job's operations do not fit the printed pattern. In (j) the printed bound for the case $c<0$ contains a minimum of two quantities whose justification is left to the reader. In (h) the printed case uses $t a_j\ge t$ , so the positivity of the data matters, and the remaining cases are only said to be analogous to (g).

Formalization scope

Jobs are Fin n and machines Fin m, both 0-based. A job's operations form a list of (machine, processing time) pairs, so machine orders may repeat machines, as $\mu_n=(M_2,M_1,M_2)$ in (i) does. Start times are natural numbers. The report computes schedules from processing orders on integer data, the makespan is a regular criterion, and release dates and precedence survive shifting operations left, so integral start times lose no value. $C_{\max}\le y$ is stated as $C_j\le y$ for every $j$ ; no maximum over an empty set is formed. Precedence $J_j<J_k$ is between jobs: every operation of $J_k$ starts no earlier than $C_j$ . A branching is an acyclic precedence graph in which every indegree is at most one or every outdegree is at most one; the report's "either … or" is read for the whole graph. Job-shop classes require at least one operation per job. A flow-shop job has exactly the operations $(M_1,M_2)$ , with times allowed to be zero.

The following readings of the report are made explicit. "Reducible" is Karp reducibility, CookPvsNP.PolyReducible from the published definitions CookPvsNP_defs. The languages are over the four-letter alphabet with binary numbers of the published definition ProjSchedTW.Complexity.Encoding. Its subsetSumLang allows zero sizes, while the report's KNAPSACK is over positive integers, so KNAPSACK is defined locally with positivity in the language. "We may assume that $0<b<A$ " becomes a hypothesis of every equivalence; the goal's reduction must still handle the other inputs. The printed "value $C_{\max}=y$ " of the forward directions is read as " $\le y$ ", as Section 2 defines the recognition version. The remark that (h) is analogous to (g) becomes the full equivalence for (h). An instance outside the problem's class is not in its language. NP-membership is not part of the goal.

The formal two-stage flow-shop models of Johnson's paper (JohnsonFlowShop.TwoStage.IsFeasible) and the job-shop model of Jansen, Solis-Oba and Sviridenko (JobShopLTAS.Core.Instance) use real start times and have neither release dates nor precedence. They were consulted, but the model here is local.

Ruled out as trivializing: a goal without the polynomial-time condition (the bare equivalence of yes-instances), a target language that accepts instances outside the class, and equivalences about some instance rather than the printed construction.

Contributions are welcome on any milestone, on a general lemma that turns a feasible schedule into a processing order per machine, and on polynomial-time computability of list arithmetic in the Turing-machine model, which every reduction of this series needs.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
S. M. Johnson, Optimal two- and three-stage production schedules with setup times included, Naval Research Logistics Quarterly 1 (1954) 61–68. https://doi.org/10.1002/nav.3800010110
J. R. Jackson, An extension of Johnson's results on job lot scheduling, Naval Research Logistics Quarterly 3 (1956) 201–203. https://doi.org/10.1002/nav.3800030307
M. R. Garey, D. S. Johnson, R. Sethi, The complexity of flowshop and jobshop scheduling, Mathematics of Operations Research 1 (1976) 117–129. https://doi.org/10.1287/moor.1.2.117
S. A. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

11 thms3 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 4: KNAPSACK Reduces to Single-Machine Total Completion Time with One Release DateResearch Paper

Motivation

Minimizing the total completion time $\sum_j C_j$ of jobs on a single machine is one of the oldest problems in scheduling theory. When every job is available at time $0$ , processing the jobs in order of nondecreasing processing time is optimal (the shortest-processing-time rule), so the problem is solved by sorting. Release dates, times before which a job may not start, change the picture. In their 1975 report Complexity of Machine Scheduling Problems (Mathematisch Centrum Report BW 43/75; journal version in Annals of Discrete Mathematics 1, 1977), Brucker, Lenstra and Rinnooy Kan used the then-new theory of NP-completeness (Cook 1971, Karp 1972) to map which classical scheduling problems are polynomially solvable and which are NP-complete. Theorem 4 of that report lists ten problems to which KNAPSACK reduces. Part (a) shows that total completion time on one machine is already hard when a single job has a nonzero release date and all weights are equal.

The result is a sharp boundary. With all release dates zero the problem is easy; with one nonzero release date it is NP-complete. It is a standard entry in the complexity classification of single-machine problems that later surveys (Lawler, Lenstra, Rinnooy Kan and Shmoys, 1993) and the scheduling-complexity databases build on.

Setting

An instance of KNAPSACK consists of positive integers $a_1,\dots,a_t$ and $b$ ; with $T=\{1,\dots,t\}$ , it has a solution if $\sum_{j\in S}a_j=b$ for some $S\subseteq T$ .

In the scheduling problem there are $n$ jobs $J_1,\dots,J_n$ and one machine. Job $J_j$ has a processing time $p_j$ , a weight $w_j$ and a release date $r_j$ , all nonnegative integers. A schedule assigns each job a starting time $B_j\ge r_j$ ; the job completes at $C_j=B_j+p_j$ , and no two jobs are processed at the same time. The problem written $n|1|r_n\ge0,w_j=1|\sum w_jC_j$ in the paper's notation is the class of instances in which every weight is $1$ and every job except the last one, $J_n$ , has release date $0$ . Its recognition version asks, given such an instance and an integer $y$ , whether some schedule has $\sum_jC_j\le y$ .

A problem $P'$ is reducible to $P$ (written $P'\propto P$ ) when every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer. The paper's construction maps $a_1,\dots,a_t,b$ (with $0<b<A=\sum_ja_j$ and $a_*=\max_ja_j$ ) to an instance with $n=t+t'+u+1$ jobs in four groups $T$ , $T'$ , $U$ and $\{J_n\}$ , with processing times $\tau+a_j$ , $\tau$ , $\upsilon$ and $1$ , the release date $r_n=t\tau+b$ , and threshold $y=\upsilon+\tfrac12u(u+1)\upsilon$ , where $t'$ , $\tau$ , $u$ , $\sigma$ , $\upsilon$ are explicit polynomials in $t$ , $a_*$ , $b$ and $A$ .

Formalization targets

Goal: Theorem 4(a)

\text{KNAPSACK}\ \propto\ n|1|r_n\ge0,w_j=1|\textstyle\sum w_jC_j ,

stated as CookPvsNP.PolyReducible knapsackLang sumCLangMult: a polynomial-time computable map on binary strings that sends codes of solvable KNAPSACK instances, and only those, to codes of yes-instances of the scheduling problem.

Milestones

Forward direction (p. 22). If $\sum_{j\in S}a_j=b$ , the processing order $(S',S,J_n,T'-S',T-S,U)$ , with $S'=\{t+j\mid j\in T-S\}$ , gives a feasible schedule with $\sum_{j\notin U}C_j\le u$ , $\sum_{j\in U}C_j=u\sigma+\tfrac12u(u+1)\upsilon$ and $\sum_jC_j\le y$ .
Claim (A). In every schedule with $\sum_jC_j\le y$ , all jobs outside $U$ precede all jobs of $U$ .
Claim (B). In every such schedule some job of $U$ starts by time $\sigma$ ; consequently $\sum_{j\notin U}C_j\le u$ .
Claim (C). Exactly $t$ jobs precede $J_n$ .
Claim (D). $B_n=t\tau+b$ .
Equivalence (pp. 22–23). For $0<b<A$ , KNAPSACK has a solution iff the constructed instance has a schedule with $\sum_jC_j\le y$ .

Significance

Together with the NP-completeness of KNAPSACK (Theorem 2(b), quoted from Karp), Theorem 4(a) shows that $n|1|r_n\ge0,w_j=1|\sum w_jC_j$ is NP-complete; with general release dates the problem $1|r_j|\sum C_j$ is then NP-hard as well. The hardness here is in the ordinary sense: the construction is polynomial only in the multiplicity encoding (see below), and the reduction is from KNAPSACK, which has a pseudo-polynomial algorithm.

The result is proved on paper. A formalization adds a machine-checked complexity reduction whose correctness proof is a sequence of delicate counting estimates with large explicit constants; the paper closes the converse with "as is easily seen", and the forward computation and claims (C), (D) contain displayed identities that a formal proof must verify exactly. The definitions (single-machine schedules with release dates, the schedule of a processing order, the multiplicity encoding) are reusable for the other single-machine reductions of the same paper and for later classification results.

Difficulty

The forward direction is a direct computation. The converse is where the difficulty lies: a schedule with $\sum_jC_j\le y$ is arbitrary, may contain idle time, and may interleave the groups. Such a schedule must be shown to be rigid (claims (A)–(D)), and the claims are statements about every schedule, not about a convenient one. Each step compares sums of the form $\sum jτ$ against $u$ with an additive slack smaller than $\tau$ , so the constants must be tracked exactly; an estimate that loses a single $\tau$ breaks the argument. Extracting the knapsack subset at the end requires recognizing which $t$ jobs fill $[0,t\tau+b)$ and why their extra lengths $a_j$ sum to exactly $b$ .

For the goal, the polynomiality of the reduction is not automatic: the constructed instance has $t'=t(t+1)a_*$ and $u$ jobs, which is exponential in the length of the binary KNAPSACK input. The paper's Remark (p. 23) resolves this by encoding groups of identical jobs by their cardinality and one copy of their data, and the formal statement adopts that encoding.

Formalization scope

Reducibility is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (polynomial-time many-one reducibility in Cook's machine model). Numbers are coded in binary over the four-letter alphabet BSym with encNats from the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's formalization); its own subsetSumLang allows zero entries, so KNAPSACK over positive integers is defined here.
Jobs are indexed by Fin n, 0-based; the groups $T$ , $T'$ , $U$ and $J_n$ are index ranges. Starting times are natural numbers: the paper computes them from processing orders on integer data (Section 3), and claim (D) is false for real starting times.
A schedule is feasible when every job starts at or after its release date and the occupied half-open intervals $[B_j,B_j+p_j)$ are pairwise disjoint; idle time is allowed.
"Precedes" in claims (A) and (C) means "starts earlier on the machine"; there are no precedence constraints.
The claims are stated with exactly the hypotheses the proof uses: the schedule is feasible and $\sum_jC_j\le y$ , for positive $a_j$ , $b$ with $0<b<A$ (the paper's "We may assume that $0<b<A$ ", p. 16).
The halves in $u$ and $y$ are exact natural-number divisions, since the products are even. The letter $u$ is both the size of $U$ and the bound $\sum_{j\notin U}C_j\le u$ , as in the paper.
The goal's target language uses the multiplicity encoding: a list of job types (count, processing time, weight, release date) and $y$ ; the class conditions (unit weights, release date $0$ for every job but the last) are checked on the expanded job list. A one-entry-per-job encoding would make the paper's construction non-polynomial, and the statement would not be the paper's.
Trivializing formalizations are ruled out: the goal includes polynomial-time computability (not just an equivalence of yes-instances), the KNAPSACK language requires positive entries as in the paper, and the target language requires class membership, so mapping to an instance outside the class is not a way out.
Welcome contributions: the arithmetic identities of the construction, the schedule of a processing order and its feasibility, the counting lemmas behind (C) and (D), and polynomial-time computability of the multiplicity-encoded construction in the CookPvsNP model.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
S. A. Cook, The complexity of theorem-proving procedures, Proc. 3rd ACM STOC, 1971, 151–158. https://doi.org/10.1145/800157.805047
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
E. L. Lawler, J. K. Lenstra, A. H. G. Rinnooy Kan, D. B. Shmoys, Sequencing and scheduling: algorithms and complexity, Handbooks in OR & MS 4, 1993, 445–522. https://doi.org/10.1016/S0927-0507(05)80189-6

14 thms3 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 7: Makespan Reduces to Total Completion Time on Identical Machines with Precedence ConstraintsResearch Paper

Motivation

Scheduling jobs on parallel machines under precedence constraints is the core model of project and parallel-processing scheduling: a job may start only after its predecessors have finished. Two criteria dominate the literature, the makespan $C_{\max}$ (when does the last job finish?) and the total completion time $\sum_j C_j$ (how long do jobs wait on average?). Knowing that one criterion is at least as hard as the other lets a hardness proof for one transfer to the other without a new reduction from a combinatorial problem.

Brucker, Lenstra and Rinnooy Kan's report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; later in Annals of Discrete Mathematics 1, 1977) collected the complexity status of the standard scheduling problems and stated a set of elementary reductions among them as Theorem 1. Part (l) reduces makespan to total completion time for identical machines with precedence constraints and bounded processing times.

Timeline.

1971–1972: Cook (doi:10.1145/800157.805047) and Karp (doi:10.1007/978-1-4684-2001-2_9) introduce NP-completeness and polynomial reducibility.
1975: Ullman (doi:10.1016/S0022-0000(75)80008-0) proves that the makespan problems $n|2|I,\mathit{prec},1\le p_{j1}\le 2|C_{\max}$ and $n|m|I,\mathit{prec},p_{j1}=1|C_{\max}$ are NP-complete, by reductions from 3-SATISFIABILITY.
1975: Brucker, Lenstra and Rinnooy Kan state Theorem 1(l); their Table III (p. 13) applies it to Ullman's two problems and concludes that the corresponding total completion time problems are NP-complete.

Setting

An instance has $n$ jobs $J_1,\dots,J_n$ , a number $m \ge 1$ of identical machines, a processing time $p_j$ for each job, and a precedence relation $<$ on the jobs: $J_j < J_k$ means that $J_k$ may start only after $J_j$ has completed. Each job is one operation, processed without interruption on any one machine. For a constant $p_*$ , the class $n|m|I,\mathit{prec},1\le p_{j1}\le p_*$ requires $1 \le p_j \le p_*$ for every job and an acyclic precedence relation.

A schedule assigns to every job a machine and a starting time $B_j \in \mathbb N$ ; the completion time is $C_j = B_j + p_j$ . It is feasible if two jobs on the same machine never overlap and $J_j < J_k$ implies $C_j \le B_k$ .

Following the paper, each optimization problem is replaced by its recognition version. Problem $P'$ asks, for an instance and a threshold $y'$ , whether some feasible schedule has $C_{\max} = \max_j C_j \le y'$ . Problem $P$ asks, for an instance of the same class and a threshold $y$ , whether some feasible schedule has $\sum_j C_j \le y$ (all weights $w_j = 1$ ).

$P'$ is reducible to $P$ , written $P' \propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer.

Formalization targets

Goal: Theorem 1(l)

For every constant $p_* \ge 1$ ,

n'|m|I,\mathit{prec},1\le p_{j1}\le p_*|C_{\max} \;\propto\; n|m|I,\mathit{prec},1\le p_{j1}\le p_*,w_j=1|\textstyle\sum w_jC_j .

Milestones

A trivial upper bound. Every instance of $P'$ with $n'$ jobs has a feasible schedule with $C_{\max} \le n'p_*$ .
The construction and the forward direction. For $0 \le y' \le n'p_*$ let $n'' = (n'-1)y'$ , $n = n'+n''$ and $y = ny' + \tfrac12 n''(n''+1)$ , and add $n''$ unit-time jobs $J_{n'+k}$ , each required to follow every original job and every earlier added job. If $P'$ has a schedule with $C_{\max} \le y'$ , the new instance has a feasible schedule with $\sum_j C_j \le y$ .
The backward direction. If every feasible schedule of $P'$ has $C_{\max} > y'$ , every feasible schedule of the new instance has $\sum_j C_j > y$ .

Significance

The result. Theorem 1(l) makes the total completion time problem at least as hard as the makespan problem in the same class. Combined with Ullman's NP-completeness results and Theorem 1(b) (reducibility transfers NP-completeness), it shows that minimizing $\sum_j C_j$ on identical machines with precedence constraints is NP-complete, already for two machines with $p_j \in \{1, 2\}$ and for unit processing times on $m$ machines. These are two rows of the paper's Table III.

Formalizing it. The result is proved on one page of a typewritten report; no machine-checked version exists. The mission produces a scheduling model for identical machines with precedence constraints, binary languages for the two recognition problems, and the reduction in Cook's Turing-machine model. The proof's displayed bounds contain a misprinted index range, which the formal statements correct.

Difficulty

The two criteria are not monotonically related: a schedule with a smaller makespan can have a larger total completion time than one with a larger makespan. So the obvious reduction, keeping the instance and asking for $\sum_j C_j \le n'y'$ , is not an equivalence: a no-instance of $P'$ can have a schedule with small total completion time. The instance has to be changed so that the total completion time is governed by the makespan, and the comparison of the two thresholds must be exact, including the strict inequality on the "no" side, which depends on integral completion times and positive processing times.

The main formal difficulty lies in the reduction itself. A polynomial-time Turing machine must decode the binary instance, check that it belongs to the class (including acyclicity of the precedence relation), compare $y'$ with $n'p_*$ , and write out an instance with $n'' = (n'-1)y'$ additional jobs and a quadratic-size precedence matrix. The size of that output is polynomial only because $p_*$ is a constant: a version with $p_*$ part of the input would make $n''$ exponential in the input length.

Formalization scope

Jobs and machines are indexed from $0$ (Fin n, Fin m). Starting times are natural numbers; Section 3 derives all times from processing orders on nonnegative integer data, and both criteria are regular. " $C_{\max} \le y$ " is written as " $C_j \le y$ for every $j$ ".
The precedence relation is a Boolean matrix. Its acyclicity and $m \ge 1$ are part of the problem class; the paper leaves both implicit, and the claim "any instance has a solution with $C_{\max} \le n'p_*$ " fails without them.
$p_*$ is a constant of the class and a parameter of both languages, not part of the input. All weights in the target problem equal $1$ and are not written.
The threshold $y = ny' + \tfrac12 n''(n''+1)$ is stated in $\mathbb Q$ exactly as printed in the milestones; it is an integer, and the reduction uses its natural-number value.
The paper's displayed bounds $n'y' + \sum_{k=n'+1}^{n}(y'+k) = y$ and $y' + \sum_{k=n'+1}^{n}(y'+1+k) = y$ have a misprinted index range (the sums must run over $k = 1,\dots,n''$ ). The milestones state the end-to-end bounds $\sum_j C_j \le y$ and $\sum_j C_j > y$ .
" $C_{\max} > y'$ " in the backward direction is read as the negation of the forward hypothesis: no feasible schedule of $P'$ has $C_{\max} \le y'$ .
"Reducible" is Cook's polynomial-time many-one reducibility from the published definition CookPvsNP_defs; numbers are written in binary with the alphabet and code encNats of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). The unit-time model ResourceScheduling.Chain.Model (Błażewicz, Lenstra and Rinnooy Kan) has the same feasibility conditions but unit processing times and real start times, so the model here is defined anew.
A trivializing formalization is ruled out: the goal asserts a polynomial-time computable map, not the bare equivalence, and codes of instances outside the class are excluded from both languages, so the reduction cannot exploit malformed inputs.
Contributions welcome: proofs of the three milestones, a Turing-machine library for arithmetic on binary codes (reusable across this series), and a proof of the goal from the milestones.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; published in Annals of Discrete Mathematics 1 (1977) 343–362. doi:10.1016/S0167-5060(08)70743-X
J. D. Ullman, NP-complete scheduling problems, Journal of Computer and System Sciences 10 (1975) 384–393. doi:10.1016/S0022-0000(75)80008-0
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. doi:10.1145/800157.805047
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. doi:10.1007/978-1-4684-2001-2_9

9 thms3 active usersReviewed

Graph Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 6: DIRECTED HAMILTON PATH Reduces to No-Wait Flow Shop Makespan and Total Completion TimeResearch Paper

Motivation

In a no-wait flow shop every job passes through the machines $M_1,\dots,M_m$ in the same order, and once it has started it may never wait between two machines. The constraint comes from processes in which the material changes state if it is left standing, such as hot metal rolling, chemical and food processing, and some pharmaceutical lines; see the survey of Hall and Sriskandarajah (doi:10.1287/opre.44.3.510). The question of how hard it is to schedule such a shop well is the question this mission formalizes.

Brucker, Lenstra and Rinnooy Kan settled it for the case in which the number of machines is part of the input. In their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977, doi:10.1016/S0167-5060(08)70743-X), Theorem 5 reduces DIRECTED HAMILTON PATH to the no-wait flow shop. Both minimizing the makespan $C_{\max}$ and minimizing the total completion time $\sum C_j$ are thereby NP-complete.

Timeline.

1964: Gilmore and Gomory solve the two-machine no-wait flow shop with makespan in polynomial time (doi:10.1287/opre.12.5.655).
1972: Wismer (doi:10.1287/opre.20.3.689) and Reddi and Ramamoorthy (doi:10.1057/jors.1972.52) show that no-wait makespan minimization is a travelling-salesman problem with arc weights computed from the processing times.
1972: Karp proves DIRECTED HAMILTON CIRCUIT NP-complete (doi:10.1007/978-1-4684-2001-2_9).
1975: Brucker, Lenstra and Rinnooy Kan reduce DIRECTED HAMILTON CIRCUIT to DIRECTED HAMILTON PATH (their Theorem 2(d)), and DIRECTED HAMILTON PATH to $n|m|F,\textit{no wait}|C_{\max}$ and to $n|m|F,\textit{no wait},w_j=1|\sum w_jC_j$ (Theorem 5).
1984: Röck shows that the problem stays NP-hard for three machines (doi:10.1145/62.65).

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines. Job $J_\ell$ needs processing time $p_{\ell i}\in\mathbb N$ on machine $M_i$ . Write

q_{\ell i}=\sum_{r=1}^{i}p_{\ell r},\qquad q_{\ell 0}=0,

for the time job $J_\ell$ spends on its first $i$ machines. Because a job never waits, a schedule is determined by the start times $B_\ell\in\mathbb N$ . The operation of $J_\ell$ on $M_i$ occupies $[B_\ell+q_{\ell,i-1},\,B_\ell+q_{\ell i})$ , and job $J_\ell$ completes at $C_\ell=B_\ell+q_{\ell m}$ . A schedule is feasible when no two distinct jobs occupy the same machine at the same time. The delay

c_{jk}=\max_{1\le i\le m}\{q_{ji}-q_{k,i-1}\}

is the least gap $B_k-B_j$ that lets $J_k$ follow $J_j$ on every machine.

A directed graph $G=(V,A)$ on $V=\{0,\dots,n-1\}$ has a Hamilton path if its vertices can be ordered $\sigma(0),\dots,\sigma(n-1)$ with every $(\sigma(i),\sigma(i+1))\in A$ .

From $G$ the paper builds an instance with $n$ jobs and $m=n(n-1)+2$ machines. Each ordered pair $(j,k)$ of distinct jobs is assigned a middle machine $\iota(j,k)\in\{2,\dots,m-1\}$ , and the partial sums $q_{\ell i}$ are perturbed from $i\mu$ by $\pm\lambda$ or $\pm(\lambda+1)$ on the machines $\iota(\ell,\cdot)$ and just before the machines $\iota(\cdot,\ell)$ , depending on whether the pair is an arc. The parameters satisfy $\lambda\ge1$ and $\mu\ge2\lambda+3$ .

Formalization targets

Goal (Theorem 5)

\text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait}|C_{\max}\quad\text{and}\quad \text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait},w_j=1|\textstyle\sum w_jC_j,

where $\propto$ is polynomial-time many-one reducibility between the binary-coded recognition languages.

Milestones, in the order the proof uses them

Eq. (9): $c_{jk}$ is the least gap between $B_j$ and $B_k$ for which $J_k$ follows $J_j$ on every machine.
The travelling-salesman reformulation: if all processing times are positive, a feasible schedule with $C_{\max}\le y$ (resp. $\sum C_\ell\le y$ ) exists iff some job order has path length (resp. summed completion times along the path) at most $y$ .
An admissible ordering $\iota$ exists for every $n\ne2$ .
All processing times of the construction are at least $1$ .
The delays of the construction: $c_{jk}=\mu+2\lambda$ if $(j,k)\in A$ , and $\mu+2\lambda+2$ otherwise.
Theorem 5(a), the equivalence: $G$ has a Hamilton path $\iff$ $C_{\max}\le(n-1)(\mu+2\lambda)+m\mu$ .
Theorem 5(b), the equivalence: $G$ has a Hamilton path $\iff$ $\sum_jC_j\le\tfrac12n(n-1)(\mu+2\lambda)+nm\mu$ .
Theorem 2(d), off the goal's path: $G'$ has a Hamilton circuit iff the graph obtained by splitting a vertex $v'$ into $v'$ and a new sink $v''$ has a Hamilton path.

Significance

The result. Theorem 5, together with the NP-completeness of DIRECTED HAMILTON PATH, places both no-wait criteria among the NP-complete problems once $m$ is part of the input. The Gilmore–Gomory algorithm for two machines therefore cannot be extended to arbitrary $m$ unless P = NP, and heuristics and exact exponential methods for no-wait shops are justified. The reduction also gives a structural fact of independent use: every directed graph can be realized, up to two arc-weight values, as the delay matrix of a no-wait flow shop.

Formalizing it. The result has been proved for fifty years; to our knowledge no machine-checked version exists. This mission produces a checked no-wait flow shop model, a checked travelling-salesman reformulation of it, the correctness of the paper's construction, and a polynomial-time reduction in an explicit Turing-machine model. It also records a gap in the printed proof: the ordering $\iota$ the paper calls easy to construct does not exist for $n=2$ .

Difficulty

Three steps are not routine.

The passage from schedules to job orders assumes that the order in which jobs start is the order in which they visit every machine. With zero processing times this fails, so the reformulation needs the positivity milestone.
Computing the delays requires a case analysis over all machines and all pairs of perturbations. The property of $\iota$ is exactly what keeps the " $+$ " and " $-$ " cases from colliding, and the constants $\lambda\ge1$ , $\mu\ge2\lambda+3$ are tight enough that the comparison must be done carefully.
The goal asks for an actual Turing machine with a polynomial step bound. It has to build $\iota$ for every $n\ne2$ and handle $n\le2$ separately. The equivalences alone do not give this.

Formalization scope

Jobs and machines are $0$ -based (Fin n, Fin m); cum p ℓ i is the paper's $q_{\ell i}$ , and the machine indices $\iota(j,k)$ are the paper's $1$ -based indices. Start times are natural numbers, and release dates are $0$ . Section 3 computes times from processing orders on integer data, and every criterion is regular, so real start times would not change the yes-instances. A zero-length operation occupies the empty interval. $C_{\max}\le y$ is stated as $C_\ell\le y$ for every job. The delays, the partial sums of the construction and its processing times are computed in $\mathbb Z$ . The instance uses their conversion to $\mathbb N$ , which is exact by milestone 4. The threshold of Theorem 5(b) is compared in $\mathbb Q$ , as printed.

The paper's loose phrases are made explicit as follows:

"scheduled directly after" means "precedes on every machine";
"equivalent to solving the TRAVELLING SALESMAN problem" means the two threshold equivalences of milestone 2, with the $\sum C_j$ version as the reading of "constructed as in (a)";
"such an ordering can easily be constructed" is stated for $n\ne2$ , the only case in which it is true.

Directed graphs are Boolean adjacency matrices. A graph with $0$ or $1$ vertices has a Hamilton path, and a one-vertex graph has a Hamilton circuit iff it has a loop.

The goal is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs, with polynomial time measured on Cook's one-tape Turing machines. Instances are coded with the alphabet BSym and binary code encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). A graph is coded as $n$ followed by its adjacency matrix; a flow-shop instance as $n$ , $m$ , the matrix $(p_{\ell i})$ and the threshold $y$ .

Stating only the equivalences 6–7 and calling the result "reducible" would drop polynomiality; the goal therefore asserts PolyReducible. The target languages contain exactly the no-wait flow-shop instances, with no waiting allowed, so the reduction cannot land in a looser problem. The parameters $\lambda,\mu$ always carry $\lambda\ge1$ , $\mu\ge2\lambda+3$ .

Contributions are welcome at every level:

the general travelling-salesman reformulation, which is reusable for any no-wait flow-shop result;
the combinatorial existence of $\iota$ ;
the arithmetic of the construction;
Turing-machine infrastructure for computing arithmetic list transformations in polynomial time, which every reduction in this series needs.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. doi:10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. doi:10.1007/978-1-4684-2001-2_9
P. C. Gilmore, R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12 (1964) 655–679. doi:10.1287/opre.12.5.655
D. A. Wismer, Solution of the flowshop-scheduling problem with no intermediate queues, Operations Research 20 (1972) 689–697. doi:10.1287/opre.20.3.689
S. S. Reddi, C. V. Ramamoorthy, On the flow-shop sequencing problem with no wait in process, Operational Research Quarterly 23 (1972) 323–331. doi:10.1057/jors.1972.52
H. Röck, The three-machine no-wait flow shop is NP-complete, Journal of the ACM 31 (1984) 336–345. doi:10.1145/62.65
N. G. Hall, C. Sriskandarajah, A survey of machine scheduling problems with blocking and no-wait in process, Operations Research 44 (1996) 510–525. doi:10.1287/opre.44.3.510
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. doi:10.1145/800157.805047

14 thms3 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 3: KNAPSACK Reduces to Single-Machine Total Weighted TardinessResearch Paper

Motivation

Minimizing total weighted tardiness on a single machine, written $n|1||\sum w_jT_j$ , is one of the basic problems of deterministic scheduling. A job that finishes after its due date is penalized in proportion to its lateness and its weight. Practitioners use this criterion to model penalty clauses and customer priority. In the theory it was a reference problem for branch-and-bound methods and dominance rules throughout the 1960s and 1970s.

Close relatives are easy: with equal weights and a common due date, shortest-processing-time order is optimal. Whether the weighted problem admits a polynomial algorithm was open until the report of Brucker, Lenstra and Rinnooy Kan in 1975. Their Theorem 4(d) shows that KNAPSACK reduces to it, so the problem is NP-hard. The unweighted case $n|1||\sum T_j$ is listed there as open (Section 5) and was settled only later by Du and Leung (1990).

Timeline:

1972: Karp proves KNAPSACK NP-complete (Karp 1972).
1975: Brucker, Lenstra and Rinnooy Kan, Mathematisch Centrum Report BW 43/75, Theorem 4(d), reduce KNAPSACK to $n|1||\sum w_jT_j$ (journal version: Annals of Discrete Mathematics 1, 1977).
1977: Lawler gives a pseudopolynomial algorithm for $n|1||\sum T_j$ and shows that $n|1||\sum w_jT_j$ is strongly NP-hard (Lawler 1977).
1990: Du and Leung prove $n|1||\sum T_j$ NP-hard (Du & Leung 1990).

Setting

A KNAPSACK instance consists of positive integers $a_1,\dots,a_t$ and $b$ . It is a yes-instance if some subset $S\subseteq T=\{1,\dots,t\}$ satisfies $\sum_{j\in S}a_j=b$ . Write $A=\sum_{j\in T}a_j$ and $a_*=\max_{j\in T}a_j$ .

An instance of $n|1||\sum w_jT_j$ consists of $n$ jobs. Job $j$ has a processing time $p_j$ , a weight $w_j$ and a due date $d_j$ , all nonnegative integers, and every job is available at time $0$ . A schedule gives each job a start time $B_j\in\mathbb N$ , and no two jobs may overlap on the machine. Job $j$ completes at $C_j=B_j+p_j$ and has tardiness $T_j=\max\{0,C_j-d_j\}$ . The instance with threshold $y$ is a yes-instance if some schedule satisfies $\sum_jw_jT_j\le y$ . A processing order $\pi=(\pi(1),\dots,\pi(n))$ determines the schedule without idle time, in which $C_{\pi(k)}=\sum_{i\le k}p_{\pi(i)}$ .

Reducibility (Section 2 of the paper) is polynomial-time many-one reducibility between the recognition versions. A polynomial-time Turing machine must map codes of KNAPSACK instances to codes of scheduling instances so that yes-instances map exactly to yes-instances.

The paper's construction has $n=t+t'$ jobs: for $j\in T$ , $p_j=\tau+a_j$ , $w_j=\tau+a_j+1$ , $d_j=t\tau+b$ ; for each of the $t'$ dummy jobs, $p_j=\tau$ , $w_j=\tau+1$ , $d_j=t\tau+b$ . The threshold is $y=\tfrac12t'(t'+1)\tau(\tau+1)+(t'+1)\tau(A-b)+t'$ , with $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ and $\tau>2t'+A$ . The proof is phrased in terms of $c_\pi=C_{\pi(t)}-(t\tau+b)$ , the amount by which the $t$ -th job of the order misses the common due date.

Formalization targets

Goal: Theorem 4(d)

\text{KNAPSACK}\;\propto\;n|1||\textstyle\sum w_jT_j,

stated as CookPvsNP.PolyReducible SchedComplexity.OneMachine.knapsackLang wtLangMult. The scheduling side uses the multiplicity encoding of the paper's Remark (p. 23), in which a class of identical jobs is written once together with its cardinality.

The equivalence and its claims

Each milestone is a statement of the paper's proof (pp. 20–21) about the construction above, for every admissible $\tau$ :

removal of idle time: every schedule is matched or improved by the schedule without idle time of some processing order;
KNAPSACK has a solution iff some order has $C_{\pi(t)}=t\tau+b$ ; moreover $-b\le c_\pi\le A-b$ ;
identities and bounds (2)–(7) for the tail sums $\sum_{j>t}v_{\pi(j)}(C_{\pi(j)}-C_{\pi(t)})$ ;
claims (A) $c_\pi=0\Rightarrow\exists\pi'$ with $c_{\pi'}=0$ and $\sum w_jT_j\le y$ ; (B) $c_\pi>0\Rightarrow\sum w_jT_j>y$ ; (C) $c_\pi<0\Rightarrow\sum w_jT_j>y$ ;
the equivalence: KNAPSACK has a solution iff the constructed instance has a schedule with $\sum w_jT_j\le y$ .

Significance

The theorem places $n|1||\sum w_jT_j$ among the NP-hard problems, so (unless P = NP) the research on it has to aim at enumerative methods, pseudopolynomial algorithms or approximation, not at an exact polynomial algorithm. Together with the companion reductions of Theorem 4, it drew the boundary between easy and hard single-machine problems that the later classification of Lageweg, Lawler, Lenstra and Rinnooy Kan made systematic.

The result is proved in the paper, and Lawler's later strong NP-hardness proof supersedes it. No machine-checked proof is known to exist. A formal proof adds three things. It makes the paper's "it is easily seen" steps and the encoding argument of the Remark explicit. It produces a reusable single-machine tardiness model with processing orders. It also fixes a gap in the printed construction: the printed $t'$ need not be an integer.

Difficulty

The equivalence is not a local exchange argument. The threshold $y$ must separate orders with $c_\pi=0$ from all others, and the objective is a quadratic function of the order. The orders with $c_\pi=0$ can still differ in $\sum w_jT_j$ by the cross terms $\sum a_{\pi(j)}a_{\pi(k)}$ and by how the late jobs are arranged. The construction therefore needs a slack $t'$ that absorbs these terms, and a scale $\tau$ large enough that a nonzero $c_\pi$ always costs more than the slack. Keeping exact track of every constant, including $t'$ and $y$ , is where errors creep in.

Polynomiality is a second, separate difficulty. The construction has $\Theta(t^2a_*^2+tA)$ jobs, which is exponential in the binary length of the KNAPSACK input. The goal holds only for the encoding of the Remark, and a solver must also produce an explicit polynomial-time Turing machine.

Formalization scope

Jobs of the order-based statements are Fin n, numbered from $0$ ; a processing order is Equiv.Perm (Fin n) with π i the paper's $\pi(i+1)$ . posCompletion p π k is the paper's $C_{\pi(k)}$ for the 1-based position $k$ .
Start times are in $\mathbb N$ . Every criterion is regular and the paper determines schedules by processing orders, so integer start times lose nothing. Tardiness and $\sum w_jT_j$ are computed in $\mathbb Z$ ; the bounds with halves are stated over $\mathbb R$ exactly as printed.
Corrected gap: the printed $t'=\tfrac12(t+1)(A-b)+\tfrac12t(t+1)a_*^2$ is a half-integer when $(t+1)(A-b)$ is odd. The formalization uses its ceiling and computes $y$ from the same $t'$ .
$\tau$ is quantified over all integers with $\tau>2t'+A$ ; the positivity of the $a_j$ and $0<b<A$ are hypotheses, as the paper assumes them.
Explicit readings of the paper's loose phrases: "we may assume [no idle time]" becomes a theorem that the schedule without idle time of some order is at least as good as any schedule; "easily seen" becomes the equivalence with $C_{\pi(t)}=t\tau+b$ ; "for some $\pi$ " in (5) and (7) becomes a reordering that keeps the first $t$ positions, and so keeps $c_\pi$ ; "we may assume $0<b<A$ " is a hypothesis of the milestones but not of the goal, whose reduction must handle every KNAPSACK instance.
Reducibility is CookPvsNP.PolyReducible from the published CookPvsNP_defs. Codes use the alphabet BSym and the binary numerals encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann's encoding). KNAPSACK is restricted to positive integers, so that encoding's subsetSumLang is not reused.
The goal must not be weakened to the bare equivalence: polynomial-time computability of the reduction is part of the statement. The one-copy-per-job encoding of the target is ruled out: the paper does not claim polynomiality for it, and the goal uses the multiplicity encoding instead.
Welcome contributions: proofs of the claims, a reusable lemma that idle time can be removed for regular criteria, and Turing-machine constructions for arithmetic on binary numerals, which the sibling missions of this series also need.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. https://ir.cwi.nl/pub/9725 , https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
E. L. Lawler, A "pseudopolynomial" algorithm for sequencing jobs to minimize total tardiness, Annals of Discrete Mathematics 1 (1977) 331–342. https://doi.org/10.1016/S0167-5060(08)70742-8
J. Du, J. Y.-T. Leung, Minimizing total tardiness on one machine is NP-hard, Mathematics of Operations Research 15 (1990) 483–495. https://doi.org/10.1287/moor.15.3.483
S. Cook, The P versus NP problem, Clay Mathematics Institute problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

18 thms3 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 2: KNAPSACK Reduces to Single-Machine Maximum Lateness, Weighted Number of Late Jobs, and Weighted Completion Time with DeadlinesResearch Paper

Motivation

Deterministic machine scheduling was one of the first application areas of the theory of NP-completeness. After Cook (1971) and Karp (1972) showed that a large family of combinatorial problems are polynomially equivalent, Brucker, Lenstra and Rinnooy Kan set out to locate the boundary between the polynomially solvable and the NP-complete scheduling problems. Their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, Report BW 43/75, 1975; journal version in Annals of Discrete Mathematics 1, 1977) introduced the four-field notation $n|m|\ell,\lambda|k$ that, in refined form, is still the standard classification of scheduling problems, and proved NP-completeness of the "easiest" hard problems by explicit reductions.

Single-machine problems with due dates sit right at that boundary. Minimizing the maximum lateness $L_{\max}$ is solved by Jackson's earliest-due-date rule (1955), and minimizing the number of late jobs by Moore's algorithm (1968). Theorem 4 of the report shows that small changes to these problems — one release date, job weights, or due dates turned into deadlines under a weighted completion-time objective — make them NP-complete, by reduction from KNAPSACK. This mission formalizes four of those reductions, parts (b), (c), (e) and (f) of Theorem 4.

Timeline, as far as this mission is concerned:

1955: Jackson — $n|1||L_{\max}$ is solved by sequencing in order of nondecreasing due dates.
1968: Moore — $n|1||\sum U_j$ (unit weights, no release dates) is solvable in polynomial time.
1972: Karp — KNAPSACK (in the subset-sum form used here) is NP-complete; Karp also notes the reduction to $n|1||\sum w_jU_j$ , which the report cites for part (e).
1975: Brucker, Lenstra and Rinnooy Kan — Theorem 4: KNAPSACK reduces to ten scheduling problems, including the four single-machine problems of this mission.

Setting

A single-machine instance consists of $n\ge1$ jobs $J_1,\dots,J_n$ . Job $J_j$ needs $p_{j1}$ units of processing on the machine $M_1$ , has a weight $w_j$ , a release date $r_j$ and a due date $d_j$ ; all data are nonnegative integers. A schedule assigns to each job a starting time $B_j\ge r_j$ such that the occupied intervals $[B_j,B_j+p_{j1})$ of distinct jobs are disjoint. Idle time is allowed; a job with $p_{j1}=0$ occupies an empty interval. The completion time is $C_j=B_j+p_{j1}$ , the lateness is $L_j=C_j-d_j$ (possibly negative), and $U_j$ is $0$ if $C_j\le d_j$ and $1$ otherwise. The criteria are

L_{\max}=\max_j L_j,\qquad \sum w_jC_j=\sum_{j=1}^n w_jC_j,\qquad \sum w_jU_j=\sum_{j=1}^n w_jU_j .

The problem class is written in the $\lambda$ field: by default every $r_j=0$ ; $r_n\ge0$ allows a nonzero release date for the last job $J_n$ only; $w_j=1$ fixes unit weights; $L_{\max}\le0$ admits only schedules that meet every due date. A problem is turned into a yes/no question by asking whether a schedule with value $\le y$ exists.

KNAPSACK (Theorem 2(b) of the report): given positive integers $a_1,\dots,a_t,b$ , is there a subset $S\subseteq T=\{1,\dots,t\}$ with $\sum_{j\in S}a_j=b$ ? Write $A=\sum_{j\in T}a_j$ .

A problem $P'$ is reducible to $P$ , $P'\propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ whose answer is the same.

Formalization targets

Goal: Theorem 4(b), (c), (e), (f)

\mathsf{KNAPSACK}\propto n|1|L_{\max}\le0|\textstyle\sum w_jC_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0|L_{\max},

\mathsf{KNAPSACK}\propto n|1||\textstyle\sum w_jU_j,\quad \mathsf{KNAPSACK}\propto n|1|r_n\ge0,w_j=1|\textstyle\sum w_jU_j ,

as polynomial-time many-one reductions between languages of binary strings.

Milestones: the four yes-instance equivalences

For positive $a_1,\dots,a_t,b$ with $0<b<A$ , and the paper's constructions:

4(c): $n=t+1$ ; $r_j=0$ , $p_{j1}=a_j$ , $d_j=A+1$ for $j\in T$ ; $r_n=b$ , $p_{n1}=1$ , $d_n=b+1$ . KNAPSACK has a solution iff some schedule has $L_{\max}\le0$ .
4(f): the same instance with unit weights; KNAPSACK has a solution iff some schedule has $\sum U_j\le0$ .
4(e): $n=t$ ; $p_{j1}=w_j=a_j$ , $d_j=b$ . KNAPSACK has a solution iff some schedule has $\sum w_jU_j\le A-b$ .
4(b): $n=t+1$ ; $p_{j1}=w_j=a_j$ , $d_j=A+1$ for $j\in T$ ; $p_{n1}=1$ , $w_n=0$ , $d_n=b+1$ . KNAPSACK has a solution iff some schedule meeting all due dates has

\sum w_jC_j\le y=\sum_{j,k\in T,\ j\le k}a_ja_k+A-b .

Significance

The result. Combined with the NP-completeness of KNAPSACK, the four reductions show that the four problems are NP-hard (in the ordinary sense; they admit pseudo-polynomial algorithms). Part (c) shows that Jackson's rule cannot be extended to a single nonzero release date unless P = NP; part (f) does the same for Moore's algorithm; part (e) explains why weights are essential in the late-jobs problem; part (b) shows that deadlines turn the weighted completion-time problem, solved by Smith's ratio rule without them, into a hard one. These are entries of the complexity tables that every later scheduling classification builds on.

Formalizing it. The reductions are classical and proved on paper, in a few lines each: for (c), (e) and (f) the report gives only the construction and a figure. None of them has a machine-checked proof. A complete formalization supplies the explicit equivalence over all feasible schedules (including schedules with idle time and arbitrary processing order), the handling of the inputs the proof sets aside by "we may assume that $0<b<A$ ", and the polynomial-time computability of the constructions in a Turing-machine model.

Difficulty

Each equivalence has an easy direction: a subset $S$ with sum $b$ gives the schedule "jobs of $S$ , then $J_n$ , then the rest" (Figures 4 and 7 of the report). The other direction must rule out every feasible schedule, not only the idle-free ones in the displayed order. The report gives no argument for this direction in (c), (e) and (f), and for (b) only a computation for idle-free schedules of one shape. The equivalences are false outside $0<b<A$ in some cases (for (c), any $b>A$ makes every schedule on time), so the goal's reduction must treat those inputs separately.

The heavier part is polynomial-time computability: the reduction must be a function on strings, computed by a one-tape Turing machine within a polynomial number of steps, that parses a binary-coded KNAPSACK instance, computes $A$ and the threshold (for (b), a sum of $O(t^2)$ products), and writes the coded scheduling instance — and maps malformed strings outside the target language.

Formalization scope

Model. Jobs are Fin n (0-based; $J_n$ is the last index), with $n>0$ in each target language. Starting times are natural numbers: Section 3 computes them from processing orders on integer data, and since all criteria here are regular and release dates survive left shifts, real starting times give the same yes-instances. Feasibility requires disjoint occupied intervals, including empty intervals when $p_{j1}=0$ . Idle time is allowed. Lateness is an integer.
Problem classes are binding. $r_n\ge0$ means at least one job and release date $0$ for every job except the last; $L_{\max}\le0$ in (b) is a constraint on schedules, not the criterion. Instances outside the class are not in the target language.
Thresholds. $y\in\mathbb N$ in all four languages; for $L_{\max}$ this restricts to nonnegative thresholds, enough for the paper's $y=0$ . " $L_{\max}\le y$ " is stated as " $L_j\le y$ for all $j$ ".
Codes. An instance with threshold $y$ is the list $n$ , then $p_{j1},w_j,r_j,d_j$ per job, then $y$ , each number in binary.
Reducibility. "Reducible" (Section 2) is read as Karp reducibility, CookPvsNP.PolyReducible from the published definition CookPvsNP_defs. The alphabet and binary number codes are those of the published definition ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann); its SUBSET SUM language is not reused because it admits zero sizes, while the paper's KNAPSACK is over positive integers.
Explicit readings of loose phrases. "We may assume that $0<b<A$ " becomes a hypothesis of each milestone and an obligation on the goal's reduction. "Cf. reduction (i) and Figure 4", "Cf. Karp [19] and Figure 7" and "The equivalence follows immediately" become the stated equivalences over all feasible schedules. Reduction (c) does not specify weights; the shared construction uses unit weights.
Not trivializable. The equivalences are stated for the paper's explicit constructions, not for an existentially chosen instance; the target languages enforce the problem class; and the goal demands polynomial-time computability, not only the equivalence.
Infrastructure. A Turing-machine library for arithmetic on binary codes (parsing, addition, multiplication, comparison) is reusable across all seven missions of this series and across every reduction posed in the same framework. Contributions of such general lemmas are welcome.

Parts (a), (d) and (g)–(j) of Theorem 4 are formalized in other missions of this series.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum, Report BW 43/75, Amsterdam, 1975; journal version: J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in: Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
S. A. Cook, The complexity of theorem-proving procedures, Proc. 3rd ACM STOC, 1971, 151–158. https://doi.org/10.1145/800157.805047
J. M. Moore, An n job, one machine sequencing algorithm for minimizing the number of late jobs, Management Science 15 (1968) 102–109. https://doi.org/10.1287/mnsc.15.1.102
J. R. Jackson, Scheduling a production line to minimize maximum tardiness, Research Report 43, Management Science Research Project, UCLA, 1955.

11 thms3 active usersReviewed

Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 1: PARTITION Reduces to Makespan and to Weighted Completion Time on Two Identical MachinesResearch Paper

Motivation

Deterministic machine scheduling asks how to process a set of jobs on a set of machines so that an overall criterion, such as the time at which the last job finishes, is as small as possible. In the early 1970s many such problems had efficient algorithms (Johnson's rule for the two-machine flow shop, Smith's ratio rule for a single machine, Lawler's rule under precedence constraints), while others resisted every attempt. The report of Brucker, Lenstra and Rinnooy Kan (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977) drew the line between the two groups systematically. It fixed the four-field notation $n|m|\ell,\lambda|k$ that the scheduling literature still uses, and it proved NP-completeness of the "easiest" hard problems by explicit reductions in the sense of Karp.

The first family of reductions in the report, Theorem 3, concerns the simplest machine environment beyond a single machine: two identical machines. It shows that already there, minimizing the makespan and minimizing the total weighted completion time are as hard as PARTITION. These two reductions are simplified versions of reductions given by Bruno, Coffman and Sethi (1974), reference [3] of the report.

Setting

PARTITION. Given positive integers $a_1,\dots,a_t$ , decide whether there is a subset $S$ of $T=\{1,\dots,t\}$ with

\sum_{j\in S}a_j=\sum_{j\in T-S}a_j .

Write $A=\sum_{j\in T}a_j$ for the total.

Two identical machines. There are $n$ jobs $J_1,\dots,J_n$ and two machines $M_1,M_2$ . Job $J_j$ has a processing time $p_j\in\mathbb N$ and a weight $w_j\in\mathbb N$ , and must be processed without interruption on one machine of its choice; all jobs are available at time $0$ . A schedule assigns to every job a machine and a starting time $B_j\in\mathbb N$ ; its completion time is $C_j=B_j+p_j$ . A schedule is feasible if no two jobs on the same machine are processed at the same time, i.e. the intervals $[B_j,B_j+p_j)$ on each machine are pairwise disjoint. Idle time is allowed. Two criteria are considered:

C_{\max}=\max_j C_j,\qquad \sum_j w_jC_j .

The problems $n|2|I|C_{\max}$ and $n|2|I|\sum w_jC_j$ ask for a feasible schedule minimizing the respective criterion.

Reducibility. Following Section 2 of the report, each problem is replaced by its recognition version: given an instance and a threshold $y$ , is there a feasible schedule with value $\le y$ ? A problem $P'$ is reducible to $P$ , written $P'\propto P$ , if every instance of $P'$ can be transformed in polynomial time into an instance of $P$ with the same answer. Instances are written as words over a finite alphabet, with every number in binary.

Formalization targets

Goal: Theorem 3

\text{PARTITION}\propto n|2|I|C_{\max}\qquad\text{and}\qquad \text{PARTITION}\propto n|2|I|\textstyle\sum w_jC_j .

Both reductions use the same instance shape: $n=t$ jobs with $p_j=a_j$ .

Milestones

Theorem 3(a), equivalence. With $p_j=a_j$ and $y=\tfrac12A$ : PARTITION has a solution iff some feasible schedule has $C_{\max}\le y$ .
Ordering independence. With $p_j=w_j=a_j$ , if $S$ is the set of jobs on $M_1$ and each machine works without idle time from $0$ , then $\sum w_jC_j=k(S)$ for every order of the jobs, where

k(S)=\sum_{j,k\in S,\,j\le k}a_ja_k+\sum_{j,k\in T-S,\,j\le k}a_ja_k ;

every feasible schedule with this assignment has value at least $k(S)$ . 3. The identity for $k(S)$ . With $c=\sum_{j\in S}a_j-\tfrac12A$ ,

k(S)=k(T)-\Big(\sum_{j\in S}a_j\Big)\Big(\sum_{j\in T-S}a_j\Big)=\sum_{j,k\in T,\,j\le k}a_ja_k-\big(\tfrac12A+c\big)\big(\tfrac12A-c\big)=y+c^2 .

Theorem 3(b), equivalence. With $p_j=w_j=a_j$ and $y=\sum_{j,k\in T,\,j\le k}a_ja_k-\tfrac14A^2$ : PARTITION has a solution iff some feasible schedule has $\sum w_jC_j\le y$ .

Significance

The result. Since PARTITION is NP-complete (Karp 1972), Theorem 3 shows that both problems are NP-hard with only two machines and a single operation per job; their recognition versions are NP-complete. Together with the single-machine and shop results in the rest of the report, it places the boundary of tractability in deterministic scheduling. The makespan problem $P2\|C_{\max}$ became a standard source problem for later hardness proofs and a standard target for pseudo-polynomial algorithms and approximation schemes. The weighted completion time result contrasts with the single-machine case, which Smith's ratio rule solves in polynomial time.

Formalizing it. The theorem is classical and fully proved on paper; the report prints the constructions and, for (b), a short calculation. To our knowledge no machine-checked proof exists. The mission produces (i) a precise model of nonpreemptive schedules on two identical machines with integer start times and idle time allowed, (ii) the two yes-instance equivalences with the paper's rational thresholds, (iii) the ordering-independence statement for $p_j=w_j$ behind part (b), and (iv) the polynomial-time computability of the reductions in a Turing machine model. Part (iv) is the formal content of "reducible" and is missing from the paper.

Difficulty

For part (a) the mathematics is short. The paper treats it as evident; a formal proof must still handle schedules with idle time and the case of odd $A$ , where $\tfrac12A$ is not an integer.

Part (b) rests on the claim that, when $p_j=w_j$ , the value $\sum w_jC_j$ does not depend on the order of the jobs on a machine. For a single machine without idle time this is a symmetric double sum. A recognition-problem proof also needs the converse direction: no schedule with idle time beats the non-idle one, so every feasible schedule with assignment $S$ has value at least $k(S)$ . The paper cites this rather than proving it.

The step the paper leaves out entirely is polynomiality. The constructions copy the input and compute $\tfrac12A$ or $\sum_{j\le k}a_ja_k-\tfrac14A^2$ , and in a one-tape Turing machine model with an explicit polynomial time bound this needs binary arithmetic (sums, products, a floor) carried out on the tape. It also needs a decoder that rejects malformed words and lists containing a zero. This is routine in principle but long in practice.

Formalization scope

Model. Jobs are Fin n and machines Fin 2 (machine 0 is $M_1$ ). Starting times are natural numbers. Section 3 of the report computes them from processing orders on nonnegative integer data, and both criteria are regular, so real starting times would give the same yes-instances. Processing times may be zero; a zero-length job occupies the empty interval. Schedules may contain idle time.
Criteria. " $C_{\max}\le y$ " is stated as $C_j\le y$ for every job, which equals $\max_jC_j\le y$ for $n\ge1$ and avoids a supremum. $\sum w_jC_j$ is a finite sum in $\mathbb N$ .
Languages. PARTITION is the set of binary codes of lists of positive integers that admit a partition; a code of a list with a zero entry is not in the language. A target word codes $n$ , the processing times (and weights, job by job), and a threshold $y\in\mathbb N$ . The number of machines is fixed by the class and not coded. Every coded instance is in the class, so the language admits nothing outside it.
Reducibility is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs (Cook's one-tape Turing machines, polynomial-time many-one reductions). The alphabet BSym and the binary code encNats are reused from the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). Its PARTITION language is not reused, because it allows zero sizes.
Thresholds. The milestones state the paper's thresholds $\tfrac12A$ and $\sum_{j\le k}a_ja_k-\tfrac14A^2$ as real numbers, exactly as printed. The goal's reduction must write a natural-number threshold; all schedule values are integers, so the floor of the printed threshold gives the same yes-instances.
Explicit readings. The equivalence of (a) is not printed; the report says on p. 14 that such equivalences are "trivial or clear" where not proved. "Only depends on the choice of $S$ " is stated as two facts: equality for non-idle schedules and a lower bound for all feasible schedules. "It is easily seen (cf. Figure 1)" is the three-step identity, one equality per printed step. $k(S)$ is defined by its closed form, and its link to schedules is a milestone.
Ruled out. A target language whose yes-instances are defined through PARTITION, an equivalence for some instance rather than the paper's construction, and a goal that drops polynomial-time computability would all make the goal vacuous or different. The statements here use the constructions as printed and Cook's reducibility.
Welcome contributions. Proofs of the four milestones; a library of polynomial-time Turing machine programs for binary arithmetic and list decoding over BSym, which every mission of this series needs and which is reusable for other reductions on the platform.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975. https://ir.cwi.nl/pub/9725/9725D.pdf
J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of machine scheduling problems, Annals of Discrete Mathematics 1 (1977) 343–362. https://doi.org/10.1016/S0167-5060(08)70743-X
J. Bruno, E. G. Coffman Jr., R. Sethi, Scheduling independent tasks to reduce mean finishing time, Communications of the ACM 17 (1974) 382–387. https://doi.org/10.1145/361011.361064
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. https://doi.org/10.1007/978-1-4684-2001-2_9
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. https://doi.org/10.1145/800157.805047
W. E. Smith, Various optimizers for single-stage production, Naval Research Logistics Quarterly 3 (1956) 59–66. https://doi.org/10.1002/nav.3800030106

11 thms3 active usersReviewed

Completed

Algebraic Geometry Linear Optimization Operations Research+1·Captain: mikedeng1

Log-Barrier Interior Point Methods Are Not Strongly Polynomial 1: Every Polygonal Curve in the Wide Neighborhood of the Central Path of LW_r(t) from μ̄ ≤ 1 to μ̄ ≥ t² Has at Least 2^(r−1) SegmentsResearch Paper

Motivation

Interior point methods solve linear programs in a number of arithmetic operations polynomial in the bit length of the input (Karmarkar 1984). Whether linear programming admits a strongly polynomial algorithm, one whose number of arithmetic operations is bounded by a polynomial in the number of variables and constraints alone, is open; it is the ninth of Smale's problems for the next century (Smale 1998/2000, see the references). A natural question is whether some interior point method is strongly polynomial. Primal-dual path-following methods follow the central path of a log-barrier problem and are the methods used in practice.

Allamigeon, Benchimol, Gaubert and Joswig (arXiv:1708.01544, SIAM J. Appl. Algebra Geom. 2018) gave such a family. For linear programs $\mathbf{LW}_r(t)$ with $2r$ variables and $3r+1$ constraints, every path-following method that stays in the wide neighborhood of the central path needs at least $2^{r-1}$ iterations once $t$ is large enough. The same family disproves the "continuous Hirsch conjecture" of Deza, Terlaky and Zinchenko (DTZ09, see the references) on the total curvature of the central path. That curvature result is the subject of a separate mission. This mission formalizes the iteration bound.

Setting

For a real $m\times n$ matrix $A$ , $b\in\mathbb R^m$ , $c\in\mathbb R^n$ and $N:=n+m$ , the paper considers the linear program in slack form and its dual,

\mathrm{LP}(A,b,c):\ \min\ \langle c,x\rangle\ \text{ s.t. }\ Ax+w=b,\ (x,w)\ge0,\qquad \mathrm{DualLP}(A,b,c):\ s-A^\top y=c,\ (s,y)\ge0 .

A primal-dual point is $z=(x,w,s,y)\in\mathbb R^{2N}$ . The set $\mathcal F^\circ$ of strictly feasible points consists of the $z$ with all $2N$ coordinates positive that satisfy both equality systems. The duality measure is

\bar\mu(z)=\frac1N\big(\langle x,s\rangle+\langle w,y\rangle\big),

and for $0<\theta<1$ the wide neighborhood of the central path is

\mathcal N^{-\infty}_\theta=\Big\{z\in\mathcal F^\circ:\ x_js_j\ge(1-\theta)\bar\mu(z)\ \forall j,\ \ w_iy_i\ge(1-\theta)\bar\mu(z)\ \forall i\Big\}.

The central path itself is the set of points where all products $x_js_j$ , $w_iy_i$ are equal. The neighborhood bounds the products only from below. It contains the $\ell_2$ and $\ell_\infty$ neighborhoods used by short-step, long-step and predictor-corrector methods.

The instance is $\mathbf{LW}_r(t)$ , for $r\ge1$ and $t>0$ :

\min\ x_1\ \text{ s.t. }\ x_1\le t^2,\ x_2\le t,\ x_{2j+1}\le t\,x_{2j-1},\ x_{2j+1}\le t\,x_{2j},\ x_{2j+2}\le t^{1-1/2^j}(x_{2j-1}+x_{2j})\ (1\le j<r),\ x_{2r-1},x_{2r}\ge0 .

With slacks $w_1,\dots,w_{3r-1}$ it becomes $\mathbf{LW}^=_r(t)=\mathrm{LP}(A,b,c)$ with $n=2r$ , $m=3r-1$ , $N=5r-1$ . Its wide neighborhood is written $\mathcal N^{-\infty}_{\theta,t}$ . A polygonal curve is a union $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ of $p$ segments, and it is contained in the neighborhood when every point of every segment is.

The milestones use the tropical semifield $\mathbb T=\mathbb R\cup\{-\infty\}$ with $a\oplus b=\max(a,b)$ and $a\odot b=a+b$ . The tropical segment $\mathsf{tsegm}(u,v)$ is the set of points $\lambda\odot u\oplus\mu\odot v$ with $\lambda\oplus\mu=0$ . The Funk metric is $\delta_F(x,y)=\max(0,\max_k(y_k-x_k))$ , with $d_\infty(x,y)=\max(\delta_F(x,y),\delta_F(y,x))$ and the directed Hausdorff distance $d_\infty(X,Y)=\sup_{x\in X}\inf_{y\in Y}d_\infty(x,y)$ . Finally, $\log_t$ is applied coordinatewise, with $\log_t0=-\infty$ .

Formalization targets

Goal: Theorem 30 (p. 27)

Let $r\ge1$ and $0<\theta<1$ , and suppose that

t>\Big(\max\Big((10r-2)!,\ \frac{((10r-1)!)^{24}}{(1-\theta)^3}\Big)\Big)^{2^{r-1}} .\tag{36}

If a polygonal curve $[z^0,z^1]\cup\dots\cup[z^{p-1},z^p]$ is contained in $\mathcal N^{-\infty}_{\theta,t}$ with $\bar\mu(z^0)\le1$ and $\bar\mu(z^p)\ge t^2$ , then

p\ge2^{r-1}.

The threshold (36) is the paper's own explicit constant. Corollary 31 (Theorem B of the introduction) restates the result for algorithms. Any method whose iterates and the segments joining them stay in the wide neighborhood performs at least $2^{r-1}$ iterations to reduce the duality measure from $t^2$ to $1$ .

Milestones

Proposition 1 (p. 5). On the primal-dual feasible set, $\bar\mu((1-\alpha)z+\alpha z')=(1-\alpha)\bar\mu(z)+\alpha\bar\mu(z')$ for all $\alpha\in\mathbb R$ .
Lemma 5 (p. 10). For $u\le v$ in $\mathbb T^d$ , $\mathsf{tsegm}(u,v)$ is a polygonal curve whose segments, oriented from $u$ to $v$ , have directions $e^{K_1},\dots,e^{K_\ell}$ with $K_1\subsetneq\dots\subsetneq K_\ell$ and $\ell\le d$ .
Lemma 8 (p. 11). For a segment $S=[u,v]$ in $\mathbb R^d_+$ and $t>1$ ,

d_\infty\big(\mathsf{tsegm}(\log_tu,\log_tv),\ \log_tS\big)\le\log_t2 .

Lemma 11 (p. 13). For a $d\times d$ matrix $\mathbf M$ with monomial entries $\pm t^{\alpha_{ij}}$ and $t>1$ , $\log_t|\det\mathbf M(t)|$ and $\operatorname{val}(\det\mathbf M)$ differ by at most $\log_td!$ ; the lower bound holds once $t\ge(d!)^{1/\eta(\mathbf M)}$ .
Proposition 20 (p. 19). The explicit recursion for $x^\lambda$ gives the greatest point of the tropical polyhedron $\{x\in\mathcal P':x_1\le\lambda\}$ , where $\mathcal P'\subseteq\mathbb T^{2r}$ is cut out by the tropicalized constraints (26) of $\mathbf{LW}_r$ .

Significance

The theorem shows that the iteration count of a large class of primal-dual log-barrier interior point methods cannot be bounded by any function of $r$ that grows more slowly than $2^{r-1}$ , uniformly in the data. The class includes the methods of Kojima–Mizuno–Yoshise, Monteiro–Adler and Mizuno–Todd–Ye. No such method is strongly polynomial. The constraint matrix of $\mathbf{LW}_r(t)$ is fixed by $r$ and $t$ alone, so the bound concerns the combinatorial dimension, not the bit length. The only property of the method used is that its trajectory stays in $\mathcal N^{-\infty}_{\theta,t}$ . The lower bound therefore applies to every method with that property, whatever rule chooses its steps.

The result is proved in the paper; no machine-checked proof of it or of its tropical ingredients is known. A formalization would check the explicit threshold (36), which the paper derives in a few lines from bounds on Puiseux polyhedra. It would also produce reusable statements about tropical segments, the Funk and Hilbert metrics on $\mathbb T^d$ , and determinants of monomial matrices.

Difficulty

Following the central path is not hard in principle: the obvious argument tracks the duality measure, which decreases by a constant factor per iteration in a neighborhood of the path. That argument gives only upper bounds. The lower bound requires showing that the neighborhood itself, for large $t$ , is too thin to be crossed in a few straight steps, uniformly over every possible trajectory. The paper does this by passing to the limit $t\to\infty$ on logarithmic scale. The image of $\mathcal N^{-\infty}_{\theta,t}$ under $\log_t$ collapses onto a piecewise-linear tropical central path, and a segment of $\mathbb R^{2N}$ becomes, up to $\log_t2$ , a tropical segment. The tropical central path of $\mathbf{LW}_r$ then has to be shown to need $2^{r-1}$ tropical segments. The limit argument has to be made quantitative at a finite, explicit $t$ . That is where the Puiseux-series machinery (Theorems 12, 15 and 19 of the paper) and the explicit constant enter.

Formalization scope

Everything is stated over $\mathbb R$ and $\mathbb T$ ; the goal typechecks without the field of Puiseux series. A primal-dual point is an element of $\mathbb R^n\times\mathbb R^m\times\mathbb R^n\times\mathbb R^m$ . The dual equation is $s-A^\top y=c$ with Mathlib's transpose, $\bar\mu$ divides by $N=n+m$ (equal to $5r-1$ for $\mathbf{LW}^=_r$ ), and the wide neighborhood is one-sided. The instance matrix is generated from the paper's 1-based row and column numbers; Lean indices are 0-based. A polygonal curve is a map $z:\{0,\dots,p\}\to\mathbb R^{2N}$ with segment ℝ (z i) (z (i+1)) ⊆ N. The power $2^{r-1}$ in (36) is a natural-number power and the factorials are natural-number factorials. $\mathbb T$ is WithBot ℝ, and distances that can be infinite take values in EReal, with the convention $-\infty+(+\infty)=-\infty$ encoded explicitly.

Two statements are repaired or restated. Lemma 11 is printed for all $t>0$ , but its first inequality fails for $0<t<1$ (for $\mathbf M=\begin{pmatrix}t&1\\1&1\end{pmatrix}$ at $t=1/2$ ), so it is stated for $t>1$ . Lemma 8 makes explicit its implicit hypotheses $t>1$ and $u,v\ge0$ . Proposition 20 is stated in the form its proof establishes, as the greatest point of a tropical polyhedron. Its identification with the valuation of the Puiseux central path is not part of the item. Monomial matrices are given by sign and exponent matrices, and the valuation of the determinant is computed from the permutation expansion.

A trivializing formalization is ruled out: $\mathcal N^{-\infty}_{\theta,t}$ is not empty, since the build includes a sorry-free proof that it contains an explicit point for $r=1$ , $t=2$ , $\theta=1/2$ . A curve with $p=0$ cannot satisfy both duality-measure conditions, since $t^2>1$ .

The paper's Puiseux-series results are not posed: Theorems 12, 15, 19 and 29, Propositions 14, 16, 21 and 28, Corollary 17, and the count $\gamma([0,2])\ge2^{r-1}$ of §6.2. They need a faithful model of the field of absolutely convergent generalized Puiseux series and of the tropical central path. Contributions of that infrastructure, and of these statements as further milestones, are welcome. So are proofs of the five milestones, which need no Puiseux series. Proposition 1, Lemma 5 and Proposition 20 are elementary, and Lemma 8 and Lemma 11 are estimates with explicit constants.

Selected references

X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1), 2018; arXiv:1708.01544v2. https://arxiv.org/abs/1708.01544
A. Deza, T. Terlaky, Y. Zinchenko, Central path curvature and iteration-complexity for redundant Klee–Minty cubes, in Advances in Applied Mathematics and Global Optimization, Adv. Mech. Math. 17, Springer, 2009, pp. 223–256. https://doi.org/10.1007/978-0-387-75714-8
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2), 1998, 7–15; reprinted in Mathematics: Frontiers and Perspectives, AMS, 2000. https://doi.org/10.1007/BF03025291
M. Develin, B. Sturmfels, Tropical convexity, Doc. Math. 9, 2004. https://arxiv.org/abs/math/0308254
S. J. Wright, Primal-Dual Interior-Point Methods, SIAM, 1997. https://doi.org/10.1137/1.9781611971453
X. Allamigeon, S. Gaubert, M. Skomra, Tropical spectrahedra, Discrete Comput. Geom. 63, 2020; arXiv:1610.06746. https://arxiv.org/abs/1610.06746

12 thms3 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

The Complexity of Computing a Nash Equilibrium 2: The Three-Colorable Addition-Multiplication Gadget Has Error Amplification 81Research Paper

Motivation

Nash's theorem guarantees that every finite game has a mixed equilibrium, but says nothing about how hard one is to find. Daskalakis, Goldberg and Papadimitriou (SIAM J. Comput. 39(1), 2009) showed that computing a Nash equilibrium is complete for the class PPAD of total search problems whose solutions are guaranteed by a parity argument on a directed graph (Papadimitriou 1994). Their proof simulates an arithmetic circuit by a graphical game: a multiplayer game in which each player's payoff depends on a few neighbours only, built from small game gadgets whose equilibria compute $x \mapsto \alpha x$ , $x + y$ , $xy$ , constants and comparisons on mixed-strategy probabilities.

These gadgets are the reusable core of the reduction. The PPAD-completeness results for three-player games, and the later results for two-player games and for approximate equilibria, all rest on gadget analyses of this kind.

Timeline.

1994: Papadimitriou defines PPAD and shows that Nash equilibrium computation lies in it (JCSS 48).
2001: Kearns, Littman and Singh introduce graphical games (UAI 2001).
2005–2006: Goldberg and Papadimitriou reduce $r$ -player games to four-player games, and Daskalakis, Goldberg and Papadimitriou prove PPAD-completeness for four players (STOC 2006). The three-player case is obtained independently by Daskalakis and Papadimitriou and by Chen and Deng (ECCC reports, 2005); the two-player case by Chen and Deng (FOCS 2006; J. ACM 56(3), 2009, with Teng).
2009: the journal version unifies the three-player argument; its Proposition 4.18 is the gadget $\mathcal G_{+,*}$ that makes the reduction to three players work.

Setting

A game has finitely many players; player $p$ has a finite set $S_p$ of pure strategies and a nonnegative payoff $u^p_s$ for each pure profile $s$ . A mixed profile $x$ gives each player a probability distribution $(x^p_j)_{j\in S_p}$ , and $x_s$ denotes the product of the probabilities of the components of a partial profile $s$ . The expected payoff of a pure strategy $j$ of $p$ is $\sum_{s\in S_{-p}} u^p_{js}x_s$ .

An $\epsilon$ -Nash equilibrium (the paper's notion, an $\epsilon$ -approximately well-supported equilibrium, Eq. (2)) is a mixed profile in which no player puts weight on a pure strategy that another of its pure strategies beats by more than $\epsilon$ :

\forall p,\ j, j' \in S_p:\quad \sum_{s\in S_{-p}} u^p_{js}x_s > \sum_{s\in S_{-p}} u^p_{j's}x_s + \epsilon \implies x^p_{j'} = 0 .

For $\epsilon = 0$ this characterizes Nash equilibria.

A player with strategies $\{0,1\}$ is binary; $\mathbf p[v]$ is the probability that it plays $1$ , and $\mathbf p[v : s]$ is the probability that $v$ plays $s$ . The affects graph (Definition 2.2) has an edge $(v_1, v_2)$ between distinct players when the payoff of $v_2$ is a nonconstant function of the action of $v_1$ . A legal $k$ -coloring (Definition 4.8) gives each player one of $k$ colors so that the two ends of an edge differ and two distinct players with a common successor differ.

The game $\mathcal G_{+,*}$ (Fig. 11) has inputs $v_1, v_2$ , output $v_3$ and intermediate players $w_1, v_1', w_2, v_2', w_3, w, u$ , all binary except $v_2'$ , which has strategies $\{0, 1, *\}$ . Its payoff tables are fixed by nonnegative integers $\alpha, \beta, \gamma$ ; the inputs' payoffs are unconstrained.

Formalization targets

Goal: Proposition 4.18

For nonnegative integers $\alpha, \beta, \gamma$ with $\alpha + \beta + \gamma \le 3$ , the affects graph of $\mathcal G_{+,*}$ has a legal 3-coloring, and for every $\epsilon \in [0, 0.01]$ , at every $\epsilon$ -Nash equilibrium,

\Big|\,\mathbf p[v_3] - \min\{1,\ \alpha\mathbf p[v_1] + \beta\mathbf p[v_2] + \gamma\mathbf p[v_1]\mathbf p[v_2]\}\Big| \le 81\,\epsilon .

The case $\epsilon = 0$ is exact computation at every Nash equilibrium.

Milestones: the four claims of the proof

Claim 1: $\mathbf p[v_1'] = \tfrac18\mathbf p[v_1] \pm \epsilon$ .
Claim 2: $\mathbf p[v_2' : 1] = \tfrac18\mathbf p[v_2] \pm \epsilon$ .
Claim 3: $\mathbf p[v_2' : *] = \tfrac{\alpha}{8}\mathbf p[v_1] + \tfrac{\beta}{8}\mathbf p[v_2] + \tfrac{\gamma}{8}\mathbf p[v_1]\mathbf p[v_2] \pm 10\epsilon$ .
Claim 4: the output bound of the goal.

Milestones: the elementary gadgets

Proposition 4.2 ( $\mathcal G_{\times\alpha}$ ): $\mathbf p[v_2] = \min(\alpha\mathbf p[v_1], 1) \pm \epsilon$ for real $\alpha \ge 0$ , $\epsilon < 1$ .
Proposition 4.3: $\mathbf p[v_3] = \min(\alpha\mathbf p[v_1] + \beta\mathbf p[v_2] + \gamma\mathbf p[v_1]\mathbf p[v_2], 1) \pm \epsilon$ for real $\alpha, \beta, \gamma \ge 0$ .
Proposition 4.5 ( $\mathcal G_\alpha$ ): $\mathbf p[v_1] = \min(\alpha, 1) \pm \epsilon$ .
Lemma 5.3 (comparator $\mathcal G_<$ ): $\mathbf p[d] = 1$ if $\mathbf p[a] < \mathbf p[b] - \epsilon$ and $\mathbf p[d] = 0$ if $\mathbf p[a] > \mathbf p[b] + \epsilon$ .

Significance

The result. The paper reduces $r$ -player games to three-player games by building a graphical game from gadgets, legally coloring it with three colors, and turning each color class into one player of a normal-form game (§4.2, §4.5). Proposition 4.18 supplies a gadget that computes $\min\{1, \alpha x + \beta y + \gamma xy\}$ and can be glued into such a construction while keeping it legally 3-colorable (p. 233), at the price of an error constant $81$ instead of the constant $1$ of the elementary gadgets. The error bound is what carries the reduction over to approximate equilibria: an $\epsilon$ -Nash equilibrium of the gadget computes its function to within $81\epsilon$ .

Formalizing it. All results here are proved in the paper (Proposition 4.5 is stated with the remark that its proof is similar to those of Propositions 4.2 and 4.3). None of them has a machine-checked proof, and no graphical-game or gadget infrastructure exists in Lean. The mission formalizes the known proofs and produces a library of verified gadgets with explicit error bounds, the first layer of any formal treatment of the PPAD-hardness of Nash equilibria.

Difficulty

Each claim is a case analysis on which strategy of an intermediate player is dominated by more than $\epsilon$ , but the cases interact. Claim 3 needs Claims 1 and 2 as inputs, and it is the step where both $\alpha + \beta + \gamma \le 3$ and $\epsilon \le 0.01$ are used: without them one of the regimes of $w$ cannot be excluded. The three-strategy player $v_2'$ cannot be handled by the "binary player copies or disagrees" argument of the elementary gadgets; its weight on $1$ and on $*$ must be tracked separately. The error constants $10$ and $81$ propagate through products of approximate quantities, so a proof that is loose at any step does not reach them.

On the Lean side, the expected payoff of a pure strategy is a sum over all pure profiles of a ten-player game; every claim first has to reduce it to the few coordinates the player's payoff actually depends on.

Formalization scope

Games, mixed profiles and expected payoffs are those of the published agt_games bundle: a finite player type, strategy types S i, payoffs u : ι → (∀ i, S i) → ℝ, AGT.IsMixedProfile, AGT.expectedPayoff. The expected payoff of a pure strategy $j$ is the expected payoff of the profile with $p$ 's strategy replaced by the point mass at $j$ . An $\epsilon$ -Nash equilibrium requires a genuine mixed profile.

Each gadget is one explicit game on its own player type, with the payoff tables of the paper. Binary strategies are Fin 2 with the paper's labels $0, 1$ , and $\mathbf p[v]$ is the weight on 1; $v_2'$ 's strategies are an inductive type {zero, one, star}. The input players' payoffs are unconstrained in the paper; here they are $0$ , which makes the $\epsilon$ -condition at the inputs vacuous. Since every non-input payoff depends only on gadget players, " $\epsilon$ -Nash equilibrium of the standalone gadget" quantifies over all mixed strategies of the inputs and imposes the condition exactly on the other players, which is the paper's meaning when the gadget sits inside a larger game. The affects graph is computed from the payoff functions, without self-loops, and colors $\{1,\dots,k\}$ are Fin k. The ranges $\alpha, \beta, \gamma \in \mathbb N$ (Proposition 4.18) and $\alpha, \beta, \gamma \in \mathbb R_{\ge 0}$ (Propositions 4.2, 4.3, 4.5) follow the paper; $\epsilon \ge 0$ is added where the paper writes only $\epsilon < 1$ .

The paper states Proposition 4.18 and Lemma 5.3 as "there is a graphical game"; an existential statement would be met by a game whose output has a dominant strategy and whose inputs are forced, so both are stated for the explicit game of the proof, with free inputs.

A complete development needs a computation lemma for the pure-strategy payoff in each gadget (reusable for any gadget on these definitions) and the case analyses of the claims. Proofs of the elementary gadgets, which are short, and of Claims 1 and 2 are good first contributions; Claim 3 is the main step.

Selected references

C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, The Complexity of Computing a Nash Equilibrium, SIAM J. Comput. 39(1):195–259, 2009. https://doi.org/10.1137/070699652
C. H. Papadimitriou, On the complexity of the parity argument and other inefficient proofs of existence, J. Comput. System Sci. 48(3):498–532, 1994. https://doi.org/10.1016/S0022-0000(05)80063-7
M. Kearns, M. L. Littman, S. Singh, Graphical Models for Game Theory, UAI 2001. https://arxiv.org/abs/1301.2281
X. Chen, X. Deng, S.-H. Teng, Settling the complexity of computing two-player Nash equilibria, J. ACM 56(3):14, 2009. https://doi.org/10.1145/1516512.1516516

15 thms3 active usersReviewed

Missions

Block Sensitivity vs. Sensitivity: Eight-layer exponent 2.0852.0852.085Open Problem

Motivation

Setting

Formalization target

Significance and current status

Difficulty

Formalization scope

Selected references

Multi-purchase Behavior: Modeling, Estimation, and Optimization: Revenue Maximization under the BundleMVL-2 Multi-Purchase Choice Model Is NP-CompleteResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Block Sensitivity vs. Sensitivity: Reach 2.075Open Problem

The quantitative sensitivity question

Boolean functions and sensitive changes

Target: exponent at least 2.075

What this entry establishes

The difficulty in improving the bound

Formalization scope and reusable foundations

Selected references and credits

Optimizing Quantum Optimization Algorithms via Faster Quantum Gradient Computation: an ε-Accurate Gradient of a Smooth Analytic Function from Õ(c√d/ε · log(d/δ)) Phase-Oracle QueriesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 25

Milestones

Significance

Difficulty

Formalization scope

Selected references

Block Sensitivity vs. Sensitivity: Reach 2.0635Open Problem

Block Sensitivity vs. Sensitivity: α ≥ 2.0391Open Problem

Block Sensitivity vs. Sensitivity: Reach 2.0205Open Problem

Block Sensitivity vs. Sensitivity: OpenAI BaselineResearch Paper

Integer Factorization: Why Two-Item Joint Replenishment Is Hard 4: For Primes p_i Near 2^(λa_i), ∏p_i Has a Divisor in [⌈L⌉, ⌊U⌋] iff the a_i Split into Two Equal-Sum PartsResearch Paper

Motivation

Setting

Formalization targets

Appendix reduction

Significance

Difficulty

Formalization scope

Selected references

Fast Integer Multiplication on Multitape Turing Machines: Schönhage–Strassen and the ToolkitResearch Paper

Motivation

Setting

Formalization targets

Goal: Schönhage–Strassen

Milestones

Formalization scope

Selected references

Settling the Complexity of Computing Approximate Two-Player Nash Equilibria: An (ε, δ)-WeakNash of a Bipartite Polymatrix Game Yields a (√ε(√ε + 5), δ)-Well-Supported WeakNashResearch Paper

Motivation

Setting

Formalization targets

Goal: Lemma 8.1

Milestones (proof of Lemma 8.1)

Significance

Difficulty

Formalization scope

Selected references

Convex Quadratic and Semidefinite Programming Relaxations in Scheduling V: 3-Occurrence Max3Sat L-Reduces to R | rⱼ | Σ Cⱼ with Constants 32 and 1Research Paper

Motivation

Setting

Formalization targets

Goal: the L-reduction inequalities (Lemma 7.1 b) and the proof of Theorem 7.2, p. 33)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An O(√nL)-Iteration Homogeneous and Self-Dual Linear Programming Algorithm 1: In O(√nL) Predictor-Corrector Iterations It Finds LP and Dual Optima or Detects InfeasibilityResearch Paper

Block Sensitivity vs. Sensitivity: Eight-layer exponent $2.085$ Open Problem