Neural Approaches to SAT Solving: Design Choices and Interpretability

Reasoning is a cognitive ability which allows humans to solve problems with previously unseen combinations of constraints. For a long time, it has been debated whether artificial neural networks can obtain such generalization skills or whether they can only learn to detect superficial patterns Fodor and Pylyshyn [1988], Marcus [2003, 2018] without being able to generalize to novel combinations of constraints. With the arrival of Large Language Models (LLMs) specially trained for reasoning Guo et al. [2025], Jaech et al. [2024], it became harder and harder to claim that these models can only detect superficial patterns. Nevertheless, the exact mechanism by which they are able to solve tasks that typically require reasoning is largely unknown and the robustness of the solving process is also not understood. In this contribution, we focus on a restricted class of problems that require reasoning, concretely on solving Boolean formulas in CNF form. This could be viewed as a prototypical task where the goal is to solve problems with novel combinations of constraints, and where detecting superficial patterns seen during training would be insufficient. It has already been demonstrated that Graph Neural Networks (GNNs) can successfully learn to solve such problems and generalize to larger problems Selsam et al. [2018], even though they are still not competitive when compared to state of the art SAT solvers. Understanding the underlying mechanisms GNNs employ to successfully solve problems, as well as their limitations, would offer significant practical and theoretical value.