Large Language Models; SAT Solving; CDCL; Algorithmic Reasoning; Neural Symbolic Learning; Scratchpad Memory; Out-of-Distribution Generalization; Tool-Augmented Inference

Large Language Models (LLMs) have recently demonstrated promising multi-step reasoning capabilities through techniques like chain-of-thought prompting and scratchpads. However, they struggle with tasks requiring complex search and backtracking, such as SAT solving. Our goal is to examine whether LLMs can learn and generalize the Conflict-Driven Clause Learning (CDCL) algorithm from supervised solver traces.

Large Language Models (LLMs) have recently demonstrated promising multi-step reasoning capabilities through techniques like chain-of-thought prompting and scratchpads. However, they struggle with tasks requiring complex search and backtracking, such as SAT solving. Our goal is to examine whether LLMs can learn and generalize the Conflict-Driven Clause Learning (CDCL) algorithm from supervised solver traces.