Can Transformers Reason Logically? A Study in SAT Solving

We formally study the logical reasoning capabilities of decoder-only Transformers in the context of the boolean satisfiability (SAT) problem. First, we prove by construction that decoder-only Transformers can decide 3-SAT, in a non-uniform model of computation, using backtracking and deduction via Chain-of-Thought (CoT). Second, we implement our construction as a PyTorch model with a tool (PARAT) that we designed to empirically demonstrate its correctness and investigate its properties. Third, rather than programming a transformer to reason, we evaluate empirically whether it can be trained to do so by learning directly from algorithmic traces ("reasoning paths") from our theoretical construction. The trained models demonstrate strong out-ofdistribution generalization on problem sizes seen during training but have limited length generalization, which is consistent with the implications of our theoretical result.