Technical Perspective: The Surprising Power of Spectral Refutation

NP-hard problems are assumed to be computationally intractable, meaning that no efficient (polynomial time) algorithm is guaranteed to correctly solve every input instance. One way of coping with NP-hardness is via the use of reliable heuristics. These are efficient algorithms that might not solve every input instance, but when they claim a solution, the solution is guaranteed to be correct.

Consider the canonical NP-complete problem of SAT (determining whether a Boolean formula of the form (x₁∨¬x₂∨x₃)∧(x₂∨¬x₄)∧. . . has a satisfying assignment). A heuristic for finding satisfying assignments will naturally be reliable, because one can efficiently check whether the assignment found indeed satisfies all clauses of the input formula. However, designing reliable refutation heuristics that certify that a formula is not satisfiable is more challenging. Under the commonly accepted assumption that NP differs from co-NP, there are no polynomial size witnesses for unsatisfiablity. Hence, there is no natural candidate for what a reliable refutation heuristic should search for to certify that an input formula is not satisfiable.

The absence of natural witnesses does not imply there are no “unnatural” witnesses. For example, consider an algorithm that constructs some matrix based on the input formula, computes the largest eigenvalue of the matrix (this can be done in polynomial time), and if this eigenvalue is sufficiently small, declares that the formula is not satisfiable. Could it be that such an algorithm, that seems unrelated to SAT, can serve as a reliable refutation heuristic? Perhaps surprisingly, the answer is yes.

Algorithms that base their decisions on eigenvalues of appropriately chosen matrices are referred to as spectral algorithms (the set of eigenvalues of a matrix is referred to as its spectrum). They have traditionally been applied to problems whose input is naturally represented as a matrix, such as clustering problems (the distance matrix) and graph problems (the adjacency matrix). The input for k-SAT (instances of SAT in which every clause has exactly k literals) does not seem to have a natural representation as a matrix. Nevertheless, over two decades ago it was proved that spectral algorithms can reliably refute most sufficiently dense k-SAT instances, when k is even. Here, a formula with n variables is sufficiently dense if the number of clauses is somewhat above n^k/2.

A sequence of works extended the result in many ways: to odd k, to all Boolean constraint satisfaction problems (CSPs, formulas in which the predicate in a clause can be different from the or predicate), to achieving strong refutation (certifying that no assignment satisfies substantially more clauses than a random assignment does), to achieving trade-offs between (super-polynomial) running time and number of clauses at lower densities (below n^k/2), and to establishing that “most” holds even in a local sense (smoothed analysis). That is, pick any sufficiently dense input formula, and consider only those formulas that differ from it by very little: for a small fraction of the literals in the formula, their polarity is flipped (for example, x_i changed to ¬x_i or vice versa). Within every such set (and not only in most of them), the spectral heuristic refutes most formulas.

Spectral refutation heuristics involve clever choices of matrices, such as Kikuchi matrices, and sophisticated techniques for analyzing their eigenvalues. The accompanying paper presents the state of the art in this line of research. It also presents implications that transcend beyond the domain of refutation heuristics. Recall the birthday paradox, which states that if there are n possible outcomes (for example, birthdates), then in a random sample of approximately $\sqrt{n}$ trials (for example, people), there is likely to be a collision: two trails with the same outcome. In contrast, to guarantee a collision with certainty, one needs n+1 trials (the pigeonhole principle).

Are there notions of collisions for which parameters like those of the birthday paradox guarantee a collision with certainty, and there is no need for the more demanding parameters of the pigeonhole principle? It was conjectured that this holds for even covers in hypergraphs. An even cover is a set of hyperedges entirely composed of collisions: every participating vertex appears in two hyperedges, or more generally, in an even number of them. The conjecture was proved using an approach inspired by the spectral refutation heuristics. It involves deriving from every hypergraph a family of Kikuchi matrices, proving that most matrices in this family do not have a large eigenvalue, and proving that if the conjecture is false then every matrix in this family has a large eigenvalue. Consequently, the conjecture must be true.

Other recent applications of spectral techniques to seemingly unrelated mathematical problems include improved lower bounds on the blocklength of locally decodable codes, and proof of the sensitivity conjecture for Boolean functions.