On the fundamentals of gradient-based SAT solvers

Gradient-based methods have received increasing attention for Boolean satisfiability, both in neural-network-based solvers and broadly as continuous local search techniques. In this work, we provide a deeper understanding of the interplay of optimization process, problem structure, common formula transformations and neural network properties. Our unified view treats both direct gradient descent over variable marginals and neural-parametrized gradient descent as instances of the same continuous SAT framework. We show that its objective, the expected number of unsatisfied clauses under independent variable marginals, equals (up to constant shift) the clausewise Fourier objective commonly used in continuous SAT methods, and characterize its relation to the exact product-measure probability of unsatisfiability. Then, we derive convergence conditions for gradient descent. A central theme is symmetry: gradient descent can become trapped in invariant subspaces induced by formula symmetries. To remedy this, we show that formula transformations commonly used as SAT preprocessing tools can be repurposed to modulate the optimization landscape. We analyze their effect on problem structure, smoothness, tightness, and expressivity barriers of the neural network. Empirically, across several benchmarks, these transformations can improve gradient-descent performance. Our experiments also indicate that transformations can improve data efficiency and inference-time performance in self-supervised neural SAT solving. Finally, we demonstrate that neural-parametrized gradient descent can improve over input-space gradient descent across several datasets.