The TCS Formalization Drive

Quantum Max-Cut asks for a high-energy state of an antiferromagnetic spin system specified by a weighted graph. Vertices carry qubits, and an edge rewards the two qubits for occupying their antisymmetric singlet state. A single qubit participates in several interactions, so maximizing each edge separately generally gives incompatible demands. The problem…

The simplex method moves between bases of a linear program, and its running time is governed by the pivot rule that picks the next basis. Whether some pivot rule needs only polynomially many pivots is a central open question in linear optimization. It is open even for 0/1-LPs, where the feasible region is a polytope whose vertices lie in $\{0,1\}^n$, although…

Integer linear programs $\min\{c^\top x : Ax\le b,\ x\in\mathbb Z^n\}$ are NP-hard in general, and one of the best-known tractable classes is the one where $A$ is totally unimodular (TU): every square submatrix has determinant in $\{-1,0,1\}$. It is a long-standing open question whether integer programs with a $\Delta$-modular constraint matrix (full column rank,…

A QMA verifier receives a quantum witness and checks it with a circuit generated efficiently from the input. An acceptance probability separated by an inverse-polynomial gap is enough to define the class, but applications often need the probability of a wrong answer to be exponentially small. Repeating the verifier on many supplied witness registers…