Concept learning for algorithmic reasoning: Insights from SAT-solving GNNs

Explainable AI and model transparency methods primarily focus on classification tasks, identifying salient input features or abstract concepts that are directly tied to the data. In contrast, algorithmic problems such as SAT solving present a deeper challenge: here, meaningful concepts depend not only on the input but also on the model’s evolving internal state; hence, such settings remain underexplored. We study concept learning in an existing model named NeuroSAT , a Graph Neural Network (GNN) trained to predict satisfiability, and uncover internal algorithmic structures, most notably the notion of support , that align with classical SAT heuristics. We then construct a significantly simplified GNN trained via a teacher–student approach: instead of learning from SAT/UNSAT labels, the student is trained to mimic NeuroSAT ’s latent representations—i.e., the concepts themselves—and achieves comparable performance using 91 % fewer parameters. For this simplified architecture, we provide a rigorous theoretical analysis that demonstrates, under certain assumptions on the input distribution and network weights, the emergence of the concept of support and its governing role in the network’s dynamics. This work bridges explainability and algorithmic reasoning by showing that classical SAT-solving strategies emerge naturally in GNNs—and can be used to simplify, compress, and formally analyze their internal dynamics. • We propose a framework for discovering algorithmic concepts learned by GNNs and showcase it on the problem of satisfiability using NeuroSAT by Selsam et al. (2018). • Key abstractions, such as variable assignment confidence-level, emerge spontaneously when the GNN is trained to predict SAT/UNSAT using only single-bit supervision and standard cross-entropy loss. • The discovered concepts enable both theoretical analysis and compression via a compact student network trained on internal representations. • Our insights guide principled modifications to the classical WalkSAT algorithm, yielding new variants that converge faster.