我们在布尔可满足性问题（SAT）的背景下，从理论和实证两方面研究了大型语言模型（LLMs）的逻辑推理能力。首先，我们构建了一个仅解码器 Transformer，它可以使用回溯和基于思维链（CoT）的推理来解决 SAT。我们通过证明其跟踪等价于著名的 DPLL SAT 求解算法来证明其正确性。其次，为了支持这种抽象构造的实现，我们设计了一个编译器 $\texttt{PARAT}$，它以过程规范作为输入，并输出一个实现此规范的 Transformer 模型。第三，我们不是 $\textit{编程}$ Transformer 进行推理，而是通过从 DPLL 算法的算法跟踪（“推理路径”）中直接学习来评估它是否可以被 $\textit{训练}$ 来执行此操作。