Can Transformers Reason Logically? A Study in SAT Solving

We theoretically and empirically study the logical reasoning capabilities of LLMs in the context of the Boolean satisfiability (SAT) problem. First, we construct a decoder-only Transformer that can solve SAT using backtracking and deduction via Chain-of-Thought (CoT). We prove its correctness by showing trace equivalence to the well-known DPLL SAT-solving algorithm. Second, to support the implementation of this abstract construction, we design a compiler $\texttt{PARAT}$ that takes as input a procedural specification and outputs a transformer model implementing this specification. Third, rather than $\textit{programming}$ a transformer to reason, we evaluate empirically whether it can be $\textit{trained}$ to do so by learning directly from algorithmic traces ("reasoning paths") of the DPLL algorithm.

@article{pan2025_2410.07432,
  title={ Can Transformers Reason Logically? A Study in SAT Solving },
  author={ Leyan Pan and Vijay Ganesh and Jacob Abernethy and Chris Esposo and Wenke Lee },
  journal={arXiv preprint arXiv:2410.07432},
  year={ 2025 }
}