Complexity Theory

Motivation

A linear two-stage stochastic program chooses a first-stage decision $x$ before an uncertain parameter $\tilde\xi$ is revealed, and pays the optimal value $Q(x,\xi)$ of a second-stage linear program once the realization $\xi$ is known. Such programs are the basic model of planning under uncertainty in operations research, and their computational complexity determines which solution methods can be expected to work. In 2006, Dyer and Stougie argued that linear two-stage stochastic programs with fixed recourse are #P-hard even when the random data follow independent uniform distributions. Hanasusanto, Kuhn and Wiesemann showed that this proof is not correct and gave a corrected one, which also covers approximate evaluation to sufficiently high accuracy; their note also shows that, when the second-stage constraint matrix itself depends on $\xi$ (random recourse), even finding an approximately optimal decision is strongly NP-hard.

This mission formalizes that last result, Theorem 4 of the note. The previous missions of the series treat the hardness of evaluating the expected recourse with fixed and with random recourse.

Setting

The Integer Feasibility Problem. An instance is an integer matrix $A\in\mathbb Z^{m\times n}$ and an integer vector $b\in\mathbb Z^m$ such that the polytope $\{y\in\mathbb R^n:Ay\le b\}$ lies in the unit cube $[0,1]^n$. The question is whether some binary vector $y\in\{0,1\}^n$ satisfies $Ay\le b$. This problem is strongly NP-hard (Garey and Johnson).

The second-stage problem. For a decision $x\in\mathbb R$ and a realization $\xi\in[0,1]^n$, write $e$ for the all-ones vector and consider

$$\begin{aligned} Q(x,\xi)=\ \text{minimize}\ \ & e^\top y\\ \text{subject to}\ \ & y\in\mathbb R^n_+,\ \lambda\in\mathbb R^m_+,\ x\ge e^\top y,\\ & y_i\ge \xi_i+(b-A\xi)^\top\lambda,\quad y_i\ge(1-\xi_i)+(b-A\xi)^\top\lambda\qquad(i=1,\dots,n). \end{aligned}$$

The coefficient of $\lambda$ in each constraint depends on $\xi$, which is what makes the recourse random.

Problem (11). With $\tilde\xi$ uniformly distributed on $[0,1]^n$,

$$\text{minimize}\ \ x+\mathbb E\big[Q(x,\tilde\xi)\big]\quad\text{subject to}\ \ x\in\mathbb R .$$

The second stage is not feasible for every $x$ (the problem lacks relatively complete recourse), so a decision $x$ is feasible only if the second stage is feasible for every $\xi\in[0,1]^n$. Let $f^\star$ be the infimum of the objective over feasible decisions. A feasible $x$ is $\epsilon$-optimal if

$$\frac{\big|f^\star-\big(x+\mathbb E[Q(x,\tilde\xi)]\big)\big|}{\max\{|f^\star|,1\}}\le\epsilon .$$

The constant $\epsilon'$. Lemma 4 fixes $\epsilon'$ with $0\le\epsilon'<\tfrac12$ and $\epsilon'\sum_j|A_{ij}|<1$ for every row $i$.

Formalization targets

Goal: Theorem 4 as a reduction

For an instance with nonempty polytope, $n\ge1$, $\epsilon'$ as above, $0\le\epsilon<\epsilon'/(4n)$, and any $\epsilon$-optimal decision $x$ of (11),

$$\exists\,y\in\{0,1\}^n:\ Ay\le b\iff x>n-\frac{\epsilon'}{2}.$$

This is the mathematical content of "determining an $\epsilon$-optimal decision is strongly NP-hard whenever $\epsilon<\epsilon'/4n$": a single comparison of any approximate decision with a threshold answers the NP-hard question.

Milestones

1. Lemma 4. $Ay\le b$ has a binary solution iff it has a solution in $([0,\epsilon']\cup[1-\epsilon',1])^n$.
2. The second stage. If $A\xi\le b$, the second stage is feasible iff $\sum_i\max\{\xi_i,1-\xi_i\}\le x$, with value $\sum_i\max\{\xi_i,1-\xi_i\}$; otherwise it is feasible iff $x\ge0$, with value $0$. Optimal $y$ is unique in both cases.
3. The optimal decision. $x$ is feasible iff $x\ge x^\star$, and $x^\star$ is the unique optimal decision, where

$$x^\star=\max\Big\{\sum_{i=1}^n\max\{\xi_i,1-\xi_i\}:A\xi\le b\Big\}.$$

4. The dichotomy. The answer is affirmative iff $x^\star=n$, and negative iff $x^\star<n-\epsilon'$.
5. Accuracy of the decision. Every $\epsilon$-optimal $x$ satisfies $|x^\star-x|\le2n\epsilon$.

Significance

The result. Theorem 4 implies that, unless the problems in NP admit an efficient solution scheme, there is no fully polynomial-time approximation scheme for two-stage stochastic programs with random recourse, even with a one-dimensional first stage and a uniform distribution. Together with the #P-hardness results of the same note, it delimits what algorithms such as sample average approximation can guarantee once relatively complete recourse and fixed recourse are dropped.

Formalizing it. The theorem has a short published proof, but that proof leaves several conventions implicit: the index set of the constraint block, the meaning of first-stage feasibility, and the condition on $\epsilon'$ when $A$ has a zero row. A machine-checked version fixes each of them and verifies that the claimed formula for $x^\star$ is correct under the chosen reading. To our knowledge none of these statements has been formalized before. The objects are elementary (finite-dimensional linear programs, a set integral on the unit cube), and the second-stage solution and rounding lemma are reusable for related reductions from integer feasibility.

Difficulty

The individual steps are short; the difficulty is bookkeeping across three layers. The second stage is an optimisation over $(y,\lambda)$ whose feasibility depends on the sign pattern of $b-A\xi$; the first stage requires a supremum over a polytope to be attained (compactness), and the expected recourse to be the same integral for all feasible decisions (integrability of a piecewise-defined value function over the cube). The tempting shortcut, reading off feasibility from the value of $Q$, fails: an infeasible linear program has no meaningful value, and treating it as cost $0$ would make every decision look optimal. Similarly, an almost-sure notion of feasibility looks natural for a stochastic program but invalidates the formula for $x^\star$ whenever the polytope has measure zero, as it typically does for integer feasibility instances written with equalities.

Formalization scope

All objects live in SPHardness.IntFeas. Vectors are functions on Fin n and Fin m; $A$ and $b$ are integer and are cast to $\mathbb R$, and integrality is kept because Lemma 4 depends on it. The uniform law on $[0,1]^n$ is Lebesgue measure restricted to the cube (volume $1$); expectations are set integrals. The recourse value, $f^\star$ and $x^\star$ are sInf/sSup in $\mathbb R$, and second-stage feasibility, first-stage feasibility and $\epsilon$-optimality are separate predicates, so no statement depends on the junk value of an empty infimum.

Pinned readings and added conventions:

• The page writes the constraint block as "$\forall i=1,\dots,m$" and $x^\star$ with $\sum_{i=1}^m$, adding "$n=m=k$". Here the block ranges over $i=1,\dots,n$, $\xi\in[0,1]^n$, and $m$ (the number of rows of $A$) is arbitrary.
• First-stage feasibility is robust: feasible for every $\xi\in[0,1]^n$, not almost every $\xi$.
• $\epsilon'<\min_i\{(\sum_j|A_{ij}|)^{-1}\}$ is encoded as $\epsilon'\sum_j|A_{ij}|<1$ for every row, together with $0\le\epsilon'<\tfrac12$.
• Added hypotheses, all disclosed in the statements: the polytope $\{A\xi\le b\}$ is nonempty (the proof's own assumption), $n\ge1$, and $\epsilon\ge0$.

Strong NP-hardness, the FPTAS consequence, running times and encoding lengths are not formalized; the goal is the correctness of the reduction. A statement in which $x$ ranges over arbitrary reals satisfying a hypothesised identity, rather than over $\epsilon$-optimal decisions of the program (11) built from $(A,b)$, would be trivial and is ruled out: every object in the goal is defined from the instance.

Contributions welcome: proofs of the milestones, in particular measurability and integrability of the recourse function on the cube and attainment of $x^\star$, which are reusable for other piecewise-linear recourse functions.

Selected references

• G. A. Hanasusanto, D. Kuhn, W. Wiesemann, A comment on "computational complexity of stochastic programming problems", Mathematical Programming (2016); preprint Optimization Online 2015/03/4825 (version of October 6, 2015). https://optimization-online.org/wp-content/uploads/2015/03/4825.pdf, DOI https://doi.org/10.1007/s10107-015-0958-2
• M. Dyer, L. Stougie, Computational complexity of stochastic programming problems, Mathematical Programming 106 (2006) 423–432. https://doi.org/10.1007/s10107-005-0597-0
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, Springer, 1997 (2nd ed. 2011, https://doi.org/10.1007/978-1-4614-0237-4).

Motivation

A two-stage stochastic program chooses a decision before uncertainty is observed and a recourse decision afterward. Its objective can involve the expected optimal value of the recourse problem. Even with linear constraints, evaluating that expectation can be difficult when the random input has many coordinates. Dyer and Stougie's 2006 complexity paper studied this question for stochastic programming. Hanasusanto, Kuhn and Wiesemann identified a false volume identity in one fixed-recourse argument, then supplied a quantitative replacement in their 2015 preprint. The replacement shows that sufficiently accurate expected-recourse values determine an exact counting answer.

The distinction matters to researchers designing numerical methods for stochastic programs. A hardness statement at a specified absolute accuracy identifies the scale at which a general exact-information guarantee would have strong complexity consequences. It does not say that useful approximations at coarser accuracy are unavailable. The present mission records the mathematical reduction behind the paper's Theorem 1 and its quantitative tolerance.

Setting

Let $k\ge1$. A realization $\xi=(\xi_1,\ldots,\xi_k)$ lies in the unit cube $C=[0,1]^k$, equipped with Lebesgue measure. This cube has volume one, so integration over it is expectation under the uniform law. Let $\alpha\in\mathbb R^k_+$ be nonnegative weights and $\beta\ge0$ a budget. The second-stage value $Q(\xi;\alpha,\beta)$ is the maximum of

$$\sum_{j=1}^k\xi_jy_j-\beta z$$

over $0\le z\le1$ and $0\le y_j\le\alpha_jz$ for each $j$. Its expected recourse value is $\mathcal Q(\alpha,\beta)=\int_C Q(\xi;\alpha,\beta)\,d\xi$. There is no first-stage decision in this instance of the model.

The knapsack polytope is $P(\alpha,\beta)=\{\xi\in C:\sum_j\alpha_j\xi_j\le\beta\}$, and $V(\alpha,\beta)$ denotes its volume. For integer weights and budget, its binary points correspond to subsets $S\subseteq\{1,\ldots,k\}$ with $\sum_{j\in S}\alpha_j\le\beta$. The #Parity count $D$ is the number of such subsets of even size minus the number of odd size. The paper invokes the counting complexity of this problem from Dyer and Frieze's 1988 volume paper.

For $i=0,\ldots,k$, define $\gamma_i=\beta+i/(k+1)$ and a square matrix $F$ by $F_{ic}=\gamma_i^{k-c}$ for $c=0,\ldots,k$. The first column has power $k$ and the last has power zero. This order matters: the first coordinate of the coefficient vector is the parity count. The matrix inverse is controlled by a column-sum bound of the kind studied by Gautschi in 1962.

Formalization targets

Goal: recourse values determine the count

Write $\varepsilon_3(\alpha)=1/[2k!(\|\alpha\|_1+2)^k(k+1)^{k+1}\prod_j\alpha_j]$ and $\delta_7(\alpha)=[\alpha_k\varepsilon_3(\alpha)/(1+\alpha_k)]^2$, exactly the right sides of (3) and (7). For positive integer weights, $\beta\le\sum_j\alpha_j$, and $0<\delta<\delta_7(\alpha)$, take any oracle $Q_\delta(t)$ with $|Q_\delta(t)-\mathcal Q(\alpha,t)|\le\delta$ at every nonnegative $t$. Set $h=2\sqrt\delta$ and

$$\widetilde g_i=\frac{Q_\delta(\gamma_i+h)-Q_\delta(\gamma_i)}{h}+1.$$

The target is that every solution of

$$F\widetilde x=\left(k!\prod_{j=1}^k\alpha_j\right)\widetilde g$$

satisfies $|\widetilde x_0-D|<1/2$. Nearest-integer rounding therefore recovers $D$.

Supporting targets

The milestones establish the value formula for the second-stage program, the inclusion–exclusion volume formula (8), the integer coefficient identity for the exact volume system, the inverse bound (4), the perturbation bound (6), the derivative identity in Lemma 2, a global volume-growth bound, and the finite-difference estimate in Theorem 1. Together they retain the paper's constants and its sequence from expected values to volume approximations to an exact count. Proposition 1 separately records why the earlier proposed identity $1-\mathcal Q=V$ fails.

Significance

The result certifies a concrete information transfer. A function returning expected-recourse values to the stated absolute tolerance also contains enough information to distinguish the exact even-minus-odd count of feasible binary points. The bound states how accurate those values must be as dimension and weights change; a qualitative assertion of hardness alone would hide that dependence. The paper concludes #P-hardness after accounting for the polynomial-time operations of the reduction. That complexity-class conclusion is part of the paper, while the Lean goal isolates the reduction's numerical correctness.

A complete formalization would give separately reusable results about cube integrals, knapsack volumes, perturbations of Vandermonde systems, and finite differences of expected hinge functions. The source paper proves the mathematical assertions; this proposal stages their Lean statements as open proof obligations. No machine-checked proof is claimed here. The companion counterexample also keeps the corrected argument anchored to the precise error it repairs.

Difficulty

The tempting identity $1-\mathcal Q(\alpha,\beta)=V(\alpha,\beta)$ fails: the expectation of the second-stage optimum is a positive-part expectation, while volume is a distribution function. The paper's Proposition 1 makes the discrepancy explicit for all-ones weights. Recovering volume requires differentiation with respect to the budget, and an approximate function value does not directly provide an accurate derivative. The difficulty is controlling both oracle error and the change of volume over a finite budget interval tightly enough that the final coefficient error is strictly below one half.

There are further exactness points. The column order of $F$ fixes which coefficient equals $D$. The $1$-norm in (4) is the maximum column sum of the inverse, not a generic matrix norm. The perturbation threshold contains $k!$, every weight, and the power $(k+1)^{k+1}$; losing one factor can invalidate the rounding guarantee.

Formalization scope

Lean uses vectors $\mathrm{Fin}(k)\to\mathbb R$, with zero-based indices; the paper's $\alpha_k$ is the final coordinate. Lebesgue measure is restricted to $C$, whose volume is one. The LP value is a real supremum of its feasible objective values. For the nonnegative weights used in the theorems, the feasible set is nonempty and bounded, so this represents the actual maximum. The expected value is a real integral over the cube. The matrix $F$ has descending powers, and its $1$-norm estimate is written as a bound on each inverse column sum. Binary vectors are represented by subsets; $D$ keeps the paper's even-minus-odd convention.

Positive weights are required where (3) and (7) divide by their product, and $\delta>0$ where $h$ divides a finite difference. The case $\beta>\sum_j\alpha_j$ is excluded from the main target because the paper first answers it directly with $D=0$. Lemma 2 excludes $\alpha=0,\beta=0$, where the claimed derivative fails to exist. The volume-growth milestone gives the content of the paper's $\mathcal Q''\le1/\alpha_k$ argument without requiring a second derivative at a kink; it applies across the actual interval starting at $\beta$. The printed determinant sign is also adjusted to the descending columns by asserting nonsingularity, which is what the proof uses. The second-stage value milestone retains only the optimal value, because the optimal decisions the page calls unique need not be unique at ties. The mission must use the LP and counting definitions above; replacing them with an arbitrary function assumed to have the desired derivative would empty the reduction.

The formal work requires measure and integration theory, finite polytope volume, finite sums over subsets, matrix inverses, and real inequalities. Contributions proving the eight milestones and any honest supporting lemmas are welcome. The setup does not encode polynomial-time computability, bit lengths, or a #P complexity class, so closure of the Lean goal alone is not a formal proof of the full complexity statement.

Selected references

• G. A. Hanasusanto, D. Kuhn and W. Wiesemann, A comment on “computational complexity of stochastic programming problems”, Optimization Online preprint 2015/03/4825, version of October 6, 2015; published in Mathematical Programming, 2016. Preprint.
• M. Dyer and L. Stougie, Computational complexity of stochastic programming problems, Mathematical Programming 106 (2006), 423–432. DOI.
• M. E. Dyer and A. M. Frieze, On the complexity of computing the volume of a polyhedron, SIAM Journal on Computing 17 (1988), 967–974. DOI.
• W. Gautschi, On inverses of Vandermonde and confluent Vandermonde matrices, Numerische Mathematik 4 (1962), 117–123. Scan.

Motivation

A promise constraint satisfaction problem $\mathrm{PCSP}(\mathbf A,\mathbf B)$ asks to distinguish instances that are satisfiable in a structure $\mathbf A$ from instances that are not even satisfiable in a weaker structure $\mathbf B$. Approximate graph colouring (tell 3-colourable graphs from graphs that are not 5-colourable) and $(1\text{-in-}3\text{-SAT},\ \mathrm{NAE\text{-}SAT})$ are standard examples. The algebraic approach to CSPs explains the complexity of such problems through polymorphisms, the multi-argument maps $A^L\to B$ that preserve every relation.

Two polynomial-time relaxations dominate the algorithmic side: the Basic LP relaxation, solved over $\mathbb Q_{\ge0}$, and the affine relaxation, the same linear system solved over $\mathbb Z$. Barto, Bulín, Krokhin and Opršal (BBKO19) characterized each one separately: BLP solves $\mathrm{PCSP}(\mathbf A,\mathbf B)$ exactly when $\mathrm{Pol}(\mathbf A,\mathbf B)$ has symmetric polymorphisms of all arities, and the affine relaxation exactly when it has alternating polymorphisms of all odd arities. Brakensiek and Guruswami (BG19) used ad hoc combinations of the two. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383) combine them into a single algorithm, BLP+Affine, and characterize its power exactly. This mission formalizes that characterization, Theorem 4 of the paper.

Setting

A signature assigns to each symbol $R$ an arity $\mathrm{ar}(R)$. A relational structure $\mathbf A$ on a finite domain $A$ fixes relations $R^{\mathbf A}\subseteq A^{\mathrm{ar}(R)}$. A homomorphism $\mathbf A\to\mathbf B$ is a map $\sigma:A\to B$ sending every tuple of $R^{\mathbf A}$ into $R^{\mathbf B}$, and $(\mathbf A,\mathbf B)$ is a promise template if one exists. An instance $X$ has variables $x_1,\dots,x_n$ and constraints $(R_j,\bar x_j)$; it is satisfiable in $\mathbf C$ (written $X\to\mathbf C$) if some assignment sends each $\bar x_j$ into $R_j^{\mathbf C}$.

A map $f:A^L\to B$ is a polymorphism if applying $f$ column-wise to any $L\times\mathrm{ar}(R)$ matrix whose rows are in $R^{\mathbf A}$ gives a tuple of $R^{\mathbf B}$. It is block-symmetric for a partition $[L]=B_1\sqcup\dots\sqcup B_\kappa$ if it is invariant under permutations of its arguments that preserve every block, and its width is the largest minimum block size over such partitions.

The Basic LP $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has a probability distribution $w_i$ on $A$ for each variable and $p_j$ on $R_j^{\mathbf A}$ for each constraint, with the marginal of $p_j$ at each position of $\bar x_j$ equal to the distribution of the variable in that position. The affine relaxation $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ is the same system over $\mathbb Z$ with unknowns $r_i$, $q_j$ and no sign constraints. BLP+Affine (Figure 1) takes a relative interior point $(w,p)$ of the LP, keeps only the integer solutions $(r,q)$ that vanish wherever $(w,p)$ does, and accepts iff one remains. It correctly solves $\mathrm{PCSP}(\mathbf A,\mathbf B)$ if it accepts every $X\to\mathbf A$ and rejects every $X\not\to\mathbf B$.

The minor of $f:A^L\to B$ along $\pi:[L]\to[L']$ is $f_{/\pi}(x_1,\dots,x_{L'})=f(x_{\pi(1)},\dots,x_{\pi(L)})$. The minion $\mathcal M_{\mathrm{BLP+Aff}}$ has as $L$-ary objects the pairs $(w,r)$ with $w:[L]\to\mathbb Q_{\ge0}$, $r:[L]\to\mathbb Z$, both summing to $1$, and $w(i)=0\Rightarrow r(i)=0$; the minor along $\pi$ sums both over fibres of $\pi$. A minion homomorphism $\xi:\mathcal M_{\mathrm{BLP+Aff}}\to\mathrm{Pol}(\mathbf A,\mathbf B)$ sends $L$-ary objects to $L$-ary polymorphisms and commutes with minors. The free structure $F_{\mathcal M_{\mathrm{BLP+Aff}}}(\mathbf A)$ has the $|A|$-ary objects as its domain, and a tuple is in $R^F$ iff it is the family of coordinate minors of one $|R^{\mathbf A}|$-ary object.

Formalization targets

Goal: Theorem 4

For a promise template $(\mathbf A,\mathbf B)$ on finite domains, the following are equivalent:

$$\text{BLP+Affine correctly solves } \mathrm{PCSP}(\mathbf A,\mathbf B) \iff \forall N\ \exists f\in\mathrm{Pol}(\mathbf A,\mathbf B):\ \mathrm{width}(f)\ge N \iff \forall L\ \exists f\in\mathrm{Pol}^{(2L+1)}\ \text{symmetric on blocks of sizes } L,\ L+1.$$

Milestones

The paper proves Theorem 4 through Lemmas 7, 8 and 9. The milestones follow that proof:

• $\mathcal M_{\mathrm{BLP+Aff}}$ is a minion (p. 10);
• Lemma 8: a minion homomorphism $\mathcal M_{\mathrm{BLP+Aff}}\to\mathrm{Pol}(\mathbf A,\mathbf B)$ yields the $(2L+1)$-ary two-block polymorphisms;
• the finite-subset construction in the proof of Lemma 9: a symmetric polymorphism of arity $L^*\ge M\ell^2$, $L^*=u\ell+v$, gives a minion homomorphism on the finite set $\mathcal M_{\ell,M}$ by repeating coordinate $i$ exactly $W_i=u\ell w(i)+v r(i)$ times;
• Lemma 9: block-symmetric polymorphisms of arbitrarily high width yield a minion homomorphism;
• Observation 15, Lemma 16 (compactness for structures) and Lemma 17 (free structures versus minion homomorphisms, for $\mathcal M_{\mathrm{BLP+Aff}}$), which together give
• Lemma 7: BLP+Affine correctly solves $\mathrm{PCSP}(\mathbf A,\mathbf B)$ iff $\mathcal M_{\mathrm{BLP+Aff}}\to\mathrm{Pol}(\mathbf A,\mathbf B)$.

A companion item, Example 10, records that the disjoint union of a directed 2-cycle and a directed 3-cycle has no block-symmetric polymorphism of width at least $2$.

Significance

Theorem 4 is an exact criterion: the power of an algorithm is read off from the polymorphisms of the template. Its sufficiency direction (Theorem 3, the subject of the companion mission) says that one fixed algorithm decides every PCSP with block-symmetric polymorphisms of unbounded width, which covers nearly all tractable Boolean PCSPs known at the time, including those with threshold and alternating-threshold polymorphisms. The necessity direction, new in Theorem 4, gives a method for proving that BLP+Affine fails on a template: exhibit, for some $L$, the absence of a $(2L+1)$-ary polymorphism with blocks of sizes $L$ and $L+1$. Example 10 is an instance: a tractable template that the algorithm does not solve. The minion $\mathcal M_{\mathrm{BLP+Aff}}$ and its free structure are the template for later characterizations of relaxation hierarchies.

The result is proved in the paper. As far as is known it has not been machine-checked. A formalization adds a checked development of minions, minion homomorphisms and free structures for PCSPs, a compactness theorem for relational structures, and a checked version of the one-block argument whose many-block extension the paper only asserts.

Difficulty

The equivalence passes through three different kinds of object: an algorithm, an infinite algebraic object (a homomorphism defined on all of $\mathcal M_{\mathrm{BLP+Aff}}$), and finite families of polymorphisms. From polymorphisms one obtains homomorphisms only on finite pieces $\mathcal M_{\ell,M}$, each from a different polymorphism, and these do not agree with one another; a single homomorphism on the whole minion needs a compactness argument over the finitely many restrictions, which uses the finiteness of $A$ and $B$. The passage from "every instance satisfiable in the free structure is satisfiable in $\mathbf B$" to a homomorphism from the infinite free structure is a second compactness step. The relative interior point of Figure 1 must be kept: accepting whenever both relaxations are merely feasible is a different, weaker algorithm.

Formalization scope

All objects are in the definitions file PCSPBLPAff.Characterization.Setting, built on Mathlib only.

• Signatures are (τ : Type) (ar : τ → ℕ), with no finiteness of $\tau$; the paper's requirement that arities be positive is dropped, and no statement needs it. Domains are finite types; instance variables are Fin n and arities Fin L.
• The LP is over $\mathbb Q$ and the affine system over $\mathbb Z$. Constraint distributions are functions on all tuples that vanish outside $R^{\mathbf A}$, and marginal conditions are imposed per position of a constraint's scope.
• The relative interior point is encoded by the only property the algorithm uses: a solution whose zero coordinates are exactly those that vanish on the whole polytope. The algorithm is formalized by its acceptance condition; the polynomial-time claims are out of scope.
• Width requires at least one block, so a nullary function does not have every width.
• There is no abstract minion structure. A minion homomorphism $\mathcal M_{\mathrm{BLP+Aff}}\to\mathrm{Pol}(\mathbf A,\mathbf B)$ is spelled out as a family of maps from objects of each arity to polymorphisms of that arity, commuting with minors. Lemma 17 is stated for $\mathcal M=\mathcal M_{\mathrm{BLP+Aff}}$. Free-structure objects are indexed by $A$ and by tuples, identifying $A$ with $[|A|]$.
• Lemma 16 drops the hypothesis that $\mathbf F$ is infinite, which is unnecessary.

Two trivializing formalizations are ruled out: the acceptance condition keeps the maximal-support requirement, and the free structure's relation requires the witnessing pair to be an object of $\mathcal M_{\mathrm{BLP+Aff}}$ supported in $R^{\mathbf A}$.

A complete development needs finite sums over fibres, transport of objects along Fintype.equivFin, Tychonoff or König's lemma (Mathlib.Order.KonigLemma, Mathlib.Combinatorics.Compactness), and the existence of a maximal-support point of a rational polytope. The compactness theorem for relational structures and the free-structure lemma are reusable beyond this mission. Proofs of any milestone, and of the general Lemma 17 for an abstract minion, are welcome.

Selected references

• J. Brakensiek, V. Guruswami, M. Wrochna, S. Živný, The Power of the Combined Basic LP and Affine Relaxation for Promise CSPs, arXiv:1907.04383v3, 2020 (also SIAM J. Comput., 2020, https://doi.org/10.1137/20M1312745). https://arxiv.org/abs/1907.04383
• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic approach to promise constraint satisfaction, arXiv:1811.00970, 2019; J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970
• J. Brakensiek, V. Guruswami, An Algorithmic Blend of LPs and Ring Equations for Promise CSPs, SODA 2019, pp. 436–455. https://arxiv.org/abs/1807.05194
• R. Diestel, Graph Theory, 5th ed., Springer, 2016, Theorem 8.1.3 (de Bruijn–Erdős compactness). https://doi.org/10.1007/978-3-662-53622-3

Motivation

A constraint satisfaction problem (CSP) asks whether variables can be assigned values from a finite domain so that every constraint, drawn from a fixed list of allowed relations, is satisfied. A promise CSP (PCSP) relaxes the question: given two templates $\mathbf A$ and $\mathbf B$ with a homomorphism $\mathbf A\to\mathbf B$, distinguish instances satisfiable in $\mathbf A$ from instances not even satisfiable in the weaker $\mathbf B$. Approximate graph colouring (colour a graph with more colours than its chromatic number) is the standard example. For CSPs, the resolution of the Feder–Vardi dichotomy conjecture by Bulatov and Zhuk (FOCS 2017) ties tractability to the existence of polymorphisms satisfying non-trivial identities; for PCSPs no such dichotomy is known, and the question of which polymorphism families yield algorithms is open in general.

A polymorphism of a PCSP is a function $f:A^L\to B$ mapping tuples of rows satisfying the strict constraints to columns satisfying the weak ones. Brakensiek, Guruswami, Wrochna and Živný (arXiv:1907.04383v3, SIAM J. Comput. 2020) give a single algorithm, BLP+Affine, that decides every PCSP with infinitely many symmetric polymorphisms, and extend it to block-symmetric polymorphisms. As a corollary the same algorithm solves all tractable Boolean CSPs of Schaefer's dichotomy (2-SAT, Horn-SAT and its dual, linear equations mod 2).

Timeline, as recorded in the paper's introduction:

• 2012: Kun, O'Donnell, Tamaki, Yoshida and Zhou (ITCS 2012): with symmetric polymorphisms of all arities, the Basic LP alone decides the CSP; with only some arities (e.g. odd majorities) it does not.
• 2017: Austrin, Guruswami and Håstad classify $(2+\epsilon)$-SAT and introduce polymorphisms for PCSPs (SIAM J. Comput. 46(5), 2017).
• 2018–2019: Brakensiek and Guruswami study PCSPs through polymorphisms; their SODA 2019 algorithm (arXiv:1807.05194) solves the search version for PCSPs with structured symmetric polymorphisms (threshold, threshold-periodic, regional), combining an LP over $\mathbb Z[\sqrt2]$ with an affine relaxation over a finite ring.
• 2019: Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970) show that the identities satisfied by polymorphisms, captured by minion homomorphisms, determine the complexity of a PCSP.
• 2019–2020: the present paper. Theorem 2 needs only that $f$ be symmetric, with no structure beyond that; Theorem 3 handles any number of blocks; Theorem 4 characterizes exactly the PCSPs that BLP+Affine solves.

Setting

A signature $\tau$ is a set of symbols $R$ with arities $\mathrm{ar}(R)$. A relational structure $\mathbf A$ on a finite domain $A$ gives, for each $R$, a relation $R^{\mathbf A}\subseteq A^{\mathrm{ar}(R)}$. A homomorphism $\mathbf A\to\mathbf B$ is a map $\sigma:A\to B$ sending every tuple of $R^{\mathbf A}$, componentwise, into $R^{\mathbf B}$; $(\mathbf A,\mathbf B)$ is a promise template when one exists.

An instance $X$ has variables $x_1,\dots,x_n$ and constraints $c_j=(R_j,\bar x_j)$, $j\in[m]$, where $\bar x_j$ is a tuple of $\mathrm{ar}(R_j)$ variables. $X$ is satisfiable in $\mathbf A$ if some assignment sends every $\bar x_j$ into $R_j^{\mathbf A}$.

A polymorphism of $(\mathbf A,\mathbf B)$ of arity $L$ is $f:A^L\to B$ such that for every $R$ and every $L\times\mathrm{ar}(R)$ matrix whose rows lie in $R^{\mathbf A}$, applying $f$ to each column gives a tuple in $R^{\mathbf B}$. It is symmetric if it is invariant under all permutations of its $L$ arguments.

The Basic LP $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has rational unknowns $w_i(a)\ge0$, a distribution on $A$ for each variable, and $p_j(y)\ge0$, a distribution on $R_j^{\mathbf A}$ for each constraint, linked by the marginal conditions $\sum_{y:\,y_k=a}p_j(y)=w_i(a)$ when $x_i$ is the $k$-th variable of $\bar x_j$. The affine relaxation $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ is the same system of equations in integer unknowns $r_i(a)$, $q_j(y)$, with no sign constraints.

The BLP+Affine algorithm (Figure 1) finds a relative interior point $(w,p)$ of $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$, rejecting if there is none; restricts the affine system to $\mathrm{Aff}'_{\mathbb Z}(X,\mathbf A)$ by forcing $r_i(a)=0$ wherever $w_i(a)=0$ and $q_j(y)=0$ wherever $p_j(y)=0$; and accepts if and only if the restricted system has an integer solution. It correctly solves $\mathrm{PCSP\text{-}Decision}(\mathbf A,\mathbf B)$ (Definition 1) if it accepts every instance satisfiable in $\mathbf A$ and rejects every instance unsatisfiable in $\mathbf B$.

Formalization targets

Goal: Theorem 2 (p. 6)

$$\Bigl(\forall N\ \exists L\ge N\ \exists f:A^L\to B \text{ symmetric polymorphism of } (\mathbf A,\mathbf B)\Bigr)\ \Longrightarrow\ \text{BLP+Affine correctly solves } \mathrm{PCSP\text{-}Decision}(\mathbf A,\mathbf B).$$

The hypothesis is a property of the template alone; the conclusion quantifies over all instances.

Milestones, in attack order

1. Footnote 1 (p. 5): a feasible $\mathrm{LP}_{\mathbb Q}(X,\mathbf A)$ has a solution of maximal support.
2. Completeness (p. 6): an instance satisfiable in $\mathbf A$ is accepted.
3. Rounding of variables (pp. 6–7): $W_i(a)=u\ell w_i(a)+v r_i(a)$ are non-negative integers with $\sum_a W_i(a)=L$, for $L=u\ell+v\ge M\ell^2$, $0\le v<\ell$.
4. Rounding of constraints (p. 7): $P_j(y)=u\ell p_j(y)+v q_j(y)$ are non-negative integers with $\sum_y P_j(y)=L$.
5. Eq. (9) (p. 7): $W_i(a)=\sum_{y:\,y|i=a}P_j(y)$.
6. Satisfying assignment (p. 7): $X_i:=f(a,\dots,a\ [W_i(a)\text{ times}])$ satisfies $X$ in $\mathbf B$.

Companion: Theorem 3 (p. 8)

The same conclusion when $\mathrm{Pol}(\mathbf A,\mathbf B)$ contains block-symmetric polymorphisms of arbitrarily large width: $[L]$ is split into blocks, each of size at least $N$, within which $f$ is invariant.

Significance

Theorem 2 gives one algorithm that decides every PCSP with an infinite family of symmetric polymorphisms, without knowing or evaluating the polymorphisms; it subsumes the BLP-then-AIP algorithm of Brakensiek and Guruswami for Boolean templates and applies over any finite domain. Theorem 3 extends this to block-symmetric families, which covers nearly all known tractable Boolean PCSPs, including 1-in-3-SAT versus NAE-SAT, whose alternating threshold polymorphisms are block-symmetric but not symmetric.

The results are proved in the paper. No machine-checked formalization of PCSPs, polymorphisms or the Basic LP is known to exist; Mathlib has no theory of constraint satisfaction. This mission produces a formal model of promise templates, instances, polymorphisms, the two relaxations and the algorithm's acceptance condition, together with a formal proof of the correctness theorem. The same model is the starting point for the characterization theorem (Theorem 4) treated in the companion mission.

Difficulty

Completeness is routine. Soundness is the substance: from a rational LP solution and an integer solution of the refined affine system one must produce an actual assignment in $\mathbf B$, using a polymorphism whose arity is chosen only after the instance is known. The natural first idea, clearing denominators of the LP solution and feeding the resulting multiplicities to a polymorphism, needs a polymorphism of exactly the arity the denominators dictate; with polymorphisms of only some arities it fails, and the paper's introduction notes that the LP alone does not suffice there. An integer affine solution, on the other hand, may have negative entries, which are not multiplicities. The paper stresses that the affine system must be the one refined by the support of a relative interior point: an arbitrary solution of the unrefined lattice gives no control on where the negative entries sit. In the formalization, the counting step (the columns of the matrix built from the constraint multiplicities have the variable multiplicities) and the passage from equal multiplicities to equal values of a symmetric function require explicit combinatorics on finite tuples, and the existence of a maximal-support LP solution requires an averaging argument over the finite set of coordinates.

Formalization scope

All declarations are in the namespace PCSPBLPAff.Symmetric. Conventions:

• Domains are Lean types with Fintype and DecidableEq; variables are Fin n, constraints Fin m, and a constraint's scope is a function Fin (ar R_j) → Fin n, possibly repeating variables.
• Arities are any natural numbers (the page asks for positive arities; every statement remains true for arity 0).
• The LP is over $\mathbb Q$ and the affine system over $\mathbb Z$. The weights $p_j$, $q_j$ are total functions on $A^{\mathrm{ar}(R_j)}$ required to vanish off $R_j^{\mathbf A}$.
• The marginal conditions (5) and (8) are imposed per position of the scope.
• The relative interior point is encoded by its only property the algorithm uses (footnote 1): a solution whose support contains the support of every solution. Acceptance requires such a solution and an affine solution vanishing outside its support.
• A block-symmetric function of width at least $N$ has at least one block, each block of size at least $N$.
• The polynomial-time claims of the paper, and the Remark on $\mathbb Z[\sqrt2]$, are out of scope: the algorithm is formalized by its acceptance condition.

The acceptance condition must not be replaced by "the LP is feasible and $\mathrm{Aff}_{\mathbb Z}(X,\mathbf A)$ has a solution", nor by an affine solution vanishing outside the support of an arbitrary LP solution; the first is a different algorithm and the second bypasses footnote 1.

Contributions welcome: proofs of the milestones, in particular the combinatorial lemma that a symmetric function takes the same value on tuples with the same multiplicities, and the averaging argument for maximal-support solutions; the block-wise version for Theorem 3.

Selected references

• J. Brakensiek, V. Guruswami, M. Wrochna, S. Živný, The Power of the Combined Basic Linear Programming and Affine Relaxation for Promise Constraint Satisfaction Problems, SIAM J. Comput. 49(6), 2020; arXiv:1907.04383v3. https://arxiv.org/abs/1907.04383v3
• J. Brakensiek, V. Guruswami, An Algorithmic Blend of LPs and Ring Equations for Promise CSPs, SODA 2019. https://arxiv.org/abs/1807.05194
• J. Brakensiek, V. Guruswami, Promise Constraint Satisfaction: Structure Theory and a Symmetric Boolean Dichotomy, SODA 2018. https://arxiv.org/abs/1704.01937
• L. Barto, J. Bulín, A. Krokhin, J. Opršal, Algebraic Approach to Promise Constraint Satisfaction, J. ACM 68(4), 2021. https://arxiv.org/abs/1811.00970

Motivation

For a real symmetric matrix, the largest eigenvalue is the maximum of the quadratic form $\mathbf x^\top A\mathbf x$ on the unit sphere, and it is computable to any accuracy in polynomial time. Tensor eigenvalues, introduced independently by Lim (2005) and Qi (2005), extend this picture to higher order: they are the stationary values of the cubic form $\mathcal A(\mathbf x,\mathbf x,\mathbf x)$ on the unit sphere. They appear in multilinear statistics, signal processing, hypergraph theory and polynomial optimization, and for these applications the symmetric case is the natural one.

Hillar and Lim, in Most Tensor Problems Are NP-Hard (J. ACM 2013), show that the eigenvalue problem stays NP-hard when the tensor is required to be symmetric (their Theorem 9.3). The proof is short once one ingredient is available: a theorem of Nesterov (2003), in a form corrected by Hillar and Lim, that expresses the stability number of a graph as the maximum of an explicit cubic polynomial over a sphere. This mission formalizes that chain.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$. A set of vertices is stable if no two of its members are adjacent; the stability number $\alpha(G)$ is the size of a largest stable set, so $1\le\alpha(G)\le v$.

Put $n=v+v(v-1)/2$ and write a vector of $\mathbb R^n$ as $\mathbf z=(\mathbf x,\mathbf y)$, with $\mathbf x=(x_1,\dots,x_v)$ indexed by vertices and $\mathbf y=(y_{ij})_{i<j}$ indexed by pairs of vertices. The tensor $\mathcal S_G=[\![s_{abc}]\!]\in\mathbb R^{n\times n\times n}$ has entry $1$ at the six orderings of the triple of coordinates $(x_i,x_j,y_{ij})$ for every non-adjacent pair $i<j$, and $0$ elsewhere. It is symmetric: its entries do not change under any permutation of the three indices.

For a real 3-tensor $\mathcal A=[\![a_{abc}]\!]$ the cubic form is $\mathcal A(\mathbf z,\mathbf z,\mathbf z)=\sum_{a,b,c}a_{abc}z_az_bz_c$, and a real $\lambda$ is a unit $\ell^2$-eigenvalue of $\mathcal A$ if

$$\sum_{a,b}a_{abc}z_az_b=\lambda z_c\quad\text{for all }c,\qquad\text{for some }\mathbf z\text{ with }\|\mathbf z\|_2=1 .$$

Finally, $\lambda_l=2\sqrt{\tfrac23\left(1-\tfrac1l\right)}$ for $l\ge1$. In Lean these are TensorNP.SymEigen.stabTensor, cubicForm, IsUnitL2Eigenvalue and lambdaL, and $\alpha(G)$ is Mathlib's SimpleGraph.indepNum.

Formalization targets

Goal: Theorem 9.3, core

$$\alpha(G)=\max\{\,l\in\{1,\dots,v\}:\ \lambda_l\text{ is a unit }\ell^2\text{-eigenvalue of }\mathcal S_G\,\}.$$

That is, $\lambda_{\alpha(G)}$ is an eigenvalue of $\mathcal S_G$, and no $\lambda_l$ with $\alpha(G)<l\le v$ is. This is the statement on which the paper's $v$-query reduction rests; nothing is claimed about $l<\alpha(G)$.

Milestones, in the paper's order

1. Theorem 9.2 (Nesterov). With $\mathbb S^{n-1}=\{(\mathbf x,\mathbf y):\|\mathbf x\|_2^2+\|\mathbf y\|_2^2=1\}$,

$$\sqrt{1-\frac1{\alpha(G)}}=3\sqrt{\frac32}\cdot\max_{(\mathbf x,\mathbf y)\in\mathbb S^{n-1}}\ \sum_{i<j,\ \{i,j\}\notin E}x_ix_jy_{ij}.$$

2. The tensor. $\mathcal S_G$ is symmetric and $\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=6\sum_{i<j,\{i,j\}\notin E}x_ix_jy_{ij}$.
3. The maximum is an eigenvalue. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)$ is attained and is a unit $\ell^2$-eigenvalue of $\mathcal S_G$.
4. Its value. $\max_{\|\mathbf z\|_2=1}\mathcal S_G(\mathbf z,\mathbf z,\mathbf z)=\lambda_{\alpha(G)}$.
5. Further result: Theorem 6.9 (Banach), (23). For every symmetric $\mathcal S\in\mathbb R^{n\times n\times n}$,

$$\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}=\sup_{\mathbf x\ne\mathbf 0}\frac{|\mathcal S(\mathbf x,\mathbf x,\mathbf x)|}{\|\mathbf x\|_2^3},$$

both sides finite. The paper uses it in §10 to transfer Theorem 9.3 to the spectral norm and the best rank-one approximation of symmetric tensors.

Significance

The result. Theorem 9.3 places symmetric tensor eigenvalue among the NP-hard problems of Hillar and Lim's Table I, and through Banach's theorem (Theorem 10.2 of the paper) the same holds for the largest singular value, the spectral norm and the best rank-one approximation of a symmetric 3-tensor. These are the quantities computed by higher-order power methods and by moment-based estimators, so the result marks where the matrix theory stops transferring.

Formalizing it. All results here are proved in the literature; none is machine-checked. Nesterov's theorem, which rests on the Motzkin–Straus theorem for the complement graph, is not on the platform or in Mathlib, and its formal statement settles the constant that the original paper got wrong by a factor $1/\sqrt2$ (Hillar–Lim, footnote 12). Banach's theorem on symmetric multilinear forms is likewise absent from Mathlib and is useful well beyond this mission.

Difficulty

The tensor identity (milestone 2) is bookkeeping. The analytic content sits in two places. First, Nesterov's theorem: the obvious route, fixing $\mathbf x$ and maximizing over $\mathbf y$ by Cauchy–Schwarz, reduces the cubic problem to a quartic one in $\mathbf x$, whose value still has to be identified with $\alpha(G)$; that identification is the Motzkin–Straus theorem, which is not available in Lean and is itself a nontrivial optimization over the simplex. Second, the passage from a maximum to an eigenvalue needs a Lagrange multiplier argument on the sphere, and the symmetry of $\mathcal S_G$ is what makes the gradient of the cubic form match the eigen-equation. Part (b) of the goal needs a further, unprinted observation relating every unit eigenpair to the cubic form. Banach's theorem has no short proof; the classical arguments go through polarization estimates or a variational argument specific to symmetric forms.

Formalization scope

• Tensors and indices. A 3-tensor is a function ι → ι → ι → ℝ on a finite index type. For $\mathcal S_G$ the index type is the disjoint union of the vertices Fin v and the pairs $\{(i,j): i<j\}$; this is $\mathbb R^n$ with coordinates labelled by name instead of by the paper's enumeration $\varphi(i,j)=(i-1)v-i(i-1)/2+j-i$. Vertices are $0,\dots,v-1$.
• Normalization. Eigenvalues are taken with a unit eigenvector. The paper's Problem 9.1 and Definition 5.1 say only $\mathbf x\ne\mathbf 0$; since $(\lambda,\mathbf x)\mapsto(t\lambda,t\mathbf x)$ preserves the eigen-equation, that reading would make every nonzero real an eigenvalue of $\mathcal S_G$ and the goal false. The unit sphere (13) is where the paper derives the notion.
• Explicit readings. The paper's index range "$1\le i<j<k\le v$" in the definition of $s_{ijk}$ is read as $k\le n$ (taken literally it gives $\mathcal S_G=0$). Every "max" is stated as a greatest element, so attainment is claimed. In (23) the suprema are real suprema over nonzero vectors with boundedness part of the conclusion. $v\ge1$ is assumed wherever the paper uses $\alpha(G)\in\{1,\dots,v\}$.
• Not formalized. The oracle procedure of the proof of Theorem 9.3, the polynomial size of $\mathcal S_G$, the input model of Problem 9.1 with quadratic irrationalities (Remark 9.4), and the NP-completeness of the stability number (Karp 1972, via $\alpha(G)=\omega(\overline G)$). The goal is the mathematical core of the Turing reduction, not a complexity statement.
• Trivializations ruled out. Without the unit normalization the eigenvalue statements are trivial or false; a goal stating only (a), or only an inequality between the maximum and $\lambda_{\alpha(G)}$, would not determine $\alpha(G)$; both are excluded by the statements above.
• Infrastructure. Everything rests on Mathlib (SimpleGraph.indepNum, real analysis on finite-dimensional spaces, Lagrange multipliers). A Motzkin–Straus theorem for SimpleGraph and Banach's theorem for symmetric trilinear forms are both reusable beyond this mission; contributions of either, or of a general "maximum of a symmetric cubic form on the sphere is an eigenvalue" lemma, are welcome.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, Journal of the ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (arXiv:0911.1393v5: https://arxiv.org/abs/0911.1393)
• Yu. Nesterov, Random walk in a simplex and quadratic optimization over convex polytopes, CORE Discussion Paper 2003/71, 2003. http://edoc.bib.ucl.ac.be:83/archive/00000238/01/dp2003-71.pdf
• E. de Klerk, The complexity of optimizing over a simplex, hypercube or sphere: a short survey, Central European Journal of Operations Research 16, 111–125, 2008. https://doi.org/10.1007/s10100-007-0052-9
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian Journal of Mathematics 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in ($L^2$), Studia Mathematica 7(1), 36–44, 1938 (reference [Banach 1938] of Hillar–Lim).
• L.-H. Lim, Singular values and eigenvalues of tensors: a variational approach, Proc. IEEE CAMSAP 1, 129–132, 2005. https://arxiv.org/abs/math/0607648
• L. Qi, Eigenvalues of a real supersymmetric tensor, Journal of Symbolic Computation 40, 1302–1324, 2005. https://doi.org/10.1016/j.jsc.2005.05.007
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

The spectral norm of a matrix, its largest singular value, is computable in polynomial time to any accuracy. Its analogue for 3-tensors appears in the analysis of multilinear systems, in the best rank-1 approximation of a data array, in quantum information (the geometric measure of entanglement), and in the injective norm of tensor products. Hillar and Lim, Most Tensor Problems Are NP-Hard (J. ACM 60(6), 2013, Article 45; final version arXiv:0911.1393v5), show that, in contrast with matrices, deciding whether a fixed nonzero rational number is a singular value or the spectral norm of a rational 3-tensor is NP-hard (their Theorems 6.5 and 1.10).

The proof is a reduction from the clique number $\omega(G)$ of a graph. It combines three classical ingredients: the theorem of Motzkin and Straus (1965), which expresses $\omega(G)$ as the value of a quadratic program over the simplex; a theorem of Banach (1938) on the spectral norm of symmetric tensors; and an observation from He, Li and Zhang (2010) on maxima of sums of squared bilinear forms. Deciding $\omega(G)\ge l$ is one of Karp's (1972) NP-complete problems.

Setting

A real 3-tensor is an array $\mathcal A=[\![a_{ijk}]\!]\in\mathbb R^{l\times m\times n}$ with trilinear form $\mathcal A(\mathbf x,\mathbf y,\mathbf z)=\sum_{i,j,k}a_{ijk}x_iy_jz_k$. With the Euclidean norm $\|\cdot\|_2$, its spectral norm is

$$\|\mathcal A\|_{2,2,2}=\sup_{\mathbf x,\mathbf y,\mathbf z\ne\mathbf 0}\frac{|\mathcal A(\mathbf x,\mathbf y,\mathbf z)|}{\|\mathbf x\|_2\|\mathbf y\|_2\|\mathbf z\|_2}.$$

A real $\sigma$ is a unit $\ell^2$-singular value of $\mathcal A$ if there are unit vectors $\mathbf u,\mathbf v,\mathbf w$ with

$$\textstyle\sum_{j,k}a_{ijk}v_jw_k=\sigma u_i,\quad \sum_{i,k}a_{ijk}u_iw_k=\sigma v_j,\quad \sum_{i,j}a_{ijk}u_iv_j=\sigma w_k$$

for all $i,j,k$: the stationarity conditions of $\mathcal A(\mathbf u,\mathbf v,\mathbf w)$ on a product of unit spheres.

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,v\}$, $v\ge1$, with $e$ edges $\{i_k,j_k\}$, $k=1,\dots,e$, and clique number $\omega$. Let $\Delta_v$ be the standard simplex, $A_G$ the adjacency matrix and $J$ the all-ones matrix. For a positive integer $l$ set $Q_l=A_G+\frac1lJ$ and $M_l=\max_{\mathbf x\in\Delta_v}\mathbf x^\top Q_l\mathbf x$. Let $E_k=\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$, and let $T_l$ be the maximum over unit $\mathbf u,\mathbf v\in\mathbb R^v$, $\mathbf w\in\mathbb R^{l+2e}$ of the multilinear form

$$\sum_{i=1}^l\Big(\mathbf u^\top\tfrac1lI\mathbf v\Big)w_i+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{l+k}+\sum_{k=1}^e(\mathbf u^\top E_k\mathbf v)w_{e+l+k}. \tag{26}$$

The graph tensor $\mathcal A_l\in\mathbb Q^{v\times v\times(l+2e)}$ has as entry $a_{ijk}$ the coefficient of $u_iv_jw_k$ in (26).

Formalization targets

Goal: Theorems 6.5 and 1.10, encoding-free core

For every graph $G$ on $v\ge1$ vertices and every enumeration of its edges:

$$\forall l\ge1:\ \|\mathcal A_l\|_{2,2,2}=1\iff l=\omega;\qquad 1\text{ is a unit singular value of }\mathcal A_\omega;\qquad \forall l>\omega:\ 1\text{ is not one of }\mathcal A_l,$$

so $\omega$ is the largest $l\in\{1,\dots,v\}$ for which $1$ is a unit singular value of $\mathcal A_l$. The paper's $v$-query Turing reductions rest on exactly this.

Milestones (in attack order)

1. Theorem 6.7 (Motzkin–Straus): $1-1/\omega=2\max_{\mathbf x\in\Delta_v}\sum_{\{i,j\}\in E}x_ix_j$.
2. (22): $M_l=1+\frac{\omega-l}{l\omega}$; so $M_\omega=1$, $M_l>1$ for $l<\omega$, $M_l<1$ for $l>\omega$.
3. Lemma 6.8: $M_l=N_l$, where $N_l=\max_{\|\mathbf u\|_2=1}\{\sum_{i=1}^l(\mathbf u^\top\frac1lI\mathbf u)^2+2\sum_k(\mathbf u^\top E_k\mathbf u)^2\}$.
4. Theorem 6.9 (Banach), (24): for a symmetric 4-tensor, $\|\mathcal S\|_{2,2,2,2}=\sup_{\mathbf x\neq\mathbf 0}|\mathcal S(\mathbf x,\mathbf x,\mathbf x,\mathbf x)|/\|\mathbf x\|_2^4$.
5. Proposition 6.10 (He–Li–Zhang): for symmetric $A_k$, $\max_{\|\mathbf u\|=\|\mathbf v\|=1}\sum_k(\mathbf u^\top A_k\mathbf v)^2=\max_{\|\mathbf v\|=1}\sum_k(\mathbf v^\top A_k\mathbf v)^2$.
6. Lemma 6.11: $T_l=M_l^{1/2}$, hence $T_l=1$ iff $l=\omega$, $T_l>1$ iff $l<\omega$, $T_l<1$ iff $l>\omega$.
7. Proof of Theorem 6.5: $\|\mathcal A_l\|_{2,2,2}=T_l$, $T_l$ is a unit singular value of $\mathcal A_l$, and every unit singular value has absolute value at most $T_l$.
8. §7 (content of Theorem 1.13): $\min_{\sigma\ge0,\ \text{unit }\mathbf u,\mathbf v,\mathbf w}\|\mathcal A-\sigma\,\mathbf u\otimes\mathbf v\otimes\mathbf w\|_F^2=\|\mathcal A\|_F^2-\|\mathcal A\|_{2,2,2}^2$, attained only with $\sigma=\|\mathcal A\|_{2,2,2}$.

Significance

The result. The goal shows that a single comparison with $1$ of the spectral norm, or of the singular-value spectrum, of an explicit rational tensor of size $v\times v\times(l+2e)$ encodes whether $l=\omega(G)$. It is the step that makes the spectral norm, the largest singular value, and (through §7) the best rank-1 approximation of a 3-tensor NP-hard, whereas all three are polynomial-time for matrices. It explains why the higher-order power method and its relatives carry no global guarantees, and it is the starting point for inapproximability results such as the paper's Theorem 1.11.

Formalizing it. The results are proved on paper; none of them is formalized. Motzkin–Straus, Banach's polarization theorem for symmetric 4-tensors, and the He–Li–Zhang identity are classical results that are not in Mathlib and not on the platform; each is reusable well beyond this mission (Turán-type bounds, polynomial optimization over spheres, injective norms). The mission also checks the paper's construction at the level of indices and constants.

Difficulty

The construction of $\mathcal A_l$ is explicit, and the comparison with $1$ is arithmetic once $T_l=M_l^{1/2}$ is known. Everything rests on the three cited theorems. Motzkin–Straus is an optimization statement over the simplex whose maximizers may lie on the boundary and need not be unique, so a first-order computation at an interior critical point does not settle it. Banach's theorem asserts equality, not equality up to a constant: the standard polarization identity bounds the 4-linear form by its diagonal values only up to a factor. Proposition 6.10 is where the paper's own argument is loose: the 4-linear form it introduces is not symmetric, so (24) does not apply as printed. Finally, the singular-value clauses require that the maximum of a trilinear form on a product of spheres is a stationary value. This must be proved, not assumed.

Formalization scope

Tensors are arrays Fin l → Fin m → Fin n → ℝ with 0-based indices: the paper's $a_{ijk}$ is A (i-1) (j-1) (k-1). The Euclidean norm is Real.sqrt (∑ i, x i ^ 2). Suprema and maxima are sSup of sets that are nonempty and bounded under the stated hypotheses; where the paper's "max" carries content (Motzkin–Straus, (22), §7), attainment is stated with IsGreatest/IsLeast. The graph is a SimpleGraph (Fin v) with $v\ge1$, clique number Mathlib's SimpleGraph.cliqueNum, and its edges are enumerated by an arbitrary Fin e ≃ G.edgeSet. Every statement holds for each enumeration, so the tensor depends on the choice and the conclusions do not. $\mathcal A_l$ is a rational tensor, read over $\mathbb R$ by casting.

Explicit readings of the paper:

• Definition 6.1 has no norm constraint. Since $(\sigma,\mathbf u,\mathbf v,\mathbf w)\mapsto(t\sigma,t\mathbf u,t\mathbf v,t\mathbf w)$ preserves (20), unnormalized singular values make every nonzero real a singular value of $\mathcal A_l$, so the clause "not for $l>\omega$" would be false. Singular vectors are therefore unit vectors, as in the paper's derivation on p. 0:21.
• The statement of Lemma 6.11 prints $w_{m+l+k}$. There is no $m$ in §6, and the proof uses $w_{e+l+k}$, which is formalized.
• $E_k$ is written entrywise as $\frac12[\{i,j\}=\{i_k,j_k\}]$, which equals $\frac12E_{i_kj_k}+\frac12E_{j_ki_k}$ for a loopless edge.
• "$T_l$ is just the maximum $\ell^2$-singular value of $\mathcal A_l$" is made explicit as milestone 7.
• The goal does not claim that $1$ fails to be a singular value of $\mathcal A_l$ for $l<\omega$; the paper neither claims nor uses this.

This is the mathematical core of a polynomial-time Turing reduction, not an NP-hardness theorem. The polynomial size of $\mathcal A_l$, the $v$-query procedure, the scaling to a general fixed $0\ne\sigma\in\mathbb Q$, and the NP-completeness of CLIQUE (Karp 1972, cited) are not formalized. Theorem 1.11 and Corollary 1.12 are out of scope.

Two formalizations would make the goal trivial, and both are excluded. One is dropping the unit-norm constraint, which makes every nonzero number a singular value. The other is a spectral norm taken as a supremum over all vectors without normalization, which makes it unbounded and junk-valued; here the quotients are normalized.

Contributions are welcome on each milestone. Motzkin–Straus, Banach (24) and He–Li–Zhang are self-contained and reusable. Lemma 6.11 and milestone 7 need Cauchy–Schwarz and a Lagrange-type stationarity argument on spheres, which Mathlib supports through IsLocalExtrOn and the Lagrange multiplier files.

Selected references

• C. J. Hillar, L.-H. Lim, Most Tensor Problems Are NP-Hard, J. ACM 60(6), Article 45, 2013. https://doi.org/10.1145/2512329 (final version arXiv:0911.1393v5, https://arxiv.org/abs/0911.1393v5)
• T. S. Motzkin, E. G. Straus, Maxima for graphs and a new proof of a theorem of Turán, Canadian J. Math. 17, 533–540, 1965. https://doi.org/10.4153/CJM-1965-053-6
• S. Banach, Über homogene Polynome in (L²), Studia Math. 7, 36–44, 1938. https://doi.org/10.4064/sm-7-1-36-44
• S. He, Z. Li, S. Zhang, Approximation algorithms for homogeneous polynomial optimization with quadratic constraints, Math. Program. Ser. B 125(2), 353–383, 2010. https://doi.org/10.1007/s10107-010-0409-z
• R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9

Motivation

In distributed computing, many graph problems (minimum spanning tree, shortest paths, connectivity checks) are solved by processors that sit at the vertices of the input network and communicate only along its edges. When every edge can carry only a few bits per round, the number of rounds an algorithm needs can be far larger than the network's diameter. Understanding by how much is the central question of the CONGEST (here: B) model of Peleg's monograph Distributed Computing: A Locality-Sensitive Approach (SIAM, 2000).

Das Sarma, Holzer, Kor, Korman, Nanongkai, Pandurangan, Peleg and Wattenhofer (SIAM J. Comput. 41 (2012) 1235–1265) proved round lower bounds for a long list of verification problems (is a given subgraph a spanning tree, a cut, a Hamiltonian cycle, …) and for approximating optimization problems such as the minimum spanning tree and shortest paths. Every one of those bounds goes through a single reduction, the Simulation Theorem (Theorem 3.1), which transfers lower bounds from two-party communication complexity to distributed algorithms.

Timeline:

• 2000: Peleg and Rubinovich (SIAM J. Comput. 30) prove an $\tilde\Omega(\sqrt n)$ lower bound for distributed MST construction on a family of graphs built from paths and a tree.
• 2006: Elkin (SIAM J. Comput. 36) extends it to MST approximation, using the networks $G(\Gamma,d,p)$ (reference [10] of the paper).
• 2011–2012: Das Sarma et al. isolate the Simulation Theorem as a general reduction for arbitrary Boolean functions $f$ and derive lower bounds for many verification and approximation problems.

Setting

A B-model network is an undirected graph whose vertices are processors with unbounded local computation. Computation proceeds in synchronous rounds; in each round, every vertex sends a message of $B$ bits along each incident edge in each direction, then updates its local state from its old state and the messages it received. Two vertices $s$ and $r$ hold inputs $x,y\in\{0,1\}^b$; all other vertices start without input. A public-coin randomized algorithm additionally lets all vertices read a shared random string. It computes $f:\{0,1\}^b\times\{0,1\}^b\to\{0,1\}$ with $\epsilon$-error in $T$ rounds if, for every $(x,y)$, both $s$ and $r$ output $f(x,y)$ after round $T$ with probability at least $1-\epsilon$. $R^{G}_\epsilon(f)$ is the least such $T$.

In the communication complexity model, Alice holds $x$, Bob holds $y$, one bit is sent per round, and both must output $f(x,y)$. $R^{cc-pub}_\epsilon(f)$ is the least number of bits of an $\epsilon$-error public-coin protocol.

The network $G(\Gamma,d,p)$ consists of $\Gamma$ paths $\mathcal P^1,\dots,\mathcal P^\Gamma$ with $d^p$ vertices $v^\ell_0,\dots,v^\ell_{d^p-1}$ each, a complete $d$-ary tree $\mathcal T$ of depth $p$ with vertices $u^\ell_0,\dots,u^\ell_{d^\ell-1}$ at level $\ell$, and spoke edges joining each leaf $u^p_j$ to $v^\ell_j$ on every path. The inputs sit at the two extreme leaves, $s=u^p_0$ and $r=u^p_{d^p-1}$. The $i$-right set $R_i$ consists of all path vertices at positions $j\ge i$, the leaves $u^p_j$ with $j\ge i$, and their ancestors; the $i$-left set $L_i$ is the mirror image, and $L_0=V\setminus\{r\}$, $R_0=V\setminus\{s\}$. $C_{R_t}$ denotes the vector of states of the vertices of $R_t$ at the end of round $t$.

Formalization targets

Goal: Theorem 3.1 (Simulation Theorem)

If a public-coin algorithm on $G(\Gamma,d,p)$ computes $f$ with $\epsilon$-error in $T$ rounds and

$$T<\frac{d^p-1}{2},$$

then some public-coin two-party protocol computes $f$ with $\epsilon$-error using at most

$$2\,d\,p\,B\,T\ \text{bits},\qquad\text{i.e.}\qquad R^{cc-pub}_\epsilon(f)\le 2dpB\,R^{G(\Gamma,d,p)}_\epsilon(f).$$

Milestones

1. Observation 3.3: the configuration of $U$ at round $t$ is determined by the configuration of $U'\supseteq U$ at round $t-1$ and the messages into $U$ from outside $U'$.
2. §3.3 edge count: for $0<t<(d^p-1)/2$, at most $dp$ edges join $V\setminus R_{t-1}$ to $R_t$ (and $V\setminus L_{t-1}$ to $L_t$).
3. Inclusion from the proof of Lemma 3.4: $V\setminus R_{t-1}\subseteq L_{t-1}$ (and its mirror image).
4. Lemma 3.4: $C_{R_t}=g_R(C_{R_{t-1}},M_1,\dots,M_{dp})$ for $dp$ messages of $B$ bits sent from $L_{t-1}$, with $g_R$ and the message edges fixed before the inputs; and symmetrically for $C_{L_t}$.

Significance

The theorem turns any lower bound $R^{cc-pub}_\epsilon(f)=\Omega(b)$, such as those for set disjointness and equality, into a round lower bound on $G(\Gamma,d,p)$: an algorithm with $T<(d^p-1)/2$ rounds forces $T\ge R^{cc-pub}_\epsilon(f)/(2dpB)$. Choosing the parameters gives the paper's bounds of order $\sqrt{n/(B\log n)}$ rounds for verification and approximation problems (§§4–7), and the same reduction underlies a large body of later CONGEST lower bounds.

The result has been proved since 2011. A machine-checked version would provide the first formal model of synchronous bandwidth-limited message passing and of public-coin two-party protocols on the platform, together with a verified reduction between them. No formalization of the theorem, of the B model, or of two-party communication protocols is known to exist in Mathlib or on the platform.

Difficulty

The informal proof is short; the work lies in making the information flow precise. The naive simulation, in which Alice simulates the vertices near $s$ and Bob those near $r$, fails because the cut between the two halves contains $\Gamma$ path edges plus the spokes, and $\Gamma$ can be large: sending every message across it costs $\Gamma B$ bits per round. The argument must instead let both parties' simulated regions shrink by one path position per round, so that the only messages crossing into Bob's region come from $p$ tree vertices with $d$ children each. Making this rigorous requires a careful accounting of which vertices belong to $R_t$, which edges leave $V\setminus R_{t-1}$, and why the functions that update the configurations do not depend on the other party's input.

Formalization scope

• Network. Vertices are (Fin Γ × Fin (d^p)) ⊕ Σ ℓ : Fin (p+1), Fin (d^ℓ); paths are numbered from $0$. The children of $u^\ell_i$ are $u^{\ell+1}_{di+k}$, $0\le k<d$. $L_i,R_i$ are Finsets defined for every $i$, with the paper's special case at $i=0$. The nodes $s,r$ require $d^p\ge1$.
• Messages are exactly $B$ bits (Fin B → Bool) on every directed edge in every round. Optional or variable-length messages would let silence carry information and make the theorem false (e.g. at $B=0$).
• Algorithms. Inputs enter only through the initial states of $s$ and $r$; a vertex receives a fixed dummy from non-neighbours. Running time is a fixed number $T$ of rounds, outputs read after round $T$; this is equivalent to the paper's worst-case time.
• Randomness is a PMF on an arbitrary type, shared by all vertices (resp. both parties); $\epsilon$-error requires both outputs to be correct on the same random string, and $\epsilon\ge0$.
• Protocols send one bit per round, so cost equals bits exchanged. Alice's moves read only $x$ and the transcript, Bob's only $y$. Modelling the two-party side as a two-vertex B-model network would carry two bits per round and weaken the constant $2dpB$ by a factor of $2$; the formalization does not do this.
• Lemma 3.4 is stated with the functions $g_L,g_R$ and the message edges chosen before the inputs. A version where they may depend on $(x,y)$ is trivially true and is ruled out.
• The "in other words" inequality between the minimal complexities is not posed through sInf, which would be $0$ on an empty set; the goal is stated for every algorithm.

Contributions welcome: proofs of the milestones, and reusable infrastructure for executions of message-passing algorithms (locality lemmas such as Observation 3.3 hold on any graph).

Selected references

• A. Das Sarma, S. Holzer, L. Kor, A. Korman, D. Nanongkai, G. Pandurangan, D. Peleg, R. Wattenhofer, Distributed Verification and Hardness of Distributed Approximation, SIAM J. Comput. 41(5), 2012, 1235–1265. https://doi.org/10.1137/11085178X
• M. Elkin, An Unconditional Lower Bound on the Time-Approximation Trade-off for the Distributed Minimum Spanning Tree Problem, SIAM J. Comput. 36(2), 2006, 433–456. https://doi.org/10.1137/S0097539704441848
• D. Peleg, V. Rubinovich, A Near-Tight Lower Bound on the Time Complexity of Distributed Minimum-Weight Spanning Tree Construction, SIAM J. Comput. 30(5), 2000, 1427–1442. https://doi.org/10.1137/S0097539700369740
• D. Peleg, Distributed Computing: A Locality-Sensitive Approach, SIAM, 2000. https://doi.org/10.1137/1.9780898719772
• E. Kushilevitz, N. Nisan, Communication Complexity, Cambridge University Press, 1997. https://doi.org/10.1017/CBO9780511574948