Linear Estimators for Boolean Satisfiability: Exact Cavity Asymptotics, Gaussian Limit of Belief Propagation, and Sparse Preconditioning

Abstract

We investigate the theoretical foundations and computational characteristics of linear estimators for Boolean Satisfiability (SAT). We establish a formal identity unifying marginal counting, spectral relaxation, and message passing. The literal majority field corresponds to the marginal of Belief Propagation (BP) after half an iteration from uninformative messages, while the Moore–Penrose pseudoinverse provides an exact linearized, iterated resolvent. Using Gaussian cavity density evolution on locally tree-like factor graphs, we derive analytical predictions for the initial clause violation rate and the thermodynamic correlation between the spectral estimator and the literal majority baseline. We also obtain a closed-form expression for the majority baseline through the Skellam distribution. We compare the spectral approach with nonlinear BP, examining convergence behavior on tree-like and cyclic topologies. In contrast to the convergence limitations of nonlinear message passing, the pseudoinverse-based estimator offers a convex least-squares formulation that can be computed efficiently using sparse LSQR. On community-structured modular graphs, it achieves a substantial reduction in initial clause violations relative to the majority baseline. Finally, we demonstrate that the spectral prior accelerates the initial descent phase (burn-in) of stochastic local search (probSAT), establishing its potential as a practical initialization strategy for SAT solvers. We discuss its possible implications for computational efficiency, energy consumption, and operating costs in large-scale constraint-solving pipelines. The algorithmic kernels are protected under the PolyForm Noncommercial License 1.0.0.